Hornova klauzule

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} {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

skutečnost: u {\displaystyle u} {\displaystyle u}

cílovou doložku: ¬ p ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg 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)} {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)}

znamená:

X ( ¬ člověk ( X ) smrtelný ( X ) ) {\displaystyle \forall X(\neg {\text{člověk}}(X)\lor {\text{smrtelný}}(X))} {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))}

což je logicky ekvivalentní:

X ( člověk ( X ) → smrtelník ( X ) ) . {\displaystyle \forall X({\text{člověk}}(X)\pravá šipka {\text{smrtelný}}(X)). } {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(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} {\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}{\displaystyle u} , zobrazit p {\displaystyle p}{\displaystyle p} a zobrazit q {\displaystyle q}q a {\displaystyle \cdots } {\displaystyle \cdots }a show t {\displaystyle 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)} {\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á.


AlegsaOnline.com - 2020 / 2021 - License CC3