Правило резолюций

Пра́вило резолю́ций — это правило вывода, восходящее к методу доказательства теорем через поиск противоречий; используется в логике высказываний и логике первого порядка. Правило резолюций, применяемое последовательно для списка резольвент, позволяет ответить на вопрос, существует ли в исходном множестве логических выражений противоречие. Правило резолюций предложено в 1930 году в докторской диссертации Жака Эрбрана для доказательства теорем в формальных системах первого порядка. Правило разработано Джоном Аланом Робинсоном в 1965 году.

Алгоритмы доказательства выводимости [math]\displaystyle{ A \vdash B }[/math], построенные на основе этого метода, применяются во многих системах искусственного интеллекта, а также являются фундаментом, на котором построен язык логического программирования «Пролог».

Исчисление высказываний

Пусть [math]\displaystyle{ C_1 }[/math] и [math]\displaystyle{ C_2 }[/math] — два предложения в исчислении высказываний, и пусть [math]\displaystyle{ C_1 = P \lor C'_1 }[/math], а [math]\displaystyle{ C_2 = \lnot P \lor C'_2 }[/math], где [math]\displaystyle{ P }[/math] — пропозициональная переменная, а [math]\displaystyle{ C'_1 }[/math] и [math]\displaystyle{ C'_2 }[/math] — любые предложения (в частности, может быть, пустые или состоящие только из одного литерала).

Правило вывода

[math]\displaystyle{ \frac{C_1, C_2}{C'_1 \lor C'_2} }[/math]

называется правилом резолюций.

Предложения C₁ и C₂ называются резольвируемыми (или родительскими), предложение [math]\displaystyle{ C'_1 \lor C'_2 }[/math] — резольвентой, а формулы [math]\displaystyle{ P }[/math] и [math]\displaystyle{ \lnot P }[/math] — контрарными литералами. В общем в правиле резолюции берутся два выражения и вырабатывается новое выражение, содержащее все литералы двух первоначальных выражений, за исключением двух взаимно обратных литералов.

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

Доказательство теорем сводится к доказательству того, что некоторая формула [math]\displaystyle{ G }[/math] (гипотеза теоремы) является логическим следствием множества формул [math]\displaystyle{ F_1, \dots, F_k }[/math] (допущений). То есть сама теорема может быть сформулирована следующим образом: «если [math]\displaystyle{ F_1, \dots, F_k }[/math] истинны, то истинна и [math]\displaystyle{ G }[/math]».

Для доказательства того, что формула [math]\displaystyle{ G }[/math] является логическим следствием множества формул [math]\displaystyle{ F_1, \dots, F_k }[/math], метод резолюций применяется следующим образом. Сначала составляется множество формул [math]\displaystyle{ \{ F_1, \dots, F_k, \neg G \} }[/math]. Затем каждая из этих формул приводится к КНФ (конъюнкция дизъюнктов) и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов [math]\displaystyle{ S }[/math]. И, наконец, ищется вывод пустого дизъюнкта из [math]\displaystyle{ S }[/math]. Если пустой дизъюнкт выводим из [math]\displaystyle{ S }[/math], то формула [math]\displaystyle{ G }[/math] является логическим следствием формул [math]\displaystyle{ F_1, \dots, F_k }[/math]. Если из [math]\displaystyle{ S }[/math] нельзя вывести #, то [math]\displaystyle{ G }[/math] не является логическим следствием формул [math]\displaystyle{ F_1, \dots, F_k }[/math]. Такой метод доказательства теорем называется методом резолюций.

Рассмотрим пример доказательства методом резолюций. Пусть у нас есть следующие утверждения:

«Яблоко красное и ароматное».

«Если яблоко красное, то яблоко вкусное».

Докажем утверждение «яблоко вкусное». Введём множество формул, описывающих простые высказывания, соответствующие вышеприведённым утверждениям. Пусть

[math]\displaystyle{ X_1 }[/math] — «Яблоко красное»,

[math]\displaystyle{ X_2 }[/math] — «Яблоко ароматное»,

[math]\displaystyle{ X_3 }[/math] — «Яблоко вкусное».

Тогда сами утверждения можно записать в виде сложных формул:

[math]\displaystyle{ X_1 \land X_2 }[/math] — «Яблоко красное и ароматное».

[math]\displaystyle{ X_1 \rightarrow X_3 }[/math] — «Если яблоко красное, то яблоко вкусное».

Тогда утверждение, которое надо доказать, выражается формулой [math]\displaystyle{ X_3 }[/math].

Итак, докажем, что [math]\displaystyle{ X_3 }[/math] является логическим следствием [math]\displaystyle{ (X_1 \land X_2) }[/math] и [math]\displaystyle{ (X_1 \to X_3) }[/math]. Сначала составляем множество формул с отрицанием доказываемого высказывания; получаем

[math]\displaystyle{ \{ (X_1 \land X_2), (X_1 \rightarrow X_3), \neg X_3 \}. }[/math]

Теперь приводим все формулы к конъюнктивной нормальной форме и зачеркиваем конъюнкции. Получаем следующее множество дизъюнктов:

[math]\displaystyle{ \{ X_1, X_2, (\neg X_1 \vee X_3), \neg X_3 \}. }[/math]

Далее ищем вывод пустого дизъюнкта. Применяем к первому и третьему дизъюнктам правило резолюции:

[math]\displaystyle{ \{ X_1, X_2, (\neg X_1 \vee X_3), \neg X_3, X_3 \}. }[/math]

Применяем к четвёртому и пятому дизъюнктам правило резолюции:

[math]\displaystyle{ \{ X_1, X_2, (\neg X_1 \vee X_3), \neg X_3, X_3, \# \}. }[/math]

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

Полнота и компактность метода

Правило резолюции обладает свойством полноты в том смысле, что с помощью него всегда можно вывести из [math]\displaystyle{ S }[/math] пустой дизъюнкт #, если исходное множество дизъюнктов [math]\displaystyle{ S }[/math] является противоречивым.

Отношение выводимости (из-за конечности вывода) является компактным: если [math]\displaystyle{ S \vdash \# }[/math], то существует такое конечное подмножество [math]\displaystyle{ S' \subseteq S }[/math], что [math]\displaystyle{ S'\vdash\# }[/math]. Поэтому предварительно нужно доказать, что отношение невыполнимости является компактным.

Лемма. Если каждое конечное подмножество [math]\displaystyle{ S' \subseteq S }[/math] имеет выполняющую оценку, то имеется выполняющая оценка для всего множества дизъюнктов [math]\displaystyle{ S }[/math].

Доказательство. Предположим, что в [math]\displaystyle{ S }[/math] встречаются дизъюнкты, использующие счетное множество пропозициональных переменных [math]\displaystyle{ p_1, \ldots, p_k, \ldots }[/math]. Построим бесконечное двоичное дерево, где из каждой вершины на высоте [math]\displaystyle{ k }[/math] выходят два ребра, помеченное литералами [math]\displaystyle{ \neg p_{k+1} }[/math] и [math]\displaystyle{ p_{k+1} }[/math] соответственно. Удалим из этого дерева те вершины, литералы по пути в которые образуют оценку, противоречащую хотя бы одному дизъюнкту [math]\displaystyle{ S }[/math].

Для каждого [math]\displaystyle{ k }[/math] рассмотрим конечное подмножество [math]\displaystyle{ S_k \subseteq S }[/math], состоящее из дизъюнктов, не содержащих переменных [math]\displaystyle{ p_{k+1}, p_{k+2}, \ldots }[/math]. По условию леммы найдётся такая оценка переменных [math]\displaystyle{ p_1, \ldots, p_k }[/math] (или путь до вершины на уровне [math]\displaystyle{ k + 1 }[/math] обрезаном дереве), что она выполняет все дизъюнты из [math]\displaystyle{ S_k }[/math]. Значит, обрезанное дерево бесконечно (то есть содержит бесконечное множество вершин). По лемме Кёнига о бесконечном пути обрезанное дерево содержит бесконечную ветвь. Этой ветви соответствует оценка всех переменных [math]\displaystyle{ p_1, \ldots, p_k, \ldots }[/math], которая делает истинными все дизъюнкты из [math]\displaystyle{ S }[/math]. Что и требовалось.

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

Теорема. Множество дизъюнктов S противоречиво тогда и только тогда, когда существует опровержение в S (или из S).

Доказательство. Необходимость (корректность метода резолюций) очевидна, так как пустой дизъюнкт не может быть истинен ни при какой оценке. Приведём доказательство достаточности. По лемме о компактности достаточно ограничиться случаем конечного числа пропозициональных переменных. Проводим индукцию по числу пропозициональных переменных [math]\displaystyle{ n }[/math], встречающихся хотя бы в одном дизъюнкте из [math]\displaystyle{ S }[/math]. Пусть теорема полноты верна при [math]\displaystyle{ n = k }[/math], докажем её истинность при [math]\displaystyle{ n = k + 1 }[/math]. Другими словами, покажем, что из любого противоречивого множества [math]\displaystyle{ S }[/math] дизъюнктов, в котором встречаются пропозициональные переменные [math]\displaystyle{ p_1, \ldots, p_{k+1} }[/math], можно вывести пустой дизъюнкт.

Выберем любую из [math]\displaystyle{ k + 1 }[/math] пропозициональных переменных, например, [math]\displaystyle{ p_{k+1} }[/math]. Построим по [math]\displaystyle{ S }[/math] два множества дизъюнктов [math]\displaystyle{ S^+_{k+1} }[/math] и [math]\displaystyle{ S^-_{k+1} }[/math]. В множество [math]\displaystyle{ S^+_{k+1} }[/math] поместим те дизъюнкты из [math]\displaystyle{ S }[/math], в которых не встречается литерал [math]\displaystyle{ \neg p_{k+1} }[/math], причем из каждого такого дизъюнкта удалим литерал [math]\displaystyle{ p_{k+1} }[/math] (если он там встречается). Аналогично, множество [math]\displaystyle{ S^-_{k+1} }[/math] содержит остатки дизъюнктов [math]\displaystyle{ S }[/math], в которых не встречается литерал [math]\displaystyle{ p_{k+1} }[/math], после удаления литерала [math]\displaystyle{ \neg p_{k+1} }[/math] (если он в них встречается).

Утверждается, что каждое из множеств дизъюнктов [math]\displaystyle{ S^+_{k+1} }[/math] и [math]\displaystyle{ S^-_{k+1} }[/math] является противоречивым, то есть не имеет выполняющей все дизъюнкты одновременно оценки. Это верно потому, что из оценки [math]\displaystyle{ \rho^+ }[/math], выполняющей все дизъюнкты множества [math]\displaystyle{ S^+_{k+1} }[/math] одновременно, можно построить оценку [math]\displaystyle{ \rho^+ \cup [\rho(p_{k+1}) = 0] }[/math], одновременно выполняющей все дизъюнкты множества [math]\displaystyle{ S }[/math]. То, что эта оценка выполняет все опущенные при переходе от [math]\displaystyle{ S }[/math] к [math]\displaystyle{ S^+_{k+1} }[/math] дизъюнкты, очевидно, ибо эти дизъюнкты содержат литерал [math]\displaystyle{ \neg p_{k+1} }[/math]. Остальные дизъюнкты [math]\displaystyle{ S }[/math] выполняются по предположению, что оценка [math]\displaystyle{ \rho^+ }[/math] выполняет все дизъюнкты множества [math]\displaystyle{ S^+_{k+1} }[/math], а, значит, и все расширенные (путём добавления выброшенного литерала [math]\displaystyle{ p_{k+1} }[/math]). Аналогично, из оценки [math]\displaystyle{ \rho^- }[/math], выполняющей все дизъюнкты множества [math]\displaystyle{ S^-_{k+1} }[/math] одновременно, можно построить оценку [math]\displaystyle{ \rho^- \cup [\rho(p_{k+1}) = 1] }[/math], одновременно выполняющей все дизъюнкты множества [math]\displaystyle{ S }[/math].

По предположению индукции из противоречивых множеств дизъюнктов [math]\displaystyle{ S^+_{k+1} }[/math] и [math]\displaystyle{ S^-_{k+1} }[/math] (так как в каждом из них встречаются только [math]\displaystyle{ k }[/math] пропозициональных переменных [math]\displaystyle{ p_1, \ldots, p_k }[/math]) имеются выводы пустого дизъюнкта. Если мы восстановим опущенный литерал [math]\displaystyle{ p_{k+1} }[/math] для дизъюнктов множества [math]\displaystyle{ S^+_{k+1} }[/math] в каждом вхождении вывода пустого дизъюнкта, то получим вывод дизъюнкта, состоящего из одного литерала [math]\displaystyle{ p_{k+1} }[/math]. Аналогично из вывода пустого дизъюнкта из противоречивого множества [math]\displaystyle{ S^-_{k+1} }[/math] получаем вывод дизъюнкта, состоящего из одного литерала [math]\displaystyle{ \neg p_{k+1} }[/math]. Осталось один раз применить правило резолюции, чтобы получить пустой дизъюнкт. Что и требовалось доказать.

Исчисление предикатов

Пусть C₁ и C₂ — два предложения в исчислении предикатов.

Правило вывода

[math]\displaystyle{ \frac{C_1, C_2}{(C'_1 \lor C'_2)\sigma}R }[/math]

называется правилом резолюции в исчислении предикатов, если в предложениях C₁ и C₂ существуют унифицированные контрарные литералы P₁ и P₂, то есть [math]\displaystyle{ C_1 = P_1 \lor C'_1 }[/math], а [math]\displaystyle{ C_2 = \lnot P_2 \lor C'_2 }[/math], причём атомарные формулы P₁ и P₂ являются унифицируемыми наиболее общим унификатором [math]\displaystyle{ \sigma }[/math].

В этом случае резольвентой предложений C₁ и C₂ является предложение [math]\displaystyle{ (C'_1 \lor C'_2)\sigma }[/math], полученное из предложения [math]\displaystyle{ C'_1 \lor C'_2 }[/math] применением унификатора [math]\displaystyle{ \sigma }[/math].

Однако вследствие неразрешимости логики предикатов первого порядка для выполнимого (непротиворечивого) множества дизъюнктов процедура, основанная на принципе резолюции, может работать бесконечно долго. Обычно резолюция применяется в логическом программировании в совокупности с прямым или обратным методом рассуждения. Прямой метод (от посылок) из посылок А, В выводит заключение В (правило modus ponens). Основной недостаток прямого метода рассуждения состоит в его ненаправленности: повторные применения метода обычно приводят к резкому росту промежуточных заключений, не связанных с целевым заключением.

Обратный метод (от цели) является направленным: из желаемого заключения В и тех же посылок он выводит новое подцелевое заключение А. Каждый шаг вывода в этом случае всегда связан с первоначально поставленной целью.

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

Литература

• Чень Ч., Ли Р. Глава 5. Метод резолюций // Математическая логика и автоматическое доказательство теорем = Chin-Liang Chang; Richard Char-Tung Lee (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press. — М.: «Наука», 1983. — С. 358.
• Гуц А. К. Глава 1.3. Метод резолюций // Математическая логика и теория алгоритмов. — Омск: Наследие. Диалог-Сибирь, 2003. — С. 108.
• Нильсон Н. Дж. Принципы искусственного интеллекта. — М., 1985.
• Мендельсон Э. Введение в математическую логику. — М., 1984.
• Рассел С., Норвиг П. Искусственный интеллект: современный подход = Artificial Intelligence: a Modern Approach. — М.: Вильямс, 2006.