Resolución SLD
Definición
La resolución SLD (Selective Linear Definite-clause resolution) es una estrategia de resolución de primer orden para programas formados por cláusulas definidas: cláusulas con exactamente un literal positivo. La consulta se representa como una cláusula objetivo (sin literal positivo).
En cada paso:
- se selecciona una meta pendiente;
- se elige un hecho o una regla cuya cabeza pueda unificarse con la meta;
- se aplica el unificador;
- la meta se sustituye por las premisas de la regla;
- el proceso termina con éxito cuando ya no quedan metas; si una rama falla, se pueden probar alternativas mediante retroceso.
flowchart TD Q["Meta: mortal(socrates)"] -->|unificar con cabeza| R["Regla: mortal(X) ← humano(X)"] R -->|θ = {X/socrates}| G["Nueva meta: humano(socrates)"] G -->|unificar| F["Hecho: humano(socrates)"] F --> E["Meta vacía: éxito"] G -. "si no hay cláusula aplicable" .-> B["Falla esta rama"] B -. "retroceso" .-> ALT["Probar alternativa"]
Ejemplo en Prolog
humano(socrates).
mortal(X) :- humano(X).
?- mortal(socrates).La meta mortal(socrates) unifica con mortal(X) mediante {X/socrates} y se reemplaza por humano(socrates). El hecho correspondiente cierra la prueba. Esta reducción dirigida por la consulta evita construir todas las consecuencias posibles del programa.
Diferencia entre significado y ejecución
El significado declarativo de una regla indica qué relación es verdadera. La ejecución de Prolog agrega una política convencional: selecciona metas de izquierda a derecha y explora cláusulas en orden, con búsqueda en profundidad y retroceso. Por eso el orden puede afectar rendimiento y terminación. La regla SLD abstracta permite distintas funciones de selección; la elección concreta de Prolog es una estrategia operacional.
Límites
- Trabaja con cláusulas definidas, no con cláusulas arbitrarias de primer orden.
- La estrategia de búsqueda puede entrar en ciclos aunque exista otra rama con una solución.
- El uso operativo de negación en Prolog suele ser negación como fallo, que no debe confundirse sin más con la negación clásica.
- La terminación no está garantizada para todos los programas y consultas.
Relaciones
- Es un caso importante de programación declarativa y constituye el mecanismo de búsqueda central de Prolog.
- Opera sobre cláusulas definidas, un subconjunto de las cláusulas de Horn.
- Depende de unificación y retroceso.
Procedencia y referencias
- Clase: Inferencia en lógica de primer orden, diapositiva 16.
- SWI-Prolog, glosario: SLD resolution y ejecución de consultas.
- Sterling, L. y Shapiro, E. The Art of Prolog, 2.ª ed., MIT Press, capítulo 3.
- Lenguajes declarativos.