# SLD resolution

SLD resolution is the basic inference rule used in logic programming. It is also
the primary computation procedure used in PROLOG. Here the name SLD is an
abbreviation of “Linear resolution with Selection function for Definite clauses”.
Firstly we introduce definitions on definite clause.

Definition 2.3 A Definite clause is a clause of the form

A :- B1,B2,…,Bn

where the head is a positive literal; the body is composed of zero, one or more
literals.

Definition 2.4 A definite program is a collection of definite clauses.

Definition 2.5 A definite goal is a clause of the form
? :- B1,B2,…,Bn

Let P and G be a program and a goal respectively, then the solving process for
the corresponding logic program is to seek a SLD resolution for P∪{G}. Two
rules should be decided for the resolution process: one is the computation rule on
how to select the sub-goal; the other is the search strategy on how to go through
the program. Theoretically, any search strategy used in artificial intelligence can
be adopted. However, in practice, strategies should be selected according to their
efficiency. Following is the standard SLD resolution process.

1. Sub-goals are selected with a “left then right” strategy;
2. The program is gone through with a strategy based on the depth-first search
and the backtracking method;
3. Clauses of the program P are selected with the same priority of their
appearance in the program;
4. The occur-check is omitted from the unification algorithm.

There are some characteristics for such a resolution process.

1. There exists simple and efficient method for the realization of depth-first
search strategy.

The depth-first search strategy can be realized with just a goal stack. A goal stack
for the SLD tree consists of branches which are going through. Correspondingly,
the searching process is composed of the pop and push operators on the stack. In
the case that the sub-goal on the top of the stack is unified with the head of some
clause of the program P, the corresponding resolvent will be put into stack. While
in the case that no clause could be unified, a backtracking operator will be
triggered with the result that an element was poped from the stack; in this case,
the resulted stack should be inspected for unification.  2. Completeness of SLD resolution proces is destroyed by the depth-first search
strategy.
This problem can be partially solved according to change the order of sub-goals
and the order of clauses of the program. For example, consider the following
program:

(1) p(f(X)):- p(X).

(2) p(a).
Let “?-p(Y)” be the goal. Then it is obvious that the SLD resolution process will
fall into an endless loop. However, if we exchange the order of clause (1) and
clause (2), then we will get the result Y=a, Y=f(a), ….
Consider another program:
(1) q(f(X)) :- q(X).
(2) q(a).
(3) r(a).

Let “G: ?-q(Y), r(Y)” be the goal. Then the SLD resolution process will fall into
an endless loop. However, if we exchange the order of sub-goals contained in G
and get the goal “G: ?- r(Y),q(Y)”, then we will get the result Y=a after the SLD
resolution process.

In order to guarantee the completeness of the SLD resolution process, the
width-first search strategy must be embodied in search rules of Prolog. Howerev,
as a result, both the time and space efficiency of the process will be decreased, as
while as the complexity of the process is increased. A trade-off is to maintain the
depth-first seach strategy that is used in Prolog, and supplement it with some
programs which embody other search strategies and are written with the Prolog language.

3. Soundness of SLD resolution is not guaranteed without occur-check.
Occur-check is a time-consuming operation in the unification algorithm. In the
case that occur-check is called, the time needed for every unification process is
linear to the size of the table, consequently the time needed for the append
operation on predications is O(n2); here n is the length of the table. Since little
unification process in the Prolog program use occur-check, the occur-check
operator is omitted form unification algorithms of most Prolog systems.

In fact, without the occur check we no longer have soundness of SLD
resolution. A sub-goal might can not be unified with a clause in the case that
some variables occurring in the term. However, since the occur-check is omitted,
the unification will still be executed and reach a wrong result. For example, let

“p(Y, f(Y))” and “?-p(X, X)”

be the program and the goal respectively. Then the unification algorithm will generate a replacement

θ={Y/X，f(Y)/Y}
for the pair