1.3. Zasada rezolucji

8 stycznia 2011

Znamy kilka sposobów sprawdzania tautologiczności wyrażeń logicznych.

Są nimi:

1.     metoda matrycowa (zero – jedynkowa).

2.     metoda skrócona (jeśli dane wyrażenie a stanowi implikacja).

3.     metoda aksjomatyczna.

4.     metoda założeniowa.

Dwie ostatnie metody dla niektórych wyrażeń mogą okazać się zbyt trudne w wykazaniu ich tautologiczności. W roku 1965 J.A. Robinson opracował bardzo prostą regułę wnioskowania do automatycznego dowodzenia twierdzeń.

Załóżmy, że mamy dany pewnie zbiór S przesłanek o skończonej liczbie zmiennych. Wszystkie przesłanki łączymy w koniunkcję i całe wyrażenie doprowadzamy do postaci normalnej koniunkcyjno – alternatywnej. Bierzemy koniunkcję dwóch dowolnych członów postaci n.k.a., lecz takich by w jednym z nich występowała pewna zmienna bez negacji, a w drugim członie z negacją (lub odwrotnie). Wykreślamy z obu członów te zmienne i jako rezultat zapisujemy alternatywę pozostałych zmiennych z obu członów koniunkcji.

Przykład. Niech S = {p, p → q, p → r, ~ r}

Tworzymy koniunkcję przesłanek

a = p ˄ (p → q) ˄ (p →  r) ˄ ~ r.

Teraz tworzymy postać n.k.a.

a^` = p ˄ (~ p ˅ q) ˄ (~ p ˅  r) ˄ ~ r.

Bierzemy np. (~ p ˅  r) ˄ ~ r. Jako wynik zastosowania reguły wnioskowania zwanej zasadą rezolucji będzie tu wyrażenie ~ p. Zasadę rezolucji możemy ująć w postać schematu wnioskowania następująco:

(p ˅ q ˅ ~ r ˅ …˅ s) ˄ (~ p ˅ r ˅ … ˅ z)

(p ˅ q ˅ … s ˅ r ˅ … ˅ z)

Uwaga. W każdym członie koniunkcji może być więcej zmiennych z negacją niż jedna. Np. (p ˅ ~ q ˅ ~ r ) ˄ (~ p ˅ ~ s ˅ r). Jako wynik możemy otrzymać w tej sytuacji dwa osobne wyrażenia. Jedno ze względu na zmienną p i jej negację, drugie ze względu na zmienną r i jej negację, czyli jako wynik zastosowania zasady rezolucji do powyższych dwóch przesłanek mamy wyrażnia:

(~ q ˅ ~ r ˅ ˅ ~ s ˅ r)

oraz

(p ˅ ~ q ˅ ~ p ˅ ~ s).

Weźmy raz jeszcze dwa dowolne wyrażenia podpadające pod zasadę rezolucji.

Np.

(~ p ˅ q) ˄ ~ q

~ p

(~ p ˅ q) i ~ q nazywają się klauzulami a ~ p nazywa się rezolwentą.

Jak stosować zasadę rezolucji w dowodzeniu poprawności logicznej (tautologiczności) schematów wnioskowania bądź praw logiki. Wyjaśnimy to na konkretnym przykładzie.

Weźmy następujący schemat logiczny:

p → q

r → s

p ˅ r

q ˅ s

Stosując zasadę rezolucji pokazać, że jest to schemat wnioskowania.

Postępowanie:

1.     wyrażenia nad kreską łączymy w koniunkcję

(p → q) ˄ (r → s) ˄ (p ˅ r).

2.     wyrażenie to doprowadzamy do postaci normalnej koniunkcyjno – alternatywnej

(~ p ˅ q) ˄ (~ r ˅ s) ˄ (p ˅ r).

3.     każdy człon koniunkcji stanowi osobną klauzulę.

4.     wypisujemy je każdą w osobnym wierszu kolumny i jednocześnie numerujemy je:

1.     ~ p ˅ q

2.     ~ r ˅ s

3.     p ˅ r.

5. negujemy wniosek (wyrażenie pod kreską) i zanegowany wniosek doprowadzamy do postaci n.k.a.,

~ (q ˅ s) ≡ (~ q) ˄ (~ s).

6.poszczególne człony koniunkcji dopisujemy do poprzedniej kolumny otrzymując zbiór klauzul.

1. ~ p ˅ q

2. ~ r ˅ s

3. p ˅r

4. ~ q

5. ~ s

7. Podkreślamy ten zbiór poziomą kreską.

1. ~ p ˅ q

2. ~ r ˅ s

3. p ˅r

4. ~ q

5. ~ s

1.     do poszczególnych wybranych par klauzul stosujemy zasadę rezolucji, otrzymane rezolwenty numerujemy kolejnymi liczbami, zaznaczając z boku resolwenty numery klauzul, z których została otrzymana resolwenta. Rezolwenty traktujemy jako nowe klauzule, do których wolno stosować jest zasadę rezolucji. Postępowanie to kontynuujemy tak długo, aż otrzymamy dwa wiersze sprzeczne. Z nich otrzymuje się rezolwentę (klauzulę) pustą. Klauzula pusta kończy dowód (Š – klauzula pusta – oznaczenie).

2.     stosowanie zasady rezolucji stanowi dowód nie wprost. Więc, jeśli jakiś schemat jest tautologią, to zaprzeczony wniosek musi doprowadzić do sprzeczności.

Dowód naszego przykładu jest więc następujący.

1.     ~ p ˅ q

2.     ~ r ˅ s

3.     p ˅ r

4.     ~ q

5.     ~ s

6.     ~ p          (1. i 4.)

7.     ~ r           (2. i 5.)

8.     p             (3. i 7.)

9.                  (6. i 8.)

Kilka innych typowych przypadków wnioskowania z użyciem zasady rezolucji przedstawia poniższa tabela.

Tabela. Zasada rezolucji, przesłanki i rezolwenty.

Przesłanki	Resolwenty	Uwagi
p ~ p ˅ q, (p → q)	q	modus poneus
p ˅ q ~ p ˅ q	q	q ˅ q daje q Rezolwenta sklejana
p ˅ q ~ p ˅ ~ q	p ˅ ~ p q ˅ ~ q	dwie rezolwenty, obie tautologie
p ~ p		klauzula pusta Oznaka sprzeczności
~ p ˅ q, (p → q) ~ q ˅ r, (q → r)	~ p ˅ r (p → r)	wnioskowanie „łańcuchowe”

Powyższa tabela wskazuje, że za pomocą zasady rezolucji można (automatycznie) otrzymywać bezpośrednie wnioski z danych przesłanek.

Przykład. Stosując zasadę rezolucji zbadać jaki lub jakie wnioski wynikają z danego zbioru przesłanek.

Przesłanki:                  S = {p → q, p → r, ~ q ˅ ~ r}.

Tworzymy klauzule:

1. ~ p ˅ q
2. ~ p ˅ r
3. ~ q ˅ ~ r

1. ~ p ˅ ~ r  (1. i 3.)
2. ~ p           (2. i 4.)
3. ~ p ˅ ~ q  (3. i 4.)

4., 5. i 6. stanowią bezpośrednie wnioski trzech powyższych przesłanek.

Zasada rezolucji może też stanowić ważne narzędzie badawcze w sprawdzaniu niesprzeczności danego zbioru przesłanek. Jeżeli zbiór przesłanek jest sprzeczny, tzn. jego koniunkcja ma wartość logiczną zero, to nie może być użyty do wnioskowania.

Przykład. Zbadać niesprzeczność następującego zbioru przesłanek:

S = {p ˅ q, p → r, ~ q ˅ r, ~ r}

Tworzymy klauzule

1. p ˅ q
2. ~ p ˅ r
3. ~ q ˅ r
4. ~ r

1. ~ p           (2. i 4.)
2. ~ q           (3. i 4.)
3. p              (1. i 6.)
4.              (5. i 7.)

Zbiór S przesłanek jest sprzeczny.

Na koniec rozwiążemy zasadą rezolucji problem znalezienia wniosku F(X, Y) wiążącego zmienne X i Y, który wynika ze zbioru następujących przesłanek:

1.     X → Z

2.     Y ≡ ~ V

3.     Z → V.

Tworzymy z tych przesłanek klauzule i szukamy  takiej rezolwenty, która składa się tylko ze zmiennych X i Y.

1.     ~ X ˅ Z

2.     ~ Y ˅ ~ V

3.     V ˅ Y

4.     ~ Z ˅ V

5.     ~ X ˅ V     (1. i 4.)

6.     ~ X ˅ ~ Y  (2. i 5.)

6. jest pożądanym wnioskiem.

Więc F (X, Y) ≡ ~ X ˅ ~ Y. Poprzednia analiza logiczna dała ten sam wynik, lecz droga analizy była dłuższa.

Zadania.

1. Znaleźć wszystkie wnioski z przesłanek.

1.      p → q i p

2.      p ≡ q i ~ p

3.      p ˅ q i p i ~ q

4.      p → q i q → r.

1. Znaleźć wszystkie wnioski dla następującego zbioru przesłanek:

A1. Jeśli suma cyfr pewnej liczby całkowitej x jest podzielna przez 3, to liczba x jest podzielna przez 3 lub przez 9.

A2. Jeśli liczba jest podzielna przez 9, to jest też podzielna przez 3.

B1. Jeśli w danym czworokącie dwa leżące naprzeciw siebie boki są równoległe i równe, to ten czworokąt jest równoległobokiem.

B2. W danym czworoboku dwa leżące naprzeciw siebie boki są równe lub są równoległe.

1. Znaleźć wszystkie przesłanki, których wnioskiem jest:

A). p → q

B). p ˅ ~ q

C). ~ (p ˅ q)

D).(p ˅ q) → (p ˄ q).

1. Ustalić jaki związek logiczny zachodzi między zdaniem: „dany czworokąt jest rombem”, „dany czworokąt jest kwadratem” na podstawie przesłanek”

1.      jeżeli dany czworokąt jest rombem, to jego przekątne są prostopadłe.

2.      jeżeli przekątne danego czworokąta nie są prostopadłe, to czworokąt ten nie jest kwadratem.

3.      jeżeli dany czworokąt jest kwadratem, to można go wpisać w okrąg.

4.      nieprawdą jest, że w danym czworokącie przekątne są prostopadłe do siebie lub może być wpisany w okrąg.

5.      Znaleźć wszystkie przesłanki zawierające zmienne p i q dla wniosku

1.      p

2.      ~ p

6.      Stosując zasadę rezolucji, znaleźć wyrażenie wiążące zmienne p i q jako wniosek dla przesłanek:

1.      ~ p ˅ r, ~ r ˄ ~ q, q → p.

2.      ~ p ˅ r, q → ~ r, s → q ˄ r, s ˅ p.

wpis by admin in Metoda założeniowa