3.1. SLD-resolution

Prolog’s proof procedure is based on resolution refutation in definite clause logic. Resolution refutation has been explained in the previous chapter. In order to turn it into an executable proof procedure, we have to specify how a literal to resolve upon is selected, and how the second input clause is found. Jointly, this is called a resolution strategy. Consider the following program:

student_of(X,T):-follows(X,C),teaches(T,C).
follows(paul,computer_science).
follows(paul,expert_systems).
follows(maria,ai_techniques).
teaches(adrian,expert_systems).
teaches(peter,ai_techniques).
teaches(peter,computer_science).

The query ?-student_of(S,peter) has two possible answers: { S → paul } and { S → maria }. In order to find these answers, we first resolve the query with the first clause, yielding

?-follows(S,C),teaches(peter,C).

Now we have to decide whether we will search for a clause which resolves on follows(S,C), or for a clause which resolves on teaches(peter,C). This decision is governed by a selection rule. Prolog’s selection rule is left to right, thus Prolog will search for a clause with a positive literal unifying with follows(S,C). There are three of these, so now we must decide which one to try first. Prolog searches the clauses in the program top-down, so Prolog finds the answer { S → paul } first. Note that the second choice leads to a dead end: the resolvent is

?-teaches(peter,expert_systems).

which doesn’t resolve with any clause in the program.

This process is called SLD-resolution: S for selection rule, L for linear resolution (which refers to the shape of the proof trees obtained), and D for definite clauses. Graphically, SLD-resolution can be depicted as in Figure 3.1. This SLD-tree should not be confused with a proof tree: first, only the resolvents are shown (no input clauses or unifiers), and second, it contains every possible resolution step. Thus, every leaf of an SLD-tree which contains the empty clause \(\square\) corresponds to a refutation and hence to a proof tree; such a leaf is also called a success branch. An underlined leaf which does not contain \(\square\) represents a failure branch.

Figure 3.1 An SLD-tree.

Exercise 3.1

Draw the proof trees for the two success branches in Figure 3.1.

As remarked already, Prolog searches the clauses in the program top-down, which is the same as traversing the SLD-tree from left to right. This not only determines the order in which answers (i.e. success branches) are found: it also determines whether any answers are found at all, because an SLD-tree may contain infinite branches, if some predicates in the program are recursive. As an example, consider the following program:

brother_of(X,Y):-brother_of(Y,X).
brother_of(paul,peter).

An SLD-tree for the query ?-brother_of(peter,B) is depicted in Figure 3.2. If we descend this tree taking the left branch at every node, we will never reach a leaf. On the other hand, if we take the right branch at every node, we almost immediately reach a success branch. Taking right branches instead of left branches in an SLD-tree corresponds to searching the clauses from bottom to top. The same effect would be obtained by reversing the order of the clauses in the program, and the SLD-tree clearly shows that this is enough to prevent Prolog from looping on this query. This is a rule of thumb that applies to most cases: put non-recursive clauses before recursive ones.

Figure 3.2 An SLD-tree with infinite branches.

However, note that, even after this modification, the program still has some problems. For one thing, the query ?-brother_of(peter,B) will be answered an infinite number of times, because there are infinitely many refutations of it. But, even worse, consider a query that does not have an answer, like ?-brother_of(peter,maria). No matter the order in which the SLD-tree is descended, Prolog will never discover that the query has in fact no answer, simply because the SLD-tree is infinite. So, one should be careful with programs like the above, which define a predicate to be symmetric.

Another property of predicates which can cause similar problems is transitivity. Consider the following program:

brother_of(paul,peter).
brother_of(peter,adrian).
brother_of(X,Y):-brother_of(X,Z),brother_of(Z,Y).

The third clause ensures that ?-brother_of(paul,adrian) is a logical consequence of the program. The SLD-tree for the query ?-brother_of(paul,B) is depicted in Figure 3.3. Not only is this SLD-tree infinite, but the resolvents get longer and longer on deeper levels in the tree.

Figure 3.3 An SLD-tree with infinite branches and expanding resolvents.

We have encountered two problems with SLD-resolution: (1) we might never reach a success branch in the SLD-tree, because we get ‘trapped’ into an infinite subtree, and (2) any infinite SLD-tree causes the inference engine to loop if no (more) answers are to be found. The first problem means that Prolog is incomplete: some logical consequences of a program may never be found. Note carefully that this incompleteness is not caused by the inference rule of resolution, which is refutation complete. Indeed, for any program and any query, all the possible answers will be represented by success branches in the SLD-tree. The incompleteness of SLD-resolution is caused by the way the SLD-tree is searched.

There exists a solution to this problem: if we descend the tree layer by layer rather than branch-by-branch, we will find any leaf before we descend to the next level. However, this also means that we must keep track of all the resolvents on a level, instead of just a single one. Therefore, this breadth-first search strategy needs much more memory than the depth-first strategy used by Prolog. In fact, Prolog’s incompleteness was a deliberate design choice, sacrificing completeness in order to obtain an efficient use of memory1. As we saw above, this problem can often be avoided by ordering the clauses in the program in a specific way (which means that we have to take the procedural meaning of the program into account).

As for the second problem, we already saw that this is due to the semi-decidability of full clausal logic, which means that there is no general solution to it.

Exercise 3.2 

Draw the SLD-tree for the following program:

list([]).
list([_H|T]):-list(T).

and the query ?-list(L).

---

1

The efficiency and completeness of search strategies will be discussed in Chapters 5 and 6.