Klauzule o rohu

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 .

Konstrukce a definice

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] :

.

Aplikace

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ý.

Poznámky

  1. 1 2 3 4 Ricardo Caferra. Logika pro informatiku a umělou inteligenci. - John Wiley & Sons, 2013. - 537 s. — ISBN 978-1-118-60426-7 .

Literatura

Odkazy