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

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

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

Пусть ${\displaystyle C_{1}}$ и ${\displaystyle C_{2}}$ — два предложения в исчислении высказываний , и пусть ${\displaystyle C_{1}=P\lor C'_{1}}$ , а ${\displaystyle C_{2}=\lnot P\lor C'_{2}}$ , где ${\displaystyle P}$ — пропозициональная переменная, а ${\displaystyle C'_{1}}$ и ${\displaystyle C'_{2}}$ — любые предложения (в частности, может быть, пустые или состоящие только из одного литерала).

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

${\displaystyle {\frac {C_{1},C_{2}}{C'_{1}\lor C'_{2}}}}$

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

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

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

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

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

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

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

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

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

${\displaystyle X_{1}}$ — «Яблоко красное»,

${\displaystyle X_{2}}$ — «Яблоко ароматное»,

${\displaystyle X_{3}}$ — «Яблоко вкусное».

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

${\displaystyle X_{1}\land X_{2}}$ — «Яблоко красное и ароматное».

${\displaystyle X_{1}\rightarrow X_{3}}$ — «Если яблоко красное, то яблоко вкусное».

Тогда утверждение, которое надо доказать, выражается формулой ${\displaystyle X_{3}}$ .

Итак, докажем, что ${\displaystyle X_{3}}$ является логическим следствием ${\displaystyle (X_{1}\land X_{2})}$ и ${\displaystyle (X_{1}\to X_{3})}$ . Сначала составляем множество формул с отрицанием доказываемого высказывания; получаем

${\displaystyle \{(X_{1}\land X_{2}),(X_{1}\rightarrow X_{3}),\neg X_{3}\}.}$

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

${\displaystyle \{X_{1},X_{2},(\neg X_{1}\vee X_{3}),\neg X_{3}\}.}$

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

${\displaystyle \{X_{1},X_{2},(\neg X_{1}\vee X_{3}),\neg X_{3},X_{3}\}.}$

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

${\displaystyle \{X_{1},X_{2},(\neg X_{1}\vee X_{3}),\neg X_{3},X_{3},\#\}.}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle {\frac {C_{1},C_{2}}{(C'_{1}\lor C'_{2})\sigma }}R}$

называется правилом резолюции в исчислении предикатов, если в предложениях C ₁ и C ₂ существуют унифицированные контрарные литералы P ₁ и P ₂ , то есть ${\displaystyle C_{1}=P_{1}\lor C'_{1}}$ , а ${\displaystyle C_{2}=\lnot P_{2}\lor C'_{2}}$ , причём атомарные формулы P ₁ и P ₂ являются унифицируемыми наиболее общим унификатором ${\displaystyle \sigma }$ .

В этом случае резольвентой предложений C ₁ и C ₂ является предложение ${\displaystyle (C'_{1}\lor C'_{2})\sigma }$ , полученное из предложения ${\displaystyle C'_{1}\lor C'_{2}}$ применением унификатора ${\displaystyle \sigma }$ .

Однако вследствие неразрешимости логики предикатов первого порядка для выполнимого (непротиворечивого) множества дизъюнктов процедура, основанная на принципе резолюции, может работать бесконечно долго. Обычно резолюция применяется в логическом программировании в совокупности с прямым или обратным методом рассуждения. Прямой метод (от посылок) из посылок А, В выводит заключение В (правило 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.