Predikátová logika - logické programovanie

Hornovské klauzuly

Neformálne možno definovať Hornovskú klauzulu ako logickú formulu v špeciálnom tvare pravidla "ak $φ_1$ a $φ_2$ a ... $φ_n$ potom $ψ$". Tento tvar prináša mnoho užitočných vlastností pre reprezentáciu znalostí a dedukciu, ako je napríklad rozhodnuteľnosť. Hornovské klauzuly sú pomenovane po logikovi Alfrédovi Hornovi, ktorý poukázal na ich dôležitosť v roku 1951. Hornovské klauzuly teda tvoria rozhodnuteľnú podmnožinu predikátovej logiky (fragment).

Hornovská klauzula je klauzula, ktorá obsahuje najviac jeden pozitívny literál.

Hornovská formula je formula, ktorá je konjunkciou Hornovských klauzúl.

Existujú štyri varianty Hornovských klauzúl:

• Klauzula obsahuje jeden pozitívny literál a aspoň jeden negatívny, napríklad: $$¬p ∨ ¬q ∨ ¬r ∨ t.$$
• Klauzula obsahuje iba jeden pozitívny literál, napríklad: $$p.$$
• Klauzula obsahuje iba negatívne literály (aspoň jeden), napríklad: $$¬p ∨ ¬q ∨ ¬r.$$
• Prázdna klauzula $□$, ktorá vyjadruje spor.

Herbrandova procedúra

Herbrandovo univerzum (Herbrand universe) formuly $φ$ predikátovej logiky v množinovej notácii Skolemovského KNF (budeme označovať $H_φ$) je množina všetkých termov, ktoré môžu vzniknúť využitím jej konštánt a funkčných symbolov. V prípade, že formula neobsahuje konštanty je použitá ľubovoľná konštanta. Všetky prvky $H_φ$ sú základné termy (neobsahujú premenné).

Model interpretujúci Herbrandovo univerzum: $$(H, I_H),$$ je definovaný pre termy a predikáty nasledovne:

• Každému termu priradí term "reálnej" interpretácie $$I_h⟦t⟧=t:H×\dots×H → H.$$
• Každému predikátu priradí predikát "reálnej" interpretácie $$I_h⟦P⟧=P:H×\dots×H → \{1,0\}.$$

Akýkoľvek model predikátovej logiky $M=(D,I)$, môže byť imitovaný modelom Herbrandovo univerza.

Veta: Formula $φ$ je splniteľná v modely vtedy a len vtedy ak je splniteľná v modely Herbrandovo univerza.

Základná inštancia formuly $φ$ v klauzulárnom tvare vznikne tak, že všetky jej premenné sú nahradené prvkami $H_φ$.

Skolem-Gödel-Herbrandová teoréma: množina klauzúl je nesplniteľná vtedy a len vtedy ak existuje jej konečná nesplniteľná základná inštancia.

Herbrandová procedúra detekcie nesplniteľnosti:

• Majme formulu $φ$ v Skolemovskom KNF.
• Za premenné formuly $φ$ sú dosadzované prvky Herbrandovho univerza, čím sú generované jej základne inštancie do vtedy, pokiaľ nie je nájdený spor.
• Následne rezolučnou metódou je možné jednoducho overiť, že daná formula je kontradikcia.

Logické programovanie

Logické programovanie je paradigma, ktorá patrí do deklaratívnej paradigmy programovania. Akýkoľvek program logickej paradigmy je množina formúl príslušného logického systému (najčastejšie predikátovej logiky). Samotný výpočet pozostáva z dôkazu programu. Je to špeciálny prípad rezolučnej metódy. Oproti všeobecnej rezolučnej metóde má nasledujúce obmedzenia:

• Pracuje iba s Hornovskými klauzulami.
• Používa sa lineárna stratégia rezolúcie spolu s navracaním (backtracking).

Používame nasledujúcu terminológiu:

• Pravidlo je Hornovská klauzula s jedným pozitívnym literálom a aspoň jedným negatívnym literálom. Zapisuje sa v tvare: $$ψ_1 ∧ ... ∧ ψ_n ⇒ φ,$$ čo je možné prečítať ako: platí $φ$ ak $ψ_1$ a ... a $ψ_n$. Pričom $\varphi$ sa nazýva hlavička, a $ψ_1 ∧ ... ∧ ψ_n$ sa nazýva telo pravidla.
• Fakt je Hornovská klauzula, ktorá obsahuje iba jeden pozitívny literál. Zapisuje sa v tvare: $$φ,$$ čo je možné prečítať ako platí $φ$ alebo $φ$ je fakt.
• Cieľ (niekedy nazývaný aj dopyt) je Hornovská klauzula, ktorá obsahuje iba negatíve literály (minimálne jeden). Zapisuje sa v tvare: $$¬φ_1∨...∨¬φ_m.$$
• Prázdna klauzula $□$ vyjadruje spor.

Nasledujúca tabuľka prezentuje ekvivalentné zápisy Hornovských klauzúl.

Logický program

Logický program je Hornovská formula $\Gamma$. Je to postupnosť príkazov, to znamená Hornovských klauzúl, ktorá pozostáva z pravidiel a faktov. Cieľová klauzula $φ$ zadáva otázky (dopyty), na ktoré má program nájsť odpovede.

Príkazy logického programu sú pravidlá a fakty.

Dopyt resp. otázka je cieľová klauzula.

Výpočet programu zjednodušene je proces $$Γ\vdash φ,$$ kde:

• $Γ$ je Hornovská formula, postupnosť faktov a pravidiel,
• $φ$ je cieľová klauzula, otázka.

Výsledok programu (odpoveď na otázku) je:

• áno, ak $Γ\vdash φ,$
• nie, ak $Γ\nvdash φ.$

V prípade, že cieľová klauzula $φ$ obsahuje voľné premenné a $Γ\vdash φ,$, potom výsledkom programu je aj posledná substitúcia termov za dané premenné, ktorá viedla k odvodeniu prázdnej klauzuly.

Doména výpočtu logického programu je Herbrandovo univerzum.

Pre zápis logických programov bude využitá notácia v tvare logického vyplývania, kde $Γ$ bude označovať postupnosť pravidiel a faktov a $φ$ bude označovať cieľ.

SLD rezolúcia

Interpretácia logického programu je špeciálny prípad rezolučnej stratégie. Najčastejšie sa využíva SLD rezolúcia (Selective Linear Definite resolution).

• $S$ (selection rule) je definované pravidlo voľby, na základe ktorého je zvolený konkrétny literál v cieľovej klauzule. Prolog vyberá literál najviac vľavo (leftmost).
• $L$ (linear) lineárna stratégia. V každom kroku rezolúcie je použitá najnovšia rezolventa. Začína sa cieľovou klauzulou a programom. Prolog používa klauzuly v poradí v akom sú napísané.
• $D$ (definite) indikuje, že všetky klauzuly v programe sú definitívne.

Algoritmus: SLD rezolúcia:

Vstup: Hornovská formula (logický program) $Γ$ a cieľ (dopyt) $φ$.

Výstup:

• Áno, ak $Γ \vdash φ$ (prípadne aj substitúcia termov $σ$, ak $φ$ obsahuje voľné premenné).
• Nie, ak $Γ ⊬ φ$.

SLD_resolution($Γ$,$φ$):

• 1: Aktuálna cieľová klauzula $φ'$ je cieľová klauzula $φ$.
• 2: Ak je aktuálna cieľová klauzula prázdna klauzula $φ'=□$.
  • 2.1: Ak pôvodná $φ$ obsahuje voľné premenné, vráť poslednú substitúciu $σ$ termov za dané premenné, a Vráť Áno
  • Vráť Áno.
• 3: Zober najľavejší literál v aktuálnej cieľovej klauzule $φ'$. Hľadaj v $Γ$ príkaz s rovnakým menom taký, pri ktorom už nebol neúspešný pokus o unifikáciu. Hľadaj zhora nadol.
• 4: Ak neexistuje v $Γ$ príkaz s rovnakým menom, vráť Nie.
• 5: Ak existuje v $Γ$ príkaz s rovnakým menom, aplikuj pravidlo rezolúcie.
  • 5.1: Ak literály nie sú unifikovateľné,
    • pokračuj krokom 3 (navracanie, backtrack).
  • 5.2: Ak literály sú unifikovateľne,
    • priraď $φ'$ rezolventu,
    • volaj rekurzívne funkciu SLD_resolution(Γ, φ')

SLD-strom

Pre daný logický program a cieľ, myšlienkou je postupne aplikovať rezolúciu až pokiaľ nie je odvodená prázdna klauzula $□$ (kontradikcia). Týmto spôsobom je vypočítaná substitúcia $σ$, ktorá viedla k prázdnej klauzule. V prípade, že pôvodný cieľ (dopyt) obsahoval voľné premenné potom obmedzenie tejto substitúcie na premenné ktoré sa nachádzajú v pôvodnom cieli je taktiež výsledkom programu.

V logickom programe môže existovať niekoľko možností odvodenia prázdnej klauzuly. Každá vetva, ktorá vedie k odvodeniu prázdnej klauzuly je výsledkom programu. To znamená, ak je požadované získať všetky odpovede, po nájdení korektnej vetvy SLD rezolúcia vráti danú substitúciu, a pokračuje prehľadávaním ostatných možností (vetiev) prostredníctvom navracania (backtracking). Takýmto prístupom vytvárame štruktúru, ktorá sa nazýva SLD-strom.

Príklad programu logickej paradigmy