Cláusula de Horn
Una cláusula Horn es una disyunción lógica de literales, en la que como máximo uno de los literales es positivo y todos los demás son negativos. Recibe su nombre de Alfred Horn, que las describió en un artículo de 1951.
Una cláusula Horn con exactamente un literal positivo es una cláusula definida; una cláusula definida sin literales negativos se llama a veces "hecho"; y una cláusula Horn sin un literal positivo se llama a veces cláusula meta. Estos tres tipos de cláusulas Horn se ilustran en el siguiente ejemplo proposicional:
cláusula definida: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} 
hecho: u {\displaystyle u} 
cláusula de meta: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\neg plor \neg q\vee \cdots \neg t} 
En el caso no proposicional, todas las variables de una cláusula están implícitamente cuantificadas universalmente con alcance a toda la cláusula. Así, por ejemplo:
¬ humano ( X ) ∨ mortal ( X ) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)} 
significa:
∀ X ( ¬ humano ( X ) ∨ mortal ( X ) ) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))} 
que es lógicamente equivalente a:
∀ X ( humano ( X ) → mortal ( X ) ) . {\displaystyle \forall X({\text{human}(X)\rightarrow {\text{mortal}(X)). } 
Las cláusulas de Horn desempeñan un papel básico en la lógica constructiva y la lógica computacional. Son importantes en la demostración automatizada de teoremas por resolución de primer orden, porque el resolvente de dos cláusulas de Horn es en sí mismo una cláusula de Horn, y el resolvente de una cláusula meta y una cláusula definida es una cláusula meta. Estas propiedades de las cláusulas de Horn pueden conducir a una mayor eficiencia en la demostración de un teorema (representado como la negación de una cláusula meta).
Las cláusulas de Horn son también la base de la programación lógica, donde es habitual escribir cláusulas definidas en forma de implicación:
( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\ rightarrow u} 
De hecho, la resolución de una cláusula meta con una cláusula definida para producir una nueva cláusula meta es la base de la regla de inferencia de resolución SLD, utilizada para implementar la programación lógica y el lenguaje de programación Prolog.
En programación lógica una cláusula definida se comporta como un procedimiento de reducción de metas. Por ejemplo, la cláusula Horn escrita anteriormente se comporta como el procedimiento:
para mostrar u {\displaystyle u} , mostrar p {\displaystyle p}
y mostrar q {\displaystyle q}
y ⋯ {\displaystyle \cdots } 
y show t {\displaystyle t} 
.
Para enfatizar este uso retrospectivo de la cláusula, a menudo se escribe en la forma retrospectiva:
u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)} 
En Prolog esto se escribe como:
u :- p, q, ..., t.La notación Prolog es en realidad ambigua, y el término "cláusula meta" se utiliza a veces también de forma ambigua. Las variables de una cláusula 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.
Van Emden y Kowalski (1976) investigaron las propiedades teóricas del modelo 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 único modelo mínimo M. Una fórmula atómica A está lógicamente implicada por 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 de modelo mínimo de las cláusulas de Horn es la base de la semántica de modelo estable de los programas lógicos.
Las cláusulas proposicionales de Horn también son de interés en la complejidad computacional, donde el problema de encontrar asignaciones de valores de verdad para hacer que una conjunción de cláusulas proposicionales de Horn sea verdadera es un problema P-completo (de hecho resoluble en tiempo lineal), a veces llamado HORNSAT. (Sin embargo, el problema de la satisfabilidad booleana no restringida es un problema NP-completo). La satisfacción de las cláusulas de Horn de primer orden es indecidible.
Preguntas y respuestas
P: ¿Qué es una cláusula de Horn?
R: Una cláusula Horn es una disyunción lógica de literales, en la que como máximo uno de los literales es positivo y todos los demás son negativos.
P: ¿Quién las describió por primera vez?
R: Alfred Horn las describió por primera vez en un artículo en 1951.
P: ¿Qué es una cláusula definida?
R: Una cláusula Horn con exactamente un literal positivo se denomina cláusula definida.
P: ¿Qué es un hecho?
R: Una cláusula definida sin literales negativos se denomina a veces "hecho".
P: ¿Qué es una cláusula meta?
R: Una cláusula de Horn sin un literal positivo se denomina a veces cláusula meta.
P: ¿Cómo funcionan las variables en los casos no proposicionales?
R: En el caso no proposicional, todas las variables de una cláusula están implícitamente cuantificadas universalmente con alcance a toda la cláusula. Esto significa que se aplican a todas las partes de la declaración.
P: ¿Qué papel desempeñan las cláusulas de Horn en la lógica constructiva y la lógica computacional? R: Las cláusulas de Horn desempeñan un papel importante en la demostración automatizada de teoremas mediante resolución de primer orden porque el resolvente de dos cláusulas de Horn o entre una cláusula meta y una definida puede utilizarse para crear una mayor eficiencia a la hora de demostrar algo representado como la negación de su cláusula meta. También se utilizan como base para lenguajes de programación lógica como Prolog, donde se comportan como procedimientos de reducción de metas.
