Cláusula de cuerno - Horn clause
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.
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 ; una cláusula definida sin literales negativos es una cláusula unitaria , y una cláusula unitaria sin variables es un hecho ; 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 |
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 . Tenga en cuenta que el problema de satisfacibilidad booleano sin restricciones 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 se pueden leer 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.
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.