Conceptos de Programación Declarativa

Cláusulas de Horn:
La programación lógica trata de representar conocimiento a través de predicados en forma de hechos y reglas (cláusulas de Horn).
Un predicado o su negación es un literal.
Un literal positivo es un hecho.
Una cláusula o regla es una consecuencia lógica: si se cumplen ciertos literales, se puede afirmar un cierto hecho. Se representa de la siguiente manera:

a1 - b1, ... , br
.
.
.
ak - b1, ... , br

Dónde las ai son las conclusiones (literales positivos) y las bj son las premisas (literales negativos).
Si no hay bi se llama hecho en lugar de cláusula.
Si no hay ai se llama cláusula negativa y sirve como consulta.
Si no hay premisas ni conclusión tenemos un cláusula vacía.

Unificación:
Los conceptos de sustitución e instanciación son nociones básicas en el motor de un intérprete lógico.
Una sustitución es una lista de pares variable - término y la aplicación de una sustitución a un termino lógico es una instancia de dicho término.
Las sustituciones son utilizadas en programación lógica para, mediante su aplicación a las variables contenidas en una cláusula, obtener la expresión de la veracidad de una relación lógica particular a partir de la veracidad de una relación lógica más general incluida en el programa. Más formalmente, dicho concepto se conoce como unificación.
Un unificador de dos términos lógicos T1 y T2 es una sustitución θ , tal que T1θ = T2θ.

Resolución:

El sistema de resolución es un sistema sin ningún axioma y con una sola regla que se denomina regla de resolución. A partir de una pregunta y una sentencia del programa se obtiene una nueva pregunta. Es un demostrador de teoremas.
Este proceso suele representarse en forma arborescente con árboles de resolución, dónde se indican las sustituciones que han sido utilizadas y el conjunto de expresiones a las que han sido aplicadas. Cada una de las expresiones que constituyen los nodos del árbol se denominan objetivos ( conjunto de cuestiones en las que hemos descompuesto el problema representado por la pregunta ).
Cuando no queda ningún objetivo por resolver es que hemos conseguido demostrar nuestro teorema.

Control:
La idea central del paradigma de progamación lógica se sintetiza en la ecuación informal de Kowalski: algoritmo = lógica + control.
La programación lógica contempla el control como parte del modelo de cómputo. Esto libera al programador del uso de estructuras de control.
El control del orden en prolog se hace o bien mediante el orden de las sentencias y literales, o bien mediante cortes. Ya sean cortes verdes (que no alteran el significado declarativo del programa y generalmente expresan determinismo) o cortes rojos (que sí afectan a la semántica declarativa del programa)

Fuentes:
-"Programación Lógica" de M. Vilares - M. Alonso - A. Valderruten (pags. 49-54, 67-71, 96) Ediciones Tórculo
- Transparencias de programación lógica y funcional . Prof. Jesús Almendros (Universidad de Almería)
- Apuntes de programación lógica de Marisa Navarro ( Facultad de Informática de San Sebastián)