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 llevan el nombre del lógico Alfred Horn , quien señaló por primera vez su significado 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 doble cuerno .
Una cláusula de Horn con exactamente un literal positivo es una cláusula definida o una cláusula de 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 de Horn sin un literal positivo es una cláusula de objetivo . Tenga en cuenta que la cláusula vacía, que no consta de literales (lo que equivale a false ), es una cláusula de objetivo. Estos tres tipos de cláusulas de Horn se ilustran en el siguiente ejemplo proposicional :
Todas las variables de una cláusula se cuantifican implícitamente de forma universal y el alcance es la cláusula completa. Así, por ejemplo:
representa:
que es lógicamente equivalente a:
Las cláusulas de Horn juegan un papel básico en la lógica constructiva y la lógica computacional . Son importantes en la demostración automatizada de teoremas mediante resolución de primer orden , porque el resolutivo de dos cláusulas de Horn es en sí mismo una cláusula de Horn, y el resolutivo 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 conducir a una mayor eficiencia en la demostración de un teorema: la cláusula objetivo es la negación de este teorema; consulte la cláusula de objetivo en la tabla anterior. Intuitivamente, si queremos probar φ, asumimos ¬φ (el objetivo) y comprobamos si tal suposición conduce a una contradicción. Si es así, entonces φ debe mantenerse. 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 verdadera una conjunción de cláusulas proposicionales de Horn se conoce como HORNSAT . Este problema es P-completo y solucionable en tiempo lineal . [6]
Tenga en cuenta que el problema de satisfacibilidad booleano sin restricciones es un problema NP-completo .
En álgebra universal , las cláusulas de Horn definidas generalmente se denominan cuasiidentidades ; Las clases de álgebras definibles por un conjunto de cuasiidentidades 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 conservan bajo productos directos . Por otro lado, hay oraciones que no son Horn pero que, sin embargo, se conservan bajo productos directos arbitrarios. [8]
Las cláusulas 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 de objetivo con una cláusula definida para producir una nueva cláusula de 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 Horn escrita arriba se comporta como el procedimiento:
Para enfatizar este uso inverso de la cláusula, a menudo se escribe en la forma inversa:
En Prolog esto se escribe como:
tu :- 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 existencialmente cuantificada de literales positivos:
La notación Prolog no tiene cuantificadores explícitos y está escrita 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 notación Prolog esto equivale 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. Usadas 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 poder computacional a una máquina de Turing universal .
Van Emden y Kowalski ( 1976) investigaron las propiedades teóricas 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á lógicamente implícita en D si y sólo si A es verdadera en M . De ello se deduce que un problema P representado por una conjunción existencialmente cuantificada de literales positivos está lógicamente implicado por D si y sólo si P es verdadero en M. La semántica del modelo mínimo de las cláusulas de Horn es la base de la semántica del modelo estable de programas lógicos. [9]