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 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 importancia en 1951. [1]
Definición
Una cláusula de Horn es una cláusula (una disyunción de literales ) con como máximo un literal positivo, es decir , innecesario .
Por el contrario, una disyunción de literales con como máximo un literal negado se denomina cláusula de cuerno dual .
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 . Tenga en cuenta que la cláusula vacía, que no consta de literales (lo que equivale a falso ) es una cláusula de objetivo. Estos tres tipos de cláusulas de Horn se ilustran en el siguiente ejemplo proposicional :
Tipo de cláusula de cuerno | Forma de disyunción | Forma de implicación | Leer intuitivamente como |
---|---|---|---|
Cláusula definitiva | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t ∨ u | u ← p ∧ q ∧ ... ∧ t | asumir que, si p y q y ... y t toda la bodega, a continuación, también u sostiene |
Hecho | tu | u ← cierto | suponer que u sostiene |
Cláusula de meta | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t | falso ← p ∧ q ∧ ... ∧ t | demostrar que p y q y ... y t toda la bodega [nota 1] |
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:
- ¬ humano ( X ) ∨ mortal ( X )
representa:
- ∀X (¬ humano ( X ) ∨ mortal ( X ))
que es lógicamente equivalente a:
- ∀X ( humano ( X ) → mortal ( X ))
Significado
Las cláusulas de Horn juegan un papel básico en la lógica constructiva y la lógica computacional . Son importantes en el teorema automatizado que demuestra por resolución de primer orden , ya que el resolutivo de dos cláusulas de Horn es en sí mismo una cláusula de Hornos y el resolutivo de una cláusula de gol y una cláusula definitiva es una cláusula de meta. Estas propiedades de las cláusulas de Horn pueden conducir a una mayor eficiencia de demostrar un teorema: la cláusula de meta es la negación de este teorema; consulte la cláusula de meta 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 aguantar. De esta manera, una herramienta de prueba mecánica necesita mantener solo un conjunto de fórmulas (supuestos), en lugar de dos conjuntos (supuestos y (sub) metas).
Las cláusulas de Horn proposicional también son de interés en la complejidad computacional . El problema de encontrar asignaciones de valor de verdad para hacer verdadera una conjunción de cláusulas proposicionales de Horn se conoce como HORNSAT . Este problema es P-completo y se puede resolver en tiempo lineal . [5] Nótese que el problema de satisfacibilidad booleano no restringido es un problema NP-completo .
Programación lógica
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 :
- ( p ∧ q ∧ ... ∧ t ) → u
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 la 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 mostrar u , muestre p y muestre q y ... y muestre t .
Para enfatizar este uso inverso de la cláusula, a menudo se escribe en forma inversa:
- u ← ( p ∧ q ∧ ... ∧ t )
En Prolog esto está escrito como:
u : - p , q , ..., t .
En la programación lógica, el cálculo y la evaluación de consultas se realizan representando la negación de un problema a resolver como una cláusula de meta. Por ejemplo, el problema de resolver la conjunción cuantificada existencialmente de literales positivos:
- ∃ X ( p ∧ q ∧ ... ∧ t )
se representa negando el problema (negando que tenga una solución) y representándolo en la forma lógicamente equivalente de una cláusula de meta:
- ∀ X ( falso ← p ∧ q ∧ ... ∧ t )
En Prolog esto está escrito como:
: - p , q , ..., t .
Resolver el problema equivale a derivar una contradicción, que está representada por la cláusula vacía (o "falso"). La solución del problema es una sustitución de términos por las variables en la cláusula de meta, que se puede extraer de la prueba de contradicción. Utilizadas de esta manera, las cláusulas de objetivo son similares a las consultas conjuntivas en las 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 .
La notación Prolog es realmente ambigua, y el término "cláusula de objetivo" a veces también se usa de manera ambigua. Las variables en una cláusula de meta pueden leerse como cuantificadas universal o existencialmente, y derivar "falso" puede interpretarse como derivar una contradicción o como derivar una solución exitosa del problema a resolver. [ se necesita más explicación ]
Van Emden y Kowalski (1976) investigaron las propiedades de teoría de modelos de 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 implicado por D si y sólo si A es cierto en M . De ello se deduce que un problema P representado por un conjunto existencialmente cuantificada de literales positivos se lógicamente implicado por D si y sólo si P es cierto 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. [6]
Notas
- ^ Como en la demostración del teorema de resolución , "mostrar φ" y "asumir ¬φ" son sinónimos ( demostración indirecta ); ambos corresponden a la misma fórmula, a saber. ¬φ.
Referencias
- ^ Horn, Alfred (1951). "Sobre oraciones que son verdaderas de uniones directas de álgebras". Revista de lógica simbólica . 16 (1): 14-21. doi : 10.2307 / 2268661 . JSTOR 2268661 .
- ^ Makowsky (1987). "Por qué son importantes las fórmulas de cuerno en informática: estructuras iniciales y ejemplos genéricos" (PDF) . Revista de Ciencias de la Computación y Sistemas . 34 (2-3): 266-292. doi : 10.1016 / 0022-0000 (87) 90027-4 .
- ^ Buss, Samuel R. (1998). "Introducción a la teoría de la prueba" . En Samuel R. Buss (ed.). Manual de teoría de la prueba . Estudios de Lógica y Fundamentos de las Matemáticas. 137 . Elsevier BV págs. 1-78. doi : 10.1016 / S0049-237X (98) 80016-5 . ISBN 978-0-444-89840-1. ISSN 0049-237X .
- ^ Lau y Ornaghi (2004). "Especificación de unidades composicionales para el correcto desarrollo del programa en lógica computacional". Apuntes de conferencias en informática . 3049 : 1–29. doi : 10.1007 / 978-3-540-25951-0_1 . ISBN 978-3-540-22152-4.
- ^ Dowling, William F .; Gallier, Jean H. (1984). "Algoritmos de tiempo lineal para probar la satisfacibilidad de fórmulas proposicionales de Horn". Revista de programación lógica . 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) . Revista de la ACM . 23 (4): 733–742. CiteSeerX 10.1.1.64.9246 . doi : 10.1145 / 321978.321991 .