3.1 The abstract interpreter (SLD resolution)

A logic program runs by SLD resolution (Selective Linear Definite-clause resolution). State = the current list of goals (the resolvent) plus the bindings made so far.

to solve goals G1, G2, ..., Gn:
  1. select the FIRST goal G1            (computation rule)
  2. find a clause  H :- B1,...,Bk  whose head H unifies with G1
       (try clauses TOP TO BOTTOM)       (search rule)
  3. replace G1 by the body:  new goals = B1,...,Bk, G2,...,Gn
     apply the unifying substitution everywhere
  4. repeat; empty goal list = SUCCESS
  5. if no clause matches → FAIL → BACKTRACK:
     undo the last choice and try the next clause for it

Standard Prolog therefore = SLD resolution + leftmost goal selection + depth-first, top-to-bottom clause search.

3.2 The SLD search tree

Every choice of clause creates a branch. For the family database of the previous lessons, the query ?- grandparent(dasharath, G) generates:

• Success branches end in the empty goal — each yields one answer substitution.
• Failure branches end in a non-empty goal with no matching clause.
• Infinite branches can exist — and because Prolog searches depth-first, an infinite branch to the left of a success branch means the answer is never reached. (Breadth-first search would find it but costs too much memory — a deliberate engineering trade-off.)

3.3 Declarative vs procedural semantics

Soundness: every answer SLD resolution returns is logically correct. Completeness: every logically correct answer is somewhere in the SLD tree — but depth-first search may fail to reach it (loop first). So Prolog the tool is sound but not complete, while SLD resolution the theory is both.

Two more theory terms worth recognising in exams:

• Herbrand universe — the set of all ground (variable-free) terms buildable from the program's constants and functors.
• Ground instance — a clause with all variables replaced by ground terms; the declarative meaning is built from these.

3.4 Negation as failure & the closed-world assumption

Logic programs contain only positive knowledge. Prolog's \+ G ("not provable G") succeeds when the attempt to prove G fails finitely — this is negation as failure, justified by the closed-world assumption (CWA): anything not derivable from the database is assumed false.

bachelor(X) :- male(X), \+ married(X).

Caution: \+ is safe only when its argument is ground at call time — call it after the variables are bound.

3.5 Applications of logic programming

The historical headline: Prolog was chosen as the core language of Japan's Fifth Generation Computer Systems project (1980s), and resolution-based reasoning remains inside SAT/SMT solvers, Answer Set Programming and the query planners of modern databases — the ideas of this unit are very much alive.

3.6 The formal vocabulary of SLD resolution (definitions to reproduce)

SLD derivation: a sequence of goals G0, G1, G2, ... where G0 is the query and each Gi+1 is obtained from Gi by resolving its selected goal against a (renamed) program clause, applying the MGU. SLD refutation: a finite SLD derivation ending in the empty goal — a proof that the query follows from the program. Computed answer substitution: the composition of all MGUs along a refutation, restricted to the query's variables — this is what Prolog prints as X = .... Renaming apart: before each clause use, its variables are renamed fresh (X → X1) so they cannot clash with variables already in the goal. Forgetting this is the most common error in hand-written traces.

3.7 A complete refutation, written formally

Program: p1: parent(ram, lav). p2: parent(dasharath, ram). a1: anc(X,Y) :- parent(X,Y). a2: anc(X,Y) :- parent(X,Z), anc(Z,Y).

Query: ?- anc(dasharath, lav).

G0:  anc(dasharath, lav)
     resolve with a2 (renamed X1,Y1,Z1):  MGU θ1 = {X1=dasharath, Y1=lav}
G1:  parent(dasharath, Z1), anc(Z1, lav)
     resolve first goal with p2:          MGU θ2 = {Z1=ram}
G2:  anc(ram, lav)
     resolve with a1 (renamed X2,Y2):     MGU θ3 = {X2=ram, Y2=lav}
G3:  parent(ram, lav)
     resolve with p1:                     MGU θ4 = {}
G4:  □   (empty goal — refutation complete)

Computed answer: the query was ground, so the answer is simply "true".

Had the query been ?- anc(dasharath, W)., composing θ1...θ4 and restricting to W would yield W = ram first (via a1), then W = lav on backtracking — practise extracting the answer substitution, it is a frequent follow-up question.

3.8 Why the occurs check belongs to this story

Soundness of SLD resolution is proved assuming unification with the occurs check. Standard Prolog skips it (unifying X with f(X) builds a cyclic term), trading a sliver of soundness for speed on the overwhelmingly common safe cases. Mention this caveat whenever you claim "Prolog is sound" — it is the examiner's favourite nuance.

3.9 The four execution outcomes of a query

The third row is the practical face of incompleteness: the answer may sit on a branch to the right of an infinite one, and depth-first search never gets there. Reordering clauses/goals — pure control, no change of logic — fixes it.

3.10 Negation as failure — the boundary cases

\+ G is not logical negation; it is "G is not provable from this database". Two consequences worth quoting:

1. Non-monotonicity: adding the fact married(ram) can destroy the previously derivable bachelor(ram). Classical logic never loses conclusions when axioms are added; CWA-based reasoning does.
2. The unbound-variable trap:

?- \+ married(X), male(X).      % WRONG order: \+ married(X) asks
                                 % "is there NO married individual at all?"
?- male(X), \+ married(X).      % RIGHT: X is bound first, then tested

Rule of thumb (worth a mark every time): call \+ only on ground goals — place it after the goals that bind its variables.

Exam pointers

• "Describe the abstract interpreter / computation model of logic programs" — reproduce the 5-step loop of §3.1, then name the two parameters: computation rule (which goal) and search rule (which clause).
• "Draw the SLD tree for query Q" — label every edge with the clause used and the MGU; mark success/failure leaves; state which answers depth-first search finds and in what order.
• "Soundness vs completeness of Prolog" — the §3.3 statements plus the occurs-check caveat (§3.8) and the infinite-branch example.
• "Explain negation as failure with the closed-world assumption" — definition, bachelor example, the two §3.10 caveats.

Self-check

1. Define: resolvent, SLD refutation, computed answer substitution, Herbrand universe.
2. Draw the SLD tree for ?- member(X, [1,2]). and list the answers in order.
3. Give a program + query pair where the SLD tree contains a success node that Prolog never reaches.
4. Why must clause variables be renamed apart at every resolution step? Construct the bug that occurs otherwise.
5. Evaluate: is \+ \+ p(X) the same as p(X)? What bindings survive?