Принцип резолюции¶

Принцип резолюции — это метод автоматического доказательства теорем в логике первого порядка, основанный на правиле вывода, которое позволяет получать новые логические следствия из заданных посылок. Принцип был разработан в 1965 году американским математиком и логиком Джоном Аланом Робинсоном и стал основой для многих систем автоматического доказательства теорем, в частности, для языка логического программирования Prolog. Суть принципа заключается в применении правила резолюции к дизъюнктам (логическим формулам определённого вида) для вывода пустого дизъюнкта, что свидетельствует о противоречивости исходного множества посылок.

¶История

Идея автоматизации логического вывода восходит к работам Аристотеля, однако формальные основы были заложены в XIX—XX веках. В 1930-х годах Жак Эрбран предложил метод, позволяющий сводить доказательство к проверке конечного множества формул. В 1960-х годах, с развитием вычислительной техники, возникла потребность в эффективных алгоритмах для доказательства теорем. В 1965 году Джон Алан Робинсон опубликовал статью «A Machine-Oriented Logic Based on the Resolution Principle», в которой впервые формализовал принцип резолюции. Этот метод стал прорывом, так как он заменил громоздкие аксиоматические системы на единое правило вывода, применимое к формулам в конъюнктивной нормальной форме.

¶Основные понятия

¶Дизъюнкт

Дизъюнкт — это дизъюнкция (логическое «ИЛИ») литералов, где литерал — это атомарная формула или её отрицание. Например, выражение P(x) ∨ ¬Q(y) является дизъюнктом. Множество дизъюнктов представляет собой конъюнкцию (логическое «И») всех дизъюнктов, что соответствует исходной задаче.

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

Правило резолюции для логики высказываний формулируется следующим образом: если имеются два дизъюнкта C1 и C2, такие что C1 содержит литерал L, а C2 содержит литерал ¬L, то можно вывести новый дизъюнкт C, который является объединением C1 и C2 без L и ¬L. Этот новый дизъюнкт называется резольвентой. Например, из P ∨ Q и ¬P ∨ R выводится Q ∨ R.

В логике первого порядка правило усложняется необходимостью унификации — подстановки термов вместо переменных, чтобы сделать литералы из разных дизъюнктов противоположными. Например, из P(x) ∨ Q(x) и ¬P(a) ∨ R(y) можно вывести Q(a) ∨ R(y) после подстановки x = a.

¶Унификация

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

¶Алгоритм доказательства

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

1. Формулировка задачи: исходное множество аксиом и отрицание доказываемого утверждения преобразуются в конъюнктивную нормальную форму (КНФ). Каждая формула представляется в виде множества дизъюнктов.
2. Применение правила резолюции: к текущему множеству дизъюнктов многократно применяется правило резолюции. На каждом шаге выбираются два дизъюнкта, содержащие противоположные литералы (после унификации), и выводится новый дизъюнкт.
3. Вывод пустого дизъюнкта: если на каком-то шаге выводится пустой дизъюнкт (обозначается как □ или {}), это означает, что исходное множество дизъюнктов противоречиво. Следовательно, отрицание утверждения не может быть истинным, и исходное утверждение доказано.
4. Завершение: если пустой дизъюнкт не выводится, а новых дизъюнктов больше не появляется, то утверждение не является логическим следствием аксиом.

¶Стратегии поиска

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

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

¶Применение

¶Автоматическое доказательство теорем

Принцип резолюции лёг в основу многих систем автоматического доказательства теорем, таких как Otter, E Prover, Vampire. Эти системы используются в математике, информатике и искусственном интеллекте для проверки логических утверждений.

¶Логическое программирование

Язык Prolog, разработанный в 1970-х годах, использует частный случай принципа резолюции — SLD-резолюцию (Selective Linear Definite clause resolution). Программы на Prolog состоят из фактов и правил, а выполнение программы сводится к доказательству целевого утверждения с помощью резолюции.

¶Проверка моделей

В верификации программ и аппаратного обеспечения принцип резолюции применяется для проверки выполнимости логических формул (SAT-решатели). Современные SAT-решатели, такие как MiniSat и Glucose, используют алгоритмы, основанные на резолюции, для решения задач выполнимости булевых формул.

¶Обработка естественного языка

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

¶Ограничения и критика

Несмотря на свою мощь, принцип резолюции имеет ряд ограничений:

• Экспоненциальная сложность: в худшем случае количество возможных резольвент растёт экспоненциально, что делает метод неприменимым для больших задач без эвристик.
• Необходимость приведения к КНФ: преобразование формул в конъюнктивную нормальную форму может привести к экспоненциальному росту размера задачи.
• Чувствительность к порядку: эффективность доказательства сильно зависит от выбора стратегии и порядка применения правил.
• Неполнота для некоторых логик: для логик высших порядков или неклассических логик принцип резолюции может быть неполным.

¶Интересные факты

• Джон Алан Робинсон за разработку принципа резолюции получил премию Хербранда в 1985 году.
• Принцип резолюции лежит в основе системы автоматического доказательства теорем Otter, которая в 1996 году доказала теорему Роббинса, остававшуюся недоказанной в течение 60 лет.
• В 2010-х годах принцип резолюции был адаптирован для квантовых вычислений, что открыло перспективы для квантового логического вывода.

¶Источники

• Robinson, J. A. (1965). «A Machine-Oriented Logic Based on the Resolution Principle». Journal of the ACM.
• Chang, C. L., & Lee, R. C. T. (1973). «Symbolic Logic and Mechanical Theorem Proving». Academic Press.
• Loveland, D. W. (1978). «Automated Theorem Proving: A Logical Basis». North-Holland.
• Russell, S., & Norvig, P. (2020). «Artificial Intelligence: A Modern Approach» (4th ed.). Pearson.