Una cláusula Horn es una disyunción de literales en la que a lo sumo uno de los literales es positivo y todos los demás son negativos. El nombre procede de Alfred Horn, que las introdujo en 1951. En lógica proposicional y de primer orden las cláusulas Horn son una clase importante por sus propiedades algorítmicas y semánticas.
Se distinguen varios casos particulares:
- Una cláusula Horn con exactamente un literal positivo se denomina cláusula definida (definite clause). Si además no contiene literales negativos (es decir, sólo el literal positivo), se habla de un hecho (fact).
- Una cláusula Horn sin literales positivos se suele llamar cláusula objetivo o cláusula meta (goal clause o negative clause).
En notación proposicional, estos tres tipos pueden ilustrarse por ejemplos de la forma:
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 \vee \neg t} 
En el caso de cláusulas de primer orden (no proposicional), las variables que aparecen en una cláusula se consideran implícitamente cuantificadas de forma universal sobre toda la cláusula. Por ejemplo:
¬ humano ( X ) ∨ mortal ( X ) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)} 
se interpreta como
∀ X ( ¬ humano ( X ) ∨ mortal ( X ) ) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))} 
y es lógicamente equivalente a la implicación universal:
∀ X ( humano ( X ) → mortal ( X ) ) . {\displaystyle \forall X({\text{human}(X)\rightarrow {\text{mortal}}(X)). } 
Las cláusulas de Horn son cerradas bajo resolución: el resolvente de dos cláusulas de Horn es otra cláusula de Horn; en particular, el resolvente de una cláusula definida (con cabeza) y una cláusula objetivo (sin cabeza) es una cláusula objetivo. Esta estabilidad hace que la demostración automática de teoremas por resolución sea más eficiente cuando la teoría está formada por cláusulas de Horn.
Las cláusulas de Horn son la base de la programación lógica, donde las cláusulas definidas suelen escribirse en forma implicativa
( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\ rightarrow u} 
La resolución de una cláusula objetivo con una cláusula definida para obtener otra cláusula objetivo es la base de la regla SLD (selección lineal por resolución), que se emplea para implementar la programación lógica y el lenguaje Prolog. En programación lógica, una cláusula definida expresa cómo reducir la demostración de un objetivo en la demostración de subobjetivos (el cuerpo de la cláusula).
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 retroactivo, las cláusulas de programación lógica suelen escribirse en forma de "reglas" con la flecha hacia la izquierda:
u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)} 
En Prolog esta regla se escribe típicamente como:
u :- p, q, ..., t.
Algunas ambigüedades terminológicas persisten: el término "cláusula meta" puede emplearse en contextos distintos para significar una cláusula con variables interpretadas universalmente o existencialmente; asimismo, la derivación de "falso" puede entenderse como prueba de contradicción o como señal de éxito según la codificación del problema en el programa.
En trabajo fundamental, Van Emden y Kowalski (1976) analizaron la semántica de programas formados por cláusulas definidas (definite programs). Mostraron que todo conjunto de cláusulas definidas D tiene un único modelo mínimo (el menor modelo de Herbrand) M; una fórmula atómica A es consecuencia lógica de D si y sólo si A es verdadera en M. Esta caracterización semántica es la base de la semántica de modelos mínimos y de la semántica estable en programas lógicos no monotónicos.
Desde el punto de vista de la complejidad, la satisfacibilidad de cláusulas proposicionales de Horn (HORNSAT) puede resolverse en tiempo lineal y es P-completo; en contraste, la satisfacibilidad booleana sin restricciones es NP-completa. En primer orden, la satisfacibilidad o la validez de cláusulas Horn sin restricciones de símbolos de función es, en general, indecidible. Sin embargo, si se prohíben los símbolos de función (como en Datalog), muchas preguntas de razonamiento y evaluación se vuelven decidibles y, en la práctica, susceptibles de evaluación eficiente.
Además de la programación lógica, las cláusulas de Horn aparecen en otras áreas como la verificación formal, las bases de datos deductivas y la representación del conocimiento, donde su estructura facilita algoritmos de inferencia y optimizaciones.
Véase también: disyunción lógica, programación lógica, Prolog, problema de la satisfabilidad booleana, NP-completo.