# 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 :- B_{1},B_{2},…,B_{n}

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

where the head is empty.

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.

- Sub-goals are selected with a “left then right” strategy;
- The program is gone through with a strategy based on the depth-first search

and the backtracking method; - Clauses of the program P are selected with the same priority of their

appearance in the program; - 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

40 Advanced Artificial Intelligence

{p(X,X), p(Y, f(Y))}.

Such a mistake will be covered if the variable Y is not used

in the SLD resolution anymore. However, once the variable Y is used again, the

resolution process will fall into an endless loop.