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ří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ě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ý 4)

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

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

  • 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ří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).

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

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.

  • 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

  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

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

  • 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)\}
  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:

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

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

Diskuze

, 2008/06/06 10:57

Ahoj, asi by chtelo upravit definici unifikace, zvlaste pak „obecně řeší uvedený problém se substitucemi proměnných unifikace “. Mozna by chtelo ten problem specifikovat. -jak instanciovat promenne, aby bylo mozne pouzıt rezolucnı pravidlo
Kdyztek to pak nejak dle uvazeni uprav, diky.

, 2008/06/16 12:49

proč je u definice predikátu ta uspořádaná pětice? ve slidech to nevidím, přijde mi to matoucí. stejně tak u konstant a funkcí.

, 2008/06/17 09:08

Ne každých 5 proměnných je uspořádaná pětice. Je to pouze zavedené značení predikátů. Dopíšu tam poznámku.

, 2011/01/06 19:06

Domnívám se, že u příkladu vázaného/volného výskytu proměnné je y též vázaná, protože existuje podformule ∀yP(z)

, 2011/01/19 19:00

Nie je to viazana premenna. Ten text k viazanosti je okopirovany zo skript popelinskeho (predikatova logika I).
Premenna y nie je viazana, pretoze ta podformula, co si uviedol ∀yP(z) neobsahuje vyskyt y.
Aby bola y viazana, musela byt ta formula A obsahovat podformulu, v ktorej sa vyskytuje y (inde nez ∀y alebo \exists y) a predchadza jej kvantifikator s y. A taka podformula vo formuly A nie je.

You could leave a comment if you were logged in.
home/inf/ap14.txt · Poslední úprava: 2020/04/12 16:56 (upraveno mimo DokuWiki)
Nahoru
CC Attribution-Noncommercial-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0