Глава 4. Метод резолюций в логике высказываний.


 

Метод резолюций – это метод автоматического доказательства теорем – основы логического программирования. Это алгоритм, проверяющий отношение выводимости . В общем случае алгоритм автоматического доказательства теорем не существует, но для формальных теорий с несложной структурой (таких как исчисление высказываний, исчисление предикатов с одним одноместным предикатом) подобные алгоритмы известны.

Вообще говоря, в построенном в главе 3 исчислении высказываний (благодаря полноте исчисления) проверка выводимости формулы состоит в проверке того, является ли формула тавтологией или нет. Это можно легко установить по таблицам истинности. Но этот метод не обеспечивает построения вывода формулы.

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

 

Теорема о доказательстве от противного. Если , , где – тождественно ложная формула, то .

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

– тавтология Û , что и требовалось доказать.

 

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

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

 

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

 

Любая формула исчисления высказываний может быть преобразована в предложение следующей последовательностью действий:

1. Замена импликации по формуле: (проверьте самостоятельно). В результате в формуле остаются связки: , , .

2. Преобразование выражений с инверсиями по закону двойного отрицания: , законам де Моргана: , . В результате инверсии остаются только перед буквами.

3. Приведение формулы к конъюнктивной нормальной форме с помощью дистрибутивных законов:

,

.

4. Преобразование конъюнктивной нормальной формы во множество предложений: .

 

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

 

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

 

Без доказательства приведем следующую теорему.

 

Теорема.Если из формулы получено множество предложений, то формула тождественно ложна тогда и только тогда, когда множество невыполнимо.

 

До сих пор мы пользовались только одним правилом вывода – Modus ponens. В других исчислениях высказываний имеют место и другие правила вывода.

 

Правило резолюций. Даны предложения: , , где – пропозициональная буква, и – предложения (в частности, пустые или содержащие только одну букву или ее отрицание). Правило резолюций формулируется так: , .

, называются резольвируемыми предложениями, а резольвентой.

Правило резолюций будем обозначать .

 

Теорема.Резольвента логически следует из резольвируемых предложений.

Доказательство.В вышеприведенных обозначениях, нам нужно доказать, что – тавтология (по теореме дедукции).

Предположим, что

Полученное противоречие доказывает утверждение теоремы.

 

Правило резолюций применяется в опровержении методом резолюций – алгоритме, устанавливающем выводимость .

Запишем . Каждая формула из множества и формула независимо преобразуются во множество предложений. В этом множестве нужно найти резольвируемые предложения и применить к ним правило резолюций. Резольвенты добавляются во множество предложений до тех пор, пока не будет получено пустое предложение. Возможны два случая:

· Среди множества предложений нет резольвируемых. Вывод: теорема опровергнута, и формула не выводима из множества формул .

· Получено пустое предложение. Теорема доказана. Имеет место выводимость .

 

Примеры.1.Методом резолюций доказать теорему ├ .

Доказательство.Запишем инверсию исходной формулы:

.

Заменим все импликации по соответствующей формуле:

.

Применим закон двойного отрицания и закон де Моргана:

.

Получаем предложения: , , . Резольвируем их:

1. – предложение.

2. – предложение.

3. – предложение.

4. . 1, 2.

 

2. Методом резолюций доказать теорему

.

Доказательство.Запишем инверсию исходной формулы:

.

Заменим все импликации по соответствующей формуле:

.

Применим закон двойного отрицания и закон де Моргана:

.

Получаем предложения: , , .

1. – предложение.

2. – предложение.

3. – предложение.

4. . 1, 3.

5. . 2, 4.

 

В Содержание.

 

Задачи.

Методом резолюций доказать теоремы:

1) ├ .

2) ├ .

3) ├ .

4) ├ .

5) ├ .

6) ├ .

7) ├ .

8) ├ .

9) ├ .

10) ├ .

11) ├ .

12) ├ .

13) ├ .

14) ├ .

15) ├ .

 

В Содержание.

 



Дата добавления: 2022-02-05; просмотров: 336;


Поиск по сайту:

Воспользовавшись поиском можно найти нужную информацию на сайте.

Поделитесь с друзьями:

Считаете данную информацию полезной, тогда расскажите друзьям в соц. сетях.
Poznayka.org - Познайка.Орг - 2016-2024 год. Материал предоставляется для ознакомительных и учебных целей.
Генерация страницы за: 0.017 сек.