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

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

cílovou doložku: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} $\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)} $\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))} $\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)). } $\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} $(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} $u$ , zobrazit p {\displaystyle p} $p$ a zobrazit q {\displaystyle q} a ⋯ {\displaystyle \cdots } $\cdots$ a show t {\displaystyle t} $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)} $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á.

Otázky a odpovědi

Otázka: Co je to rohová doložka?

Odpověď: Hornova věta je logická disjunkce literálů, kde nejvýše jeden z literálů je kladný a všechny ostatní jsou záporné.

Otázka: Kdo je jako první popsal?

Odpověď: Poprvé je popsal Alfred Horn v článku z roku 1951.

Otázka: Co je to definiční klauzule?

A: Hornova věta s přesně jedním kladným literálem se nazývá definitní věta.

Otázka: Co je to fakt?

A: Určitá věta bez záporných literálů se někdy označuje jako "fakt".

Otázka: Co je to cílová věta?

A: Hornova věta bez kladného literálu se někdy nazývá cílová věta.

Otázka: Jak fungují proměnné v nepropozičních větách?

Odpověď: V nepropozičním případě jsou všechny proměnné v klauzuli implicitně univerzálně kvantifikovány s rozsahem celé klauzule. To znamená, že se vztahují na každou část výroku.

Otázka: Jakou roli hrají Hornovy klauzule v konstruktivní a výpočtové logice? Odpověď: Hornovy klauzule hrají důležitou roli v automatizovaném dokazování tvrzení pomocí rezoluce prvního řádu, protože rezoluce dvou Hornových klauzulí nebo mezi jednou cílovou a jednou definiční klauzulí lze využít k větší efektivitě při dokazování něčeho, co je reprezentováno jako negace jeho cílové klauzule. Používají se také jako základ logických programovacích jazyků, jako je Prolog, kde se chovají jako procedury redukce cílů.