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ⁿ. 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)¹ i wszystkie są niepuste² wykonuj następujące reguły zastępowania zbioru

1. [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.

1. [Affirmative-negative rule]

Jeśli l występuje w jakiejś klauzuli, a ¬l nie występuje w zbiorze, usuń wszystkie

klauzule zawierające l.

1. [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;

1. [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}

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

---

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↩