Лаборатория языковых инструментов

В основе стандартных реализаций языка Prolog лежит использование SLD-резолюции (Simple Linear Resolution with Definite Clauses). В общем случае SLD-резолюцию можно описать как недетерминированное построение SLD-дерева, которое позволяет найти контрпримеры для некоторой формулы, полученной преобразованием исходной спецификации и запроса. В такой формулировке можно доказать полноту и корректность SLD-резолюции.

Однако при практической реализации избирается некоторый детерминированный способ получения контрпримеров (чаще всего обход глубину); при этом ряд полезных свойств теряется (при обходе в глубину --- полнота). Существует несколько способов исправить этот недостаток.

В докладе будет описан альтернативный способ реализации поиска, основанный на мемоизации, и рассмотрены его свойства.

Материалы к докладу: Hisao Tamaki, Taisuke Sato. OLD Resolution with Tabulation // ICLP, 1986.

Докладчик: Дмитрий Булычев