====== 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 [[home:inf:ap4|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 <math>P,Q,R,P_1,P_2</math>) 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 <math>a,b,c,a_1,a_2</math>) reprezentují jména objektů; jedná se o prvky předem specifikované množiny hodnot D -- **domény**
**Proměnné** (značíme <math>x,y,z,x_1,x_2</math>) zastupují jména objektů, mohou nabývat libovolných hodnot z dané domény

**Funkce** (značíme <math>f,g,h,f_1,f_2</math>) reprezentují složená jména objektů, <math>f : D^n \rightarrow D</math>
<box 100% round blue|Příklad((slidy č.4, strana 4))>
Nechť funkce <math>f(x,y)</math> reprezentují sčítání. Pak <math>f(1,2)</math> (stejně jako <math>f(0,3)</math>, <math>f(2,1)</math>) jsou možná složená jména pro konstantu 3.
</box>
**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 <math>f</math> //n//-ární funkční symbol a <math>t_1,...,t_n</math> jsou termy, pak <math>f(t_1,...,t_n)</math> je term
  - nic jiného není term

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

<box 100% round blue|Kvantifikátory((slidy č.4, strana 4))>
**Univerzální (obecný) kvantifikátor** <math>\forall</math>:
<math>\forall x P(x)</math> -- pro každý prvek <math>x</math> domény platí <math>P(x)</math>

\\

**Existenční kvantifikátor** <math>\exists</math>:
<math>\exists x P(x)</math> -- existuje alespoň jeden prvek <math>x</math> domény, pro který platí <math>P(x)</math>
</box>

**Atomická formule**
  - je-li <math>P</math> //n//-ární predikátový symbol a <math>t_1,...,t_n</math> jsou termy, pak <math>P(t_1,...,t_n)</math> je atomická formule
  - jsou-li <math>t_1</math> a <math>t_2</math> termy, pak <math>t_1 = t_2</math> je atomická formule
  - nic jiného není atomická formule

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

**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 <math>A</math> formule, pak <math>\neg A</math> je formule
  - jsou-li <math>A, B</math> formule, pak <math>(A \vee B),(A \wedge B),(A \Rightarrow B),(A \Leftrightarrow B)</math> jsou formule
  - je-li <math>x</math> proměnná a <math>A</math> formule, pak <math>(\forall x A)</math> a <math>(\exists x A)</math> jsou formule
  - nic jiného není formule
**Podformule** formule <math>A</math> je libovolná spojitá podčást <math>A</math>, která je sama formulí.
<box 100% round blue|Příklad podformule((slidy č.4, strana 11))>
Formule <math>A = \exists x((\forall y P(z)) \Rightarrow R(x,y))</math> má kromě sebe samé následující podformule:
<math>(\forall y P(z)) \Rightarrow R(x,y)</math>, <math>\forall y P(z)</math>, <math>R(x,y)</math>, <math>P(z)</math>
</box>
**Vázaný/volný výskyt** 
  * výskyt proměnné <math>x</math> ve formuli <math>A</math> je **vázaný**, pokud existuje podformule <math>B</math> formule <math>A</math>, která obsahuje tento výskyt  <math>x</math> a začíná <math>\forall x</math>, resp. <math>\exists x</math>
  * výskyt proměnné je **volný**, není-li vázaný ((prevzato ze skript Úvod do logiky a logického programování, Luboš Popelínský, Eva Mráková))

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

**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é.
<box 100% round blue|Příklad substituce((slidy č.4, strana 12))>
Ve formuli: <math>A = \exists x P(x,y)</math> lze provést například následující substituce.
substituce: <math>A</math>(<math>y/z</math>) = <math>\exists x P(x,z)</math>, <math>A</math>(<math>y/2</math>) = <math>\exists x P(x,2)</math>, <math>A</math>(<math>y/f(z,z)</math>) = <math>\exists x P(x,f(z,z))</math> 
**nelze!**: <math>A</math>(<math>y/f(x,x)</math>) = <math>\exists x P(x,f(x,x))</math> -- došlo by k nežádoucí vazbě proměnných
</box>

==== Sématika ====

**Interpretace** (**realizace**) jazyka predikátové logiky je struktura <math>I</math> složená z
  * libovolné neprázdné množiny <math>D</math> (domény, oboru interpretace)
  * zobrazení <math>I(f): D^n \rightarrow D</math> pro každý //n//-ární funkční symbol <math>f, n \geq 0</math>
  * //n//-ární relace <math>I(P) \subseteq D^n</math> pro každý //n//-ární predikátový symbol <math>P</math>, <math>n \geq 1</math>
<box 100% round blue|Příklad((slidy č.5, strana 2))>
<math>D</math> = celá čísla
<math>I(a) = 0</math>, <math>I(a_1)= 1, ...</math> (nulární funkce)
<math>I(b_1)=-1, ...</math>
<math>I(f) = +</math> (funkce zadaná pomocí rovnosti funkcí: zobrazení <math>I(f)</math> definujeme jako funkci sčítání celých čísel; pak např. <math>I(f)(4;-2) = 2</math>)

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

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

**Valuace** -- Interpretace volných proměnných spočívá v jejich ohodnocení, což je libovolné zobrazení <math>V</math> (**valuace**) z množiny všech proměnných do <math>D</math>. Neformálně řečeno, přiřazení konkrétních hodnot proměnným.
  * <math>V[x/d]</math> značí ohodnocení, které přiřazuje proměnné <math>x</math> prvek <math>d \in D</math> a na ostatních proměnných splývá s valuací <math>V</math>

**Hodnota termu** <math>t</math> v interpretaci <math>I</math> a valuaci <math>V</math> je prvek <math>|t|_{I,V}</math> z <math>D</math> takový že:
  * je-li <math>t</math> proměnná, <math>|t|_{I,V} = V(t)</math>
  * je-li <math>t = f(t_1,...,t_n)</math>, pak <math>|t|_{I,V}</math> je hodnotou funkce <math>I(f)</math> pro argumenty <math>|t_1|_{I,V},...,|t_n|_{I,V}</math>

<box 100% round blue|Příklad((slidy č.5, strana 3))>
Mějme interpretaci <math>I</math> z předchozího příkladu (celá čísla s > a +) a valuaci <math>V(x) = 2</math>. Pak
<math>|f(b_1, f(b_2, b_2))|_{I,V} = +(-1, +(-2,-2)) = -5</math>
<math>|f(f(a, b_1), f(x, a_1))|_{I,V} = +(+(0, -1), +(2, 1)) = 2</math>
</box>

<box 100% round blue|Pravdivost formulí>
  * Formuli <math>A</math> nazveme pravdivou v interpretací <math>I</math>, je-li splňována <math>I</math> pro libovolnou valuaci; píšeme <math>|={ }_I A</math>
  * Formule <math>A</math> je 
    - **tautologie**, pokud je pravdivá pro každou interpretaci
    - **splnitelná**, pokud je pravdivá pro alespoň jednu interpretaci a valuaci.
    - **kontradikce**, pokud <math>\neg A</math> je tautologie
</box>

==== 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
<box 100% round blue|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 <math>\neg</math>, <math>\wedge</math> a <math>\vee</math>
  - přesunout negaci dovnitř
  - přesunout kvantifikátory doleva
  - použít distributivní zákony k převodu jádra do KNF (DNF)
</box>

==== Skolemizace ====
**Skolemova normální forma** je prenexová normální forma s pouze univerzálními kvantifikátory.
  * odstraníme existenční (<math>\exists</math>) kvantifikátory
  * formuli <math>\forall x_1,...,\forall x_n \exists y P(x_1,...,x_n,y)</math> převedeme na <math>\forall x_1,...,\forall x_n P(x_1,...,x_n,f(x_1,...,x_n))</math>
<box 100% round blue|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
</box>

==== 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** <math>\phi</math> je konečná množina <math>\{x_1{/}t_1,x_2{/}t_2,...,x_n{/}t_n\}</math>, kde všechna <math>x_i</math> jsou vzájemně různé proměnné a každé <math>t_i</math> je term různý od <math>x_i</math>. 
  * pokud jsou všechna <math>t_i</math> uzavřené termy (neobsahují proměnné), jedná se o **uzavřenou substituci**
  * pokud jsou <math>t_i</math> proměnné, označujeme <math>\phi</math> jako **přejmenování proměnných**
<box 100% round blue|Konečná substituce>
  * označme libovolný term nebo literál jako výraz <math>E</math>
  * <math>E \phi</math> je pak výsledek nahrazení všech výskytů všech <math>x_i</math> odpovídajícími termy <math>t_i</math>
  * <color red>!POZOR!</color> Nahrazení v rámci jedné substituce <math>\phi</math> probíhají paralelně. Když se použijí dvě substituce <math>\phi\psi</math>, probíhají postupně.
</box>
**Kompozice substitucí** -- postupně bereme prvky z první substituce a hledáme ve druhé, zda není možnost nahradit nahrazovaného (tranzitivně)

**Unifikátor** 
Substituci <math>\phi</math> nazveme **unifikátorem** množiny formulí <math>S = \{E_1,...,E_n\}</math>, pokud <math>E_1 \phi = E_2 \phi = ... = E_n \phi</math>, tedy v případě, že <math>S \phi</math> má jeden prvek.
  * Existuje-li unifikátor množiny, označíme ji jako unifikovatelnou
<box 100% round blue|Unifikátor příklad>
  * unifikátorem <math>\{{P(x,c),P(b,c)}\}</math> je <math>\phi = \{{x{/}b}\}</math>
  * <color red>!POZOR!</color> Unifikujeme vždy tak, že místo proměnné dáme term a ne naopak
</box>

Unifikátor <math>\phi</math> množiny <math>S</math> je **[[http://webdocs.cs.ualberta.ca/~you/courses/325/Mynotes/Log/unif.html|nejobecnějším unifikátorem]]** (mgu) <math>S</math>, pokud pro libovolný unifikátor <math>\psi</math> množiny <math>S</math> existuje substituce <math>\lambda</math> taková, že <math>\phi \lambda = \psi</math> -- pro unifikovatelné množiny existuje pouze jediný mgu (až na přejmenování proměnných)
**Rozdíly mezi výrazy** označujeme jako <math>D(S)</math> 

<note>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 <math>E \in S</math> začínajících na této pozici.((prevzato ze skript Úvod do logiky a logického programování, Luboš Popelínský, Eva Mráková))
</note>

<box 100% round blue|Unifikační algoritmus pro množinu výrazů S>
  * krok 0: <math>S_{0} := S</math>, <math>\phi_{0} := \epsilon</math>
  * krok k+1:
    * je-li <math>S_{k}</math> jednoprvková, ukonči algoritmus s výsledkem <math>mgu(S) = \phi_{0}\phi_{1}\phi_{2} ... \phi_{k}</math>
    * jinak, pokud v <math>D(S_{k})</math> není proměnná v a term t, který ji neobsahuje, ukonči algoritmus s výsledkem neexistuje <math>mgu(S)</math>
    * jinak vyber takovou proměnnou v a term t, který neobsahuje v, <math>\phi_{k+1} := \{v/t\}</math>, <math>S_{k+1} := S_{k}\phi_{k+1}</math> a pokračuj krokem k+2
</box>

<note>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 [[http://www.fi.muni.cz/usr/popelinsky/lectures/bak_logika/p6.pdf|Predikátová logika III]].</note>

==== 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
<box 100% round blue|Příklad rezoluční formule>
formule: <math>\forall x \forall y ((P(x,f(x))\vee \neg Q(y))\wedge(\neg R(f(x))\vee \neg Q(y)))</math>
rezoluční forma: <math>\{\{P(x,f(x)),\neg Q(y)\},\{ \neg R(f(x)),\neg Q(y)\}\}</math>
</box>
**Rezoluční pravidlo** pro predikátovou logiku. Mějme klauzule <math>C_1</math>, <math>C_2</math> bez společných proměnných (po případném přejmenování) ve tvaru:
  * <math>C_1 = C_1' \cup \{P(x_1),...,P(x_n)\}</math>
  * <math>C_2 = C_2' \cup \{\neg P(y_1),...,\neg P(y_m)\}</math>.
  * Je-li <math>\phi</math> mgu množiny <math>\{P(x_1),...,P(x_n),P(y_1),...,P(y_m)\}</math>, pak rezolventou <math>C_1</math> a <math>C_2</math> je <math>C_1' \phi \cup C_2' \phi</math>
<box 100% round blue|Příklad rezolventy>
Rezolvujeme klauzule <math>\{{P(x,y),\neg R(x)}\}</math> a <math>\{\neg P(a,b)\}</math> 
  - mgu <math>(\{P(x,y),P(a,b)\}) = \{{x{/}a,y{/}b}\}</math> 
  - aplikujeme mgu na <math>\{{\neg R(x)}\}</math> 
  - rezolventa <math>\{{\neg R(a)}\}</math> 
</box>

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
<note>
Měli byste znát jednotlivé druhy rezolucí více podrobně -- tak jako jsou uvedeny v dalších otázkách:
[[home:inf:ap4|AP4, IN4 Výroková logika]] a [[home:inf:ap13|AP13 Prolog]]
</note>

===== Předměty =====
  * [[https://is.muni.cz/auth/predmety/predmet.pl?kod=IB101|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.

~~DISCUSSION~~