JetBrains Research unites scientists working in challenging new disciplines

Seminar On Complete Refutation with Memoization

SLD resolution (Simple Linear Resolution with Definite Clauses) forms a basis for standard Prolog implementations. In general, SLD resolution can be considered as a non-deterministic process of construction of SDL-trees, which allows us to discover a counterexamples for a certain formula, acquired via a transformation of a query in the context of some specification. Under this formulation it is possible to show the soundness and completeness of SLD resolution.

In practical implementations, however, some deterministic way of SLD-tree construction has to be chosen (in the default case --- depth-first), which leads to a loss of certain properties (for depth-first search --- the completeness). There exist several approaches to fix this deficiency.

In the talk an alternative to the default way of search implementation, based on memoization, as well as its properties, will be considered.

Supplementary materials: Hisao Tamaki, Taisuke Sato. OLD Resolution with Tabulation // ICLP, 1986.

Presenter: Dmitry Boulytchev

Date: April 16, 2018

Time: 17:15

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28