Логическое следствие и метод резолюции.

Правило резолюции: Из дизъюнктов ˥ P (t1,..., tn) \/ F и P (s1,..., sn) \/ G выводИм дизъюнкт

(F) \/ (G), где наиболее общий унификатор множества {P (t1,..., tn), P (s1,..., sn)}. Дизъюнкт (F) \/ (G) называется бинарной резольвентой, а литералы ˥ P (t1,..., tn) и P (s1,..., sn) отрезаемыми литералами.

Системы автоматического доказательства используют метод резолюций, впервые описанный Дж. Робинсоном в 1965 году. Метод предусматривает использование следующей последовательности доказательства:

1. Сначала к доказываемой формуле применяется операция отрицания.

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

Если полученная в результате отрицания формула действительно является противоречивой, то исходная формула должна представлять собой тавто-логию (то есть должна быть истинной при любой интерпретации). Процесс, направленный на обнаружение противоречия, состоит из после-довательного применения правила резолюции к дизъюнктам. Метод резолюций – это метод доказательства того, что формула G являет-ся логическим следствием формул F1, F2,..., Fk.

Задача о логическом следствии сводится к задаче о выполнимости: Формула G есть логическое следствие формул F1, F2,..., Fk тогда и только тогда, когда множество формул

{F1, F2,..., Fk, ˥ G} невыполнимо.

Особенности метода резолюций:

1. Метод устанавливает невыполнимость.

2. Метод оперирует не с произвольными формулами, а с дизъюнктами.

Метод резолюций является обобщением метода доказательства от про-тивного. Вместо того чтобы пытаться вывести некоторую формулу-гипотезу из имеющегося непротиворечивого множества аксиом, добавля-ется отрицание формулы к множеству аксиом и делается попытка вывести из полученного множества противоречие. Если удаѐ тся это сделать, то приходят к выводу (пользуясь законом исключенного третьего), что ис-ходная формула выводИма из множества аксиом. Процесс применения правила резолюции продолжается до тех пор, пока не получится пустой дизъюнкт. Возможны, вообще говоря, три случая:

1. Этот процесс никогда не завершается.

2. Среди текущего множества дизъюнктов не окажется таких, к кото-рым можно применить правило резолюции. Это означает, что мно-жество дизъюнктов выполнимо, и значит исходная формула не вы-водИма.

3. На очередном шаге получена пустая резольвента. Это означает, что множество дизъюнктов невыполнимо и, следовательно, начальная формула выводИма.

Имеет место теорема о том, что процесс обязательно завершится за конеч-ное число шагов, если множество дизъюнктов было невыполнимым.