SLD-резолюция¶

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

¶История

Метод резолюций был разработан в 1965 году американским математиком и логиком Джоном Аланом Робинсоном как основа для автоматического доказательства теорем в логике первого порядка. Однако общий метод резолюций был неэффективен для практических вычислений из-за комбинаторного взрыва возможных вариантов. В 1970-х годах французский учёный Роберт Ковальски и британский логик Патрик Хейз предложили ограниченную версию резолюции — линейную резолюцию, которая работает только с хорновскими дизъюнктами. Позднее, в 1972 году, Ковальски совместно с французским информатиком Аленом Колмероэ разработали SLD-резолюцию как основу для языка Пролог. Именно SLD-резолюция стала стандартным механизмом вывода в большинстве реализаций Пролога, включая такие известные, как SWI-Prolog, GNU Prolog и SICStus Prolog.

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

¶Хорновские дизъюнкты

SLD-резолюция оперирует только хорновскими дизъюнктами — логическими предложениями, которые содержат не более одного положительного литерала. В контексте логического программирования хорновские дизъюнкты делятся на два типа:

• Факты — дизъюнкты, состоящие из одного положительного литерала (например, человек(сократ).).
• Правила — дизъюнкты вида A :- B1, B2, ..., Bn, где A — голова правила (положительный литерал), а B1, B2, ..., Bn — тело правила (отрицательные литералы). Логически это эквивалентно импликации (B1 ∧ B2 ∧ ... ∧ Bn) → A.

¶Целевой дизъюнкт

Запрос к программе формулируется как целевой дизъюнкт, состоящий только из отрицательных литералов (например, ?- человек(сократ).). В процессе SLD-резолюции этот дизъюнкт последовательно преобразуется до пустого дизъюнкта, что означает успешное доказательство.

¶Унификация

Унификация — это процесс нахождения подстановки (набора замен переменных на термы), которая делает два литерала идентичными. Например, для литералов человек(X) и человек(сократ) унификатор — это {X = сократ}. SLD-резолюция использует унификацию для сопоставления литерала из целевого дизъюнкта с головой правила или факта из программы.

¶Алгоритм SLD-резолюции

SLD-резолюция выполняется в рамках дерева вывода, где каждый узел представляет собой целевой дизъюнкт, а рёбра — применение одного шага резолюции. Алгоритм включает следующие шаги:

1. Выбор литерала — из текущего целевого дизъюнкта выбирается один литерал (обычно самый левый, в соответствии со стратегией Пролога).
2. Поиск подходящего правила — в программе ищется правило или факт, голова которого унифицируется с выбранным литералом.
3. Унификация — выполняется унификация выбранного литерала и головы правила. Если унификация невозможна, происходит откат (backtracking) к предыдущему шагу.
4. Резолюция — выбранный литерал заменяется телом правила (с учётом подстановки унификации). Если правило является фактом (тело пусто), литерал просто удаляется.
5. Повторение — процесс повторяется с новым целевым дизъюнктом до тех пор, пока не будет получен пустой дизъюнкт (успех) или не останется вариантов для выбора (неудача).

¶Пример

Рассмотрим простую программу на Прологе: `` родитель(анна, иван). родитель(иван, петр). предок(X, Y) :- родитель(X, Y). предок(X, Y) :- родитель(X, Z), предок(Z, Y). ` Запрос: ?- предок(анна, петр).`

Шаги SLD-резолюции:

1. Целевой дизъюнкт: ?- предок(анна, петр).
2. Выбор литерала: предок(анна, петр). Унификация с головой первого правила предок(X, Y) даёт подстановку {X = анна, Y = петр}. Тело правила: родитель(анна, петр).
3. Новый целевой дизъюнкт: ?- родитель(анна, петр).
4. Унификация с фактом родитель(анна, иван) не удаётся (петр ≠ иван). Происходит откат.
5. Поиск другого правила: второе правило предок(X, Y) :- родитель(X, Z), предок(Z, Y). Унификация даёт {X = анна, Y = петр}. Тело: родитель(анна, Z), предок(Z, петр).
6. Новый целевой дизъюнкт: ?- родитель(анна, Z), предок(Z, петр).
7. Выбор первого литерала родитель(анна, Z). Унификация с фактом родитель(анна, иван) даёт {Z = иван}.
8. Новый целевой дизъюнкт: ?- предок(иван, петр).
9. Унификация с первым правилом: предок(иван, петр) → родитель(иван, петр).
10. Унификация с фактом родитель(иван, петр) успешна. Целевой дизъюнкт становится пустым.
11. Доказательство завершено успешно. Ответ: true.

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

SLD-резолюция не определяет однозначно порядок выбора литералов и правил, поэтому на практике используются различные стратегии:

¶Стратегия глубины (DFS)

В большинстве реализаций Пролога применяется стратегия поиска в глубину (depth-first search) с возвратом. Это означает, что система выбирает первый подходящий вариант и углубляется в него, а при неудаче возвращается к предыдущему выбору. Такая стратегия проста в реализации, но может приводить к зацикливанию при наличии бесконечных рекурсий.

¶Стратегия ширины (BFS)

Поиск в ширину (breadth-first search) рассматривает все варианты на одном уровне глубины перед переходом на следующий. Эта стратегия гарантирует нахождение решения, если оно существует, но требует значительно больше памяти.

¶Эвристические стратегии

Некоторые системы (например, Prolog с мета-интерпретаторами) используют эвристики для выбора наиболее перспективных правил, что ускоряет поиск в сложных задачах.

¶Свойства

¶Полнота

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

¶Детерминированность

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

¶Эффективность

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

¶Применение

SLD-резолюция является основным механизмом вывода в логическом программировании. Она используется в:

• Языке Пролог — для выполнения запросов к базам знаний, решения задач искусственного интеллекта, обработки естественного языка.
• Экспертных системах — для вывода заключений на основе правил.
• Символьных вычислениях — для доказательства теорем и автоматического синтеза программ.
• Обработке знаний — в системах, основанных на логике, таких как Datalog и Answer Set Programming (ASP).

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

SLD-резолюция имеет ряд ограничений:

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

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

• Термин «SLD-резолюция» был введён Робертом Ковальски в 1974 году в статье «Predicate Logic as a Programming Language».
• В 1980-х годах японский проект «Компьютер пятого поколения» активно использовал SLD-резолюцию как основу для параллельных логических языков, таких как KL1.
• SLD-резолюция является частным случаем более общего метода SL-резолюции (Selective Linear resolution), который не требует хорновской формы.
• В современных реализациях Пролога SLD-резолюция часто дополняется механизмами отсечения (cut) и отрицания как неудачи (negation as failure), что расширяет её выразительность.

¶Источники

• Ковальски Р. «Логика в решении проблем». — М.: Наука, 1990.
• Колмероэ А. «Основы логического программирования». — М.: Мир, 1988.
• Стерлинг Л., Шапиро Э. «Искусство программирования на языке Пролог». — М.: Мир, 1990.
• Lloyd J. W. «Foundations of Logic Programming». — Springer, 1987.
• Robinson J. A. «A Machine-Oriented Logic Based on the Resolution Principle». — Journal of the ACM, 1965.