Русская Википедия:Правило резолюций

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

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

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

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

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

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

<math>\frac{C_1, C_2}{C'_1 \lor C'_2}</math>

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

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

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

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

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

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

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

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

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

<math>X_1</math> — «Яблоко красное»,

<math>X_2</math> — «Яблоко ароматное»,

<math>X_3</math> — «Яблоко вкусное».

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

<math>X_1 \land X_2</math> — «Яблоко красное и ароматное».

<math>X_1 \rightarrow X_3</math> — «Если яблоко красное, то яблоко вкусное».

Тогда утверждение, которое надо доказать, выражается формулой <math>X_3</math>.

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

<math>\{ (X_1 \land X_2), (X_1 \rightarrow X_3), \neg X_3 \}.</math>

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

<math>\{ X_1, X_2, (\neg X_1 \vee X_3), \neg X_3 \}.</math>

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

<math>\{ X_1, X_2, (\neg X_1 \vee X_3), \neg X_3, X_3 \}.</math>

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

<math>\{ X_1, X_2, (\neg X_1 \vee X_3), \neg X_3, X_3, \# \}.</math>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

<math>\frac{C_1, C_2}{(C'_1 \lor C'_2)\sigma}R</math>

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

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

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

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

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

Литература

• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга