4 Je±li k jest nagacj¡ prawdy lub faªszu, to zamieniamy j¡ na faªsz lub prawd¦

Metod¦ rezolucji, znan¡ z rachunku

zda«, mo»na teraz naturalnie uogólni¢ na rachunek predykatów.

Przypomnijmy, »e struktur¡ reprezentuj¡c¡ formuª¦ jest zbiór zbiorów literaªów, albo ogólniej formuª:

L = {a1, . . . ,as} = {{k₁¹, . . . ,k_m¹}, . . . , {k₁^s, . . . ,k_n^s}}

Zbór ten opisuje formuª¦ ϕ_L, która jest koniunkcj¡ s-alternatyw typu k₁¹∨ . . . ∨k_m¹. Formuªa ta jest niespeªnialna, gdy L zawiera zbiór pusty. Uwzgl¦dnimy te», »e nie zdeniowali±my jeszcze poj¦cia klauzuli dla rachunku kwantykatorów, wi¦c trzeba pami¦ta¢, o przeksztaªaniu formuª tak, aby faktycznie byªy

koniunkcjami alternatyw! Pami¦tajmy te», »e tutaj dodaje si¦ do zbioru nowe formuªy.

Reguªy dowodu dla metody rezolucji: Niech k ∈ a_i ∈L

1 Je±li k = ¬¬l, dodajemy do L zbiór powstaªy z ai przez zast¡pienie k formuª¡ l.

2 Je±l k jest β formuª¡ dodajemy zbiór powstaªy z a_i, w którym formuªa k zast¡piona jest skªadnikami β₁, β₂.

3 Je±l k jest α formuª¡ dodajemy dwa zbiory powstaªe z a_i, w których formuªa k zast¡piona jest skªadnikiem α₁ albo α₂.

4 Je±li k jest nagacj¡ prawdy lub faªszu, to zamieniamy j¡ na faªsz lub prawd¦.

5 Je±li k jest γ-formuª¡, to dodajemy zbiór powstaªy z a_i, w którym formuªa k zast¡piona jest przez formuª¦ powstaj¡c¡ z niej przez podstawienie termu bazowego za zmienn¡ zwi¡zan¡

usuwanym kwantykatorem uniwersalnym.

6 Je±li k jest δ-formuª¡, to dodajemy zbiór powstaªy z a_i, w którym formuªa k zast¡piona jest przez formuª¦ powstaj¡c¡ z niej przez podstawienie za zmienn¡ nowej staªej.

1 Je±li dwa zbiory a_i oraz a_j zawieraj¡ par¦ formuª

komplementarnych k i ¬k, to dodajemy do L ich rezolwent¦:

a_i ∪a_j \ {k, ¬k}.

Przykªad 1. Wykorzystamy metod¦ rezolucji w dowodzie twierdzenia rachunku kwantykatorów:

∀_x(ϕ ⇒ ψ) ⇒ (∀_xϕ ⇒ ∀_xψ). W kolejnych punktach wypisujemy tylko dodawane zbiory formuª.

1 {{¬(∀_x(ϕ ⇒ ψ) ⇒ (∀_xϕ ⇒ ∀_xψ)}}

2 {∀_x(ϕ ⇒ ψ)}, {¬(∀_xϕ ⇒ ∀_xψ))}

3 {∀_xϕ}, {¬∀_xψ}

4 {¬ψ(a)}, gdzie a jest now¡ staª¡;

5 {ϕ(a)}

6 {ϕ(a) ⇒ ψ(a)}

7 {¬ϕ(a), ψ(a)}, a bior¡c rezpolwent¦ z 5 mamy

8 {ψ(a)} i rezolwenta z 4 daje pusty zbiór.

Werykowanie, czy mo»na bra¢ rezolwent¦ dwóch zbiorów, gdy rozwa»amy dowolne formuªy, a nie literaªy mo»e by¢ ograniczone do specjalnych formuª, które równie» b¦dziemy nazywa¢ literaªami, czyli formuª atomowych lub ich negacji.

Denicja

Formuªa jest w preneksowej postaci normalnej, gdy jest postaci:

Q₁. . .Q_nM

gdzie Q_i jest postaci ∃x lub ∀x, a M jest w koniunkcyjnej postaci normalnej, czyli jest koniunkcj¡ alternatyw literaªów. Wtedy

Q₁. . .Q_n nazywamy preksem, a M matryc¡ formuªy. Formuªa jest w postaci klauzulowej, je±li w preksie wyst¦puje tylko

kwantykator uniwersalny. Oczywi±cie zbiór literaªów rozumiany jako ich alternatywa nazywamy klauzul¡.

Przypomnijmy, »e w metodzie rezolucji zachowywana jest speªnialno±¢.

Denicja

Dla formuª A, A⁰, niekoniecznie tego samego j¦zyka, zapis A ≈ A⁰ oznacza, »e A i A⁰ s¡ jednocze±nie speªnialne lub niespeªnialne.

Okazuje si¦, »e gdy chodzi o speªnialno±¢ zda« (czyli prawdziwo±¢) mo»emy rozwa»a¢ tylko klauzule!

Twierdzenie (Skolem)

Dla ka»dego zdania A istnieje zdanie A⁰ w postaci klauzulowej takie, »e A ≈ A⁰.

Uwaga Przykªad formuªy ∀_x∃_yp(x, y) rozwa»any w poprzednim rozdziale obja±nia, jak usuwa si¦ kwantykator ∃: prawdziwo±¢ tego zdania oznacza, »e dla ka»dego x mo»na dobra¢ y, aby otrzyma¢

warto±ciowanie, przy którym p(x, y) jest speªnialne. To odpowiada intuicji funkcji, wi¦c nietrudno wykaza¢, »e A⁰ = ∀_xp(x, f (x)) jest dobrym zdaniem A ≈ A⁰. Opiszemy odpowiedni algorytm na przykªadzie zdania z przykªadu 1.

Algorytm skolemizacji Wej±cie: zdanie A

Wyj±cie: zdanie A⁰ w postaci klauzulowej takie,»e A ≈ A⁰.

1 Zmieniamy zmienne kwantykowane tak, aby »adna nie wyst¦powaªa w dwóch kwantykatorach.

∀_x(ϕ(x) ⇒ ψ(x)) ⇒ (∀_yϕ(y) ⇒ ∀_zψ(z))

2 Przeksztaªamy formuª¦ do postaci, w której wyst¦puje tylko nagacja, alternatywa i koniunkcja.

¬∀_x(¬ϕ(x) ∨ ψ(x)) ∨ ¬∀_yϕ(y) ∨ ∀_zψ(z)

3 Korzystamy z praw de Morgana, aby przesun¡¢ negacj¦ "do

±rodka"i usun¡¢.

∃_x(ϕ(x) ∧ ¬ψ(x)) ∨ ∃_y¬ϕ(y) ∨ ∀_zψ(z)

4 Wyci¡gamy na zwen¡trz wszystkie kwantykatory np. w kolejno±ci ich wyst¦powania.

∃_x∃_y∀_z((ϕ(x) ∧ ¬ψ(x)) ∨ ¬ϕ(y) ∨ ψ(z))

1 Teraz matryc¦ przeksztaªcamy do postaci normalnej koniunkcyjnej:

∃_x∃_y∀_z((ϕ(x) ∨ ¬ϕ(y) ∨ ψ(z)) ∧ (¬ψ(x) ∨ ¬ϕ(y) ∨ ψ(z))

2 Dla ka»dego kwantykatora ∃x i kwantykatorów

uniwersalnych dla zmiennych y₁, . . . ,y_n poprzedzaj¡cych go wprowadzamy nowy symbol funkcji n-argumentowej f (gdy n = 0 wprowadzamy staª¡). Nast¦pnie usuwamy ∃x i zast¦pujemy ka»de wyst¡pienie zmiennej x termem f (y₁, . . . ,y_n).

∀_z((ϕ(a) ∨ ¬ϕ(b) ∨ ψ(z)) ∧ (¬ψ(a) ∨ ¬ϕ(b) ∨ ψ(z))

Uwagi:

1 Nietrudno wykaza¢, »e pierwszych pi¦¢ kroków algorytmu zachowuje logiczn¡ równowa»no±¢.

2 Algorytm jest niedterministyczny, wi¦c np. wybór kolejno±ci wyci¡gni¦cia kwantykatorów wpªywa na otrzymane wyj±cie.

Twierdzenie Skolema mo»na wykorzysta¢ modykuj¡c algorytm rezolucji nast¦puj¡co:

1 Je±li k jest γ-formuª¡, to dodajemy zbiór powstaªy z a_i, w którym formuªa k zast¡piona jest przez formuª¦ powstaj¡c¡ z niej przez podstawienie nowej zmiennej za zmienn¡ zwi¡zan¡

usuwanym kwantykatorem uniwersalnym.

2 Je±li k jest δ-formuª¡, to dodajemy zbiór powstaªy z ai, w którym formuªa k zast¡piona jest przez formuª¦ powstaj¡c¡ z niej przez podstawienie za zmienn¡ termu f (y₁, . . . ,y_n), gdzie f jest nowym symbolem funkcyjnym, a y1, . . . ,yn zmiennymi wolnymi formuªy ϕ_L.

3 Reguªa rezolucji jest stosowana przy wªa±ciwym podstawieniu uzgadniaj¡cym.

Zauwa»my, »e wobec powy»szych modykacji nawet gdy

zastosujemy metod¦ do zdania zaczn¡ si¦ pojawia¢ formuªy, które nie b¦d¡ zdaniami. Mo»emy przykªadowo otrzyma¢ lieraªy

{¬r(d(v), v, w))} i {r(u, a, f (u))}, gdzie a jest staª¡, a u, v, w zmiennymi, które nie s¡ komplementarne, ale za zmienne mo»emy podstawi¢ termy tak, aby uzyska¢ par¦ literaªów

komplementarnych. Metody wyznaczania (najbardziej ogólnego) unikatora s¡ wa»nym dziaªem programowania równo±ciowego. W podanym przykªadzie nie wyst¦puj¡ kwantykatory, wi¦c ªatwo zauwa»y¢, »e oryginalna para formuª jest niespeªnialna wtw, gdy ich rezolwenta uzyskana przez podstawienie

v := a, u := d(a), w := f (d(a)) jest niespeªnialna.

Przykªad Rozwa»my formuª¦ ∃_yx = y arytmetyki liczb naturalnych. Oczywi±cie jest ona twierdzeniem tej arytmetyki.

Podstawmy za x term y + 1, otrzymane zdanie ∃_yy + 1 = y nie jest prawdziwe! Jest to mo»liwe poniewa» postawienie to nie jest wªa±ciwe.

Denicja

Term t jest wolny dla zmiennej x i formuªy ϕ, je±li »adne wyst¡pienie zmiennej x w ϕ nie jest w zasi¦gu kwantykatora

∀_y, ∃_y dla zmiennej y wyst¦puj¡cej w t. Wtedy podstawienie t za x w ϕ nazywamy wªa±ciwym.

Mo»na pokaza¢, »e stosowanie wªa±ciwych podstawie« zachowuje speªnialno±¢.

Przykªad 2. Przeprowadzimy dowód zdania

∃_z∀_xr(x, z, f (x)) ⇒ ∃z∀_x∃_yr(x, z, y))

1 {{¬(∃_z∀_xr(x, z, f (x)) ⇒ ∃z∀_x∃_yr(x, z, y)))}}

2 {∃_z∀_xr(x, z, f (x))}

3 {¬∃_z∀_x∃_yr(x, z, y))}

4 {∀_xr(x, a, f (x))}

5 {¬∀_x∃_yr(x, v, y))}

6 {¬∃_yr(d(v), v, y))}

7 {¬r(d(v), v, w))}

8 {r(u, a, f (u))}

Tutaj a jest now¡ staª¡, u, v, w nowymi zmiennymi. Bior¡c dwie ostatnie klauzule, dokonuj¡c podstawienia

v := a, u := d(a), w := f (d(a)) i stosuj¡c rezolucj¦ otrzymamy klauzul¦ pust¡.

Opisana wersja metody rezolucji jest dosy¢ trudna w implementacji.

Po pierwsze, w czasie dowodu zmienia si¦ j¦zyk, co trzeba kontrolowa¢. Po drugie, wyszukiwanie unikatora najbardziej ogólnego tylko dla jednej pary klauzul cz¦sto wydªu»a dowód.

Dlatego pojawiªy si¦ wersje rezolucji, które uwzgl¦dniaj¡c te uwagi s¡ bardziej efektywne.