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

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

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

Дизъюнкт и клаузальная форма

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

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

Основное правило вывода метода резолюций формулируется следующим образом: если имеются два дизъюнкта, содержащих противоположные литералы (один — литерал L, другой — его отрицание ¬L), то из них можно вывести новый дизъюнкт, который является дизъюнкцией всех литералов исходных дизъюнктов, за исключением пары противоположных. Формально:

• Из дизъюнкта A ∨ L и дизъюнкта B ∨ ¬L выводится резольвента A ∨ B.

Здесь A и B — произвольные дизъюнкции литералов (возможно, пустые). Если после удаления пары L и ¬L не остаётся литералов, то резольвента считается пустым дизъюнктом, обозначаемым символом □ (или ⊥). Пустой дизъюнкт означает противоречие (ложь).

Унификация

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

Алгоритм метода резолюций

Метод резолюций используется для доказательства того, что данная формула G является логическим следствием множества формул F1, F2, ..., Fn. Алгоритм состоит из следующих шагов:

1. Формирование множества посылок и отрицания цели. Все посылки Fi и отрицание доказываемой формулы ¬G приводятся к клаузальной форме. Полученное множество дизъюнктов S считается исходным.
2. Применение правила резолюции. К дизъюнктам из S многократно применяется правило резолюции (с учётом унификации). Каждая полученная резольвента добавляется в множество S.
3. Проверка на пустой дизъюнкт. Если на каком-то шаге получен пустой дизъюнкт □, это означает, что множество S противоречиво, а следовательно, исходное предположение ¬G ложно, и формула G является логическим следствием посылок. Если пустой дизъюнкт не получен, а новых резольвент больше не появляется (процесс зацикливается), то G не является следствием.

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

Стратегии поиска резольвент

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

• Линейная резолюция. Каждая новая резольвента строится на основе предыдущей и одного из исходных дизъюнктов. Это напоминает цепочку рассуждений.
• Стратегия насыщения (level-saturation). Сначала генерируются все возможные резольвенты из исходных дизъюнктов (первый уровень), затем из них и исходных (второй уровень) и так далее.
• Стратегия опорного множества. Выбирается подмножество дизъюнктов (обычно включающее отрицание цели), и резолюция применяется только если хотя бы один из исходных дизъюнктов принадлежит этому подмножеству.
• Стратегия поглощения. Если новый дизъюнкт содержит в себе литералы уже существующего (то есть является его подмножеством), то он отбрасывается как избыточный.

Применение

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

Метод резолюций лежит в основе языка Пролог, где он реализован в виде SLD-резолюции (Selective Linear Definite clause resolution). В Прологе программа состоит из хорновских дизъюнктов (дизъюнктов с не более чем одним положительным литералом), а доказательство цели выполняется путём линейной резолюции с возвратами (backtracking).

Системы автоматического доказательства теорем

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

Искусственный интеллект

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

Ограничения и сложность

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

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

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

• Джон Робинсон предложил метод резолюций в 1965 году, что стало прорывом в автоматическом доказательстве теорем, так как предыдущие методы (например, метод Эрбрана) были значительно менее эффективны.
• Метод резолюций является обобщением modus ponens и modus tollens на случай дизъюнктивной формы.
• В 1972 году Роберт Ковальски и Маартен ван Эмден показали, что SLD-резолюция эквивалентна вычислениям в языке Пролог, что привело к созданию первого интерпретатора Пролога.
• Метод резолюций используется в некоторых современных системах проверки моделей (model checking) для доказательства свойств программ.

Источники

• Робинсон Дж. А. Машино-ориентированная логика, основанная на принципе резолюции // Кибернетический сборник. — М.: Мир, 1970. — Вып. 7.
• Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. — М.: Наука, 1983.
• Ковальски Р. Логика в решении проблем. — М.: Наука, 1990.
• Рассел С., Норвиг П. Искусственный интеллект: современный подход. — 2-е изд. — М.: Вильямс, 2006.
• Handbook of Automated Reasoning / Ed. by A. Robinson, A. Voronkov. — Elsevier, 2001.