2. SLD-Resolution and Back-tracking

Principle of Resolution In order to prove a goal $\text{:- }{G}_{!},\dots ,G_n$ with respect to a set $P$ of program clauses, resolution seeks to show that $P\cup \{\neg G_1\vee \dots \vee \neg G_n\}$ leads to a contradiction.

A contradiction is obtained when a literal and its negation are stated at the same time. If a contradiction does not arise, a new goal is derived by unifying the current goal with a program clause, the derived goals are called resolvents.

SLD-Resolution

• Selective: at each resolution step, a fixed computation rule is applied to select which atom from the goal will be resolved next
• Linear: at each resolution step, the most recently derived resolvent is used as the next goal
• Definite: all the program clauses are definite clauses

Properties of SLD-Resolution

1. SLD-resolution is refutation-complete: given a program and a goal, if a contradiction can be derived, then SLD-resolution will eventually generate it.
2. Independence of selection rule: if there exists a solution, SLD-resolution will find it. (regardless of the selection rule employed)

Computing resolvents with SLD-resolution

1. Given a goal clause $\text{:- }{G}_1,\dots ,G_k$, we select an atom $G_i$ of the form $p(s_1,\dots ,s_n)$.
2. We select a program clause $p(t_1,\dots ,t_n)\text{ :- }{B}_1,\dots ,B_m$ such that $p(t_1,\dots ,t_n)$ and $p(s_1,\dots ,s_n)$ are unifiable using the mgu $\sigma$.
3. Obtain resolvent $\text{:- }{B}_1{\sigma }_1,\dots ,B_m\sigma ,G_1\sigma ,\dots ,G_{i-1}\sigma ,\dots ,G_k\sigma$ from which $G_i\sigma$ has been eliminated.

We continue deriving new resolvents until an empty one is found, indicating that a contradiction has been found. When an empty resolvent is generated, the composition of the substitutions applied at each resolution step, restricted to the variables of the query, is the solution to the goal.

SLD-resolution in Prolog

• Prolog always selects the left-most literal
• Prolog uses clauses in the program in the order they are written
• SLD-resolution is complete but Prolog’s implementation is not because of its search strategy: it uses depth-first search which is efficient but not complete (we may get stuck in a branch that expands infinitely)

Example resolution in Prolog

Take the following program:

based(prolog, logic).
based(haskell, maths).
likes(max, logic).
likes(claire, maths).
likes(X, P) :- based(P, Y), likes(X, Y).

Lets take the query :- likes(Z, prolog).

1. using the last clause and mgu $\{X\mapsto Z,P\mapsto \text{prolog}\}$, we obtain the resolvent :- based(prolog, Y), likes(Z, Y).
2. using the first clause and mgu $\{Y\mapsto \text{logic}\}$, we obtain the resolvent :- likes(Z, logic).
3. since we can now unify with the fact likes(max, logic) using the substitution $\{Z\mapsto \text{max}\}$, we can obtain an empty resolvent.
4. the composition of substitutions generated is $\{X\mapsto \text{max},P\mapsto \text{prolog},Y\mapsto \text{logic},Z\mapsto \text{max}\}$

Hence, the solution to the initial query is $\{Z\mapsto \text{max}\}$.

SLD-Resolution Trees

We can represent each resolution step graphically, and since there might be several clauses in the program that can be used to generate a resolvent from a goal, we obtain a SLD-resolution tree:

Every branch in the tree that leads to an empty resolvent (denoted by $\square$) yields a solution. If a goal unifies with no program clause, the branch is a failure.

Example SLD-resolution tree and failure

Backtracking

When a branch ends, Prolog will back-track over the tree to search alternative branches. The previous resolution step is taken back and the next possible resolvent is generated.

Failure branches back-track automatically, and solution branches can be back-tracked from on request.

Back-tracking can be stopped by using the cut predicate, written $!$, which means do not back-track beyond this point.

Example of back-tracking