WikiSort.ru - Не сортированное

ПОИСК ПО САЙТУ | о проекте

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

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

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

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

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

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

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

Предложения C₁ и C₂ называются резольвируемыми (или родительскими), предложение $C'_{1}\lor 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}$ . Осталось один раз применить правило резолюции, чтобы получить пустой дизъюнкт. Что и требовалось доказать.

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

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

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

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

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

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

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

Ссылки

↑ Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 77
↑ Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 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.

Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".

Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.

Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .

Текст в блоке "Читать" взят с сайта "Википедия" и доступен по лицензии Creative Commons Attribution-ShareAlike; в отдельных случаях могут действовать дополнительные условия.

Другой контент может иметь иную лицензию. Перед использованием материалов сайта WikiSort.ru внимательно изучите правила лицензирования конкретных элементов наполнения сайта.

2019-2024
WikiSort.ru - проект по пересортировке и дополнению контента Википедии

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

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