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

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

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

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

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

[править | править код]

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

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

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

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

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

[править | править код]

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

Для доказательства того, что формула является логическим следствием множества формул , метод резолюций применяется следующим образом. Сначала составляется множество формул . Затем каждая из этих формул приводится к КНФ (конъюнкция дизъюнктов) и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов . И, наконец, ищется вывод пустого дизъюнкта из . Если пустой дизъюнкт выводим из , то формула является логическим следствием формул . Если из нельзя вывести #, то не является логическим следствием формул . Такой метод доказательства теорем называется методом резолюций.

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

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

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

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

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

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

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

Итак, докажем, что является логическим следствием и . Сначала составляем множество формул с отрицанием доказываемого высказывания; получаем

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

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

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

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

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

[править | править код]

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

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

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

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

Для каждого рассмотрим конечное подмножество , состоящее из дизъюнктов, не содержащих переменных . По условию леммы найдётся такая оценка переменных (или путь до вершины на уровне обрезаном дереве), что она выполняет все дизъюнты из . Значит, обрезанное дерево бесконечно (то есть содержит бесконечное множество вершин). По лемме Кёнига о бесконечном пути обрезанное дерево содержит бесконечную ветвь. Этой ветви соответствует оценка всех переменных , которая делает истинными все дизъюнкты из . Что и требовалось.

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

[править | править код]

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

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

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

Утверждается, что каждое из множеств дизъюнктов и является противоречивым, то есть не имеет выполняющей все дизъюнкты одновременно оценки. Это верно потому, что из оценки , выполняющей все дизъюнкты множества одновременно, можно построить оценку , одновременно выполняющей все дизъюнкты множества . То, что эта оценка выполняет все опущенные при переходе от к дизъюнкты, очевидно, ибо эти дизъюнкты содержат литерал . Остальные дизъюнкты выполняются по предположению, что оценка выполняет все дизъюнкты множества , а, значит, и все расширенные (путём добавления выброшенного литерала ). Аналогично, из оценки , выполняющей все дизъюнкты множества одновременно, можно построить оценку , одновременно выполняющей все дизъюнкты множества .

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

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

[править | править код]

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

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

называется правилом резолюции в исчислении предикатов, если в предложениях C1 и C2 существуют унифицированные контрарные литералы P1 и P2, то есть , а , причём атомарные формулы P1 и P2 являются унифицируемыми наиболее общим унификатором .

В этом случае резольвентой предложений C1 и C2 является предложение , полученное из предложения применением унификатора .[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.
  • Гуц А. К. Глава 1.3. Метод резолюций // Математическая логика и теория алгоритмов. — Омск: Наследие. Диалог-Сибирь, 2003. — С. 108.
  • Нильсон Н. Дж. Принципы искусственного интеллекта. — М., 1985.
  • Мендельсон Э. Введение в математическую логику. — М., 1984.
  • Рассел С., Норвиг П. Искусственный интеллект: современный подход = Artificial Intelligence: a Modern Approach. — М.: Вильямс, 2006.