Scan0023

3.1 Metoda rezolucji dla logiki zdaniowej 31

i-tym kroku. Wybierz parę klauzul kolidujących Ci, C2 £ S_l} które jeszcze nie były wybrane. Niech C będzie rezolwentą C1 i C2 zgodnie z definicją reguły rezolucji. Niech Si+i = Si U {C}. Jeśli:

•    C — □, to zakończ algorytm stwierdzając, ze S jest niespełnialny,

•    Si+1 = Si dla wszystkich możliwych wyborów klauzul kolidujących, to zakończ algorytm stwierdzając, że S jest spełnialny.

3.1.3 Zastosowanie metody rezolucji

Dowody metodą rezolucji będziemy przeprowadzać następująco:

•    aby zbadać prawdziwość formuły F, negujemy tę formułę i stosujemy metodę rezolucji dla ~ F,

•    aby zbadać, czy formuła B wynika logicznie z U negujemy B, dołączamy ~ B do zbioru formuł i stosujemy metodę rezolucji.

Uzasadnienie dla podanego postępowania jest następujące. Biorąc

F = (Ai A ... A A_n) => B

otrzymujemy

~ F = ~ [(Ai A ... A A_n) => B) =

= ~ [~ (Ai A ... A An) V B] =

= Ai A ... A A_n A ~ B.

Przykład 3.3 Zbadać poprawność wnioskowania p => (q A r), r => 5, ~ (q A s)

1. Wyznaczamy kpn:

p => (q A r) = ~ p V (g A r) = (~ p V ę) A (~ p V r) r => s = ~ r V s ~(gAs)=~^V~s ~ (~ p) = p (negacja wniosku!)