# data[].attributes.body
Una claúsula de Horn es una secuencia de literales que contiene a lo sumo un literal positivo. Al escribirla en notación de Kowalski tendr´a una de estas cuatro formas:

# data[].attributes.body
Los hechos representan “hechos acerca de los objetos” (de nuestro universo de discurso), relaciones elementales entre estos objetos las reglas expresan relaciones condicionales entre los objetos, dependencias.
Las reglas engloban todos los casos en el siguiente sentido: u
Un hecho es una regla con cuerpo vacío un objetivo es una regla con cabeza vacía y el éxito es una regla con cabeza y cuerpo vacíos

# data[].attributes.body
Un predicado p queda definido por el conjunto de claúsulas (hechos y reglas) cuyas cabezas tienen ese símbolo de predicado. Así pues la definición de un predicado en general tendrá el aspecto:

# data[].attributes.body
Es un conjunto de definiciones de predicados (es decir, un conjunto de cla´usulas definidas: hechos y reglas).

# data[].attributes.body
El nombre "resolución SLD" fue dado por Maarten van Emden para la regla de inferencia sin nombre introducida por Robert Kowalski . Su nombre se deriva de la resolución SL, que es a la vez sólida y refutación completa para la forma clausal irrestricta de la lógica. "SLD" significa "resolución SL con cláusulas definidas".

# data[].attributes.body
Todas las variables lógicas en de una claúsula están cuantificadas universalmente de forma implícita. Por ejemplo, en la claúsula:
Es decir, las variables que sólo aparecen a la derecha de la claúsula están localmente afectadas de una cuantificación existencial. Se dice que son variables existenciales o extra o locales. Interpretarlas existencialemente facilita la lectura de la claúsula: Para todo X y todo Y , hay un camino entre X e Y si existe Z tal que hay arco de X a Z y hay camino entre Z e Y

# data[].attributes.body
La resolución SLD define implícitamente un árbol de búsqueda de cálculos alternativos, en el que la cláusula de objetivo inicial está asociada con la raíz del árbol. Para cada nodo en el árbol y para cada cláusula definida en el programa cuyo literal positivo se unifica con el literal seleccionado en la cláusula objetivo asociada con el nodo, hay un nodo hijo asociado con la cláusula objetivo obtenida por resolución SLD.

# data[].attributes.headline
La interpretación computacional de la resolución SLD 

# data[].attributes.subject
La interpretación computacional de la resolución SLD 

# data[].attributes.body
En la lógica de las cláusulas, una refutación SLD demuestra que el conjunto de cláusulas de entrada es insatisfactorio. En la programación lógica, sin embargo, una refutación SLD también tiene una interpretación computacional. La cláusula superior puede interpretarse como la negación de una conjunción de subobjetivos . La derivación de la cláusula de es la derivación, mediante el razonamiento hacia atrás , de un nuevo conjunto de subobjetivos utilizando una cláusula de entrada como procedimiento de reducción de la meta.