En lógica matemática y programación lógica , una cláusula de Horn es una fórmula lógica de una forma particular similar a una regla que le otorga propiedades útiles para su uso en programación lógica, especificación formal , álgebra universal y teoría de modelos . Las cláusulas de Horn reciben su nombre del lógico Alfred Horn , quien señaló por primera vez su importancia en 1951. [1]
Una cláusula de Horn es una cláusula disyuntiva (una disyunción de literales ) con como máximo un literal positivo, es decir , no negado .
Por el contrario, una disyunción de literales con como máximo un literal negado se denomina cláusula de Horn dual .
Una cláusula Horn con exactamente un literal positivo es una cláusula definida o una cláusula Horn estricta ; [2] una cláusula definida sin literales negativos es una cláusula unitaria , [3] y una cláusula unitaria sin variables es un hecho ; [4] Una cláusula Horn sin un literal positivo es una cláusula de objetivo . La cláusula vacía, que no consta de literales (lo que es equivalente a false ) es una cláusula de objetivo. Estos tres tipos de cláusulas Horn se ilustran en el siguiente ejemplo proposicional :
Todas las variables de una cláusula se cuantifican de forma implícita y universal , y su alcance es la cláusula completa. Por ejemplo:
significa:
lo cual es lógicamente equivalente a:
Las cláusulas de Horn desempeñan un papel básico en la lógica constructiva y la lógica computacional . Son importantes en la demostración automatizada de teoremas por resolución de primer orden , porque el resolvente de dos cláusulas de Horn es en sí mismo una cláusula de Horn, y el resolvente de una cláusula de objetivo y una cláusula definida es una cláusula de objetivo. Estas propiedades de las cláusulas de Horn pueden llevar a una mayor eficiencia en la demostración de un teorema: la cláusula de objetivo es la negación de este teorema; vea la cláusula de objetivo en la tabla anterior. Intuitivamente, si deseamos demostrar φ, asumimos ¬φ (el objetivo) y verificamos si tal suposición conduce a una contradicción. Si es así, entonces φ debe cumplirse. De esta manera, una herramienta de demostración mecánica necesita mantener solo un conjunto de fórmulas (supuestos), en lugar de dos conjuntos (supuestos y (sub)objetivos).
Las cláusulas proposicionales de Horn también son de interés en la complejidad computacional . El problema de encontrar asignaciones de valores de verdad para hacer que una conjunción de cláusulas proposicionales de Horn sea verdadera se conoce como HORNSAT . Este problema es P-completo y solucionable en tiempo lineal . [6] Por el contrario, el problema de satisfacibilidad booleano sin restricciones es un problema NP-completo .
En álgebra universal , las cláusulas de Horn definidas generalmente se denominan cuasi-identidades ; las clases de álgebras definibles por un conjunto de cuasi-identidades se denominan cuasivariedades y disfrutan de algunas de las buenas propiedades de la noción más restrictiva de variedad , es decir, una clase ecuacional. [7] Desde el punto de vista de la teoría de modelos, las oraciones de Horn son importantes ya que son exactamente (hasta la equivalencia lógica) aquellas oraciones preservadas bajo productos reducidos ; en particular, se preservan bajo productos directos . Por otro lado, hay oraciones que no son de Horn pero que, sin embargo, se preservan bajo productos directos arbitrarios. [8]
Las cláusulas de Horn también son la base de la programación lógica , donde es común escribir cláusulas definidas en forma de implicación :
De hecho, la resolución de una cláusula objetivo con una cláusula definida para producir una nueva cláusula objetivo es la base de la regla de inferencia de resolución SLD , utilizada en la implementación del lenguaje de programación lógica Prolog .
En programación lógica, una cláusula definida se comporta como un procedimiento de reducción de objetivos. Por ejemplo, la cláusula de Horn escrita anteriormente se comporta como el procedimiento:
Para enfatizar este uso inverso de la cláusula, a menudo se escribe en forma inversa:
En Prolog esto se escribe así:
u :- p , q , ..., t .En programación lógica, una cláusula de objetivo, que tiene la forma lógica
representa la negación de un problema a resolver. El problema en sí es una conjunción cuantificada existencialmente de literales positivos:
La notación Prolog no tiene cuantificadores explícitos y se escribe en la forma:
:- p , q , ..., t .Esta notación es ambigua en el sentido de que puede leerse como un enunciado del problema o como un enunciado de la negación del problema. Sin embargo, ambas lecturas son correctas. En ambos casos, resolver el problema equivale a derivar la cláusula vacía. En la notación Prolog esto es equivalente a derivar:
:- verdadero .Si la cláusula de objetivo de nivel superior se lee como la negación del problema, entonces la cláusula vacía representa falso y la prueba de la cláusula vacía es una refutación de la negación del problema. Si la cláusula de objetivo de nivel superior se lee como el problema en sí, entonces la cláusula vacía representa verdadero y la prueba de la cláusula vacía es una prueba de que el problema tiene una solución.
La solución del problema es una sustitución de términos por las variables X en la cláusula de objetivo de nivel superior, que se puede extraer de la prueba de resolución. Utilizadas de esta manera, las cláusulas de objetivo son similares a las consultas conjuntivas en bases de datos relacionales , y la lógica de la cláusula de Horn es equivalente en potencia computacional a una máquina de Turing universal .
Van Emden y Kowalski (1976) investigaron las propiedades de teoría de modelos de las cláusulas de Horn en el contexto de la programación lógica, mostrando que cada conjunto de cláusulas definidas D tiene un modelo mínimo único M . Una fórmula atómica A está implícita lógicamente por D si y solo si A es verdadera en M . De ello se deduce que un problema P representado por una conjunción cuantificada existencialmente de literales positivos está implícito lógicamente por D si y solo si P es verdadera en M . La semántica del modelo mínimo de las cláusulas de Horn es la base para la semántica del modelo estable de los programas lógicos. [9]