cláusula de cuerno

En lógica matemática y programación lógica , una cláusula de Horn es una fórmula lógica con una forma particular de regla que le confiere 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 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 dual de Horn .

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 meta . La cláusula vacía, que no consta de literales (lo cual es equivalente a falso ), es una cláusula de meta. Estos tres tipos de cláusulas de Horn se ilustran en el siguiente ejemplo proposicional :

Todas las variables en una cláusula se cuantifican implícitamente de forma universal, siendo el alcance la cláusula completa. Por ejemplo:

significa:

lo cual es lógicamente equivalente a:

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 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 como:

u :- p , q , ..., t .

En programación lógica, una cláusula 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 de Prolog no tiene cuantificadores explícitos y se escribe de la siguiente forma:

:- p , q , ..., t .

Esta notación es ambigua en el sentido de que puede interpretarse como un enunciado del problema o como una negación del mismo. Sin embargo, ambas interpretaciones son correctas. En ambos casos, resolver el problema equivale a derivar la cláusula vacía. En notación de Prolog, esto es equivalente a derivar:

:- verdadero .

Si la cláusula principal del objetivo se interpreta como la negación del problema, entonces la cláusula vacía representa lo falso y la prueba de la cláusula vacía refuta dicha negación. Si la cláusula principal del objetivo se interpreta como el problema en sí, entonces la cláusula vacía representa lo verdadero y la prueba de la cláusula vacía demuestra que el problema tiene solución.

La solución del problema consiste en sustituir términos por las variables X en la cláusula objetivo de nivel superior, lo cual se puede extraer de la prueba de resolución. Utilizadas de esta manera, las cláusulas objetivo son similares a las consultas conjuntivas en bases de datos relacionales , y la lógica de las cláusulas de Horn es equivalente en potencia computacional a una máquina de Turing universal .

Van Emden y Kowalski (1976) investigaron las propiedades de la teoría de modelos de las cláusulas de Horn en el contexto de la programación lógica, demostrando que todo conjunto de cláusulas definidas D tiene un modelo mínimo único M. Una fórmula atómica A está lógicamente implicada 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á lógicamente implicado por D si y solo 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 los programas lógicos. ^{[ 9 ]}

• Cláusulas Horn restringidas
• Cálculo proposicional

• Burris, Stanley; Sankappanavar, HP, eds. (1981). Un curso de álgebra universal . Springer-Verlag. ISBN 0-387-90578-2.
• Buss, Samuel R. (1998). «Introducción a la teoría de la demostración» . En Samuel R. Buss (ed.). Manual de teoría de la demostración . Estudios en lógica y fundamentos de las matemáticas. Vol.  137. Elsevier BV, pp. 1–78 . doi : 10.1016/S0049-237X(98)80016-5 . ISBN  978-0-444-89840-1ISSN 0049-237X​​ 
• Chang, Chen Chung ; Keisler, H. Jerome (1990) [1973]. Teoría de modelos . Estudios en lógica y fundamentos de las matemáticas (3.ª  ed.). Elsevier. ISBN 978-0-444-88054-3.
• Dowling, William F.; Gallier, Jean H. (1984). "Algoritmos de tiempo lineal para probar la satisfacibilidad de fórmulas proposicionales de Horn" . Journal of Logic Programming . 1 (3): 267– 284. doi : 10.1016/0743-1066(84)90014-1 .
• van Emden, MH ; Kowalski, RA (1976). "La semántica de la lógica de predicados como lenguaje de programación" (PDF) . Journal of the ACM . 23 (4): 733–742 . CiteSeerX 10.1.1.64.9246 . doi : 10.1145/321978.321991 . S2CID 11048276 .  
• Horn, Alfred (1951). "Sobre las oraciones que son verdaderas de uniones directas de álgebras". Journal of Symbolic Logic . 16 (1): 14– 21. doi : 10.2307/2268661 . JSTOR 2268661. S2CID 42534337 .  
• Lau, Kung-Kiu; Ornaghi, Mario (2004). «Especificación de unidades compositivas para el correcto desarrollo de programas en lógica computacional». Desarrollo de programas en lógica computacional . Notas de clase en ciencias de la computación. Vol.  3049. pp. 1–29 . doi : 10.1007/978-3-540-25951-0_1 . ISBN  978-3-540-22152-4.
• Makowsky, JA (1987). "Por qué las fórmulas de Horn importan en la informática: estructuras iniciales y ejemplos genéricos" (PDF) . Journal of Computer and System Sciences . 34 ( 2–3 ): 266–292 . doi : 10.1016/0022-0000(87)90027-4 .