Основные понятия и методы теории формальных систем. Волохович А.В. - 11 стр.

   Из составляющих КНФ K(P,Q) дизъюнктов в качестве
логического следствия выведен пустой дизъюнкт. Это означает
противоречивость данной КНФ.
   В дизъюнктах D 1 ' ∨ X i и D 2 ' ∨ ¬ X i вхождения переменой X i
именуются контрарными. Так, в дизъюнктах 1) и 2), 3) и 4)
контрарны вхождения буквы P; в дизъюнктах 5) и 6) контрарны
вхождения буквы Q. Пустой дизъюнкт есть резолюция контрарных
литер.
   Пример 4. Известно следующее: прямая L 1 либо параллельна
прямой L 2 , либо совпадает с ней; параллельные прямые не имеют
общих точек; прямые L 1 и L 2 имеют общую точку. Методом
резолюции требуется доказать, что прямые L 1 и L 2 совпадают.
   Исходные предположения на языке ИВ записываются следующим
образом:
                 1) A ∨ B;
                 2) A → ¬ C;
                 3) C.
   Требуется доказать справедливость утверждения B. Утверждение
B является логическим следствием предположений 1),2),3) тогда и
только тогда, когда формула

                        (A ∨ B)&(A → ¬ C)& C & ¬ B
невыполнима.
   Так как формула A → ¬ C эквивалентна ¬ A ∨ ¬ C, нам требуется
показать противоречивость следующей совокупности дизъюнктов:

                 1')   A ∨ B;
                 2')   ¬ A ∨ ¬ C;
                 3')   C;
                 4')   ¬ B.

     Конструируем резольвенты:

                 5') A              (1', 4');
                 6') ¬ C            (5', 2');
                 7')                (3', 6').

   Итак, прямые L 1 и L 2 действительно совпадают.
   Пример 5. Если футбольная команда A выигрывает, то город А'
торжествует; если команда В выигрывает, то торжествует город B'.
Выигрывает либо команда A, либо команда В. Однако, если команда
A выигрывает, то город В' не торжествует; если выигрывает команда




11