JetBrains Research — наука, меняющая мир

Семинар по полному поиску опровержения с мемоизацией

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

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

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

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

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

16.04.2018, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28