−Obsah

AP14 Predikátová logika prvního řádu
- Zadání
- Vypracování
  - Syntax
  - Sématika
  - Prenexace
  - Skolemizace
  - Unifikace
  - Rezoluce
- Předměty
- Použitá literatura
- Vypracoval
Diskuze

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

Zadání

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

Vypracování

Predikátová logika

plně přejímá výsledky výrokové logiky
zabývá se navíc strukturou jednotlivých jednoduchých výroků – na základě této analýzy lze odvodit platnost některých výroků, které ve výrokové logice platné nejsou

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.

unární predikáty vyjadřují vlastnosti
binární, ternární, …, n-ární vyjadřují vztahy mezi dvojicemi, trojicemi, …, n-ticemi objektů.
nulární predikáty (sentence) představují původní výroky ve výrokové logice (bez vypuštěných výrazů)

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říklad¹⁾

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

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

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

Kvantifikátory²⁾

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

je-li $P$ n-ární predikátový symbol a $t_1,...,t_n$ jsou termy, pak $P(t_1,...,t_n)$ je atomická formule
jsou-li $t_1$ a $t_2$ termy, pak $t_1 = t_2$ je atomická formule
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

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

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

Příklad podformule³⁾

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ěnné $x$ ve formuli $A$ je vázaný, pokud existuje podformule $B$ formule $A$ , která obsahuje tento výskyt $x$ a začíná $\forall x$ , resp. $\exists x$
výskyt proměnné je volný, není-li vázaný ⁴⁾

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 substituce⁵⁾

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

libovolné neprázdné množiny $D$ (domény, oboru interpretace)
zobrazení $I(f): D^n \rightarrow D$ pro každý n-ární funkční symbol $f, n \geq 0$
n-ární relace $I(P) \subseteq D^n$ pro každý n-ární predikátový symbol $P$ , $n \geq 1$

Příklad⁶⁾

$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.

$V[x/d]$ značí ohodnocení, které přiřazuje proměnné $x$ prvek $d \in D$ a na ostatních proměnných splývá s valuací $V$

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

je-li $t$ proměnná, $|t|_{I,V} = V(t)$
je-li $t = f(t_1,...,t_n)$ , pak $|t|_{I,V}$ je hodnotou funkce $I(f)$ pro argumenty $|t_1|_{I,V},...,|t_n|_{I,V}$

Příklad⁷⁾

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).

každá formule se dá převést

Algoritmus převodu

eliminovat zbytečné kvantifikátory
přejmenovat proměnné tak, aby u každého kvantifikátoru byla jiná proměnná
eliminovat všechny spojky různé od $\neg$ , $\wedge$ a $\vee$
přesunout negaci dovnitř
přesunout kvantifikátory doleva
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.

odstraníme existenční ( $\exists$ ) kvantifikátory
formuli $\forall x_1,...,\forall x_n \exists y P(x_1,...,x_n,y)$ převedeme na $\forall x_1,...,\forall x_n P(x_1,...,x_n,f(x_1,...,x_n))$

Algoritmus převodu

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

Unifikace

směřuje k rezoluci v predikátové logice
formule uvádíme ve Skolemově normální formě
všeobecné kvantifikátory nepíšeme
problém se substitucemi proměnných obecně řeší 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$ .

pokud jsou všechna $t_i$ uzavřené termy (neobsahují proměnné), jedná se o uzavřenou substituci
pokud jsou $t_i$ proměnné, označujeme $\phi$ jako přejmenování proměnných

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.

Existuje-li unifikátor množiny, označíme ji jako unifikovatelnou

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.⁸⁾

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í.

formule ve Skolemově normální formě, nepíšeme kvantifikátory
literály představují atomické formule a jejich negace
klauzule: množiny reprezentující disjunkci literálů
formule: množiny klauzulí reprezentující jejich konjunkci

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:

$C_1 = C_1' \cup \{P(x_1),...,P(x_n)\}$
$C_2 = C_2' \cup \{\neg P(y_1),...,\neg P(y_m)\}$ .
Je-li $\phi$ mgu množiny $\{P(x_1),...,P(x_n),P(y_1),...,P(y_m)\}$ , pak rezolventou $C_1$ a $C_2$ je $C_1' \phi \cup C_2' \phi$

Příklad rezolventy

Rezolvujeme klauzule $\{{P(x,y),\neg R(x)}\}$ a $\{\neg P(a,b)\}$

mgu $(\{P(x,y),P(a,b)\}) = \{{x{/}a,y{/}b}\}$
aplikujeme mgu na $\{{\neg R(x)}\}$
rezolventa $\{{\neg R(a)}\}$

Vlastnosti rezoluce:

stejně jako ve výrokové logice je rezoluce v predikátové logice korektní a úplná
stejný problém jako ve výrokové logice: strategie generování rezolvent (příliš velký prohledávaný prostor)
lze použít všechny metody zjemnění uvedené pro výrokovou logiku
Druhy rezolucí:
- Lineární rezoluce
- LI-rezoluce
- LD-rezoluce
- SLD-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

FI:IB101 Úvod do logiky a logického programování, doc. RNDr. Lubomír Popelínský, Ph.D.

Použitá literatura

POPELÍNSKÝ, Lubomír: Studijní materiály předmětu IB101 Úvod do logiky a logického programování. Dostupné z URL:

<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.

¹⁾ , ²⁾

slidy č.4, strana 4

³⁾

slidy č.4, strana 11

⁴⁾ , ⁸⁾

prevzato ze skript Úvod do logiky a logického programování, Luboš Popelínský, Eva Mráková

⁵⁾

slidy č.4, strana 12

⁶⁾

slidy č.5, strana 2

⁷⁾

slidy č.5, strana 3