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 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 significado en 1951.

Definición

A Horn clause is a clause (a disjunction of literals) with at most one positive, o.n.e. negative, literal.

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 Horn con exactamente un literal positivo es una cláusula definida o una cláusula 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 objetivo. Tenga en cuenta que la cláusula vacía, que no contiene 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:

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:

¬ humanos()X) mortal()X)

significa:

ОX(¬ humanos()X) mortal()X)

que es lógicamente equivalente a:

VALXhumanos()X) → mortal()X)

Importancia

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 solucionador de dos cláusulas de Horn es en sí mismo una cláusula de Horn, y el solucionador 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. Tenga en cuenta que el problema de satisfacibilidad booleano sin restricciones es un problema NP-completo.

Programación lógica

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:

()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 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 mostrar u, show p y espectáculo q y... t.

Para enfatizar este uso inverso de la cláusula, a menudo se escribe en la forma inversa:

u ←p ∧ q ∧... ∧ t)

En Prolog esto se escribe como:

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

En 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 objetivo. Por ejemplo, el problema de resolver la conjunción existencialmente cuantificada de literales positivos:

∃X ()p ∧ q ∧... ∧ t)

se representa negando el problema (negando que tenga 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 se escribe como:

:- p, q, ... t.

Resolver el problema equivale a derivar una contradicción, que está representada por la cláusula vacía (o "falsa"). 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 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.

La notación Prolog es en realidad ambigua y el término “cláusula de objetivo” a veces también se utiliza 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 derivar una solución exitosa del problema a resolver.

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.