Hornova věta je logická disjunkce literálů, kde nejvýše jeden z literálů je kladný a všechny ostatní jsou záporné. Je pojmenována po Alfredu Hornovi, který ji popsal v článku z roku 1951.
Hornova věta s přesně jedním kladným literálem je definitní věta, definitní věta bez záporných literálů se někdy nazývá "fakt" a Hornova věta bez kladného literálu se někdy nazývá cílová věta. Tyto tři druhy Hornových klauzulí ilustruje následující výrokový příklad:
věta určitá: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} 
skutečnost: u {\displaystyle u} 
cílovou doložku: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} 
V nepropozičním případě jsou všechny proměnné v klauzuli implicitně univerzálně kvantifikovány s rozsahem celé klauzule. Tak např:
¬ člověk ( X ) ∨ smrtelný ( X ) {\displaystyle \neg {\text{člověk}}(X)\lor {\text{smrtelný}}(X)} 
znamená:
∀ X ( ¬ člověk ( X ) ∨ smrtelný ( X ) ) {\displaystyle \forall X(\neg {\text{člověk}}(X)\lor {\text{smrtelný}}(X))} 
což je logicky ekvivalentní:
∀ X ( člověk ( X ) → smrtelník ( X ) ) . {\displaystyle \forall X({\text{člověk}}(X)\pravá šipka {\text{smrtelný}}(X)). } 
Hornovy klauzule hrají základní roli v konstruktivní a výpočtové logice. Jsou důležité při automatizovaném dokazování tvrzení pomocí rezoluce prvního řádu, protože resolvent dvou Hornových klauzulí je sám Hornovou klauzulí a resolvent cílové klauzule a definiční klauzule je cílovou klauzulí. Tyto vlastnosti Hornových klauzulí mohou vést k větší efektivitě při dokazování věty (reprezentované jako negace cílové klauzule).
Hornovy věty jsou také základem logického programování, kde se běžně zapisují definiční věty ve formě implikace:
( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u} 
Rozlišení cílové klauzule s definiční klauzulí za účelem vytvoření nové cílové klauzule je základem inferenčního pravidla SLD, které se používá při implementaci logického programování a programovacího jazyka Prolog.
V logickém programování se definiční klauzule chová jako procedura redukce cílů. Například výše zapsaná Hornova klauzule se chová jako procedura:
zobrazit u {\displaystyle u} , zobrazit p {\displaystyle p}
a zobrazit q {\displaystyle q}
a ⋯ {\displaystyle \cdots } 
a show t {\displaystyle t}
.
Aby se zdůraznilo toto zpětné užití věty, píše se často ve zpětném tvaru:
u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)} 
V jazyce Prolog se to zapíše jako:
u :- p, q, ..., t.Zápis v Prologu je ve skutečnosti nejednoznačný a termín "cílová věta" se také někdy používá nejednoznačně. Proměnné v cílové klauzuli lze číst jako univerzálně nebo existenčně kvantifikované a odvození "false" lze interpretovat buď jako odvození rozporu, nebo jako odvození úspěšného řešení řešeného problému.
Van Emden a Kowalski (1976) zkoumali modelově teoretické vlastnosti Hornových klauzulí v kontextu logického programování a ukázali, že každá množina definičních klauzulí D má jedinečný minimální model M. Atomická formule A je logicky implikována D tehdy a jen tehdy, je-li A pravdivá v M. Z toho vyplývá, že problém P reprezentovaný existenčně kvantifikovanou konjunkcí pozitivních literálů je logicky implikován D tehdy a jen tehdy, je-li P pravdivá v M. Minimální modelová sémantika Hornových klauzulí je základem stabilní modelové sémantiky logických programů.
Propoziční Hornovy klauzule jsou zajímavé také z hlediska výpočetní složitosti, kde problém nalezení přiřazení pravdivostních hodnot, aby konjunkce propozičních Hornových klauzulí byla pravdivá, je P-úplný problém (ve skutečnosti řešitelný v lineárním čase), někdy nazývaný HORNSAT. (Problém neomezené booleovské splnitelnosti je však problémem NP-úplným.) Splnitelnost Hornových klauzulí prvního řádu je nerozhodnutelná.