Resolution is the computation rule used by Prolog. Given a set of facts and rules as a program, execution begins with a query, which is an initial goal that is to be resolved. The set of goals that still have to be resolved is called the resolvent.
Consider again the ancestor/2 and parent/2 predicate shown above.
ancestor(X,Y) :- parent(X,Y). % clause 1 ancestor(X,Y) :- parent(Z,Y), ancestor(X,Z). % clause 2 parent(abe, homer). % clause 3 parent(abe, herbert). % clause 4 parent(homer, bart). % clause 5 parent(marge, bart). % clause 6 |
Program execution is started by issuing a query, for example
?- ancestor(X, bart).
This is our initial resolvent. The execution mechanism is now as follows:
- Pick one (usually the leftmost) goal from the resolvent. If the resolvent is empty, stop.
- Find all clauses whose head successfully unifies with this goal. If there is no such clause, go to step 6.
- Select the first of these clause. If there are more, remember the remaining ones. This is called a choice point.
- Unify the goal with the head of the selected clause. (this may instantiate variables both in the goal and in the clause’s body).
- Prefix this clause body to the resolvent and go to 1.
- Backtrack: Reset the whole computation state to how it was when the most recent choice point was created. Take the clauses remembered in this choice point and go to 3.
Figure 3.3: Execution Algorithm
In our example, the Prolog system would attempt to unify ancestor(X, bart) with the program’s clause heads. Both clauses of the ancestor/2 predicate can unify with the goal, but the textually first clause, clause 1, is selected first, and successfully unified with the goal:
Goal (Query): ancestor(X,bart) Selected: clause 1 Unifying: ancestor(X,bart) = ancestor(X1,Y1) results in: X=X1, Y1=bart New resolvent: parent(X, bart) More choices: clause 2
The body goal of clause 1 parent(X, bart) is added to the
resolvent, and the system remembers that there is an untried
alternative – this is referred to as a choice-point.
In the same way, parent(X, bart) is next selected for
unification. Clauses 5 and 6 are possible matches for this goal,
with clause 5 selected first. There are no body goals to add, and
the resolvent is now empty:
Goal: parent(X, bart) Selected: clause 5 Unifying: parent(X,bart) = parent(homer,bart) results in: X = homer New resolvent: More choices: clause 6, then clause 2
The execution of a program completes successfully when there is an empty resolvent. The program has thus found the first solution to the query, in the form of instantiations to the original Query’s variables, in this case X = homer. ECLiPSe returns this solution, and also asks if we want more solutions:
?- ancestor(X,bart). X = homer More? (;)
Responding with ’;’ will cause ECLiPSe to try to find alternative solutions by backtracking to the most recent choice-point, i.e. to seek an alternative to parent/2. Any bindings done during and after the selection of clause 5 are undone, i.e. the binding of X to homer is undone. Clause 6 is now unified with the goal parent(X,Y), which again produces a solution:
Goal: parent(X, bart) Selected: clause 6 Unifying: parent(X,bart) = parent(marge,bart) results in: X = marge New resolvent: More choices: clause 2
If yet further solutions are needed, then ECLiPSe would again backtrack. This time, parent/2 no longer has any alternatives left to unify, so the next older choice-point, the one made for ancestor/2, is the one that would be considered. The computation is returned to the state it was in just before clause 1 was selected, and clause 2 is unified with the query goal:
Goal: ancestor(X,bart) Selected: clause 2 Unifying: ancestor(X,bart) = ancestor(X1,Y1) results in: Y1 = bart, X1 = X New resolvent: parent(Z1, bart), ancestor(X1, Z1) More choices:
For the first time, there are more than one goal in the resolvent, the leftmost one, parent(Z1,bart) is then selected for unification. Again, clauses 5 and 6 are candidates, and a new choice-point is created, and clause 5 tried first.
Goal: parent(Z1, bart) Selected: clause 5 Unifying: parent(Z1, bart) = parent(homer, bart) results in: Z1 = homer New resolvent: ancestor(X1, homer) More choices: clause 6
Eventually, after a few more steps (via finding the ancestor of homer), this leads to a new solution, with abe returned as an ancestor of bart:
?- ancestor(X,bart). X = abe More? (;)
If yet more solutions are requested, then because only one parent for
homer is given by the program, ECLiPSe would backtrack to the only
remaining choice-point, unifying clause 6 is unified with the goal,
binding Z1 to marge. However, no ancestor for marge
can be found, because no parent of
marge is specified in the program. No more choice-points remains to
be tried, so the execution terminates.