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 refutación completa para las cláusulas de Horn .
La regla de inferencia SLD
Dada una cláusula de meta, representada como la negación de un problema a resolver:
con literal seleccionado , y una cláusula de entrada definida :
cuyo literal positivo (átomo) se unifica con el átomo del literal seleccionado , La resolución SLD deriva otra cláusula de objetivo, en la que el literal seleccionado se reemplaza por los literales negativos de la cláusula de entrada y la sustitución unificadora Está aplicado:
En el caso más simple, en lógica proposicional, los átomos y son idénticos, y la sustitución unificadora 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 origen del nombre "SLD"
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 refutación completa para la forma clausal irrestricta 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:
donde la "cláusula superior" es una cláusula de entrada, y todas las demás cláusulas es resolutivo uno de cuyos padres es la cláusula anterior . La prueba es una refutación si la última cláusula es la cláusula vacía.
En SLD, todas las cláusulas de la secuencia son cláusulas de objetivo y el otro padre es una cláusula de entrada. En la resolución de SL, el otro padre es una cláusula de entrada o una cláusula anterior en la secuencia.
Tanto en SL como en SLD, "S" representa el hecho de que el único literal resuelto en cualquier cláusula es uno que se selecciona de forma exclusiva mediante una regla de selección o una función de selección. En la resolución SL, el literal seleccionado está restringido a uno que se haya introducido más recientemente en la cláusula. En el caso más simple, esta función de selección de último en entrar, primero en salir se puede especificar por 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 restricción sobre el literal que se puede seleccionar.
La interpretación computacional de la resolución SLD
En la lógica de las cláusulas, una refutación de 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 objetivos. La sustitución unificadoraambos pasan la entrada del subobjetivo seleccionado al cuerpo del procedimiento y simultáneamente pasan la salida del jefe del procedimiento al resto de subobjetivos 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.
Estrategias de resolución SLD
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.
Un nodo hoja, que no tiene hijos, es un nodo exitoso si su cláusula de objetivo asociada es la cláusula vacía. Es un nodo de falla si su cláusula de objetivo asociada no está vacía pero su literal seleccionado se unifica sin 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 la profundidad del árbol primero, una rama a la vez, usando el retroceso cuando encuentra un nodo de falla. La búsqueda en profundidad es muy eficiente en el uso de los recursos informáticos, pero es incompleta si el espacio de búsqueda contiene ramas infinitas y la estrategia de búsqueda las busca con preferencia a las ramas finitas: el cálculo no termina. Otras estrategias de búsqueda, incluyendo en amplitud , primero el mejor , y rama-y-bound de búsqueda también son posibles. Además, la búsqueda se puede realizar secuencialmente, 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 o, en el que diferentes ramas representan cálculos alternativos. En el caso de los programas de lógica proposicional, SLD puede generalizarse de modo que el espacio de búsqueda sea un árbol y-o , 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 yo es más complicada.
Ejemplo
Dado el programa lógico:
q : - pág .p .
y el objetivo de nivel superior:
q .
el espacio de búsqueda consta de una única rama, en la que q
se reduce a lo p
que se reduce al conjunto vacío de subobjetivos, lo que indica un cómputo exitoso. En este caso, el programa es tan simple que no hay ningún papel para la función de selección y no es necesario realizar ninguna búsqueda.
En lógica clausal, el programa está representado por el conjunto de cláusulas:
y el objetivo de nivel superior está representado por la cláusula de objetivo con un solo literal negativo:
El espacio de búsqueda consta de la única refutación:
dónde representa la cláusula vacía.
Si se agregó la siguiente cláusula al programa:
q : - r .
entonces habría una rama adicional en el espacio de búsqueda, cuyo nodo hoja r
es 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 están escritas las cláusulas para determinar el orden en el que se investigan las ramas del espacio de búsqueda. Prolog probaría esta nueva rama primero, fallaría y luego retrocedería para investigar la rama única del programa original y tendría éxito.
Si la cláusula
p : - p .
ahora se agregaron al programa, entonces 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
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 la negación como literales de falla, por ejemplo, de la forma, que solo se pueden seleccionar si no contienen variables. Cuando se selecciona un literal libre de variables de este tipo, se intenta una subprueba (o subcomputación) para determinar si hay una refutación SLDNF a partir del literal innecesario correspondiente.como cláusula superior. El subobjetivo seleccionado tiene éxito si la subprueba falla, y falla si la subprueba tiene éxito.
Ver también
Referencias
- ^ Robert Kowalski Predicate Logic as a Programming Language Memo 70, Departamento de Inteligencia Artificial, Universidad de Edimburgo. 1973. También en Proceedings IFIP Congress, Estocolmo, North Holland Publishing Co., 1974, págs. 569-574.
- ^ Robert Kowalski y Donald Kuehner, Resolución lineal con función de selección Inteligencia artificial, Vol. 2, 1971, págs. 227-60.
- ^ Krzysztof Apt y Maarten van Emden, Contribuciones a la teoría de la programación lógica , Revista de la Asociación de Maquinaria de Computación. Vol. 1982 - portal.acm.org
- Jean Gallier , SLD-Resolution and Logic Programming capítulo 9 de Logic for Computer Science: Foundations of Automatic Theorem Proving , 2003 revisión en línea (descarga gratuita), publicado originalmente por Wiley, 1986
- John C. Shepherdson, SLDNF-Resolución con igualdad , 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
enlaces externos
- [1] Definición del Diccionario gratuito de informática en línea