Scan0022

30 Metoda rezolucji. Elementy logiki pierwszego rzędu

Twierdzenie 3.2 Klauzula pusta □ jest niespełnialna.

Aby udowodnić, że formuła F jest tautologią stosujemy pewien algorytm wykazując, że ~ F jest niespełnialna. Algorytm ten składa się z ciągu zastosowań reguły rezolucji do zbioru klauzul. Jeśli uda się uzyskać niespełnialną klauzulę pustą, to pierwotny zbiór klauzul jest niespełnialny.

Definicja 3.2 (Reguła rezolucji, [4]) Niech l~ oznacza dopełnienie literału l. Niech Ci, C2 będą klauzulami takimi, ze l £ C\, l~ 6 C2. Klauzule Ci, C2 nazywamy klauzulami kolidującymi i mówimy, że kolidują względem komplementarnych literałów l, l~. Rezolwentą klauzul Ci i C2 nazywamy klauzulę C postaci:

C = Rez(C_uC₂) = (Cl - {/}) U (C₂ - {/"}).

Klauzule Ci i C2 nazywamy klauzulami macierzystymi dla C.

Przykład 3.2 Para klauzul

Ci = {p,q,~r}, C₂ = {q,r,~s}

koliduje względem literałów r, ~ r. Rezolwentą tych klauzul jest klauzula

C = ({p, q, ~ r} - {- r}) U ({g, r, ~ s} - {r}) =

= {p, q] U {q, ~ s} = {p, q, q, ~ s}

= (p,g,~ s}.

Ponieważ klauzula jest zbiorem, stąd powtarzające się literały są usuwane z sumy zbiorów¹.

Algorytm 3.3 (Metoda rezolucji, [4]) Wejściem jest zbiór klauzul S, natomiast wyjściem odpowiedz, czy S jest spełnialny lub niespełnialny. Przyjmujemy na początku, że Sq = S. Niech Si oznacza zbiór klauzul w

1

Wyznaczając rezolwenty należy mieć na uwadze, że:

Rez ({p, ~ q} , {~ p, <7}) ± □,

Rez ({p, ~ <7} , {~ p, <7}) = {~ <7, q} (tautologia),

Rez ({p, ~ q, r} , {~ p, q, ~ s}) ^ {r, ~ s} ,

Rez ({p, ~ q,r}, p, q, ~ s}) = {~ p,p, r, ~ s} (tautologia).