Метод резолюций в исчислении высказываний
Метод резолюций – это метод, позволяющий автоматически доказывать теоремы.
Метод резолюций лежит в основе логического программирования. По сути, он представляет собой алгоритм, который проверяет отношение выводимости. Абсолютно универсального алгоритма автоматического доказательства теорем не разработано, но известны подобные алгоритмы для таких имеющих несложную структуру формальных теорий как:
- исчисление высказываний,
- исчисление предикатов.
Если говорить об исчислении высказываний, то в нем, благодаря полноте исчисления, для проверки выводимости формулы нужно проверить, является ли эта формула тавтологией. Такую проверку легко провести по таблице истинности, но в таком случае не будет обеспечено построение вывода формулы.
Метод резолюций является классическим алгоритмом, используемым для доказательства теорем. Рассмотрим его применение в исчислении высказываний. Метод дает утвердительный ответ для любой формулы А и любого множества формул Г, если Г├А, и отрицательный ответ, если это неверно.
Теорема о доказательстве от противного.
Если Г, А├F и F – формула, являющаяся тождественно ложной, то Г├А.
Доказательство. Проведем доказательство для частного случая: предположим, что Г – это одна формула. В соответствии с теоремой дедукции, Г, ¬А├F эквивалентно Г →(¬А→F). Учитывая тождественную ложность формулы F, преобразуем правую часть эквивалентности:
Г →(¬А→F) = ¬Г ˅(¬¬А ˅ F)= ¬Г ˅ А ˅ F=¬Г ˅ А – тавтология. Следовательно, Г├А, что и требовалось доказать.
Обычно в качестве формулы F выбирают пустую формулу, не имеющую ни в какой интерпретации никакого значения (является противоречием по определению).
В методе резолюций используется специальная форма формул, называемая предложением.
Под предложением понимают дизъюнкцию формул вида А или ¬А, где А является атомом.
Чтобы получить предложение из любой формулы исчисления высказываний, используется следующая схема преобразований:
- импликации заменяются по формуле А→В = ¬А ˅ В. В результате формула содержит операции ¬ (отрицание), ˅ (дизъюнкция) и ˄ (конъюнкция);
- выражения с инверсией преобразуются по законам де Моргана (¬(А ˅ В)= ¬А ˄¬В; ¬(А ˄ В)= ¬А ˅ ¬В) и закону двойного отрицания ¬¬А=А. В результате сохраняются инверсии, только относящиеся к отдельным атомам;
- формулы приводятся к конъюнктивной нормальной форме при помощи применения дистрибутивных законов (А ˄ (В ˅ С) = (А ˄ В) ˅ (В ˄ С), А ˅ (В ˄ С) = (А ˅ В) ˄ (В ˅ С));
- конъюнктивная нормальная форма преобразуется во множество предложений: из АВ получается А, В.
Множество формул называют невыполнимым, если для него не существует модели (интерпретации), в которой все формулы являются истинными.
Если множество предложений Δ получено из формулы А, то формула А является тождественно ложной в том и только том случае, если множество Δ невыполнимо.
Метод резолюций базируется на применении правила резолюций.
Правило резолюций.
Пусть даны предложения: С1=Р ˅ С1’, С2=¬ Р ˅ С2’, где Р – это пропозициональная буква, С1’ и С2’ – предложения (как вариант, они могут быть пустыми или содержать один атом или его отрицание). Тогда правило резолюций может быть сформулировано следующим образом: С1, С2├ С1’ ˅ С2’, где С1, С2 – резольвируемые предложения, С1’ ˅ С2’ – резольвента.
Резольвента логически следует из резольвируемых предложений.
Правило резолюций используется в алгоритме, устанавливающем выводимость Г├А – опровержении методом резолюций.
Метод резолюций в исчислении предикатов
В методе резолюций используются резольвенты, представляющие собой вершины дерева вывода (каждая из которых соответствует выводимым дизъюнктам).
Под резолютивным выводом Ф из множества дизъюнктов S понимают конечную последовательность Ф1,…Фk дизъюнктов такую, что Фk=Ф и каждый из дизъюнктов Фi или принадлежит S, или представляет собой резольвенту дизъюнктов, предшествующих Фi.
Принцип резолюций является логичным, т.е. резольвента представляет собой логическое следствие из резольвируемых предложений. Метод резолюций является мощным правилом вывода, его частные случаи – многие правила:
- modus ponens,
- транзитивность,
- слияние.
Всякая тавтология может быть выведена с помощью использования одного принципа резолюций. В этом смысле принцип резолюций полон.
Чтобы применить принцип резолюций, в резольвируемых предложениях требуются контрарные литералы. В исчислении высказываний в их роли выступают пропозициональные переменные со своими отрицаниями. Для определения контрарности в случае предикатов требуется определить унифицируемые формулы (формулы, которые имеют совместный частный случай) и общие унификаторы (наборы подстановок).
Метод резолюций – это основа языков логического программирования. Они отличаются от языков процедурного программирования тем, что программа описывает некоторый набор элементов и систему существующих между ними связей и ставит цель, а не указывает, как (с помощью каких шагов) нужно решать задачу. При этом компьютер сам ищет стратегию, позволяющую решить поставленные вопросы.
Основные положения метода резолюций:
- исследуемый мир моделируется с помощью множества аксиом, преобразуемых во множество дизъюнктов S;
- чтобы доказать справедливость некоторой теоремы, берут ее отрицание, преобразуют его в форму дизъюнкта и добавляют к множеству S. Если исходная теорема верна, полученное таким образом множество дизъюнктов будет противоречивым;
- чтобы доказать противоречивость, требуется доказать, что из этого множества дизъюнктов можно вывести пустой дизъюнкт;
- с технической точки зрения, метод резолюций представляет собой унификации и получение множества резольвент до тех пор, пока не удастся получить пустую резольвенту;
- стратегия вывода влияет (притом существенно) на число резольвент (соответственно, и эффективность вывода);
- для противоречивого множества дизъюнктов S нахождение пустого дизъюнкта осуществляется за конечное число шагов. Если же множество дизъюнктов непротиворечиво, установление факта его непротиворечивости может быть бесконечно.
