Hornova klauzula

Hornova klauzula je logická disjunkcia literálov, kde najviac jeden z literálov je kladný a všetky ostatné sú záporné. Je pomenovaná podľa Alfreda Horna, ktorý ju opísal v článku v roku 1951.

Hornova veta s presne jedným kladným literálom je určitá veta; určitá veta bez záporných literálov sa niekedy nazýva "fakt"; a Hornova veta bez kladného literálu sa niekedy nazýva cieľová veta. Tieto tri druhy Hornových klauzúl ilustruje nasledujúci propozičný príklad:

určitá veta: ¬ 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$

skutočnosť: u {\displaystyle u} $u$

cieľová klauzula: ¬ 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čnom prípade sú všetky premenné v klauzule implicitne univerzálne kvantifikované s rozsahom celej klauzuly. Tak napríklad:

¬ človek ( X ) ∨ smrteľník ( X ) {\displaystyle \neg {\text{človek}}(X)\lor {\text{smrteľník}}(X)} $\neg {\text{human}}(X)\lor {\text{mortal}}(X)$

znamená:

∀ X ( ¬ človek ( X ) ∨ smrteľník ( X ) ) {\displaystyle \forall X(\neg {\text{ľudský}}(X)\lor {\text{smrteľný}}(X))} $\forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))$

čo je logicky ekvivalentné:

∀ X ( človek ( X ) → smrteľník ( X ) ) . {\displaystyle \forall X({\text{ľudský}}(X)\pravá šipka {\text{smrteľný}}(X)). } $\forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).$

Hornove klauzuly zohrávajú základnú úlohu v konštruktívnej logike a výpočtovej logike. Sú dôležité pri automatizovanom dokazovaní tvrdení pomocou rezolúcie prvého rádu, pretože rezolvent dvoch Hornových klauzúl je sám Hornovou klauzulou a rezolvent cieľovej klauzuly a definitnej klauzuly je cieľovou klauzulou. Tieto vlastnosti Hornových klauzúl môžu viesť k väčšej efektivite pri dokazovaní vety (reprezentovanej ako negácia cieľovej klauzuly).

Hornove klauzuly sú tiež základom logického programovania, kde je bežné zapisovať definičné klauzuly vo forme implikácie:

( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u} $(p\wedge q\wedge \cdots \wedge t)\rightarrow u$

Rozlíšenie cieľovej klauzuly s definitívnou klauzulou na vytvorenie novej cieľovej klauzuly je v skutočnosti základom inferenčného pravidla SLD resolution, ktoré sa používa pri implementácii logického programovania a programovacieho jazyka Prolog.

V logickom programovaní sa definičná klauzula správa ako procedúra redukcie cieľa. Napríklad vyššie zapísaná Hornova klauzula sa správa ako procedúra:

zobraziť u {\displaystyle u} $u$ , zobraziť p {\displaystyle p} $p$ a zobraziť q {\displaystyle q} a ⋯ {\displaystyle \cdots } $\cdots$ a show t {\displaystyle t} $t$ .

Aby sa zdôraznilo toto spätné použitie klauzuly, často sa píše v spätnom tvare:

u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)} $u\leftarrow (p\land q\land \cdots \land t)$

V jazyku Prolog sa to zapisuje ako:

u :- p, q, ..., t.

Zápis v Prologu je v skutočnosti nejednoznačný a termín "cieľová klauzula" sa tiež niekedy používa nejednoznačne. Premenné v cieľovej klauzule možno čítať ako univerzálne alebo existenčne kvantifikované a odvodenie "false" možno interpretovať buď ako odvodenie protirečenia, alebo ako odvodenie úspešného riešenia riešeného problému.

Van Emden a Kowalski (1976) skúmali modelovo-teoretické vlastnosti Hornových klauzúl v kontexte logického programovania a ukázali, že každá množina definitných klauzúl D má jedinečný minimálny model M. Atomická formula A je logicky implikovaná D vtedy a len vtedy, ak A je pravdivá v M. Z toho vyplýva, že problém P reprezentovaný existenčne kvantifikovanou konjunkciou pozitívnych literálov je logicky implikovaný D vtedy a len vtedy, ak P je pravdivá v M. Minimálna modelová sémantika Hornových klauzúl je základom stabilnej modelovej sémantiky logických programov.

Propozičné Hornove klauzuly sú zaujímavé aj z hľadiska výpočtovej zložitosti, kde problém hľadania priradenia pravdivostných hodnôt, aby bola konjunkcia propozičných Hornových klauzúl pravdivá, je P-úplný problém (v skutočnosti riešiteľný v lineárnom čase), niekedy nazývaný HORNSAT. (Problém neobmedzenej boolovskej splniteľnosti je však NP-úplný problém). Uspokojiteľnosť Hornových klauzúl prvého rádu je nerozhodnuteľná.

Otázky a odpovede

Otázka: Čo je to rohová doložka?

Odpoveď: Hornova klauzula je logická disjunkcia literálov, kde najviac jeden z literálov je kladný a všetky ostatné sú záporné.

Otázka: Kto ich prvý opísal?

Odpoveď: Alfred Horn ich prvýkrát opísal v článku v roku 1951.

Otázka: Čo je to definitívna klauzula?

Odpoveď: Hornova veta s presne jedným kladným literálom sa nazýva definitná veta.

Otázka: Čo je to fakt?

Odpoveď: Definitná klauzula bez záporných literálov sa niekedy označuje ako "fakt".

Otázka: Čo je to cieľová veta?

A: Hornova veta bez kladného literálu sa niekedy nazýva cieľová veta.

Otázka: Ako fungujú premenné v nepropozičných pádoch?

Odpoveď: V nepropozičnom prípade sú všetky premenné v klauzule implicitne univerzálne kvantifikované s rozsahom celej klauzuly. To znamená, že sa vzťahujú na každú časť výroku.

Otázka: Akú úlohu zohrávajú Hornove klauzuly v konštruktívnej logike a výpočtovej logike? Odpoveď: Hornove klauzuly zohrávajú dôležitú úlohu v automatizovanom dokazovaní tvrdení pomocou rezolúcie prvého rádu, pretože rezolvent dvoch Hornových klauzúl alebo medzi jednou cieľovou a jednou definitívnou klauzulou sa môže použiť na vytvorenie väčšej efektívnosti pri dokazovaní niečoho, čo je reprezentované ako negácia jeho cieľovej klauzuly. Používajú sa aj ako základ logických programovacích jazykov, ako je Prolog, kde sa správajú ako procedúry redukcie cieľov.