Полезное:
Как сделать разговор полезным и приятным
Как сделать объемную звезду своими руками
Как сделать то, что делать не хочется?
Как сделать погремушку
Как сделать так чтобы женщины сами знакомились с вами
Как сделать идею коммерческой
Как сделать хорошую растяжку ног?
Как сделать наш разум здоровым?
Как сделать, чтобы люди обманывали меньше
Вопрос 4. Как сделать так, чтобы вас уважали и ценили?
Как сделать лучше себе и другим людям
Как сделать свидание интересным?
Категории:
АрхитектураАстрономияБиологияГеографияГеологияИнформатикаИскусствоИсторияКулинарияКультураМаркетингМатематикаМедицинаМенеджментОхрана трудаПравоПроизводствоПсихологияРелигияСоциологияСпортТехникаФизикаФилософияХимияЭкологияЭкономикаЭлектроника
|
Глава 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.
В Содержание.
|