Теорема о полноте метода резолюций
Множество дизъюнктов в логике высказываний S невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт. Доказать с помощью метода резолюций, что формула G является логическим следствием множества формул F 1,…, Fk 1. Составляем множество формул T ={ F 1,…, Fk, G }. 2. Каждую из этих формул приводим к КНФ и в полученных формулах зачеркиваются знаки конъюнкции ( 3. Имеется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул F 1,…, Fk. Если из S нельзя вывести пустой дизъюнкт, то G не является логическим следствием формул F 1,…, Fk. Пример: доказать что формула G = Z является логическим следствием формул F 1= X 1: T ={ F 1, F 2, G } 2: F 1 равносильна X F 2 равносильна (Y Тогда множество дизъюнктов S ={ X, Y 3: Y Следовательно формула G является логическим следствием формул F 1 и F 2.
Пример: доказать истинность заключения (A→B) (A Посылки (в КНФ) F1=(A→B) F2=(D F3=M Отрицание заключения в КНФ: G=(A Множество дизъюнктов S={A;C;M;(A Вывод (резольвенты) D1=A D2=B D3=(D D4=(C D5=C Истинность значения (A
|
). Получается множество дизъюнктов S.
Y → X 
(из множества S выводим пустой дизъюнкт)
