Formalna weryfikacja wyrażeń logicznych
Jednym z zagadnie« badanych w ramach informatyki teoretycznej jest automatyzacja
procedury dowodzenia. W teorii rachunku zda« sprowadza się to do problemu rozwaŜenia czy
dane zdanie p jest tautologią, czyli takim zdaniem, które niezaleŜnie od wartości logicznych
występujących w nim zdań prostych, przyjmuje zawsze wartość logiczną TRUE. Jest to
problem rozstrzygalny, gdyŜ jednym z najprostszych sposobów sprawdzenia jest
wygenerowanie wszystkich moŜliwych bool`owskich wartościowa« dla skończonej ilości
zdań prostych, występujących w p (niech ich będzie n). PoniewaŜ dowolne zdanie proste
moŜe przyjąć tylko jedną z dwóch wartości (TRUE lub FALSE), wnioskujemy, iŜ wszystkich
moŜliwych wartościowań będzie 2
n
. Zatem widzimy, Ŝe problem tautologii ma złoŜoność
wykładniczą, a poniewaŜ problem P = NP wciąŜ naleŜy do nierozwiązanych, nie ma
algorytmu o mniejszej złoŜoności. Sprawdzanie jednak wszystkich wartościowań jest
podejściem "naiwnym" i niewątpliwie bardzo czasochłonnym, szczególnie dla duŜych n.
W tym celu powstało wiele algorytmów działających znacznie szybciej. Innym podejściem do
dowodzenia tautologii jest aksjomatyczny system Hilberta, który opiera się na kilku
aksjomatach i regule "modus ponens", która okazała się niezwykle trudna do realizacji
automatycznej. Dzieje się to dlatego, iŜ w regule tej naleŜy wybrać podcel. Wybór ten
niejednokrotnie przesądza o sukcesie wyprowadzenia dowodu, zatem jego trafność zaleŜy
głównie od inteligencji człowieka. Istnieją jednak systemy, które w procesie dowodzenia
wykorzystują rachunek sekwencyjny. Operuje on na wyraŜeniach nazywanych sekwentami
i okazuje się, Ŝe rachunek tych sekwentów pozwala nam dowodzić tautologii. Jednym z takich
algorytmów jest algorytm Algorytm Davisa-Putnama.
Algorytm Davisa-Putnama
Formuła x języka logiki zdań wynika ze zbioru formuł X wtedy i tylko wtedy, gdy zbiór
X lub {!x} jest niespełnialny.
Algorytm Davisa-Putnama:
wejście: zbiór S klauzul rachunku zdań.
1. Usuń wszystkie tautologie z S.
2. Dopóki wszystkie zbiory nie są explicite sprzeczne (tzn. zawierają literał l i ¬l)
1
i
wszystkie są niepuste
2
wykonuj następujące reguły zastępowania zbioru
a) [One-literal clause rule]
Jeśli występuje klauzula 1-literałowa l, usuń wszystkie klauzule zawierające l z l
włącznie oraz wszystkie wystąpienia ¬l.
b) [Affirmative-negative rule]
Jeśli l występuje w jakiejś klauzuli, a ¬l nie występuje w zbiorze, usuń wszystkie
klauzule zawierające l.
c) [Splitting rule]
Jeśli reguła (a) ani (b) nie jest stosowalna, wybierz literał l taki, Ŝe l i ¬l występują
w zbiorze klauzul i zastąp ten zbiór dwoma zbiorami:
(i) zbiór klauzul z usuniętymi wszystkimi klauzulami zawierającymi l i usuniętymi
wszystkimi wystąpieniami ¬l;
(ii) zbiór klauzul z usuniętymi wszystkimi klauzulami zawierającymi ¬l i usuniętymi
wszystkimi wystąpieniami l;
d) [Subsumption rule]
Usuń kaŜdą klauzulę A taką, Ŝe w zbiorze występuje podklauzula dla A.
Przykład
S = {p, ¬p q, q s, r s, r ¬s,¬r t,¬r ¬t, p ¬p}
Rozwiązanie
1. S = {p, ¬p q, q s, r s, r ¬s,¬r t,¬r ¬t}
reguła 1
2. S = {q, q s, r s, r ¬s,¬r t,¬r ¬t}
reguła 2a
3. S = {r s, r ¬s,¬r t,¬r ¬t}
1
Jeśli wszystkie zbiory są sprzeczne, to S jest niespełnialny
2
Jeśli zostanie wyprowadzony pusty zbiór klauzul, to zbiór S jest spełnialny
reguła 2b
4. S1 = {t,¬t}
S2 = {s,¬s}
reguła 2c
5. S1 oraz S2 są sprzeczne, więc S jest niespełnielny.
Przykład - twierdzenie logiczne
Twierdzenie logiczne o św. Franciszku (rozdał majątek ubogim)
Jeśli załoŜyć, ze fakt posiadania ziemi implikuje bogactwo i ze nie moŜna być jednocześnie
świątobliwym i bogatym, to ziemianin nie moŜe być świątobliwy.
Zmienne:
b – bogaty,
% jest bogaty
z – ziemianin,
% posiada ziemię,
s – świątobliwy,
% jest świątobliwy
ZałoŜenia:
zal1 = Implikacja(z,b),
% z -> b – zmienianin -> bogaty
zal2 = Negacja(Koniunkcja(s,b)), % !(s*b) – nie moŜna być jednocześnie
% świątobliwym i bogatym,
Teza:
teza = Implikacja(z,negacja(s)),
% z -> !s - ziemianin nie jest świątobliwy
Twierdzenie:
twierdzenie = implikacja(koniunkcja(zal1,zal2),teza), % z załoŜeń wynika teza
Twierdzenie naleŜy udowodnić lub obalić.
Zadana dedukcyjne
Wiadomo było, ze w pewnym miasteczku mieszkają ludzie:
1) zawsze mówiący prawdę,
2) zawsze mówiący nieprawdę.
Przyjezdny spytał przechodnia - "czy jesteś prawdomówny?".
Ten odparł ze śmiechem - "jeśli jestem prawdomówny, to zjem swój kapelusz."
Przyjezdny po chwili namysłu rzekł - "w takim razie powinieneś zjeść swój kapelusz."
Udowodnij, ze przyjezdny miał racje.
Zdanie elementarne:
a – osoba mówiąca prawdę lub nieprawdę,
k – zje swój kapelusz,
ZałoŜenie:
zalozenie = Alt(Kon(a,Impl(a,k)), Kon(Neg a, Neg(Impl(a,k))));
Wniosek:
teza = Kon(a,k);
Twierdzenie:
Twierdzenie = Impl(zalozenie,teza);
Dowód ?
Negacyjna forma normalna – NNF
W negacyjnej postaci normalnej tylko atomy zostają zanegowane, korzysta się tutaj z praw
logiki – np. . negacja sumy = suma negacji, podwójna negacja itd.
Normalna postać koniunkcyjna - CNF
Koniunkcyjna postać normalna (ang. conjunctive normal form, CNF) danej formuły
logicznej to równowaŜna jej formuła zapisana w postaci koniunkcji klauzul. Jeśli wyraŜenie
rachunku zdań jest zapisane w koniunkcyjnej postaci normalnej, to łatwo (tj. istnieje
wielomianowy algorytm realizujący to zadanie) sprawdzić czy jest tautologią. Jeśli bowiem
istnieje klauzula, która nie zawiera ani stałej prawda ani przynajmniej jednej zmiennej
zarówno pozytywnie, jak i negatywnie, to moŜna tak dobrać zmienne, Ŝeby była ona fałszywa
- kaŜdej zmiennej występującej pozytywnie przyporządkujemy fałsz, kaŜdej zaś występującej
negatywnie prawdę. Wtedy cała CNF nie będzie spełniona, tak więc nie jest on tautologią.