How Prolog Executes

7.1 SLD resolution

To answer a query, Prolog:

Takes the leftmost goal.

Searches the database top to bottom for a clause whose head unifies with it.

Replaces the goal with the clause body (with fresh variables).

Repeats until no goals remain (success) or no clause matches (failure).

On failure, backtracks to the most recent choice point and tries the next alternative.

This is depth-first search with chronological backtracking.

7.2 Tracing an example

parent(tom, bob).
parent(bob, ann).
parent(bob, pat).
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

?- trace, grandparent(tom, Who).
   Call: grandparent(tom, _G1)
   Call: parent(tom, _G2)
   Exit: parent(tom, bob)
   Call: parent(bob, _G1)
   Exit: parent(bob, ann)
   Exit: grandparent(tom, ann)
Who = ann ;
   Redo: parent(bob, _G1)
   Exit: parent(bob, pat)
Who = pat.

7.3 The four-port (Byrd box) model

Call: goal is first tried.

Exit: goal succeeded.

Redo: backtracking into the goal for another solution.

Fail: no (more) solutions.

(SWI adds Exception and Unify ports.)

+----------------+
 Call → |                | → Exit
        |   predicate    |
 Fail ← |                | ← Redo
        +----------------+

7.4 Search trees & order matters

Clause order affects which solution comes first and termination:

(Tabling, §31, fixes left recursion declaratively.)

% Left recursion → infinite loop
ancestor(X, Y) :- ancestor(X, Z), parent(Z, Y).   % BAD: loops forever
ancestor(X, Y) :- parent(X, Y).

% Correct: base case first, recursive call after a grounding goal
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

7.5 Determinism

det: exactly one solution, no choice points left.

semidet: zero or one solution.

nondet: zero or more solutions.

multi: one or more solutions.

These terms are used in documentation (%! member(?X, ?List) is nondet.).