Метод резолюций

Содержание:

• Метод резолюций для логики высказываний
• Теорема о полноте метода резолюций в логике высказываний
  • Доказательство
• Практика

Метод доказательства того, что формула является логическим следствием формул $F_1, F_2, …, F_n$ называется методом резолюций.

Отметим, что задача о логическом следствии сводится к задаче о выполнимости. Действительно, формула $G$ есть логическое следствие формул $F_1, F_2, …, F_k$ тогда и только тогда, когда множество формул $ {F_1, F_2, …, F_k, ¬G}$ невыполнимо. Метод резолюций, если говорить более точно, устанавливает невыполнимость. Это первая особенность метода.

Вторая особенность метода состоит в том, что он оперирует не с произвольными формулами, а с дизъюнктами (или элементарными дизъюнкциями).

Литерал - атомарная формула или ее отрицание.

Дизъюнкт - дизъюнкция литералов.

Дизъюнкт может состоять из одного литерала. На дизъюнкт мы иногда будем смотреть, как на множество литералов, т.е. не будем различать дизъюнкты, которые получаются один из другого с помощью коммутативности и ассоциативности дизъюнкции, а также идемпотентности. Последнее означает, например, что дизъюнкты $X \lor \neg Y \lor X$ и $X \lor \neg Y$ равны.

Пустой дизъюнкт($\square$) - дизъюнкт, не содержащий литералов.

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

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

Пусть имеется некоторая формула (построенная по алфавиту, введенному в первой главе). Запишем эту формулу в КНФ (выберем любую из них) и отныне будем работать только с этой новой формулой.

Итак, наша фомула представляет из себя выражение вида $F_1\land F_2 \land F_3 \land …\land F_n$, причем ни одно из выражений $F_i$ конъюнкций не содержит.

Любую конъюнкивно нормальную форму можно привести к конъюнкции некоторого числа дизъюнкторов. Действительно, повторяющиеся литералы и их отрицания можно исключить из всех выражений $F_i$, используя закон идемпотентности $x_i \lor x_i = x_i $ и закон исключенного третьего $x_i \lor \neg x_i = 1$.

Если выведены формулы $x_i \lor F$ и $\neg x_i \lor G$, то формула $F \lor G$ считается выведенной методом резолюций.

Условимся, что выводить какую-либо формулу $G$ из системы дизъюнкторов ${F_1; F_2; …; F_n}$ означает указать такую последовательность дизъюнкторов ${G_1; G_2; …; G_m}$, что каждый дизъюнктор $G_j$ либо совпадает с некоторым дизъюнктором $F_i$ из исходной системы ${F_i}, 1 \le i \le n$, либо получен из предыдующих дизъюнкторов этой самой последовательности методом резолюций. Таким образом, под выведенной фомулой $G$ будет подразумеваться самый последний элемент $G_m$ последовательности ${G_j}, 1 \le j \le m$.

Метод резолюций обозначается следующим образом: $\Large \frac {x \lor F, \neg x \lor G} {F \lor G}$.

Теорема о полноте метода резолюций в логике высказываний

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

Доказательство

• Если множество дизъюнктов непротиворечиво, значит, существует интерпретация, в которой они все истинны. Но тогда истинной является и формула, полученная по правилу резолюций. А тогда не может быть выведен пустой дизъюнкт.

• Доказательство проведём индукцией по количеству различных предметных символов, фигурирующих в записях всех дизъюнктов. Обозначим это количество $n$. Без ограничения общности можно считать, что используемые предметные символы – это $x_1, x_2, …, x_n$.

  • Б.И. $n = 1$, т.е. все дизъюнкты состоят из одного литерала, каждый из которых $x_1$ или $\neg x_1$. Тогда противоречивость означает, что оба таких литерала присутствуют. Из этой пары выводим пустой дизъюнкт.

  • Ш.И. Пусть для противоречивых множеств дизъюнктов с числом предметных символов, меньшим $n$, уже доказано. Рассмотрим противоречивое множество $M$ с $n$ предметными символами. Через $M_+$ обозначим множество тех дизъюнктов из $M$, которые не содержат $\neg x_n$, а через $M_-$– множество тех дизъюнктов из $M$, которые не содержат $x_n$. (Вообще говоря, множество $M_+ \cap M_–$ может быть непустым). Через $\widehat{M}+$ обозначим множество дизъюнктов, получаемых из дизъюнктов множества $M+$ вычёркиванием символа $x_n$, а через $\widehat{𝑀̂}-$ - множество дизъюнктов, получаемых из дизъюнктов множества $M-$ вычёркиванием литерала $\neg x_n$. Покажем, что каждое их этих множеств противоречиво.

    Допустим, что $\widehat{M}+$ непротиворечиво. Значит, существует такая интерпретация $\varphi$ символов $x_1, x_2, …, x{n –1}$, при которой каждый дизъюнкт из $\widehat{M}+$ имеет значение 1. Тогда построим интерпретацию $\varphi^*$ множества $M$ по правилу $\varphi^*(x_i) = \varphi(x_i)$ при $ 1 \leq i \leq n – 1$ и $\varphi^*(x_n) = 0$. Ясно, при интерпретации $\varphi^*$ все дизъюнкты из $M-$ тоже получат значение 1. Поскольку $M = M_+ \cup M_–$, $\varphi^*$ – интерпретация, при которой все формулы из $M$ получают значение 1. Но $M$ противоречиво!

    Аналогично доказывается, что $\widehat{M}_–$ тоже противоречиво.

    По предположению индукции из $\widehat{M}+$ выводится пустой дизъюнкт. Это значит, что из $M+$ по правилу резолюций выводится либо пустой дизъюнкт (и тогда всё доказано), либо $x_n$.

    Аналогично, из $M_-$ выводится либо пустой дизъюнкт (и тогда всё доказано), либо $\neg x_n$. Но тогда во вторых случаях из $M = M_+ \cup M_–$ выводится ${x_n, \neg x_n}$, откуда выводится пустой дизъюнкт.

Практика

Для доказательства того, что формула $G$ является логическим следствием множества формул $F_1, …, F_k$, метод резолюций применяется следующим образом.

Сначала составляется множество формул $T = {F_1, …, F_k, \neg G}$. Затем каждая из этих формул приводится к КНФ и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов $S$. И, наконец, ищется вывод пустого дизъюнкта из $S$. Если пустой дизъюнкт выводим из $S$, то формула $G$ является логическим следствием формул $F_1, …, F_k$. Если из $S$ нельзя вывести $\square$, то $G$ не является логическим следствием формул $F_1, …, F_k$.

Пример. Покажем, что формула $G = Z$ является логическим следствием формул $F_1 = \neg X \lor Y \rightarrow X \land Z, F_2 = \neg Y \rightarrow Z$. Сформируем множество формул $T = {F_1, F_2, \neg G}$. Приведем формулы $F_1$ и $F_2$ к КНФ (формула $\neg G$ сама имеет эту форму). Мы получим, что $F_1$ равносильна $X \land (\neg Y \lor Z)$, $F_2$ равносильна $Y \lor Z$.

Тогда множество дизъюнктов $S​$ равно ${ X, \neg Y \lor Z, Y \lor Z, \neg Z }​$. Из множества $S​$ легко выводится пустой дизъюнкт: $\neg Y \lor Z, \neg Z, \neg Y, Y \lor Z, Y, \square​$. Следовательно, формула $G​$ является логическим следствием формул $F_1​$ и $F_2​$. 􀀀