Для установки нажмите кнопочку Установить расширение. И это всё.

Исходный код расширения WIKI 2 регулярно проверяется специалистами Mozilla Foundation, Google и Apple. Вы также можете это сделать в любой момент.

4,5
Келли Слэйтон
Мои поздравления с отличным проектом... что за великолепная идея!
Александр Григорьевский
Я использую WIKI 2 каждый день
и почти забыл как выглядит оригинальная Википедия.
Статистика
На русском, статей
Улучшено за 24 ч.
Добавлено за 24 ч.
Что мы делаем. Каждая страница проходит через несколько сотен совершенствующих техник. Совершенно та же Википедия. Только лучше.
.
Лео
Ньютон
Яркие
Мягкие

Из Википедии — свободной энциклопедии

Пра́вило резолю́ций — это правило вывода, восходящее к методу доказательства теорем через поиск противоречий; используется в логике высказываний и логике первого порядка. Правило резолюций, применяемое последовательно для списка резольвент, позволяет ответить на вопрос, существует ли в исходном множестве логических выражений противоречие. Правило резолюций предложено в 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.
Эта страница в последний раз была отредактирована 31 мая 2020 в 15:00.
Как только страница обновилась в Википедии она обновляется в Вики 2.
Обычно почти сразу, изредка в течении часа.
Основа этой страницы находится в Википедии. Текст доступен по лицензии CC BY-SA 3.0 Unported License. Нетекстовые медиаданные доступны под собственными лицензиями. Wikipedia® — зарегистрированный товарный знак организации Wikimedia Foundation, Inc. WIKI 2 является независимой компанией и не аффилирована с Фондом Викимедиа (Wikimedia Foundation).