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

      В принятых обозначениях требуется доказать справедливость
следующего заключения:

                 А&В ¬ F.          (4)
   Покажем, что из истинности всех посылок следует истинность
заключения, т.е. что утверждение     (4) является   логическим
следствием утверждений (1) – (3).
   Совокупность посылок представляем в виде формулы

       (А&В → C)&(C&D → ¬ E)&(F → D&E).

    Эта формула эквивалентна следующей КНФ:

      K 1 =( ¬ А ∨ ¬ В ∨ C) & ( ¬ C ∨ ¬ D ∨ ¬ E)&( ¬ F ∨ D) &( ¬ F ∨ E).

    Формулу (4) также представим в виде КНФ:

                  K 2 =( ¬ А ∨ ¬ В ∨ ¬ F).

Согласно теореме 2, формула (4) является логическим следствием
формул (1) – (3) тогда и только тогда, когда формула K 1 & ¬ K 2
противоречива. Имеем

         K 1 & ¬ K 2 =( ¬ А ∨ ¬ В ∨ C) & ( ¬ C ∨ ¬ D ∨ ¬ E)&( ¬ F ∨ D)
                              &( ¬ F ∨ E)&A&B&F=
                        A&B&F&C&( ¬ D ∨ ¬ E)&D&E.

   Противоречивость последней формулы очевидна, ибо три
дизъюнкта, ( ¬ D ∨ ¬ E), D и Е, одновременно не могут быть
истинными. Таким образом, заключение (4) действительно вытекает
из утверждений (1)- (3), является их логическим следствием.
   Далее общезначимые формулы будем обозначать символом         , а
противоречивые – символом . Как очевидно, A ∨ ¬ A=     и A& ¬ A= .
   Как известно, проблема определения по КНФ, является ли она
выполнимой (непротиворечивой), относится к числу NP-полных. В
предположении       Р ≠ NР    полиномиальных       по    временной
вычислительной сложности (числу выполняемых элементарных
операций) алгоритмов решения этой проблемы не существует.
Выполнимость КНФ от n переменных может быть определена путем
последовательного тестирования всех наборов логических значений
этих переменных (общее число наборов равно 2 n ).
   Практика показала, что достаточно часто эффективным средством
определения противоречивости КНФ является принцип резолюции.




9