Лаборатория языковых инструментов
Полный поиск опровержения с мемоизацией
В основе стандартных реализаций языка Prolog лежит использование SLD-резолюции (Simple Linear Resolution with Definite Clauses). В общем случае SLD-резолюцию можно описать как недетерминированное построение SLD-дерева, которое позволяет найти контрпримеры для некоторой формулы, полученной преобразованием исходной спецификации и запроса. В такой формулировке можно доказать полноту и корректность SLD-резолюции.
Однако при практической реализации избирается некоторый детерминированный способ получения контрпримеров (чаще всего обход глубину); при этом ряд полезных свойств теряется (при обходе в глубину --- полнота). Существует несколько способов исправить этот недостаток.
В докладе будет описан альтернативный способ реализации поиска, основанный на мемоизации, и рассмотрены его свойства.
Материалы к докладу: Hisao Tamaki, Taisuke Sato. OLD Resolution with Tabulation // ICLP, 1986.
Докладчик: Дмитрий Булычев