Čtení: 40 minHodnotí se: test 2 (15 b), zkouška

4 Logika prvního řádu a rezoluce

Po přečtení umíš

zapsat větu v logice prvního řádu bez typických chyb
převést formuli do CNF včetně skolemizace
unifikovat dva termy
dokázat tvrzení rezolucí zamítáním

4.1 Ukázka: Sokrates

Všichni lidé jsou smrtelní a Sokrates je člověk. Chceme dokázat, že je smrtelný. Rezoluce dokazuje sporem: přidá opak a hledá prázdnou klauzuli.

$\neg Man(x) \vee Mortal(x)$
$Man(Sokrates)$
$\neg Mortal(Sokrates)$ (negace tvrzení)
Z 1 a 3 s $x / Sokrates$ : $\neg Man(Sokrates)$
Ze 4 a 2: prázdná klauzule $\bot$

Spor, tedy tvrzení platí.

4.2 Zápis vět

Varování 4.2 (Dvě klasické chyby)

Všichni se píšou s implikací: $\forall x\, Cat(x) \Rightarrow Mammal(x)$ . S konjunkcí by to znamenalo, že všechno je kočka.

Existuje se píše s konjunkcí: $\exists x\, Cat(x) \wedge Black(x)$ . S implikací to platí už díky čemukoli, co není kočka.

4.3 Převod na CNF

Odstraň $\Rightarrow$ a $\Leftrightarrow$ .
Přesuň negace k atomům: $\neg\forall x\, p$ je $\exists x\, \neg p$ .
Přejmenuj proměnné, aby se neopakovaly.
Skolemizuj: existenční proměnnou nahraď funkcí všeobecných proměnných, které jsou nad ní.
Zahoď $\forall$ .
Distribuuj $\vee$ přes $\wedge$ .

Varování 4.3 (Skolemizace závisí na vnějších proměnných)

$\forall x\, \exists y\, Loves(x, y)$ dá $Loves(x, F(x))$ , ne $Loves(x, A)$ . Konstanta by tvrdila, že všichni milují stejného.

4.4 Unifikace

Definice 4.4 (Nejobecnější unifikátor)

Substituce $\theta$ s nejméně omezeními, po které jsou dva výrazy stejné.

Výrazy	Výsledek
$Knows(John, x)$ , $Knows(John, Jane)$	$\{x / Jane\}$
$Knows(John, x)$ , $Knows(y, Mother(y))$	$\{y / John, x / Mother(John)\}$
$Knows(John, x)$ , $Knows(x, Elizabeth)$	selhání

Třetí případ selže jen kvůli stejnému jménu proměnné. Po standardizaci na $Knows(z, Elizabeth)$ vyjde $\{z / John, x / Elizabeth\}$ . Proto se před rezolucí proměnné v klauzulích přejmenují.

4.5 Rezoluce a faktorizace

Definice 4.5 (Rezoluční pravidlo)

Z $(x_1 \vee \dots \vee z)$ a $(y_1 \vee \dots \vee \neg z')$ při unifikátoru $\theta$ literálů $z$ a $z'$ odvoď $(x_1 \vee \dots \vee y_1 \vee \dots)\theta$ .

Samotná rezoluce v logice prvního řádu není úplná. Holičův paradox ji přivede k nekonečnému běhu. Doplňuje ji faktorizace: sloučení unifikovatelných literálů v jedné klauzuli.

Rezoluce je jen semi-rozhodovací. Je-li tvrzení důsledkem, najde důkaz, ale jinak nemusí skončit.

ANL smyčka odvozuje rezolventy ze seznamů waiting a usable, dokud nenajde $\bot$ .

4.6 Rovnost a SMT

Pro logiku s rovností se rovnosti převádějí na SAT s doplněnou tranzitivitou, nebo se línou cestou přidává jen to, co řešič poruší. SMT spojuje SAT řešič s teoriemi, třeba aritmetikou.

4.7 Kvíz

Kvíz

1. Jak zapíšeš „každý student má učitele“?

\forall s\, \exists u\, Student(s) \wedge Teach(u, s)

\forall s\, Student(s) \Rightarrow \exists u\, Teach(u, s)

\exists u\, \forall s\, Student(s) \Rightarrow Teach(u, s)

2. Skolemizace

\forall x\, \forall y\, \exists z\, P(x, y, z)

dá:

P(x, y, A)

P(x, y, F(x))

P(x, y, F(x, y))

3. Unifikuje se

P(x, x)

P(A, B)

pro různé konstanty? Ano,

x / A

Ano,

x / B

4. Co platí pro rezoluci v logice prvního řádu? Může být správně více možností, ale také žádná. Dokazuje sporem Vyžaduje CNF Vždy skončí S faktorizací je zamítavě úplná

5. Proč negujeme dokazované tvrzení?

Ukázat řešení

Pokud

T \cup \{\neg C\}

vede ke sporu, není model

T

, ve kterém by

C

neplatilo, tedy

T \models C

4.8 Příklady na procvičení

Cvičení 4.6

Vyjádři „Existuje právník, jehož všichni zákazníci jsou lékaři“ pomocí $Occupation(p, o)$ a $Customer(p_1, p_2)$ .

Řešení

$\exists l\, Occupation(l, Lawyer) \wedge \forall c\, (Customer(c, l) \Rightarrow Occupation(c, Doctor))$ . Uvnitř je implikace, protože jde o všechny zákazníky.

Cvičení 4.7

Je $\forall x\, P(x) \vee \neg P(x)$ pravdivá?

Řešení

Ano, pro každé $x$ platí jedna ze dvou možností, v každé struktuře.

Cvičení 4.8

Které formule říkají „žádná země z Jižní Ameriky nesousedí se zemí v Evropě“?

(a) $\neg[\exists c, d\, In(c, SA) \wedge In(d, E) \wedge Borders(c, d)]$

(b) $\forall c, d\, [In(c, SA) \wedge In(d, E)] \Rightarrow \neg Borders(c, d)$

Řešení

Správně jsou (a) a (b), které jsou navzájem ekvivalentní. Možnost (c) říká něco jiného.

4.9 Tahák

Tahák

$\forall$ s $\Rightarrow$ , $\exists$ s $\wedge$ .
CNF: spojky, negace dovnitř, přejmenuj, skolemizuj, zahoď $\forall$ , distribuuj.
Skolem: funkce vnějších $\forall$ .
Unifikace: nejobecnější $\theta$ , před ní standardizuj.
Důkaz: $T \cup \{\neg C\} \vdash \bot$ .
Bez faktorizace neúplná, celkově semi-rozhodovací.

Kapitolu mám prostudovanou