Главная arrow книги arrow Копия Глава 9. Логический вывод в логике первого п arrow Алгоритм обратного логического вывода
Алгоритм обратного логического вывода

Листинг 9.3. Простой алгоритм обратного логического вывода

В этом алгоритме используется композиция подстановок. Здесь Compose (θ1, θ2) — это подстановка, результат которой идентичен результату применения каждой подстановки по очереди, следующим образом:

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

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