Метод резолюций и унификация

Мотивация: автоматическое доказательство теорем

Как компьютер может доказывать математические теоремы? Метод резолюций (Робинсон, 1965) — алгоритм, который сводит проверку логического следования к поиску противоречия: мы отрицаем заключение, добавляем к посылкам, и пытаемся вывести пустой дизъюнкт ☐. Это основа языка Prolog и современных ATP-систем.

Приведение к клаузальной форме

Шаги:

Устранить → и ↔.
Загнать ¬ внутрь (де Морган, снятие двойного отрицания).
Переименовать переменные (каждый квантор — своя переменная).
Вынести кванторы (привести к предварённой форме).
Сколемизация: устранить ∃. ∃x P(x) → P(c) (новая константа Сколема); ∀y ∃x P(x,y) → ∀y P(f(y),y) (новая функция Сколема f).
Убрать ∀ (переменные считаются универсально квантифицированными).
Распределить ∨ над ∧ → КНФ (множество дизъюнктов).

Сколемизация сохраняет выполнимость (но не логическое следование).

Унификация

Подстановка σ — отображение переменных → термы. σ(t) — результат применения σ к терму t.

Унификатор для множества пар {(s₁,t₁),...,(sₙ,tₙ)}: σ такой, что σ(sᵢ) = σ(tᵢ) для всех i.

Наиболее общий унификатор (НОУ / MGU): σ такой, что любой другой унификатор τ = τ' ∘ σ. MGU единственен с точностью до переименования переменных.

Алгоритм унификации:

Если s = x (переменная): проверить occur check (x не входит в t) → σ = {x↦t}.
Если s = f(s₁,...,sₙ) и t = f(t₁,...,tₙ): унифицировать попарно.
Если s и t — различные константы или функторы разной арности → неудача.

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

Пропозициональная резолюция: из (D₁ ∨ l) и (D₂ ∨ ¬l) → резольвента D₁ ∨ D₂.

Резолюция первого порядка: из клауз C₁ (с литералом l₁) и C₂ (с литералом ¬l₂), если σ = MGU(l₁, l₂): Резольвента = σ(C₁ {l₁}) ∨ σ(C₂ {l₂}).

Теорема Робинсона (полнота резолюции): Множество клауз S невыполнимо ⟺ из S выводится пустой дизъюнкт ☐ конечной цепочкой резолюций.

Численный пример

Задача: Доказать «Сократ смертен» из «Все люди смертны» и «Сократ — человек».

Шаг 1. Формализация:

∀x (Human(x) → Mortal(x)) → клауза: {¬Human(x) ∨ Mortal(x)}
Human(Socrates) → клауза: {Human(Socrates)}
Отрицание заключения: ¬Mortal(Socrates) → клауза: {¬Mortal(Socrates)}

Шаг 2. Унификация x ↦ Socrates для первой клаузы и {Human(Socrates)}: MGU: {x ↦ Socrates}. Резольвента из {¬Human(x) ∨ Mortal(x)} и {Human(Socrates)}: {Mortal(Socrates)}.

Шаг 3. Резолюция {Mortal(Socrates)} и {¬Mortal(Socrates)} (MGU = ε): Резольвента: ☐ (пустой дизъюнкт).

Вывод: Множество клауз невыполнимо → заключение следует из посылок ✓.

Реальное приложение

Prolog — язык программирования, основанный на резолюции. Запрос ?- mortal(X). решается поиском унификатора и резолюцией с базой знаний. Используется в экспертных системах, NLP, планировании.

Дополнительные аспекты

Метод резолюций — единственное правило вывода, которого достаточно для опровержения противоречивых множеств клауз (теорема о полноте резолюции). В сочетании с алгоритмом унификации он даёт эффективный механический способ доказательства теорем в логике предикатов. Алгоритм Робинсона (1965) находит наиболее общий унификатор за линейное время в подходящем представлении. Современные системы (Vampire, E) используют резолюцию плюс сотни эвристик отбора клауз: literal selection, term ordering (KBO/LPO), redundancy elimination. Это позволило в 1996 г. компьютеру доказать гипотезу Роббинса о булевой алгебре — первая значимая открытая теорема, решённая ATP-системой.

Связь с другими разделами математики

Резолюции и унификация, будучи инструментами логики первого порядка, пересекаются с рядом «чисто математических» дисциплин через модельно-теоретический и вычислительный аспекты. Сколемизация опирается на результаты Лёвгейма и Сколема о нормальных формах и тесно связана с леммой Лёвенгейма–Сколема: всякая счетно аксиоматизируемая теория с бесконечной моделью имеет счетную модель. Именно существование сколемовских функций интерпретируется как выбор конкретных «свидетелей» для кванторов в моделях.

В универсальной алгебре и теории переписываний унификация появляется как решение уравнений в свободных алгебрах: классический результат Мартелли–Монтанари (1976) формализует унификацию в терминах систем переписывания. Здесь же строятся мосты к коммутативной алгебре через унификацию модуло эквивалентности (unification modulo theories), например модуло ассоциативности и коммутативности; это перекликается с техникой базисов Гребнера (Бухбергер) при решении полиномиальных уравнений.

В теории доказательств резолюционный метод сопоставляется с секвенциальным исчислением Гентцена: теорема о полноте резолюции может трактоваться как существование определенного класса вырезаний (cut) в исчислении LK. Работы Смаляна, Шютте, позднее – Бухбергера и Баумгарта указывают на связь между стратегиями резолюции и нормальными формами доказательств.

В прикладной математике и численных методах резолюционные техники используются косвенно через SMT-солверы (Z3, CVC4), где логические части гибридных задач оптимизации и дифференциальных уравнений (например, в проверке инвариантов для систем ОДУ) решаются именно логическими движками на основе унификации и резолюции. В вероятностной логике и байесовских сетях Маркоса и Халперна используются обобщения резолюции для вывода условных вероятностей в символической форме.

Историческая справка и развитие идеи

Корни метода резолюций восходят к классической работе Давида Гильберта и Пола Бернайса «Grundlagen der Mathematik» (1934–1939), где формализовались доказательства в первом порядке. Идея нормальных форм и устранения кванторов через функции была развита Торфином Сколемом в 1920-е годы, что стало предпосылкой для сколемизации. Собственно правило резолюции в современном виде было введено Джоном Аланом Робинсоном в статье «A Machine-Oriented Logic Based on the Resolution Principle» (Journal of the ACM, 1965). Робинсон объединил две линии: секвенциальные методы Гентцена и практическую задачу автоматизации доказательств. Его мотивацией была реализация эффективного, по сути единственного, правила вывода, удобного для машинной реализации, в отличие от громоздких натуральных выводов. В 1970–1980-х годах резолюционные методы стали ядром систем автоматического доказательства теорем: работы Ловланда, Льюка, Воссалена и объединенного проекта Boyer–Moore сформировали культуру «машинных доказательств». Параллельно развивалась теория унификации: работы Хербранда, затем П. Мартелли и У. Монтанари (Journal of the ACM, 1982) дали общий алгоритм и доказали единственность наиболее общего унификатора. Прорывом стало создание языка Prolog (Кольмеро, Рюссель, 1972) и монографии Клоберда и Ллойда, где SLD-резолюция стала основой логического программирования. В конце XX века резолюция эволюционировала в мощные ATP-системы: Otter (Мак-Коннелл), затем Vampire (Рашкович, Вран, 1990-е), E (Шульц). В 1996 году Ларри Воспен и сотрудники подтвердили гипотезу Роббинса о булевой алгебре с помощью EQP, что стало символом зрелости резолюционных методов.