Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Rezoluce v predikátové logice
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
1/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Základní myšlenky 1
M |= ϕ iff X = M ∪ {¬ϕ} nesplnitelná. (M musí být množina sentencí, ϕ sentence.)
2
X nesplnitelná iff X |= ff.
3
Hledání „kritickýchÿ důsledků X syntakticky. K tomu je zapotřebí speciální tvar X .
4
Speciální tvar X je klausální tvar X .
Vše budeme dělat pro konečnou množinu M. Pak i X je konečná. Tudíž: (syntaktický) algoritmus. V zásadě stejný algoritmus jako ve VL, některé kroky jsou však složitější — dáno složitostí syntaxe PL.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
2/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Sentence v CNF Řekneme, že ψ je v CNF, když má tvar buď tt nebo ψ1 ∧ . . . ∧ ψn , kde 1
každé ψi je sentence tvaru buď τi nebo ∀x1 .∀x2 . . . ∀xmi .τi
2
každé τi (tzv. tělo klausule ψi ) je buď ff nebo nebo `1 ∨ . . . ∨ `ki
3
každé `j (literál) je buď atom nebo negace atomu.
Upozornění Nedefinujeme CNF jako synonymum. Při hledání CNF může dojít ke změně jazyka: tzv. Skolemovo rozšíření, neboli skolemisace.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
3/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Převod sentence ϕ na CNF 1
Vyčištění výskytu proměnných: každý kvantifikátor musí vázat jinou proměnnou. (α-konverse, to může vyžadovat deklaraci fresh proměnných.)
2
Odstranění nepohodlných spojek.
3
Distribuce ¬ těsně před atomy (de Morganova pravidla).
4
Distribuce ∨ na nejnižší možnou hladinu (distributivní a asociativní zákony — další strana).
5
Distribuce ∧ na nejvyšší možnou hladinu a eliminace existenčních kvantifikátorů (distributivní a asociativní zákony a skolemisace — viz další strany).
6
Výslednou sentenci označíme cnf(ϕ).
Obecně nedosáhneme ϕ |=| cnf(ϕ) Bude platit: ϕ a cnf(ϕ) jsou ekvisplnitelné. Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
4/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Nové distributivní a asociativní zákony Platí: 1
Asociativita ∀ a ∧: ∀x.(α ∧ β) |=| ∀x.α ∧ ∀x.β pro libovolné formule α, β.
2
Asociativita ∃ a ∨: ∃x.(α ∨ β) |=| ∃x.α ∨ ∃x.β pro libovolné formule α, β.
3
Distributivita ∀ a ∨: ∀x.(α ∨ β) |=| ∀x.α ∨ β pro libovolné formule α, β, kde v β se nevyskytuje x.
4
Distributivita ∃ a ∧: ∃x.(α ∧ β) |=| ∃x.α ∧ β pro libovolné formule α, β, kde v β se nevyskytuje x.
Intuice: ∀ je nekonečné and a ∃ je nekonečné or.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
5/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Skolemovo rozšíření Sentenci ∀x1 . . . ∀xm .∃y .α,
m≥0
nahraďte sentencí ∀x1 . . . ∀xm .α[y := f (x1 , . . . , xm )] kde f je fresh funkční symbol arity m.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
6/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Příklad Najděte cnf(ϕ) pro sentenci ϕ ve tvaru ¬ ∀x.(P(x) ⇒ ∃y .Q(x, y )) ⇒ ¬∀x.(P(x) ⇒ ∃y .P(f (y ))) Pozorování Zjevně pro obecnou sentenci ϕ platí: ϕ a cnf(ϕ) jsou ekvisplnitelné.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
7/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Klausální tvar množiny sentencí α ∈ kt(X ) iff α je klausule nějaké cnf(ϕ) pro ϕ ∈ X . Upozornění kt(X ) není jednoznačně určen! Pozorování X a kt(X ) jsou ekvisplnitelné.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
8/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Komplementární výskyt Dvě klausule ψ1 , ψ2 pro CNF obsahují komplementární výskyt predikátu formule P, pokud se v ψ1 vyskytuje P a v ψ2 se vyskytuje ¬P (nebo naopak). Příklady Ať f ∈ Pred arity 1, R ∈ Pred, arity 2 a x, y , u, v ∈ Var. 1
Klausule ∀x∀y (¬x = y ∨ ¬R(x, y )), ∀u∀v (¬u = v ∨ R(u, v )). Komplementární výskyt predikátu R.
2
Klausule ∀x∀y (¬x = y ∨ ¬R(x, f (y ))), ∀u∀v (¬u = v ∨ R(u, v )). Komplementární výskyt predikátu R.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
9/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Příklad, pokrač. 3
Klausule ∀x∀y (x = y ∨ ¬R(x, f (y ))), ∀u∀v (¬u = f (v ) ∨ R(u, v )). Komplementární výskyt predikátu = a komplementární výskyt predikátu R.
4
Klausule ∀x∀y (x = y ∨ ¬R(x, f (y ))), ∀u∀v (u = f (v ) ∨ ¬R(u, v )). Žádný komplementární výskyt predikátu.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
10/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Jak utvořit resolventu dvou klausulí ψ1 a ψ2 1
Obsahují ψ1 a ψ2 komplementární výskyt predikátu? (Pokud ne, stop: resolventa neexistuje.)
2
Označte predikát s komplementárním výskytem jako P.
3
Existuje maximální unifikátor pro atomy vytvořené z P? (Pokud ne, stop: resolventa podle P neexistuje.)
4
Označte maximální unifikátor jako ϑ.
5
Spočítejte ψ1 [ϑ] a ψ2 [ϑ]. Těla těchto klausulí označte jako τ1 a τ2 .
6
Vytvořte tělo, které obsahuje všechny literály obsažené v τ1 a τ2 kromě literálů začínajících P a ¬P. Toto tělo označte τ .
7
Tělo τ doplňte obecnými kvantifikátory na sentenci.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
11/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Příklady: nalezněte maximální unifikátor 1
P(x, y ) a P(t, f (z)) (x, y , z, t st. proměnné, P predikát arity 2, f funkční symbol arity 1)
2
Q(a, y , f (y )) a Q(z, z, u) (x, y , z st. proměnné, Q predikát arity 3, f funkční symbol arity 1, a, u funkční symboly arity 0)
3
R(x, g (x)) a R(y , y ) (x, y st. proměnné, R predikát arity 2, g funkční symbol arity 1)
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
12/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Definice Ať X 0 je konečná množina klausulí pro CNF. Posloupnost Res0 (X 0 ), Res1 (X 0 ), Res2 (X 0 ), Res3 (X 0 ), . . . definujeme takto: Res0 (X 0 ) = X 0 Resn+1 (X 0 ) = Resn (X 0 ) ∪ {α | α je resolventa nějaké dvojice z Resn (X 0 )} Pozorování Ekvisplnitelnost je invariantem a tvorba posloupnosti množin se zastaví po konečně krocích.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
13/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Důsledek: základní resoluční algoritmus 1
Rozhodněte, zda M |= ϕ (M konečná).
2
Utvořte X = M ∪ {¬ϕ}.
3 4
Ať X 0 = kt(X ). Potom X 0 a X jsou ekvisplnitelné. Existuje n0 tak, že platí Resn0 +1 (X 0 ) = Resn0 (X 0 ). Dále platí: 1 2
5
Množiny X 0 a Resn0 (X 0 ) jsou ekvisplnitelné. Množina X 0 není splnitelná právě tehdy, když platí ff ∈ Resn0 (X 0 ).
M |= ϕ platí iff X 0 není splnitelná.
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
14/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Pozor! Na přednášce bude zmíněna i mírná varianta klasického resolučního algoritmu, kterou v tomto textu nenajdete. Tuto variantu (zamítací stromy) naleznete ve skriptu M. Demlová a B. Pondělíček, Matematická logika, FEL ČVUT, Praha 1997
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
15/16
Klausální tvar množiny formulí Tvorba rezolvent — maximální unifikátor Rezoluční algoritmus
Příklad Resolučním algoritmem rozhodněte, zda platí {∀x.∀y .((P(x) ∧ Q(x, y )) ⇒ R(y )), ∀x.Q(f (x), g (x)), P(f (a))} |= R(g (a)) (Samozřejmě: popište jazyk PL, ve kterém jde o sentence.)
Jiří Velebil: X01DML
15. října 2010: Rezoluce v PL
16/16