Метод резолюций в логике высказываний
Обновлено: 22.12.2024
Вообще говоря, в построенном в главе 3 исчислении высказываний (благодаря полноте исчисления) проверка выводимости формулы состоит в проверке того, является ли формула тавтологией или нет. Это можно легко установить по таблицам истинности. Но этот метод не обеспечивает построения вывода формулы.
Как правило, в качестве формулы используют пустую формулу , которая не имеет никакого значения ни в какой интерпретации, и, по определению, является противоречием.
Метод резолюций использует специальную форму формул, которая называется предложением.
Определение. Предложением называется дизъюнкция формул вида или , где – атом (буква).
Любая формула исчисления высказываний может быть преобразована в предложение следующей последовательностью действий:
1. Замена импликации по формуле: (проверьте самостоятельно). В результате в формуле остаются связки: , , .
2. Преобразование выражений с инверсиями по закону двойного отрицания: , законам де Моргана: , . В результате инверсии остаются только перед буквами.
3. Приведение формулы к конъюнктивной нормальной форме с помощью дистрибутивных законов:
,
.
4. Преобразование конъюнктивной нормальной формы во множество предложений: .
Напомню, что связки , используются здесь для удобства записи.
Определение. Множество формул называется невыполнимым, если оно не имеет модели, то есть интерпретации, в которой все формулы истинны.
Без доказательства приведем следующую теорему.
Теорема. Если из формулы получено множество предложений, то формула тождественно ложна тогда и только тогда, когда множество невыполнимо.
До сих пор мы пользовались только одним правилом вывода – Modus ponens. В других исчислениях высказываний имеют место и другие правила вывода.
, называются Резольвируемыми предложениями, а – Резольвентой.
Правило резолюций будем обозначать .
Теорема. Резольвента логически следует из резольвируемых предложений.
Доказательство. В вышеприведенных обозначениях, нам нужно доказать, что – тавтология (по теореме дедукции).
Предположим, что
Полученное противоречие доказывает утверждение теоремы.
Запишем . Каждая формула из множества и формула независимо преобразуются во множество предложений. В этом множестве нужно найти резольвируемые предложения и применить к ним правило резолюций. Резольвенты добавляются во множество предложений до тех пор, пока не будет получено пустое предложение. Возможны два случая:
· Среди множества предложений нет резольвируемых. Вывод: теорема опровергнута, и формула не выводима из множества формул .
Доказательство. Запишем инверсию исходной формулы:
.
Заменим все импликации по соответствующей формуле:
.
Применим закон двойного отрицания и закон де Моргана:
.
Получаем предложения: , , . Резольвируем их:
1. – предложение.
2. – предложение.
3. – предложение.
4. . 1, 2.
2. Методом резолюций доказать теорему
Доказательство. Запишем инверсию исходной формулы:
.
Заменим все импликации по соответствующей формуле:
.
Применим закон двойного отрицания и закон де Моргана:
.
Получаем предложения: , , .
1. – предложение.
2. – предложение.
3. – предложение.
4. . 1, 3.
5. . 2, 4.
Читайте также: