Resolución SLD

La resolución SLD ( resolución selectiva de cláusulas lineales definidas ) 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 completa en cuanto a refutación 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${\displaystyle \neg L_{i}}$y una cláusula definida de entrada :

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

cuyo literal positivo (átomo)${\displaystyle L\,}$se unifica con el átomo${\displaystyle L_{i}\,}$del literal seleccionado${\displaystyle \neg L_{i}\,}$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 la sustitución unificadora.${\displaystyle \theta \,}$se aplica:

$${\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${\displaystyle L_{i}\,}$y${\displaystyle L\,}$son idénticos y la sustitución unificadora${\displaystyle \theta \,}$es vacío. Sin embargo, en el caso más general, la sustitución unificadora es necesaria para que los dos literales sean idénticos.

El nombre «resolución SLD» fue dado por Maarten van Emden a la regla de inferencia sin nombre introducida por Robert Kowalski . ^{[ 1 ]} Su nombre deriva de la resolución SL, ^{[ 2 ]} que es sólida y completa en cuanto a refutación para la forma clausal no restringida de la lógica. «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"${\displaystyle C_{1}\,}$es una cláusula de entrada y todas las demás cláusulas${\displaystyle C_{i+1}\,}$es una resolución de cuyos padres es la cláusula anterior${\displaystyle C_{i}\,}$La prueba es una refutación si la última cláusula${\displaystyle C_{l}\,}$es la cláusula vacía.

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

Tanto en SL como en SLD, "S" representa el hecho de que el único literal resuelto en cualquier cláusula${\displaystyle C_{i}\,}$Es un literal que se selecciona de forma única mediante una regla o función de selección. En la resolución SL, el literal seleccionado se limita al que se ha 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 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.

En lógica clausal, 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${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}$puede interpretarse como la negación de una conjunción de subobjetivos${\displaystyle L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}}$. La derivación de la cláusula ${\displaystyle C_{i+1}\,}$de${\displaystyle C_{i}\,}$es la derivación, mediante razonamiento hacia atrás , de un nuevo conjunto de subobjetivos utilizando una cláusula de entrada como procedimiento de reducción de objetivos. La sustitución unificadora${\displaystyle \theta \,}$Ambos transfieren la entrada del subobjetivo seleccionado al cuerpo del procedimiento y, simultáneamente, transfieren la salida del encabezado del procedimiento a los subobjetivos restantes no seleccionados. La cláusula vacía es simplemente un conjunto vacío de subobjetivos, lo que indica que la conjunción inicial de subobjetivos en la cláusula superior se ha resuelto.

La resolución SLD define implícitamente un árbol de búsqueda de cálculos alternativos, en el que la cláusula objetivo inicial se asocia 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 al nodo, existe un nodo hijo asociado a la cláusula objetivo obtenida mediante la resolución SLD.

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

La resolución SLD no es determinista, ya que no determina la estrategia de búsqueda para explorar el árbol. Prolog busca en el árbol en profundidad, rama por rama, utilizando retroceso cuando encuentra un nodo de fallo. La búsqueda en profundidad es muy eficiente en el uso de recursos computacionales, pero es incompleta si el espacio de búsqueda contiene ramas infinitas y la estrategia de búsqueda las explora con preferencia a las ramas finitas: el cálculo no finaliza. También son posibles otras estrategias de búsqueda, como la búsqueda en amplitud , la búsqueda del mejor primero y la búsqueda de ramificación y acotación . Además, la búsqueda puede realizarse secuencialmente, nodo por nodo, o en paralelo, procesando varios 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 por un procedimiento de decisión independiente, que puede ser sensible a la dinámica del proceso de ejecución del programa.

El espacio de búsqueda de resolución de SLD es un árbol OR, en el que las distintas 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 con literales simples que representan subobjetivos, y los nodos se unen mediante conjunción o disyunción. En el caso general, donde los subobjetivos conjuntos comparten variables, la representación del árbol AND-OR es más compleja.

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 pque 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 necesidad de la función de selección ni de ninguna búsqueda.

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

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

$${\displaystyle p\,}$$

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

$${\displaystyle \neg q}$$

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

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

dónde${\displaystyle {\mathit {false}}\,}$representa la cláusula vacía.

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

q :- r .

Entonces, habría una rama adicional en el espacio de búsqueda, cuyo nodo hoja res un nodo de fallo. En Prolog, si esta cláusula se añadiera al principio del programa original, Prolog usaría el orden en que se escriben las cláusulas para determinar el orden en que se investigan las ramas del espacio de búsqueda. Prolog intentaría primero esta nueva rama, fallaría y luego retrocedería para investigar la única rama del programa original y tendría éxito.

Si la cláusula

p :- p .

Si se añadiera ahora al programa, el árbol de búsqueda contendría una rama infinita. Si se intentara esta cláusula primero, 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 fallo . En SLDNF, las cláusulas de objetivo pueden contener literales de negación como fallo, por ejemplo de la forma${\displaystyle not(p)\,}$, que solo se pueden seleccionar si no contienen variables. Cuando se selecciona un literal sin variables, se intenta una subprueba (o subcomputación) para determinar si existe una refutación SLDNF a partir del literal no negado correspondiente.${\displaystyle p\,}$como cláusula superior. El subobjetivo seleccionado${\displaystyle not(p)\,}$tiene éxito si la subprueba falla, y falla si la subprueba tiene éxito.

• Juan Alan Robinson

• Jean Gallier , Resolución SLD y programación lógica, capítulo 9 de Lógica para la informática: Fundamentos de la demostración automática de teoremas , 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.

• Definición del Diccionario en línea gratuito de informática