Obsah

AP14 Predikátová logika prvního řádu

Zadání

(syntax, sémantika, prenexace, skolemizace, unifikace, rezoluce)

Vypracování

Predikátová logika

Syntax

Predikát (značíme velkými písmeny, např. predikáty P,Q,R,P_1,P_2) je n-ární relace; vyjadřuje vlastnosti objektů a vztahy mezi objekty.

Konstanty (značíme a,b,c,a_1,a_2) reprezentují jména objektů; jedná se o prvky předem specifikované množiny hodnot D – domény Proměnné (značíme x,y,z,x_1,x_2) zastupují jména objektů, mohou nabývat libovolných hodnot z dané domény

Funkce (značíme f,g,h,f_1,f_2) reprezentují složená jména objektů, f : D^n \rightarrow D

Příklad1)

Nechť funkce f(x,y) reprezentují sčítání. Pak f(1,2) (stejně jako f(0,3), f(2,1)) jsou možná složená jména pro konstantu 3.

Termy jsou výrazy složené pouze z funkčních symbolů, konstant a proměnných

  1. každá proměnná a každá konstanta je term
  2. je-li f n-ární funkční symbol a t_1,...,t_n jsou termy, pak f(t_1,...,t_n) je term
  3. nic jiného není term

příklad termu: f(x, g(y, h(x, y), 1), z)

Kvantifikátory2)

Univerzální (obecný) kvantifikátor \forall:
\forall x P(x) – pro každý prvek x domény platí P(x)


Existenční kvantifikátor \exists:
\exists x P(x) – existuje alespoň jeden prvek x domény, pro který platí P(x)

Atomická formule

  1. je-li P n-ární predikátový symbol a t_1,...,t_n jsou termy, pak P(t_1,...,t_n) je atomická formule
  2. jsou-li t_1 a t_2 termy, pak t_1 = t_2 je atomická formule
  3. nic jiného není atomická formule

Je to tedy vlastně také predikát, ale často se uvádí zvlášť.

Formule jsou výrazy složené pouze z funkčních symbolů, konstant a proměnných

  1. každá atomická formule je formule
  2. je-li A formule, pak \neg A je formule
  3. jsou-li A, B formule, pak (A \vee B),(A \wedge B),(A \Rightarrow B),(A \Leftrightarrow B) jsou formule
  4. je-li x proměnná a A formule, pak (\forall x A) a (\exists x A) jsou formule
  5. nic jiného není formule

Podformule formule A je libovolná spojitá podčást A, která je sama formulí.

Příklad podformule3)

Formule A = \exists x((\forall y P(z)) \Rightarrow R(x,y)) má kromě sebe samé následující podformule:
(\forall y P(z)) \Rightarrow R(x,y), \forall y P(z), R(x,y), P(z)

Vázaný/volný výskyt

Výskyt proměné x z formule A předchozího příkladu je vázaný (podformulí je celá formule A), proměnné y a z jsou volné.

Sentence (uzavřená formule) – formule bez volných výskytů proměnných (všechny výskyty všech proměnných jsou vázané)
Otevřená formule – formule bez kvantifikátorů

Substituce – substituovat lze pouze volné proměnné.

Příklad substituce5)

Ve formuli: A = \exists x P(x,y) lze provést například následující substituce.
substituce: A(y/z) = \exists x P(x,z), A(y/2) = \exists x P(x,2), A(y/f(z,z)) = \exists x P(x,f(z,z)) nelze!: A(y/f(x,x)) = \exists x P(x,f(x,x)) – došlo by k nežádoucí vazbě proměnných

Sématika

Interpretace (realizace) jazyka predikátové logiky je struktura I složená z

Příklad6)

D = celá čísla
I(a) = 0, I(a_1)= 1, ... (nulární funkce)
I(b_1)=-1, ... I(f) = + (funkce zadaná pomocí rovnosti funkcí: zobrazení I(f) definujeme jako funkci sčítání celých čísel; pak např. I(f)(4;-2) = 2)

I(P) = >(relace zadaná pomocí rovnosti relací: I(P) definujeme jako relaci „větší než“ pro celá čísla; např. (2;-1) \in I(P) a (2;4) \notin I(P))

Neformálně řečeno, interpretace je přiřazení konkrétních významů všem konstantám, funkčním a predikátovým symbolům.

Valuace – Interpretace volných proměnných spočívá v jejich ohodnocení, což je libovolné zobrazení V (valuace) z množiny všech proměnných do D. Neformálně řečeno, přiřazení konkrétních hodnot proměnným.

Hodnota termu t v interpretaci I a valuaci V je prvek |t|_{I,V} z D takový že:

Příklad7)

Mějme interpretaci I z předchozího příkladu (celá čísla s > a +) a valuaci V(x) = 2. Pak
|f(b_1, f(b_2, b_2))|_{I,V} = +(-1, +(-2,-2)) = -5 |f(f(a, b_1), f(x, a_1))|_{I,V} = +(+(0, -1), +(2, 1)) = 2

Pravdivost formulí

  • Formuli A nazveme pravdivou v interpretací I, je-li splňována I pro libovolnou valuaci; píšeme |={ }_I A
  • Formule A je
    1. tautologie, pokud je pravdivá pro každou interpretaci
    2. splnitelná, pokud je pravdivá pro alespoň jednu interpretaci a valuaci.
    3. kontradikce, pokud \neg A je tautologie

Prenexace

Cílem Prenexové normální formy je převést libovolnou (uzavřenou) formuli do tvaru, v němž jsou všechny kvantifikátory na začátku a následuje otevřené (= bez kvantifikátorů) jádro v KNF (DNF).

Algoritmus převodu

  1. eliminovat zbytečné kvantifikátory
  2. přejmenovat proměnné tak, aby u každého kvantifikátoru byla jiná proměnná
  3. eliminovat všechny spojky různé od \neg, \wedge a \vee
  4. přesunout negaci dovnitř
  5. přesunout kvantifikátory doleva
  6. použít distributivní zákony k převodu jádra do KNF (DNF)

Skolemizace

Skolemova normální forma je prenexová normální forma s pouze univerzálními kvantifikátory.

Algoritmus převodu

  1. převést formuli do (konjunktivní) pnf
  2. provést Skolemizaci: odstranit všechny existenční kvantifikátory a nahradit jimi vázané proměnné pomocnými Skolemovými funkcemi

Unifikace

Konečná substituce \phi je konečná množina \{x_1{/}t_1,x_2{/}t_2,...,x_n{/}t_n\}, kde všechna x_i jsou vzájemně různé proměnné a každé t_i je term různý od x_i.

Konečná substituce

  • označme libovolný term nebo literál jako výraz E
  • E \phi je pak výsledek nahrazení všech výskytů všech x_i odpovídajícími termy t_i
  • !POZOR! Nahrazení v rámci jedné substituce \phi probíhají paralelně. Když se použijí dvě substituce \phi\psi, probíhají postupně.

Kompozice substitucí – postupně bereme prvky z první substituce a hledáme ve druhé, zda není možnost nahradit nahrazovaného (tranzitivně)

Unifikátor Substituci \phi nazveme unifikátorem množiny formulí S = \{E_1,...,E_n\}, pokud E_1 \phi = E_2 \phi = ... = E_n \phi, tedy v případě, že S \phi má jeden prvek.

Unifikátor příklad

  • unifikátorem \{{P(x,c),P(b,c)}\} je \phi = \{{x{/}b}\}
  • !POZOR! Unifikujeme vždy tak, že místo proměnné dáme term a ne naopak

Unifikátor \phi množiny S je nejobecnějším unifikátorem (mgu) S, pokud pro libovolný unifikátor \psi množiny S existuje substituce \lambda taková, že \phi \lambda = \psi – pro unifikovatelné množiny existuje pouze jediný mgu (až na přejmenování proměnných)
Rozdíly mezi výrazy označujeme jako D(S)

Mějme množinu výrazů S. Najdeme první (nejlevější) pozici, na které nemají všechny prvky S stejný symbol. Rozdíl D(S) mezi výrazy pak definujeme jako množinu podvýrazů všech E \in S začínajících na této pozici.8)

Unifikační algoritmus pro množinu výrazů S

  • krok 0: S_{0} := S, \phi_{0} := \epsilon
  • krok k+1:
    • je-li S_{k} jednoprvková, ukonči algoritmus s výsledkem mgu(S) = \phi_{0}\phi_{1}\phi_{2} ... \phi_{k}
    • jinak, pokud v D(S_{k}) není proměnná v a term t, který ji neobsahuje, ukonči algoritmus s výsledkem neexistuje mgu(S)
    • jinak vyber takovou proměnnou v a term t, který neobsahuje v, \phi_{k+1} := \{v/t\}, S_{k+1} := S_{k}\phi_{k+1} a pokračuj krokem k+2

Na pochopení fungování unifikačního algoritmu je dobré se podívat do skript Úvod do logiky a logického programování, na posledni stranu kapitoly Predikátová logika III.

Rezoluce

Metoda vhodná pro strojové zpracování. Založená na vyvracení.

Příklad rezoluční formule

formule: \forall x \forall y ((P(x,f(x))\vee \neg Q(y))\wedge(\neg R(f(x))\vee \neg Q(y))) rezoluční forma: \{\{P(x,f(x)),\neg Q(y)\},\{ \neg R(f(x)),\neg Q(y)\}\}

Rezoluční pravidlo pro predikátovou logiku. Mějme klauzule C_1, C_2 bez společných proměnných (po případném přejmenování) ve tvaru:

Příklad rezolventy

Rezolvujeme klauzule \{{P(x,y),\neg R(x)}\} a \{\neg P(a,b)\}
  1. mgu (\{P(x,y),P(a,b)\}) = \{{x{/}a,y{/}b}\}
  2. aplikujeme mgu na \{{\neg R(x)}\}
  3. rezolventa \{{\neg R(a)}\}

Vlastnosti rezoluce:

Měli byste znát jednotlivé druhy rezolucí více podrobně – tak jako jsou uvedeny v dalších otázkách:
AP4, IN4 Výroková logika a AP13 Prolog

Předměty

Použitá literatura

<http://www.fi.muni.cz/~popel/lectures/bak_logika/>.

Vypracoval

Martin Kotlík, UČO: 143208.

Otázku si přečetl pan RNDr. Jan Bouda a rámcově prošel. Jeho podněty pro doplnění textu, opravy nesrovnalostí a odstranění matoucích či k otázce se nevztahujících textů byly do otázky zaneseny. Tato kontrola je jen rámcová, stále se může stát, že v otázce zůstala zapomenutá chybka či nesrovnalost, vyučující za toto nenese odpovědnost, berte tuto rámcovou kontrolu jako formu pomoci od vyučujících pro studenty.

1) , 2)
slidy č.4, strana 4
3)
slidy č.4, strana 11
4) , 8)
prevzato ze skript Úvod do logiky a logického programování, Luboš Popelínský, Eva Mráková
5)
slidy č.4, strana 12
6)
slidy č.5, strana 2
7)
slidy č.5, strana 3