Rezoluce v predikátové logice

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


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.



2/16


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.



3/16


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


4/16


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.



5/16


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.



6/16


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



7/16


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



8/16


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.



9/16


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.



10/16


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.



11/16


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)



12/16


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.



13/16


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



14/16


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



15/16


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



16/16

Rezoluce v predikátové logice

Recommend Documents