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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

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

Исчисление высказываний[править | править исходный текст]

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

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

\frac{C_1, C_2}{C'_1 \or C'_2} R

называется правилом вывода.[1]

Предложения C1 и C2 называются резольвируемыми (или родительскими), предложение C'_1 \or C'_2 — резольвентой, а формулы P и \lnot P — контрарными литералами. В общем в правиле резолюции берутся два выражения и вырабатывается новое выражение, содержащее все литералы двух первоначальных выражений, за исключением двух взаимно обратных литералов.

Метод резолюции[править | править исходный текст]

Доказательство теорем сводится к доказательству того, что некоторая формула ~G (гипотеза теоремы) является логическим следствием множества формул ~F_1,...,F_k (допущений). То есть сама теорема может быть сформулирована следующим образом: «если ~F_1,...,F_k истинны, то истинна и ~G».

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

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

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

X1 — «Яблоко красное»,
X2 — «Яблоко ароматное»,
X3 — «Яблоко вкусное».

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

X1 \And X2  — «Яблоко красное и ароматное.»
X1 \rightarrow X3 — «Если яблоко красное, то яблоко вкусное.»

Тогда утверждение, которое надо доказать, выражается формулой X3.
Итак, докажем, что X3 является логическим следствием (X1 \And X2) и (X1 \rightarrow X3). Сначала составляем множество формул с отрицанием доказываемого высказывания; получаем:
\mathcal {f} (X1 \And X2), (X1 \rightarrow X3), \neg X3 \mathcal {g}.
Теперь приводим все формулы к конъюнктивной нормальной форме и зачеркиваем конъюнкции. Получаем следующее множество дизъюнктов:
\mathcal {f} X1, X2, (\neg X1 \vee X3), \neg X3 \mathcal {g}.
Далее ищем вывод пустого дизъюнкта.
Применяем к первому и третьему дизъюнктам правило резолюции:
\mathcal {f} X1, X2, (\neg X1 \vee X3), \neg X3, X3 \mathcal {g}.
Применяем к четвёртому и пятому дизъюнктам правило резолюции:
\mathcal {f} X1, X2, (\neg X1 \vee X3), \neg X3, X3, \# \mathcal {g}.
Таким образом пустой дизъюнкт выведен, следовательно выражение с отрицанием высказывания опровергнуто, следовательно само высказывание доказано.

Полнота и компактность метода[править | править исходный текст]

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

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

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

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

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

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

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

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

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

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

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

Исчисление предикатов[править | править исходный текст]

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

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

\frac{C_1, C_2}{(C'_1 \or C'_2)\sigma}R

называется правилом резолюции в исчислении предикатов, если в предложениях C1 и C2 существуют унифицированные контрарные литералы P1 и P2, то есть C_1 = P_1 \or C'_1, а C_2 = \lnot P_2 \lor C'_2, причём атомарные формулы P1 и P2 являются унифицируемыми наиболее общим унификатором \sigma.

В этом случае резольвентой предложений C1 и C2 является предложение (C'_1 \or C'_2)\sigma, полученное из предложения C'_1 \or C'_2 применением унификатора \sigma.[2]

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

Ссылки[править | править исходный текст]

  1. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 77
  2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 85

Литература[править | править исходный текст]

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