SLD resolution


Also found in: Wikipedia.

SLD resolution

(logic, programming)
(Selected, Linear, Definite) Linear resolution with a selection function for definite sentences.

A definite sentence has exactly one positive literal in each clause and this literal is selected to be resolved upon, i.e. replaced in the goal clause by the conjunction of negative literals which form the body of the clause.

This article is provided by FOLDOC - Free Online Dictionary of Computing (foldoc.org)
References in periodicals archive ?
Thus the revised representation, exemplified in Figure 6, is simply a slightly more incremental version of the SLD resolution strategy, one in which variable values are passed explicitly into and out of procedures.
Prolog's power as a programming language comes from the fact that when SLD resolution is used as the evaluation technique, a Horn clause can be understood as defining a procedure (in the ordinary sense of procedural languages, e.g., a Pascal procedure), and evaluation can be understood as executing such a procedural program.
As stated in the introduction, SLD resolution can be understood procedurally as executing a nondeterministic program with procedure calls.
Formally, SLD resolution is refutation complete for Horn clauses [15].