Klauzule o rohu je disjunktivní monomial s nejvýše jedním kladným literálem [1] . Studoval Alfred Horn v roce 1951 v souvislosti s jejich důležitou rolí v teorii modelů a univerzální algebře . Následně se staly základem pro logický programovací jazyk Prolog , ve kterém je program přímo sadou Hornových klauzulí, a také našly důležité aplikace v konstruktivní logice a teorii výpočetní složitosti .
U kladných literálů mohou mít klauzule o rohu jednu z následujících forem [1] :
Klauzule rohu s přesně jedním kladným literálem je klauzule určitá ; v univerzální algebře jsou určité klauzule kvazi-identity . Klauzule Horn bez kladných literálů se někdy nazývá cíl nebo dotaz, zejména v logickém programování . Hornova formule je konjunkcí Hornových klauzulí, tedy formule v konjunktivní normální formě , jejíž všechny klauze jsou Hornovy. Dvojitá klauzule Horn je klauzule s nejvýše jedním záporným literálem.
Příklad (určité) klauzule o rohu:
.Tento vzorec lze převést na ekvivalentní vzorec s implikací [1] :
nebo [1] :
.Klauzule rohů mohou být buď výrokové formule nebo formule prvního řádu , v závislosti na tom, zda jsou uvažovány výrokové literály nebo literály prvního řádu.
Klauzule o rohu souvisejí s dokazováním teorému prostřednictvím usnesení prvního řádu , protože řešením dvou klauzulí Horn je klauzule Horn. Kromě toho je řešením cíle a klauzulí definitivní také klauzule Hornova. V automatickém dokazování teorémů to může být efektivnější při dokazování teorému prezentovaného jako cíl.
Řešení cíle se specifickou klauzulí k získání nového cíle je základem pro pravidlo odvození v rozlišení SLD , používané k implementaci logického programování a programovacího jazyka Prolog . V logickém programování se určitá klauzule používá jako postup snižování cíle. Například klauzule z výše uvedeného příkladu funguje jako procedura: "to show , show , a " .
Pro zdůraznění této obrácené aplikace disjunkce se často používá operátor :
V Prologu je to napsáno takto:
u :- p, q, ..., t.Výrokové Hornovy klauzule jsou také zajímavé v teorii výpočetní složitosti , kde HORNSATův problém nalezení sady pravdivostních hodnot, které splňují konjunkci Hornových klauzulí, je P-úplný . Toto je varianta třídy P pro SAT , nejdůležitější NP-úplný problém. Problém splnitelnosti Hornových klauzulí 1. řádu není řešitelný.