En programación lógica , la resolución SLD (SLD significa Seleccionado , Lineal , Definido ) es un algoritmo que se utiliza para probar una fórmula lógica de primer orden a partir de un conjunto de cláusulas Horn . Se basa en una resolución lineal, con función de selección sobre las cláusulas definidas. La resolución SLD es más conocida por su extensión, SLDNF (NF significa negación como falla , la negación como falla ), que es la resolución utilizada por el lenguaje del algoritmo Prolog .
Una cláusula definida es una cláusula de Horn que contiene exactamente un literal positivo. Por lo tanto, la noción abarca cláusulas Horn estrictas y cláusulas Horn positivas. En el contexto de la resolución SLD, el literal positivo de una cláusula definida se denomina cabeza , conclusión o meta . La disyunción de literales negativos, si existen, se llama cuerpo , antecedentes o subobjetivos . Por ejemplo, la cláusula Horn
¬ a ∨ ¬ b ∨ c
es lógicamente equivalente a:
( a ∧ b ) → c
o la siguiente regla de Prolog:
c :- a, b.
En cada caso, c es la conclusión, un y b son los antecedentes.
Dado un programa (un conjunto de cláusulas de Horn) y una consulta (una conjunción de literales positivos que queremos probar que son verdaderos del programa), la resolución de SLD funciona globalmente como otras formas de resolución, intentando unificar las cláusulas de Horn para cree nuevos, hasta que se alcance una contradicción, o no se pueda realizar una nueva unificación.
Más precisamente, la resolución SLD comienza construyendo la negación de la solicitud (obtenemos así una cláusula Horn negativa, que llamaremos la lista de objetivos ), luego unifica el primer elemento de esta negación con una cláusula del programa. La cláusula en cuestión se busca de forma determinista, buscando la primera cláusula del programa cuyo encabezado sea la contraparte positiva de la primera negación de la lista de objetivos.
Si se encuentra una contradicción, entonces la negación de la solicitud es inconsistente con el programa, por lo que la solicitud finaliza con éxito. Si no se puede encontrar unificación para el primer término negativo en la lista de objetivos, la consulta falla. Si existe una unificación sin contradicción, entonces la nueva lista de objetivos se convierte en la conjunción de la anterior con la cláusula seleccionada, y la resolución SLD se reinicia (recursivamente) en la nueva lista de objetivos. Si una subconsulta falla, la unificación de nivel superior de la que proviene falla y el algoritmo busca otra unificación (en el resto del programa) para el primer término en la lista de objetivos. Este paso se llama retroceso .
Tomemos el siguiente programa como ejemplo:
q ∨ ¬ p pagasí como la consulta:
{ q }La lista de objetivos consta de la única negación {¬ q } y se busca una cláusula unificable en el programa. La primera cláusula coincide, está seleccionada. La conjunción de la lista de objetivos con la cláusula da:
( q ∨ ¬ p ) ∧ ¬ qEs :
¬ pAl relanzar el algoritmo en esta nueva lista de objetivos, encontramos una unificación con la segunda cláusula del programa, lo que conduce a una contradicción:
p ∧ ¬ pPor lo tanto, la lista de objetivos {¬ q } es incompatible con el programa, por lo que la solicitud { q } se completa con éxito.
Nota: En Prolog, se escribiría la primera cláusula q :- p . El algoritmo se describiría entonces de la siguiente manera: “Para probar q, busque una cláusula que tenga qcomo encabezado. La primera cláusula coincide y pdebe mostrarse. La segunda cláusula muestra p, por qlo tanto, está probada. "
Si se añadiera la siguiente cláusula en la parte superior del programa:
q ∨ ¬ rluego, el algoritmo de resolución de SLD lo seleccionaría primero, obteniendo ¬ r por unificación, y luego fallaría en unificar ¬ r . Esto induciría a retroceder; el algoritmo buscaría nuevamente unificar ¬ q con una cláusula en el resto del programa. Se seleccionaría la cláusula q ∨ ¬ p , y recurriríamos al caso anterior.