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

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

¶История

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

В 1970-х годах правило резолюции легло в основу языка логического программирования Prolog, разработанного Аленом Колмероэ и Филиппом Русселем. Prolog использует частный случай резолюции — линейную резолюцию с упорядочиванием целей (SLD-резолюцию), что позволяет эффективно обрабатывать запросы к базам знаний. В последующие десятилетия правило резолюции было усовершенствовано в различных направлениях: появились стратегии резолюции (например, семантическая резолюция, гиперрезолюция), а также методы, ориентированные на работу с равенством (резолюция с параметризацией).

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

¶Дизъюнкт и литерал

В резолюционном исчислении формулы представляются в конъюнктивной нормальной форме (КНФ). Каждая формула в КНФ есть конъюнкция дизъюнктов. Дизъюнкт — это дизъюнкция литералов. Литерал — это атомарная формула (предикат) или её отрицание. Например, дизъюнкт \( A \lor \neg B \lor C \) состоит из трёх литералов: \( A \), \( \neg B \) и \( C \).

¶Резольвента

Правило резолюции для исчисления высказываний формулируется следующим образом: если имеются два дизъюнкта \( C_1 = L \lor A \) и \( C_2 = \neg L \lor B \), где \( L \) — литерал, а \( A \) и \( B \) — дизъюнкты (возможно, пустые), то резольвентой является дизъюнкт \( A \lor B \). Пустой дизъюнкт (обозначаемый как \( \square \)) означает противоречие (ложь).

Пример:

• \( C_1 = P \lor Q \)
• \( C_2 = \neg P \lor R \)
• Резольвента: \( Q \lor R \)

¶Унификация

В логике первого порядка правило резолюции требует дополнительной процедуры — унификации. Унификация — это алгоритм, который находит наиболее общую подстановку термов вместо переменных, делающую два литерала идентичными. Например, для литералов \( P(x, a) \) и \( \neg P(b, y) \) унификатор \( \sigma = \{x \leftarrow b, y \leftarrow a\} \) приводит их к виду \( P(b, a) \) и \( \neg P(b, a) \). После унификации применяется резолюция.

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

¶Доказательство теорем

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

Пример доказательства в исчислении высказываний:

• Аксиомы: \( P \), \( \neg P \lor Q \), \( \neg Q \lor R \)
• Требуется доказать: \( R \)
• Отрицание: \( \neg R \)
• Применение резолюции:

1. Резольвента \( P \) и \( \neg P \lor Q \): \( Q \)
2. Резольвента \( Q \) и \( \neg Q \lor R \): \( R \)
3. Резольвента \( R \) и \( \neg R \): \( \square \) (пустой дизъюнкт)

• Противоречие доказано, следовательно, \( R \) истинно.

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

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

¶Автоматическое рассуждение и ИИ

Правило резолюции лежит в основе многих систем автоматического доказательства теорем (ATP), таких как Vampire, E Prover, SPASS. Эти системы используются для верификации программного обеспечения, проверки корректности цифровых схем, решения задач в математике и формальной логике. В области искусственного интеллекта резолюция применяется в планировании, диагностике и обработке естественного языка.

¶Виды и модификации правила резолюции

¶Линейная резолюция

Линейная резолюция — это стратегия, при которой на каждом шаге один из родительских дизъюнктов является резольвентой предыдущего шага. Это упрощает управление поиском и используется в Prolog.

¶Семантическая резолюция

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

¶Гиперрезолюция

Гиперрезолюция — это обобщение, при котором за один шаг обрабатывается несколько дизъюнктов. Она особенно эффективна для дизъюнктов Хорна и используется в некоторых системах ATP.

¶Резолюция с параметризацией

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

¶Критика и ограничения

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

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

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

• Правило резолюции является основой для многих коммерческих и исследовательских систем верификации, включая системы, используемые компаниями Intel и Microsoft для проверки корректности микропроцессоров.
• В 2018 году система доказательства теорем E Prover, основанная на резолюции, выиграла конкурс CASC (CADE ATP System Competition) в категории для логики первого порядка.
• Существует вариант правила резолюции для неклассических логик, например, для модальной логики и логики высшего порядка, но эти расширения значительно сложнее в реализации.

¶Источники

• 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.
• Lloyd, J. W. (1987). «Foundations of Logic Programming». Springer-Verlag.
• Loveland, D. W. (1978). «Automated Theorem Proving: A Logical Basis». North-Holland.