Weryfikacja układów (twierdzeń) logicznych sprowadza się do weryfikacji tautologii.
Tautologia występuje wówczas, jeśli dla wszystkich możliwych kombinacji wartości wejściowych, na wyjściu dostajemy prawdę (logika boolowska).
Przykład:
Czy prawdziwe jest twierdzenie ?
~(p && q) <=> ~p || ~q
Należy udowodnić, że wyrażenie zawsze jest prawdziwe. Można to zrobić na wiele sposobów, najprostszy polega na sprawdzeniu wszystkich możliwości ustawienia wejść, i badamy stan wyjść.
Dla podanej funkcji pełna analiza wygląda następująco:
| p | q | ~p | ~q | P && q | ~(p && q) | ~p || ~q | |
|---|---|---|---|---|---|---|---|
| 0 | 0 | 1 | 1 | 0 | 1 | 1 | 1 |
| 0 | 1 | 1 | 0 | 0 | 1 | 1 | 1 |
| 1 | 0 | 0 | 1 | 0 | 1 | 1 | 1 |
| 1 | 1 | 0 | 0 | 1 | 0 | 0 | 1 |
Widzimy, że podane wyrażenie jest tautologią, gdyż w kolumnie otrzymaliśmy same jedynki.
Przedstawioną metodę można zasymulować w środowisku Prolog, w oparciu o następujące fakty
i predykaty:
% zakres dopuszczalnych wartości
boolean(true).
boolean(false).
% definicja faktów – elementarnych funkcji logicznych tworzących system pełny
not(true,false).
not(false,true).
and(false,false,false).
and(false,true,false).
and(true,false,false).
and(true,true,true).
or(false,false,false).
or(false,true,true).
or(true,false,true).
or(true,true,true).
% lewa I prawa strona dowodzonego twierdzenia
f_left(X,Y,Z):-and(X,Y,O),not(O,Z).
f_right(X,Y,Z):-not(X,O1),not(Y,O2),or(O1,O2,Z).
% funkcja równoważności – dlaczego tak ?
eq(X,Y,Z):-not(X,O1),not(Y,O2),or(O1,Y,W1),or(O2,X,W2),and(W1,W2,Z).
% reguła badająca tautologię, jakie znaczenie mają podcele: \+X i ! ? Czy można je usunąć bez
% wpływu na wynik badania ?
check(X):-
maplist(boolean,[A,B]),
f_left(A,B,W1),
f_right(A,B,W2),
eq(W1,W2,X),
\+X,!.
check(X):-X=true.
W przypadku bardziej złożonych wyrażeń weryfikacji dokonuje się w postaci symbolicznej, doprowadzając wyrażenia do koniunkcyjnej postaci normalnej (CNF). Formuła w koniunkcyjnej postaci normalnej jest tautologią wtw, gdy każda z alternatyw elementarnych składających się na tę formułę jest tautologią.