Ciele
- Naštudovať potrebné pojmy z formálneho aparátu predikátovej logiky.
- Preštudovať vzorové príklady prezentované v rámci teoretickej časti.
- Vypracovať zadané úlohy.
Základne pojmy
Na predchádzajúcom cvičení boli predstavené metódy prevodu ľubovoľnej formuly predikátovej logiky na prenexný normálny tvar a následne na skolemovský normálny tvar, z ktorého je možné jednoducho vytvoriť skolemovský konjunktívny normálny tvar v množinovej notácii, ktorý je vstupom rezolučnej metódy v v predikátovej logike.
Začneme zopakovaním potrebnej terminológie.
Atomická formula v predikátovej logike je predikát $P(t,..,t)$, logické konštanty vérum $⊤$ a absurdum $⊥$.
Literál $l$ je atomická formula (pozitívny literál) alebo jej negácia (negatívny literál).
Klauzula je disjunkcia literálov. Prázdna klauzula sa označuje symbolom $\square$.
Prenexný normálny tvar:
Formula $φ$ je v prenexnom normálnom tvare ak: $$φ=(Q_1x_1)(Q_2x_2)...(Q_nx_n)φ',$$ kde:
- $Q_i ∈ \{∀,∃\}$ pre akékoľvek $(1≤i≤n)$,
- $φ'$ neobsahuje kvantifikátory.
Zjednodušene povedané, všetky kvantifikátory $Q_ix_i$ musia byť na začiatku formuly, všetky premenné $x_i$ musia byť navzájom rôzne a $φ'$ je otvorená formula (jadro formuly).
Konjunktívny normálny tvar je formula v prenexnom normálnom tvare, ktorej jadro je konjunkcia klauzúl (disjunkcia literálov).
Skolemovský normálny tvar je získaný skolemizáciou, prostredníctvom ktorej sú z formuly v prenexnom normálnom tvare odstránené existenčné kvantifikátory.
Skolemovský konjunktívny normálny tvar je KNF po procese skolemizácie.
Množinová notácia Skolemovského KNF vznikne vynechaním všeobecných kvantifikátorov a následného prepisu jadra formuly v KNF do množinovej notácie. Všetky premenné sú implicitne všeobecne kvantifikované.
Poznámka
$~\\~$
Prepis formuly do prenexného normálneho tvaru a Skolemovského normálneho tvaru bol prezentovaný na predchádzajúcom cvičení.
Rezolučná metóda a automatické dokazovanie v predikátovej logike
Na štvrtom cvičení bola prezentovaná rezolučná metóda ako spôsob automatického dokazovania vo výrokovej logike. Zovšeobecnenie rezolučnej metódy pre predikátovú logiku žiaľ nie je také triviálne ako v prípade Gentzenových dedukčných kalkulov.
Rezolučná metóda v predikátovej logike je konzistentná a úplná sporom (refutation completeness) avšak je semi-rozhodnuteľná. To znamená, ak formula je kontradikcia, tak rezolučná metóda v konečnom počte krokov túto skutočnosť zistí a zastaví svoje vykonávanie. Avšak ak je formula splniteľná (nie tautológia), algoritmus nemusí skončiť svoje vykonávanie.
Pre aplikovanie rezolučnej metódy musí byť formula predikátovej logiky v množinovej notácii Skolemovského KNF. Keďže cieľom rezolučnej metódy je detekcia kontradikcie, obdobne ako vo výrokovej logike, prvý krok pozostáva z negácie formuly.
Zjednodušený postup ako dostať formulu predikátovej logiky do požadovaného tvaru je nasledovný:
- Prevod formuly na prenexný normálny tvar, v ktorom všetky kvantifikátory sa nachádzajú na začiatku formuly.
- Úprava formuly na Skolemovský normálny tvar, kde sa procesom nazývaním skolemizácia odstránia existenčné kvantifikátory.
- Vynechanie všeobecných kvantifikátorov (formula je uzavretá, každá premenná je implicitne všeobecne kvantifikovaná).
- Prevod formuly na Skolemovský konjunktívny normálny tvar.
- Úprava formuly v KNF na množinovú notáciu Skolemovského KNF.
Poznámka
$~\\~$
Postup pre formuly v tvare logického vyplývania $Γ\vdash φ$ je analogický ako vo výrokovej logike.
- Na každú formulu z množiny predpokladov $Γ$ aplikujeme kroky 1-5, výsledok pridáme do množiny klauzúl.
- Formulu $φ$ - záver najskôr negujeme a aplikujeme kroky 1-5, výsledok pridáme do množiny klauzúl.
Príklad
Negujte nasledujúcu formulu a preveďte ju do množinovej notácie Skolemovského KNF: $$(∃x)(∃y)(P(x,a)⇒P(f(b),y)).$$
Riešenie
V prvom kroku pristúpime k negácii formuly:
$$ \begin{array}{lc} ¬(∃x)(∃y)(P(x,a)⇒P(f(b),y)) & ≡ \\ ¬(∃x)(∃y)(¬P(x,a) ∨ P(f(b),y)) & ≡ \\ (∀x)¬(∃y)(¬P(x,a) ∨ P(f(b),y)) & ≡ \\ (∀x)(∀y)¬(¬P(x,a) ∨ P(f(b),y)) & ≡ \\ (∀x)(∀y)(¬¬P(x,a) ∧ ¬P(f(b),y)) & ≡ \\ (∀x)(∀y)(P(x,a) ∧ ¬P(f(b),y)) & ~ \end{array} $$ Prevod formuly do množinovej notácie Skolemovského KNF: $$(∀x)(∀y)(P(x,a) ∧ ¬P(f(b),y)).$$
- Daná formula je v prenexnom tvare.
- Daná formula je v Skolemovskom tvare.
- Jadro formuly je v konjunktívnom tvare.
- Pokračujeme vynechaním všeobecných kvantifikátorov $$(P(x,a) ∧ ¬P(f(b),y)),$$ a prevodom do množinovej notácie: $$\{\{P(x,a)\}, \{¬P(f(b),y)\}\}.$$
Pred samotným zavedením dedukčného pravidla rezolučnej metódy začneme demonštráciou problémov, ktoré je potrebné vyriešiť. Aj po prevode formuly na množinovú notáciu Skolemovského KNF, na rozdiel od formúl výrokovej logiky, v predikátovej logike môžu formuly obsahovať premenné, klauzuly môžu obsahovať ekvivalentné formuly vo forme variantov formúl a pod. Tieto problémy rieši unifikácia a faktorizácia.
Unifikácia
Inštancia formuly vzniká aplikáciou substitúcie $σ=[t/x]$ na jadro formuly $(∀x)P(x)$, kde za viazanú premennú $x$ všeobecným kvantifikátorom je možné substituovať ľubovoľný term $t$: $$σ(P(x)) = P(t).$$ Vychádza zo zákona generalizácie $(∀x)P(x) ⇒ P(t)$.
Unifikácia formúl $φ$ a $ψ$ je taká substitúcia $\sigma$, že platí: $$σ(φ)=σ(ψ).$$
Poznámka
Substitúcia slúžiaca na unifikáciu sa nazýva unifikátor.
Výsledok predchádzajúceho príkladu:
$$\{\{P(x,a)\}, \{¬P(f(b),y)\}\},$$
obsahuje dve jednotkové klauzuly, ktoré pozostávajú z komplementárnych literálov, aj keď to na prvý pohľad nie je zrejme. Je potrebné si uvedomiť, že všetky premenné sú implicitne všeobecne kvantifikované. Preto je možné vytvoriť ľubovoľne inštancie klauzúl príslušnou substitúciou $σ$, to znamená unifikovať ich tak, že
$$\sigma (P(x,a)) = σ(P(f(b),y)).$$
Príklad
Majme nasledujúce dve atomické formuly: $$P(x,a), P(f(b),y).$$ Nájdite takú substitúciu $σ$, ktorá umožní ich unifikáciu.
Riešenie
Substitúcia: $$σ=[f(b)/x,a/y].$$ Aplikácia substitúcie na atomické formuly:
$$ \begin{array}{rcl} σ(P(x,a)) & = & σ(P(f(b),y))\\ P(f(b),a) & = & P(f(b),a) \end{array} $$
Formuly $φ$ a $ψ$ sú unifikovateľné, ak existuje taký unifikátor $σ$, že $$σ(φ)=σ(ψ).$$
Unifikácia nemusí byť vždy možná.
Pravidlá pre unifikáciu:
- Ak sú obidva výrazy identické, potom unifikátor je prázdna substitúcia.
- Ak je jeden výraz premenná, a ta istá premenná sa nenachádza v druhom výraze, potom unifikátor je substitúcia, ktorá nahradí danú premennú druhým výrazom.
- Dve konštanty je možné unifikovať, len ak sú rovnaké.
- Dva funkčné symboly je možné unifikovať len ak majú rovnaký názov a rovnaký počet argumentov.
- Dva predikátové symboly je možné unifikovať len ak majú rovnaký názov a rovnaký počet argumentov.
Príklad
Nájdite unifikátor pre nasledujúce dvojice termov resp. formúl:
$$ \begin{array}{lcl} \textbf{1. výraz} & \quad & \textbf{2. výraz} \\ \hline x & \quad & x \\ x & \quad & y \\ a & \quad & x \\ a & \quad & a \\ b & \quad & y \\ f(x) & \quad & y \\ f(x) & \quad & x \\ g(a) & \quad & y \\ g(x) & \quad & g(a) \\ h(x,a,z) & \quad & h(f(y),u,b) \\ P(f(x),y,a) & \quad & P(f(a),c,z) \\ P(f(x),y,a) & \quad & P(g(x),y,a) \\ P(f(x),y,a) & \quad & P(g(x),y) \\ P(f(x),y,a) & \quad & Q(f(a),c,z) \\ \end{array} $$
Riešenie
$$ \begin{array}{lclcl} \textbf{1. výraz} & \quad & \textbf{2. výraz} & \quad \quad & \textbf{Substitúcia} \\ \hline x & \quad & x & \quad \quad & σ=[] \\ x & \quad & y & \quad \quad & σ=[y/x] \\ a & \quad & x & \quad \quad & σ=[a/x] \\ a & \quad & a & \quad \quad & σ=[] \\ b & \quad & y & \quad \quad & σ=[b/y] \\ f(x) & \quad & y & \quad \quad & σ=[f(x)/y] \\ f(x) & \quad & x & \quad \quad & \text{neunifikovateľné} \\ g(a) & \quad & y & \quad \quad & σ=[g(a)/y] \\ g(x) & \quad & g(a) & \quad \quad & σ=[a/x] \\ h(x,a,z) & \quad & h(f(y),u,b) & \quad \quad & σ=[f(y)/x,a/u,b/z] \\ P(f(x),y,a) & \quad & P(f(a),c,z) & \quad \quad & σ=[a/x,c/y,a/z] \\ P(f(x),y,a) & \quad & P(g(x),y,a) & \quad \quad & \text{neunifikovateľné} \\ P(f(x),y,a) & \quad & P(g(x),y) & \quad \quad & \text{neunifikovateľné} \\ P(f(x),y,a) & \quad & Q(f(a),c,z) & \quad \quad & \text{neunifikovateľné} \end{array} $$
Najoptimálnejší unifikátor
Ako už bolo spomenuté, unifikácia dvoch výrazov nemusí byť vždy možná. Avšak ak sú výrazy unifikovateľné, unifikátorov môže existovať viacero.
Hovoríme, že unifikátor $σ$ je optimálnejší (viac všeobecný, z ang. more general) ako unifikátor $σ_2$, ak existuje taký unifikátor $σ_1$, že kompozíciou $σ_1 ∘ σ = σ_2$.
Príklad
Majme dve unifikátory: $$\sigma_1=[h(z)/x, h(u)/y], \quad \sigma_2=[a/z, h(a)/x, h(u)/y],$$ potom $\sigma_1$ je optimálnejší ako $\sigma_2$, keďže: $$\sigma_2=[a/z]∘\sigma_1.$$
Príklad
Majme formuly $P(x,a)$ a $P(y,a)$. Potom ich unifikátor $σ=[y/x]$ je optimálnejší ako unifikátor $σ=[a/x, a/y]$.
Najoptimálnejší unifikátor (Most General Unifier (MGU)) dvoch výrazov $φ,ψ$ je taký unifikátor $σ$, že platí:
- $σ$ je unifikátor $φ,ψ$,
- $σ$ je optimálnejší (viac všeobecný) ako akýkoľvek iný unifikátor $φ,ψ$.
Najoptimálnejší unifikátor budeme označovať $\sigma_{MGU}$.
Vo všeobecnosti, najoptimálnejší unifikátor nemusí byť jedinečný.
Príklad
Majme formuly $P(x)$ a $P(y)$. Potom ich najoptimálnejší unifikátor je $[y/x]$ ale aj $[x/y]$.
Poznámka
$~\\~$
Využitie najoptimálnejšieho unifikátora je dôležité v procese rezolúcie. V nasledujúcich kapitolách bude vysvetlený algoritmus ako nájsť takýto unifikátor a na príklade demonštrované problémy, ktoré môžu vzniknúť pri nepoužití najoptimálnejšieho unifikátora.
Unifikačný algoritmus
V predchádzajúcej kapitole boli neformálne uvedené pravidlá unifikácie a hľadali sme vhodnú substitúciu hádaním (keďže sa jednalo o triviálne prípady). Takýto postup zároveň nezaručuje, že uhádnutý unifikátor je najoptimálnejší. Pre komplexnejšie prípady a hlavne pre automatizáciu dokazovania formúl je potrebné proces hľadania najoptimálnejšieho unifikátora algoritmizovať. Prvý takýto algoritmus predstavil John Alan Robinson v roku 1965.
Robinsonov unifikačný algoritmus:
Algoritmus: Robinsonov unifikačný algoritmus:
Vstup: Dve atomické formuly alebo termy $φ,ψ$ predikátovej logiky
Výstup: Najoptimálnejší unifikátor $σ_{MGU}$ ak $φ,ψ$ sú unifikovateľné, FAILURE inak
Unify($φ$,$ψ$):
- Krok 1: Ak $φ$ alebo $ψ$ je premenná alebo konštanta, potom:
- a) Ak $φ$ a $ψ$ sú identické, vráť prázdnu substitúciu $σ=[~~]$.
- b) Inak, ak $φ$ je premenná,
- a. potom ak $φ$ sa vyskytuje v $ψ$, vráť FAILURE.
- b. Inak vráť substitúciu $σ=[ψ/φ]$.
- c) Inak ak $ψ$ je premenná,
- a. Ak $ψ$ sa vyskytuje v $φ$, vráť FAILURE.
- b. Inak vráť substitúciu $σ=[φ/ψ]$.
- d) Inak vráť FAILURE.
- Krok 2: Ak predikátový alebo funkčný symbol $φ$ a $ψ$ nemá rovnaký názov, potom vráť FAILURE.
- Krok 3: Ak $φ$ a $ψ$ má rozdielny počet argumentov (prvkov), potom vráť FAILURE.
- Krok 4: Pre $i=1$ po počet prvkov v $φ$.
- a) Volaj rekurzívne funkciu Unify s $i$-tym prvkom $φ$ a $i$-tym prvkom $ψ$, výsledok vlož do substitúcie $σ$.
- b) Ak rekurzívne volanie funkcie Unify zlyhá, vráť FAILURE.
- c) Ak $σ ≠ [~~]$ potom,
- a. Aplikuj $σ$ na výrazy $φ$ a $ψ$ a optimálny unifikátor $σ_{MGU}$.
- b. Pridaj $\sigma$ do najoptimálnejšieho unifikátora $σ_{MGU}$= $σ_{MGU} ∘ σ$.
- c. Zmaž obsah $σ$.
- Krok 5: Vráť $σ_{MGU}$.
Príklad
Prostredníctvom Robinsonovho unifikačného algoritmu nájdite najoptimálnejší unifikátor nasledujúcej dvojice formúl: $$P(f(x_1,x_3,x_2)) \quad \quad P(f(g(x_2),j(x_4),h(x_3,a))).$$
Riešenie
Voláme funkciu $Unify(P(f(x_1,x_3,x_2)), P(f(g(x_2),j(x_4),h(x_3,a))))$.
| 1. výraz | 2. výraz | $\sigma$ | $\sigma_{MGU}$ | Opis |
|---|---|---|---|---|
| $P(f(x_1,x_3,x_2))$ | $P(f(g(x_2),j(x_4),h(x_3,a)))$ | $[~~]$ | $[~~]$ | Výrazy majú rovnaký názov predikátového symbolu. Výrazy majú rovnaký počet argumentov. Voláme rekurzívne funkciu $Unify$ s prvými prvkami výrazov. |
| $f(x_1,x_3,x_2)$ | $f(g(x_2),j(x_4),h(x_3,a))$ | $[~~]$ | $[~~]$ | Výrazy majú rovnaký názov funkčného symbolu. Výrazy majú rovnaký počet argumentov. Voláme rekurzívne funkciu $Unify$ s prvými prvkami výrazov. |
| $x_1$ | $g(x_2)$ | $[g(x_2)/x_1]$ | $[~~]$ | Prvý výraz je premenná, ktorá sa nevyskytuje v druhom výraze. Vráť $σ=[g(x_2)/x_1]$. |
| $P(f(g(x_2),x_3,x_2))$ | $P(f(g(x_2),j(x_4),h(x_3,a)))$ | $[~~]$ | $[~~]$ | Aplikuj $\sigma$ na výrazy a najoptimálnejší unifikátor, pridaj $\sigma$ do najoptimálnejšieho unifikátora. |
| $x_3$ | $j(x_4)$ | $[j(x_4)/x_3]$ | $[g(x_2)/x_1]$ | Prvý výraz je premenná, ktorá sa nevyskytuje v druhom výraze. Vráť $σ=[j(x_4)/x_3]$. |
| $P(f(g(x_2),j(x_4),x_2))$ | $P(f(g(x_2),j(x_4),h(j(x_4),a)))$ | $[~~]$ | $[g(x_2)/x_1]$ | Aplikuj $\sigma$ na výrazy a najoptimálnejší unifikátor, pridaj $\sigma$ do najoptimálnejšieho unifikátora. Pokračuj ďalším výrazom. |
| $x_2$ | $h(j(x_4),a))$ | $[h(j(x_4),a)/x_2]$ | $[g(x_2)/x_1, j(x_4)/x_3]$ | Prvý výraz je premenná, ktorá sa nevyskytuje v druhom výraze. Vráť $σ=[j(x_4)/x_3]$. |
| $P(f(g(h(j(x_4),a)),j(x_4),h(j(x_4),a)))$ | $P(f(g(h(j(x_4),a)),j(x_4),h(j(x_4),a)))$ | $[~~]$ | $[g(h(j(x_4),a))/x_1, j(x_4)/x_3, h(j(x_4),a)/x_2]$ | Aplikuj $\sigma$ na výrazy a najoptimálnejší unifikátor, pridaj $\sigma$ do najoptimálnejšieho unifikátora. |
| $P(f(g(h(j(x_4),a)),j(x_4),h(j(x_4),a)))$ | $P(f(g(h(j(x_4),a)),j(x_4),h(j(x_4),a)))$ | $[~~]$ | $[g(h(j(x_4),a))/x_1, j(x_4)/x_3, h(j(x_4),a)/x_2]$ | Výrazy sú unifikované, vráť $\sigma_{MGU}$. |
Následne aplikujeme najoptimálnejší unifikátor:
$$\sigma_{MGU}=[g(h(j(x_4),a))/x_1, j(x_4)/x_3, h(j(x_4),a)/x_2],$$
na obidve formuly:
$$
\sigma_{MGU}(P(f(x_1,x_3,x_2))) = \sigma_{MGU}(P(f(g(x_2),j(x_4),h(x_3,a)))) = P(f(g(h(j(x_4),a)),j(x_4),h(j(x_4),a))).
$$
Rezolučná metóda
Rezolučná metóda v predikátovej logike je dedukčný systém ktorý obsahuje dve dedukčné pravidlá a to rezolúcie a faktorizácie.
Rezolúcia
- Pravidlo rezolúcie je definované nasledovne:
- Zjednodušené pravidlo pre prípad detekcie kontradikcie:
Príklad
Dokážte rezolučnou metódou, že nasledujúca množina klauzúl je kontradikcia: $$ \{\{ P(x) \},\{ ¬P(f(z)), Q(h(x)) \},\{¬Q(h(f(a))) \} \} $$
Riešenie
Dôkazový strom:
- Voľba komplementárnych literálov $P(x), ¬P(f(z))$.
- Aplikáciou pravidla rezolúcie bol nájdený ich najoptimálnejší unifikátor $\sigma_1=[f(z)/x]$.
- $\sigma_1$ bol následne aplikovaný na zvyšné lietrály v klauzulách, ktoré obsahovali komplementárne literály t.j. $\sigma_1(Q(h(x)))$ z čoho vznikla nová klauzula $Q(h(f(z)))$.
- Voľba komplementárnych literálov, ktoré sú jednotkové klauzuly $Q(h(f(z))), ¬Q(h(f(a)))$.
- Aplikáciou pravidla rezolúcie bol nájdený ich najoptimálnejší unifikátor $\sigma_2=[a/z]$, na základe čoho bola odvodená kontradikcia $□$.
Príklad
Ako bolo spomenuté, je dôležité aby pri rezolúcii bol použitý najoptimálnejší unifikátor.
Majme nasledujúcu množinu klauzúl.
$$ \{\{ P(x,y),Q(y) \},\{ ¬P(x,x), R(f(x)) \}\}.$$ Ak by v prvom kroku rezolúcie nebol zvolený najoptimálnejší unifikátor, napr. $σ=[d/x,d/y]$. Vznikne rezolventa v nasledujúcom tvare: $$\{Q(d) , R(f(d))\},$$ pričom $d$ je konštanta, ktorej následná unifikácia je značne obmedzená.
V prípade voľby najoptimálnejšieho unifikátora $σ_{MGU}=[y/x]$. Vznikne rezolventa $$\{Q(x) , R(f(x))\},$$ pričom $x$ je premenná a tým pádom existuje viac možností ich ďalšej rezolúcie, čo znamená maximum možností odvodenia kontradikcie (dosiahnutia cieľa).
Faktorizácia
Pokiaľ vo výrokovej logike množinová notácia klauzúl rieši prípady opakujúcich sa formúl v jednej klauzule automaticky, v predikátovej logike môžu nastať prípady keď klauzula obsahuje varianty formúl, ktoré je potrebné odstrániť, napr. $$ \{\{ P(x),P(y)\}\}.$$
Pre tento účel je definované dedukčné pravidlo faktorizácie:
Príklad
V najjednoduchšom prípade vyzerá aplikácia pravidla faktorizácie nasledovne. Majme klauzulu: $$\{ P(x),P(y)\}.$$ Aplikovaním pravidla faktorizácie nájdeme najoptimálnejší unifikátor $\sigma_{MGU}=[y/x]$. Aplikujeme $$\sigma_{MGU}$ na klauzulu $\sigma_{MGU}(\{ P(x),P(y)\})$ a odvodíme novú klauzulu: $$\{ P(x)\}.$$
Príklad
Majme nasledujúcu množinu klauzúl: $$ \{\{ P(x),P(y)\},\{¬P(x),¬P(y)\}\}.$$
Bez použitia pravidla faktorizácie nie je možné odvodenie kontradikcie. Pri akejkoľvek voľbe kombinácie komplementárnych literálov a príslušnej substitúcie v rezolvente vznikne inštancia tautológie.
Dôkaz s využitím pravidla faktorizácie:
Postup
Krok 1: Nájdite najoptimálnejší unifikátor nasledujúcich dvojíc výrazov prostredníctvom Robinsonovho unifikačného algoritmu.
Úloha 1.1
$$ \begin{array}{lcl} \textbf{1. výraz} & \quad & \textbf{2. výraz} \\ \hline x & \quad & x \\ x & \quad & a \\ a & \quad & z \\ f(x) & \quad & x \\ g(x) & \quad & g(y) \\ P(x,g(x)) & \quad & P(g(a),g(z)) \\ P(x,g(x),z) & \quad & P(g(a),g(z)) \\ P(x,g(x),z) & \quad & P(g(a),g(z),b) \\ P(x,g(x),z) & \quad & R(g(a),g(z),b) \\ P(f(j(x)),g(x),z) & \quad & P(g(a),g(z),b) \\ P(f(j(x)),g(x),z) & \quad & P(f(z),g(z),b) \\ P(f(j(x)),g(x),z) & \quad & P(f(z),g(z),y) \end{array} $$
Krok 2: Odvoďte rezolventy z nasledujúcich dvojíc formúl.
Úloha 2.1
$$ \begin{array}{lcl} \textbf{1. výraz} & \quad & \textbf{2. výraz} \\ \hline P(x) & \quad & ¬P(f(j(x)))∨ Q(x) \\ P(x) ∨ Q(x) & \quad & ¬P(f(j(z))) ∨ Q(y) \\ P(j(z)) ∨ Q(z) & \quad & ¬P(j(a)) \\ P(f(j(x)),g(x),z) & \quad & ¬P(f(j(a)),g(a),z) ∨ Q(x, z)\\ P(f(j(x)),g(x),z) & \quad & ¬P(f(j(a)),g(b),z) ∨ Q(x, z)\\ P(f(j(x)),g(x),z) & \quad & ¬P(f(j(x)),f(x),z) ∨ Q(x, z)\\ P(z,x) ∨ P(y,u) & \quad & ¬P(z,x) ∨ ¬P(y,u) \end{array} $$
Krok 3: Dokážte pomocou rezolučnej metódy nasledujúce formuly predikátovej logiky.
Úloha 3.1
$$(∀x) P(x) ⇒ P(t)$$
Úloha 3.2
$$P(t) ⇒ (∃y) P(y)$$
Úloha 3.3
$$(∀x) P(x) ⇒ (∃y) (P(y))$$
Úloha 3.4
$$¬(∀x) P(x) ⇒ (∃x) (¬P(x))$$
Úloha 3.5
$$¬(∃x) P(x) ⇒ (∀x) ¬(P(x))$$
Úloha 3.6
$$(∀x) R(x) ⇒ (∀x)P(x) ⇒ (∀y)(R(y) ∧ P(y))$$
Úloha 3.7
$$(∃x)(∀y) R(x,y) ⇒ (∀y)(∃x) R(x,y)$$
Úloha 3.8
$$(∀x)(P(x) ⇒ Q(x)) ⇒ (∀x)P(x) ⇒ (∀x)Q(x)$$
Krok 4: Preložte nasledujúce tvrdenia v tvare logického vyplývania do jazyka predikátovej logiky a dokážte ich prostredníctvom rezolučnej metódy.
Úloha 4.1
Všetci ľudia sú smrteľní.
Sokrates je človek.
-------------------------
Teda Sokrates je smrteľný.
Úloha 4.2
Puňťo je pes.
Všetky psy sú zvieratá.
Všetky zvieratá nevedia rozprávať.
-------------------------
Puňťo nevie rozprávať.
Úloha 4.3
Každý kto je vo väzení, je odsúdený.
Všetci odsúdení sú zločinci.
Horislav je vo väzení.
-------------------------
Horislav je zločinec.
Úloha 4.4
Každý hokejista, je športovec.
Levoslav nie je športovec.
Každý kto nie je športovec, nie je hokejista.
-------------------------
Levoslav nie je hokejista.
Úloha 4.5
Ďalšie príklady (niektoré aj riešené) môžete nájsť na adrese: https://www.cs.utexas.edu/users/novak/reso.html
Krok 5: Preložte nasledujúce tvrdenia do jazyka predikátovej logiky a dokážte prostredníctvom rezolučnej metódy či platí záver.
Úloha 5.1
Anna je matkou Evy.
Anna je nažive.
Každý kto je niekoho matkou, je aj jeho rodičom.
Každý kto je niekoho rodičom a je nažive, je starší ako daná osoba.
-------------------------------------------------------------------
Anna je staršia ako Eva.
Poznámka
Predpoklady nad čiarou sú znalostná báza, prostredníctvom ktorej môžeme odvádzať/dedukovať ďalšie fakty, pýtať sa otázky a pod. Pouvažujte čo bude odpoveďou otázok:
Existuje niekto starší ako Eva?
Kto je starší ako Eva?
Nájdite odpovede na nasledujúce otázky:
Existuje niekto starší ako Eva?
Kto je starší ako Eva?
Kto je mladší ako Anna?
Kto je starší ako kto?
Je Anna rodičom Evy?
Kto je rodičom Evy?
Kto je rodičom koho?
Rozšírte množinu predpokladov tak, aby umožňovala dedukciu nasledujúcich vlastností a formulujte nové otázky:
Byť mladší ako niekto.
Byť niekoho dcéra.