Математическая логика и теория алгоритмов. Сергиевская И.М. - 19 стр.

является ли формула тавтологией или нет. Это можно легко установить по таблицам
истинности. Но этот метод не обеспечивает построения вывода формулы.
      Метод резолюций – классический алгоритм автоматического доказательства
теорем. Для простоты изложения рассмотрим его для исчисления высказываний.
Для любого множества формул Γ и любой формулы A метод дает утвердительный
ответ, если Γ ├ A , и дает отрицательный ответ, если неверно, что Γ ├ A .

      Теорема о доказательстве от противного. Если Γ , ¬A ├ F , где F –
тождественно ложная формула, то Γ ├ A .
      Доказательство. Доказательство проведем для частного случая, когда Γ
представляет     собой     одну      формулу.      По      теореме дедукции,
Γ , ¬A ├ F ⇔ Γ → (¬A → F ) – тавтология. Преобразуем правую часть
равносильности, учитывая, что формула F тождественно ложна.
Γ → (¬A → F ) = ¬Γ ∨ (¬¬A ∨ F ) = ¬Γ ∨ A ∨ F = ¬Γ ∨ A =
= Γ → A – тавтология ⇔ Γ ├ A , что и требовалось доказать.

     Как правило, в качестве формулы F используют пустую формулу , которая
не имеет никакого значения ни в какой интерпретации, и, по определению, является
противоречием.
     Метод резолюций использует специальную форму формул, которая
называется предложением.

      Определение. Предложением называется дизъюнкция формул вида A или
¬A , где A – атом (буква).

      Любая формула исчисления высказываний может быть преобразована в
предложение следующей последовательностью действий:
1. Замена импликации по формуле: A → B = ¬A ∨ B (проверьте самостоятельно). В
   результате в формуле остаются связки: ¬ , ∨ , ∧ .
2. Преобразование выражений с инверсиями по закону двойного отрицания:
   ¬¬A = A , законам де Моргана: ¬( A ∨ B ) = ¬A ∧ ¬B , ¬( A ∧ B ) = ¬A ∨ ¬B . В
   результате инверсии остаются только перед буквами.
3. Приведение формулы к конъюнктивной нормальной форме с помощью
   дистрибутивных законов:
    A ∧ (B ∨ C ) = ( A ∧ B ) ∨ ( A ∧ C ) ,
    A ∨ (B ∧ C ) = ( A ∨ B ) ∧ ( A ∨ C ) .
4. Преобразование конъюнктивной нормальной формы во множество предложений:
   AB ⇒ A, B .

     Напомню, что связки ∨ , ∧ используются здесь для удобства записи.

     Определение. Множество формул называется невыполнимым, если оно не
имеет модели, то есть интерпретации, в которой все формулы истинны.



                                       24