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
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28