Un paradigma de programación y razonamiento en el que los programas se expresan como conjuntos de cláusulas lógicas y la computación procede mediante búsqueda dirigida de pruebas, utilizando típicamente unificación y retroceso para encontrar derivaciones que satisfacen metas.

Principio

Escribir especificaciones como hechos y reglas; interpretar la computación como intento de demostrar una meta a partir de esas reglas mediante resolución o SLD-resolución, con unificación que instancia variables y retroceso que explora alternativas.

Demostración

Programa estilo Prolog para un árbol genealógico: hechos describen relaciones de parentesco y reglas definen ancestro como clausura transitiva; la consulta ancestor(X,Y) inicia una búsqueda que unifica variables y hace retroceso para enumerar soluciones.

Aplicación incorrecta

Tratar un programa lógico puramente como código imperativo y depender de predicados con efectos secundarios u orden-dependientes socava la semántica declarativa y dificulta razonar sobre la corrección.

Consecuencia

Un uso adecuado produce programas concisos y declarativos, control de búsqueda inherente mediante retroceso y potentes capacidades de metaprogramación y razonamiento simbólico; también facilita el prototipado rápido de aplicaciones orientadas a búsqueda.

Inversión

Cambiar a programación funcional o imperativa donde la computación se da por evaluación determinista de funciones o comandos ordenados en lugar de búsqueda de pruebas; esto enfatiza el flujo de control en lugar de la especificación lógica.

Límite

Suele ocuparse de fragmentos de cláusulas de Horn y de semánticas operacionales dirigidas por metas; excluye teorías arbitrarias del primer orden con comportamiento de resolución no interpretado, y la terminación y completitud no están garantizadas sin restricciones.

Tensión semántica

Tensión entre lecturas modelo-teóricas (declarativas) y operacionales (procedurales): el mismo programa puede verse como especificación de consecuencias lógicas o como receta operativa cuyo comportamiento depende de la estrategia de evaluación.

Síntesis

La programación lógica trata los programas como teorías lógicas y la computación como prueba automatizada: codificando conocimiento en cláusulas se usa unificación y retroceso para realizar especificaciones declarativas mediante búsqueda dirigida por metas.