La programación lógica es un paradigma de programación que se basa en gran medida en la lógica formal . Cualquier programa escrito en un lenguaje de programación lógica es un conjunto de oraciones en forma lógica, que expresan hechos y reglas sobre algún dominio de problemas. Las principales familias de lenguajes de programación lógica incluyen Prolog , programación de conjuntos de respuestas (ASP) y Datalog . En todos estos lenguajes, las reglas se escriben en forma de cláusulas :
Hse llama la cabeza de la regla y , ..., se llama cuerpo . Los hechos son reglas que no tienen cuerpo y están escritas en forma simplificada:B1Bn
En el caso más simple en el que,, H... , son todas fórmulas atómicas , estas cláusulas se denominan cláusulas definidas o cláusulas de Horn . Sin embargo, hay muchas extensiones de este caso simple, siendo la más importante el caso en el que las condiciones en el cuerpo de una cláusula también pueden ser negaciones de fórmulas atómicas. Los lenguajes de programación lógica que incluyen esta extensión tienen las capacidades de representación del conocimiento de una lógica no monótona .B1Bn
En ASP y Datalog, los programas lógicos tienen solo una lectura declarativa , y su ejecución se realiza mediante un procedimiento de prueba o generador de modelos cuyo comportamiento no está destinado a ser controlado por el programador. Sin embargo, en la familia de lenguajes Prolog, los programas lógicos también tienen una interpretación procedimental como procedimientos de reducción de objetivos:
basado en un ejemplo usado por Terry Winograd [1] para ilustrar el lenguaje de programación Planner . Como cláusula en un programa lógico, se puede usar como un procedimiento para probar si Xes fallibleprobando si Xes human, y como un procedimiento para encontrar un Xcuál es fallibleal encontrar un Xcuál es human. Incluso los hechos tienen una interpretación procesal. Por ejemplo, la cláusula:
se puede utilizar como un procedimiento para mostrar que socrateses humany como un procedimiento para encontrar un Xque es human"asignando" socratesa X.