Resolución SLD

La resolución SLD ( resolución de cláusula definida lineal selectiva ) es la regla de inferencia básica utilizada en la programación lógica . Es un refinamiento de la resolución , que es a la vez sólida y refutable para las cláusulas de Horn .

Dada una cláusula objetivo, representada como la negación de un problema a resolver:

${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}$

con literal seleccionado y una cláusula definida de entrada :${\displaystyle \neg L_{i}}$

${\displaystyle L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}}$

cuyo literal positivo (átomo) se unifica con el átomo del literal seleccionado , la resolución SLD deriva otra cláusula objetivo, en la que el literal seleccionado se reemplaza por los literales negativos de la cláusula de entrada y se aplica la sustitución unificadora:${\estilo de visualización L\,}$ ${\displaystyle L_{i}\,}$${\displaystyle \neg L_{i}\,}$${\displaystyle \theta \,}$

${\displaystyle (\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \neg K_{m}\ \lor \cdots \lor \neg L_{n})\theta }$

En el caso más simple, en lógica proposicional, los átomos y son idénticos, y la sustitución unificadora es nula. Sin embargo, en el caso más general, la sustitución unificadora es necesaria para que los dos literales sean idénticos.${\displaystyle L_{i}\,}$${\estilo de visualización L\,}$${\displaystyle \theta \,}$

El nombre "resolución SLD" fue dado por Maarten van Emden para la regla de inferencia sin nombre introducida por Robert Kowalski . ^[1] Su nombre se deriva de la resolución SL, ^[2] que es a la vez sólida y refutable para la forma de lógica sin restricciones. "SLD" significa "resolución SL con cláusulas definidas".

Tanto en SL como en SLD, "L" representa el hecho de que una prueba de resolución puede restringirse a una secuencia lineal de cláusulas:

${\displaystyle C_{1},C_{2},\cdots ,C_{l}}$

donde la "cláusula superior" es una cláusula de entrada y todas las demás cláusulas son resolutivas, una de cuyas cláusulas principales es la cláusula anterior . La prueba es una refutación si la última cláusula es la cláusula vacía.${\estilo de visualización C_{1}\,}$${\displaystyle C_{i+1}\,}$${\displaystyle C_{i}\,}$${\displaystyle C_{l}\,}$

En la resolución SLD, todas las cláusulas de la secuencia son cláusulas de objetivo y la otra cláusula principal es una cláusula de entrada. En la resolución SL, la otra cláusula principal es una cláusula de entrada o una cláusula principal anterior en la secuencia.

Tanto en SL como en SLD, "S" representa el hecho de que el único literal que se resuelve en cualquier cláusula es aquel que se selecciona de forma única mediante una regla de selección o una función de selección. En la resolución SL, el literal seleccionado se limita a aquel que se haya introducido más recientemente en la cláusula. En el caso más simple, dicha función de selección de último en entrar, primero en salir se puede especificar mediante el orden en el que se escriben los literales, como en Prolog . Sin embargo, la función de selección en la resolución SLD es más general que en la resolución SL y en Prolog. No hay ninguna restricción sobre el literal que se puede seleccionar.${\displaystyle C_{i}\,}$

En lógica clausular, una refutación SLD demuestra que el conjunto de cláusulas de entrada es insatisfacible. Sin embargo, en programación lógica, 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, por medio del razonamiento inverso , de un nuevo conjunto de subobjetivos utilizando una cláusula de entrada como un procedimiento de reducción de objetivos. La sustitución unificadora pasa la entrada del subobjetivo seleccionado al cuerpo del procedimiento y, simultáneamente, pasa la salida del encabezado del procedimiento a los subobjetivos no seleccionados restantes. La cláusula vacía es simplemente un conjunto vacío de subobjetivos, lo que indica que se ha resuelto la conjunción inicial de subobjetivos en la cláusula superior.${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}$${\displaystyle L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}}$${\displaystyle C_{i+1}\,}$${\displaystyle C_{i}\,}$${\displaystyle \theta \,}$

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

Un nodo de hoja, que no tiene hijos, es un nodo de éxito si su cláusula de objetivo asociada es la cláusula vacía. Es un nodo de error si su cláusula de objetivo asociada no está vacía pero su literal seleccionado no se unifica con ningún literal positivo de cláusulas definidas en el programa.

La resolución SLD no es determinista en el sentido de que no determina la estrategia de búsqueda para explorar el árbol de búsqueda. Prolog busca en el árbol en profundidad, una rama a la vez, utilizando el retroceso cuando encuentra un nodo fallido. La búsqueda en profundidad es muy eficiente en su uso de los recursos informáticos, pero es incompleta si el espacio de búsqueda contiene infinitas ramas y la estrategia de búsqueda busca en estas en lugar de en ramas finitas: el cálculo no termina. También son posibles otras estrategias de búsqueda, incluidas la búsqueda en amplitud , la búsqueda en mejor lugar y la búsqueda de rama y límite . Además, la búsqueda se puede realizar de forma secuencial, un nodo a la vez, o en paralelo, muchos nodos simultáneamente.

La resolución SLD también es no determinista en el sentido, mencionado anteriormente, de que la regla de selección no está determinada por la regla de inferencia, sino que está determinada por un procedimiento de decisión separado, que puede ser sensible a la dinámica del proceso de ejecución del programa.

El espacio de búsqueda de resolución SLD es un árbol or, en el que las diferentes ramas representan cálculos alternativos. En el caso de los programas de lógica proposicional, SLD se puede generalizar de modo que el espacio de búsqueda sea un árbol and-or , cuyos nodos están etiquetados por literales simples, que representan subobjetivos, y los nodos están unidos por conjunción o por disyunción. En el caso general, donde los subobjetivos conjuntos comparten variables, la representación del árbol and-or es más complicada.

Dado el programa lógico en lenguaje Prolog :

q  :-  p .pag .

y el objetivo de nivel superior:

q .

El espacio de búsqueda consta de una única rama, en la que qse reduce a pla que se reduce al conjunto vacío de subobjetivos, lo que indica un cálculo exitoso. En este caso, el programa es tan simple que no hay papel para la función de selección y no es necesario realizar ninguna búsqueda.

En lógica clausular, el programa está representado por el conjunto de cláusulas:

${\displaystyle q\lor \neg p}$

${\estilo de visualización p\,}$

y el objetivo de nivel superior está representado por la cláusula de objetivo con un solo literal negativo:

${\displaystyle \neg q}$

El espacio de búsqueda consta de la única refutación:

${\displaystyle \neg q,\neg p,{\mathit {falso}}}$

donde representa la cláusula vacía.${\displaystyle {\mathit {falso}}\,}$

Si se añadiera la siguiente cláusula al programa:

o  :-  r .

En ese caso, habría una rama adicional en el espacio de búsqueda, cuyo nodo de hoja res un nodo de falla. En Prolog, si esta cláusula se agregara al principio del programa original, Prolog usaría el orden en el que se escriben las cláusulas para determinar el orden en el que se investigan las ramas del espacio de búsqueda. Prolog probaría primero esta nueva rama, fallaría y luego volvería atrás para investigar la rama única del programa original y tendría éxito.

Si la cláusula

pág  .​ ​

Si ahora se añadieran al programa, el árbol de búsqueda contendría una rama infinita. Si se probara primero esta cláusula, Prolog entraría en un bucle infinito y no encontraría la rama correcta.

SLDNF ^[3] es una extensión de la resolución SLD para tratar la negación como falla . En SLDNF, las cláusulas de objetivo pueden contener literales de negación como falla, por ejemplo de la forma , que pueden seleccionarse solo si no contienen variables. Cuando se selecciona un literal sin variables, se intenta una subprueba (o subcomputación) para determinar si hay una refutación SLDNF a partir del literal no negado correspondiente como cláusula superior. El subobjetivo seleccionado tiene éxito si la subprueba falla, y falla si la subprueba tiene éxito.${\displaystyle no(p)\,}$${\estilo de visualización p\,}$${\displaystyle no(p)\,}$

• Juan Alan Robinson

• Jean Gallier , SLD-Resolution and Logic Programming, capítulo 9 de Logic for Computer Science: Foundations of Automatic Theorem Proving , revisión en línea de 2003 (descarga gratuita), publicado originalmente por Wiley, 1986
• John C. Shepherdson, SLDNF-Resolution with Equality , Journal of Automated Reasoning 8: 297-306, 1992; define la semántica con respecto a la cual la resolución SLDNF con igualdad es sólida y completa

• [1] Definición del Diccionario Gratuito de Informática en Línea