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

                            Метод линейной резолюции

    Линейным выводом из множества дизъюнктов M назовем
конечную последовательность дизъюнктов D 1 , D 2 , … D i , в которой
D 1 принадлежит M , а каждый последующий дизъюнкт D i (i=2,…,m)
является резольвентой дизъюнкта D i - 1 и одного из дизъюнктов
совокупности S i - 1 =M ∪ {D 2 } ∪ {D 3 } ∪ … ∪ {D i - 2 }. При этом в процессе
вывода каждый очередной дизъюнкт D i именуется центральным
дизъюнктом, а дизъюнкт, выбираемый из совокупности S i - 1 , боковым
дизъюнктом.
    Пример 6. Методом линейной резолюции требуется доказать
противоречивость следующей совокупности дизъюнктов (см. пример
5):
      1) ¬ A ∨ А';    2) ¬ В ∨ В';         3) A ∨ B; 4) ¬ A ∨ ¬ В';
      5) ¬ В ∨ ¬ А'; 6) А' ∨ ¬ В';         7) В' ∨ ¬ А'.
    Реализуемый методом линейной резолюции вывод пустого
дизъюнкта представим следующей схемой:

               ¬ В ∨ ¬ А'          A∨B
               А' ∨ ¬ В'           A ∨ ¬ А'
               ¬ A ∨ ¬ В'          А' ∨ ¬ В'
               В' ∨ ¬ В            ¬ В'
               A∨B                 ¬В
               А' ∨ ¬ A            A
               ¬ А' ∨ B            А'
               ¬В                  B


   Теорема о полноте принципа линейной резолюции. Если конечная
совокупность дизъюнктов противоречива, то данный факт может
быть доказан методом линейной резолюции.
   Отметим, что если в методе линейной резолюции боковой
дизъюнкт брать только из исходного множества M, то, существенно
упрощаясь, он теряет свойство полноты. Перебором вариантов
можно      показать,   что таким    образом   нельзя    доказать
противоречивость совокупности дизъюнктов {Р ∨ Q, ¬ Р ∨ Q, Р ∨ ¬ Q,
¬ Р ∨ ¬ Q} (см. пример 3).
   Верхняя оценка временной вычислительной сложности алгоритма
проверки непротиворечивости КНФ, основанного на принципе
линейной резолюции, остается экспоненциальной, что связано с
полнотой данного принципа и NP - полнотой задачи выполнимости
КНФ.




13