En Horn-klausul är en logisk disjunktion av bokstäver där högst en av bokstäverna är positiv och alla andra är negativa. Den är uppkallad efter Alfred Horn som beskrev dem i en artikel 1951.
En Horn-klausul med exakt en positiv bokstavlig mening är en bestämd klausul, en bestämd klausul utan negativa bokstavliga meningar kallas ibland för ett "faktum", och en Horn-klausul utan en positiv bokstavlig mening kallas ibland för en målklausul. Dessa tre typer av Horn-klausuler illustreras i följande exempel på en proposition:
bestämd sats: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} 
faktum: u {\displaystyle u} 
målklausul: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} 
I det icke-propositionella fallet är alla variabler i en sats implicit universellt kvantifierade med räckvidd för hela satsen. Till exempel:
¬ människa ( X ) ∨ dödlig ( X ) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)} 
står för:
∀ X ( ¬ mänsklig ( X ) ∨ dödlig ( X ) ) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))} 
vilket är logiskt likvärdigt med:
∀ X ( människa ( X ) → dödlig ( X ) ) . {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)). } 
Hornklausuler spelar en grundläggande roll inom konstruktiv logik och beräkningslogik. De är viktiga för automatiserad teoremprövning genom första ordningens upplösning, eftersom upplösaren av två Horn-klausuler i sig själv är en Horn-klausul, och upplösaren av en målklausul och en bestämd klausul är en målklausul. Dessa egenskaper hos Horn-klausuler kan leda till större effektivitet när det gäller att bevisa en sats (representerad som negationen av en målklausul).
Hornklausuler ligger också till grund för logisk programmering, där det är vanligt att skriva bestämda klausuler i form av en implikation:
( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u} 
Upplösningen av en målklausul med en bestämd klausul för att skapa en ny målklausul ligger till grund för SLD-upplösningsregeln, som används för att genomföra logisk programmering och programmeringsspråket Prolog.
I logisk programmering fungerar en bestämd klausul som en målreduktionsprocedur. Till exempel beter sig Horn-klausulen ovan som en procedur:
att visa u {\displaystyle u} , visa p {\displaystyle p}
och visa q {\displaystyle q}
och ⋯ {\displaystyle \cdots } 
och visa t {\displaystyle t}
.
För att betona denna bakåtriktade användning av klausulen skrivs den ofta i bakåtriktad form:
u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)} 
I Prolog skrivs detta som:
u :- p, q, ..., t.Prolog-notationen är faktiskt tvetydig, och termen "målklausul" används ibland också på ett tvetydigt sätt. Variablerna i en målklausul kan tolkas som universellt eller existentiellt kvantifierade, och att härleda "false" kan tolkas antingen som att härleda en motsägelse eller som att härleda en lyckad lösning av det problem som skall lösas.
Van Emden och Kowalski (1976) undersökte de modellteoretiska egenskaperna hos Horn-klausuler i samband med logisk programmering och visade att varje uppsättning bestämda klausuler D har en unik minimimodell M. En atomformel A är logiskt implicerad av D om och endast om A är sann i M. D innebär att ett problem P som representeras av en existentiellt kvantifierad konjunktion av positiva bokstäver är logiskt implicerad av D om och endast om P är sann i M. Den minimala modellsemantiken för Horn-klausuler utgör grunden för den stabila modellsemantiken för logiska program.
Propositionella Horn-klausuler är också av intresse för beräkningskomplexitet, där problemet med att hitta sanningsvärden som gör en konjunktion av propositionella Horn-klausuler sann är ett P-komplett problem (som faktiskt kan lösas på linjär tid), ibland kallat HORNSAT. (Det obegränsade Boolska uppfyllbarhetsproblemet är dock ett NP-komplett problem). Tillfredsställelse av Horn-klausuler av första ordningen är oavgörbar.