Hornová klauzula — definícia, príklady a význam v logike a Prologu

Hornová klauzula: jasná definícia, príklady a význam v logike a Prologu — pochopte typy, inferenciu a uplatnenie pri automatizovanom dokazovaní a logickom programovaní.

Hornova klauzula je logická disjunkcia literálov, v ktorej je najviac jeden kladný literál (t. j. literál bez negácie) a všetky ostatné literály sú záporné. Pomenovaná je podľa Alfreda Horna, ktorý ich popísal v roku 1951. Hornove klauzuly sú dôležitou triedou klauzúl v matematickej logike a v logickom programovaní, pretože kombinujú výraznú výpočtovú účinnosť s prirodzeným vyjadrením pravidiel a faktov.

Druhy Hornových klauzúl a príklady

Rozlišujeme tri základné typy Hornových klauzúl:

• definitná (určitá) veta: ma obsah presne jeden kladný literál a ľubovoľný počet záporných literálov. Príklad (propozičný):

určitá veta: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

• fakt: určitá veta bez záporných literálov (len kladný literál). Príklad:

skutočnosť: u {\displaystyle u}

• cieľová (taktiež nazývaná negatívna) klauzula: klauzula bez kladných literálov, teda zložená výhradne z negácií. Príklad:

cieľová klauzula: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t}

Prvý rád (predikátová logika) a kvantifikátory

V prípade predikátovej logiky sú premenné v klauzule implicitne univerzálne kvantifikované v rozsahu celej klauzuly. Napríklad klauzula

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

znamená

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

a to je logicky ekvivalentné implikácii

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

Prevod na implikácie a použitie v logickom programovaní

Definitná Hornova klauzula sa bežne zapisuje v tvare implikácie, ktorý je prirodzenejší pre programovanie a odvodenie:

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

V spätnom (procedurálnom) tvare sa často zapisuje ako:

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

V jazyku Prolog sa to zapisuje ako:

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

Takáto klauzula sa interpretuje ako procedúra, ktorá znižuje (rozkladá) cieľ u na podciele p, q, ..., t a volá ich rekurzívne až kým nenájde fakty alebo nezlyhá.

Inferenčné pravidlá: rezolúcia, SLD resolution, unifikácia

Rezolúcia medzi dvoma Hornovými klauzulami zachováva Hornovu formu: rezolvent dvoch Hornových klauzúl je opäť Hornova klauzula. Konkrétne, rezolvent medzi definitnou (s kladným literálom) a cieľovou klauzulou vedie k novej cieľovej klauzule — to je jadrom inferenčného pravidla SLD resolution (Selective Linear Definite clause resolution), ktoré sa používa pri implementácii logického programovania a jazyka Prolog.

Pri dedukcii sa často používa unifikácia — nájdenie substitúcie, ktorá spraví dva literály identickými. SLD resolution kombinuje výber literálu v cieľovej klauzule, unifikáciu s kladným literálom definitnej klauzuly a nahradenie vybraného literálu v cieli jej telom (t. j. množinou nových podcieľov).

Tento mechanizmus prirodzene realizuje spätné reťazenie (backward chaining). Pre porovnanie, aplikovaním všetkých pravidiel do predu (naopak) dostávame vpredné reťazenie (forward chaining), ktoré tiež funguje efektívne pre Hornove klauzuly.

Semantika: minimálny model a dôsledky

Van Emden a Kowalski (1976) ukázali, že každá množina definitných klauzúl D má jedinečný minimálny model M (tzv. najmenej model podľa usporiadania podľa inklúzie množín atómov). Atómická formula A je logicky dôsledkom D práve vtedy, keď je A pravdivá v tomto minimálnom modeli M. Táto minimálna modelová sémantika je základom rôznych sémantík logických programov (napr. Herbrandov model, stabilné modely v rozšírených prípadoch).

Význam pre prax: pre množinu definitných klauzúl existuje zmysluplná „najmenšia“ interpretácia, ktorá obsahuje len tie atómy, ktoré je možné odvodzovať z pravidiel a faktov — čo umožňuje jednoznačnú deklaratívnu interpretáciu logického programu.

Výpočtová zložitosť a rozhodnuteľnosť

• Propozičné Hornove klauzuly: problém nájdenia priradenia pravdivostných hodnôt, ktoré robia konjunkciu Hornových klauzúl pravdivou (HORNSAT), je P-úplný, takže je rozhodnuteľný v polynomiálnom čase; v praxi sa rieši veľmi efektívne (lineárny čas pomocou algoritmov podobných unit propagation).
• Bežný Booleovský satisfiability problém (SAT) je naopak NP-úplný, takže Hornove klauzuly predstavujú dôležitú restrikciu z hľadiska efektívnosti.
• Satisfiabilita Hornových klauzúl v prvom ráde (predikátový prípad) je vo všeobecnosti nerozhodnuteľná, pretože prvý rád bez ďalších obmedzení umožňuje vyjadriť vlastnosti, ktoré vedú k neobmedzeným problémom (napr. rekurzia cez funkčné symboly atď.).

Použitie a obmedzenia

Hornove klauzuly a ich vlastnosti sú základom pre:

• logické programovanie a jazyky ako Prolog (vyjadrenie pravidiel a faktov),
• databázové dotazovacie jazyky založené na pravidlách, najmä Datalog (podmnožina Prologu bez funkčných symbolov, s rozhodnuteľnou sémantikou),
• automatizované dokazovanie (efektívne rezolventné metódy),
• analýzu programov, typové inferencie a odvozovanie závislostí.

Obmedzenie „najviac jeden kladný literál“ je kľúčové: zabezpečuje, že inferenčné pravidlá (ako rezolúcia) nemajú explozívne kombinatorické správanie, ktoré sa objavuje pri všeobecných klauzulách, a tým umožňuje efektívnejšie algoritmy.

Semantické nejednoznačnosti pri cieľových klauzulách

Zápis cieľovej klauzuly a jej premenné môže byť interpretovaný rôzne v praktických systémoch: premenné možno čítať ako univerzálne alebo existenčne kvantifikované a odvodenie „false“ sa môže interpretovať ako odvodenie protirečenia (štruktúra dôkazu) alebo ako úspešné riešenie problému (napr. v Prologu odmietnutie či úspech dotazu). Preto pri modelingových úlohách treba jednoznačne špecifikovať, akú sémantiku program využíva.

Krátke praktické ukážky v Prologu

Príklad definície v Prologu (jednoduchá dedukcia smrteľnosti):

 človek(jan). človek(maria). smrteľník(X) :- človek(X). 

Dotaz:

 ?- smrteľník(jan). 

Prolog odpovie "true", pretože existuje unifikácia a pravidlo, ktoré odvodí smrteľník(jan) z faktu človek(jan).

Záver

Hornove klauzuly predstavujú vyváženú kombináciu expresivity a výpočtovej efektivity. Vďaka ich špeciálnej štruktúre (najviac jeden kladný literál) sú základom praktických systému pre logické programovanie, databázové pravidlá a efektívne algoritmy automatizovaného dokazovania. Zároveň rozšírenia mimo triedy Hornových klauzúl prinášajú silnejšiu expresivitu, no často za cenu vyššej zložitosti alebo neriešiteľnosti.

Otázky a odpovede

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

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

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

Otázka: Čo je to fakt?

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

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

Hľadajte podľa písmena