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òwskich 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 2n. 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ą niepuste2 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ą.