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ą.