Теорема о полноте метода резолюций

Множество дизъюнктов в логике высказываний S невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт.

Доказать с помощью метода резолюций, что формула G является логическим следствием множества формул F 1,…, Fk

1. Составляем множество формул T ={ F 1,…, Fk, G }.

2. Каждую из этих формул приводим к КНФ и в полученных формулах зачеркиваются знаки конъюнкции (). Получается множество дизъюнктов S.

3. Имеется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул F 1,…, Fk. Если из S нельзя вывести пустой дизъюнкт, то G не является логическим следствием формул F 1,…, Fk.

Пример: доказать что формула G = Z является логическим следствием формул

F 1= X Y → X Z; F2= Y → Z

1: T ={ F 1, F 2, G }

2: F 1 равносильна X (Y Z)

F 2 равносильна (Y Z)

Тогда множество дизъюнктов S ={ X, Y Z, Y Z, Z }

3: Y Z, Z, Y, Y Z, Y, (из множества S выводим пустой дизъюнкт)

Следовательно формула G является логическим следствием формул F 1 и F 2.

 

Пример: доказать истинность заключения

(A→B) (C→D); (D B → M); M

(A C)

Посылки (в КНФ)

F1=(A→B) (C→D)=(A B) (C D)

F2=(D B→M)=(D B) M=(D B M)

F3=M

Отрицание заключения в КНФ: G=(A C)=A C

Множество дизъюнктов

S={A;C;M;(A B);(C D);(D B M}

Вывод (резольвенты)

D1=A (A B)=B

D2=B (D B M)=(D M)

D3=(D M) (C D)=(C M)

D4=(C M) M=C

D5=C C=

Истинность значения (A C) доказана.