Resolution and SLD: How a Machine Proves

📍 Where we are: Part II · Reasoning as Computation — Chapter 6. Inference and Proof ran the rules forward, firing every rule until the whole model appeared; now we run them backward, starting from a single question and chasing it down to the facts.

Forward chaining answered a question we never asked: it computed everything the academic world's rules could derive, all 47 atoms, whether or not we cared about any particular one. But most of the time you arrive with one question, not a wish for the entire universe of consequences. Is alice carol's grand-advisor? Who are alice's colleagues? This chapter is about the reasoning that starts from exactly such a goal and works backward, asking which rule could possibly conclude it, then what that rule would in turn require, until the demand bottoms out in facts you already have. The trace it leaves behind is not a yes-or-no; it is a proof tree you can read line by line.

We will not treat "the machine proved it" as a black box. We will define unification precisely and trace its inner loop as the substitution dictionary fills in, read a rule as the logical formula it stands for, derive the single resolution step that turns one goal into its subgoals, run a full proof as a sequence of goal lists collapsing to the empty clause, and tie every equation to the exact line of the companion code that executes it. By the end you will be able to read sld.py and see a proof procedure, not a script.

The simple version

Imagine proving you are descended from someone famous. You do not list every person who ever lived and check which are your ancestors — that is the forward, compute-everything way. Instead you work backward from the claim: "I descend from her if one of my parents does; which parent, and can I show that?" Each "if" hands you a smaller question about someone one step closer, and you keep going until you hit a birth certificate you can point at. Backward chaining is that habit made mechanical: start from what you want to prove, ask which rule could conclude it, and recurse on what the rule needs, stopping when every branch lands on a recorded fact.

What this chapter covers

• Goal-directed proof — why starting from the question and working backward to the facts is often smarter than deriving everything, and how it turns proving into a search.
• Unification, the shared primitive — a precise definition of substitution, unifier, and most general unifier, the twenty-line unify.py primitive, and a line-by-line trace of its loop filling in a binding dictionary.
• The SLD resolution step, derived — a rule read as the logical clause it abbreviates, the single resolution step that replaces a goal with its instantiated body, why deriving the empty clause is a proof, and the core loop of sld.py where this happens.
• A worked proof, as a resolvent sequence — the full goal-list-to-empty-clause derivation for grandAdvisor(alice, carol), the rendered proof tree, and the recursive, backtracking derivation for citesTransitively(p3, p1).
• Query answering — the search tree for "colleagues of alice," including the branch the inequality guard kills, and every binding a query enumerates, quoted from the real run.
• Forward versus backward — when computing all consequences wins and when chasing one goal wins, and a well-founded-descent argument for exactly why the backward search terminates here.

Goal-directed proof: start from the question

The previous chapter, Inference and Proof, computed the least fixpoint by firing every rule over and over until nothing new appeared, the chase, forward from the facts. Backward chaining inverts the arrow. You hand it a goal, an atom you want to establish, like ("grandAdvisor", "alice", "carol"), and it asks a single question: which rule has a head that could conclude this goal? Every such rule offers a bargain: "I will give you the goal, but first you must prove my body." So the one goal is replaced by the rule's body atoms, each of which becomes a new sub-goal, and the process repeats. A branch succeeds when it reaches a fact, a rule with an empty body, nothing left to prove [1]. This is the strategy behind Prolog (short for Programming in Logic), and its formal name is SLD resolution, for Selective Linear resolution for Definite clauses, a specialization of J. A. Robinson's general resolution rule to the Horn clauses (definite clauses) our rules already are [2][3].

The reason to prefer it is economy, and it is measurable on the running example. Forward chaining reaches the whole model in three waves whose sizes grow and then hold, [23, 41, 47, 47]: 23 base facts, then 41, then 47, then 47 again with nothing new added. To answer "is alice carol's grand-advisor?" that way, you would materialize all 24 derived atoms ($47 - 23 = 24$, where $|\cdot|$ counts atoms in a set) and then look yours up. Backward chaining, as we will see step by step, touches exactly three atoms. Proving becomes a search directed by the question, and the search visits only what the question needs.

Unification: the primitive that decides a match

Both engines rest on one operation, and it is worth meeting on its own, with its definitions made exact before we read the code.

Fix the vocabulary. An atom is a tuple (predicate, arg1, arg2, ...), for example ("advises", "alice", "bob"). A term is one argument: a string that is a variable if it starts with an uppercase letter (X, Y, Who) and a constant otherwise (alice, carol, mit). That single convention is decided in one place, is_var at lines 25–28 of kb.py. A substitution $\sigma$ (the Greek letter sigma) is a finite map from variables to terms, written $\sigma = \{X \mapsto \text{alice},\ Z \mapsto \text{carol}\}$, where the arrow $\mapsto$ reads "is replaced by." Applying $\sigma$ to an atom means replacing every variable in the atom by whatever $\sigma$ maps it to; that is precisely apply_sub at lines 46–48 of unify.py. We write $A\sigma$ for "the atom $A$ with substitution $\sigma$ applied."

Now the operation. Given two atoms $A$ and $B$, a unifier is a substitution $\sigma$ that makes them literally identical: $A\sigma = B\sigma$. Two atoms may have many unifiers or none. When one exists, there is a canonical cheapest one, the most general unifier (MGU): a unifier $\sigma$ such that every other unifier can be obtained from $\sigma$ by binding still more variables, so $\sigma$ commits to nothing it does not have to. Unification is the procedure that returns the MGU when the atoms can be matched and fails otherwise [1]. Here is the whole primitive, from unify.py:

def unify(a: tuple, b: tuple, sub: dict | None = None) -> dict | None:
    sub = {} if sub is None else dict(sub)
    if a[0] != b[0] or len(a) != len(b):
        return None
    for x, y in zip(a[1:], b[1:]):
        x, y = walk(x, sub), walk(y, sub)
        if x == y:
            continue
        if is_var(x):
            sub[x] = y
        elif is_var(y):
            sub[y] = x
        else:
            return None  # two different constants — clash
    return sub

Read it as three rules. First (line 31 above, the guard), the predicate name and the arity (the argument count, len(a)) must agree, or the atoms cannot match at all and the function returns None. Then, argument by argument (the loop, lines 33–42): if the two are already equal, move on; if one side is a variable, bind it to the other by writing an entry into the dictionary (sub[x] = y, line 38); and if both sides are distinct constants, that is a clash, and unify returns None. The helper walk (lines 16–20) first follows any bindings already made, so once X is bound to alice it stays alice for the rest of the match, which is what keeps the MGU consistent with itself.

The loop, traced

Watch the dictionary fill in. Unify the rule head grandAdvisor(X_1, Z_1) (its variables already stamped apart, on which more below) with the goal grandAdvisor(alice, carol). Each row is one pass through the loop:

step in unify.py	comparison	outcome	sub afterward
guard, line 31	predicate grandAdvisor = grandAdvisor, arity $3 = 3$	pass	$\{\}$
loop iter 1, lines 33–42	x = X_1, y = alice; unequal; is_var(X_1) true	bind, line 38	$\{X_1 \mapsto \text{alice}\}$
loop iter 2, lines 33–42	x = Z_1, y = carol; unequal; is_var(Z_1) true	bind, line 38	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$
return, line 43	loop exhausted	return sub	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$

The result is the rule head dressed up as the exact goal we asked about: applying $\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$ to grandAdvisor(X_1, Z_1) yields grandAdvisor(alice, carol), and it commits to nothing more, so it is the MGU. Contrast the failing case, which is just as short. Unifying the goal advises(alice, carol) against the fact advises(alice, bob): iteration one compares alice with alice, equal, continue; iteration two compares the two distinct constants carol and bob, neither a variable, so the final else fires and unify returns None (line 42). That single clash is why provable(("advises", "alice", "carol")) comes back False: alice advises only bob, and no substitution can make carol equal bob.

Why is this the simple version of a famously subtle operation? Because our language has no function symbols: it is Datalog, the function-free fragment of logic programming. In full first-order logic a term can be nested, like f(g(X)), and unification must run an occurs-check to refuse binding a variable to a term that contains it, which would otherwise spin up an infinite structure. Here every argument is a flat constant or variable, so there is nothing to nest, no occurs-check, and no way to build a term larger than the ones you started with. Only finitely many atoms can ever be formed from the fixed constants of the academic world, a finite Herbrand base. That finiteness is what makes forward chaining stop; backward SLD is subtler, and we return to why it too terminates here at the end of the chapter, for a different reason than the Herbrand base.

The SLD resolution step, derived

Before the engine, read a rule as the logic it abbreviates, because the whole method is one logical step applied over and over. The grand-advisor rule at line 79 of kb.py,

$$\text{grandAdvisor}(X, Z) \leftarrow \text{advises}(X, Y)\ \wedge\ \text{advises}(Y, Z),$$

uses three connectives a first-year reader should have decoded once and for all. The arrow $\leftarrow$ reads "if": the head on the left holds if the body on the right does. The wedge $\wedge$ reads "and." Later we will meet $\vee$ ("or") and $\neg$ ("not"). Logically, "$H$ if $B_1$ and $B_2$" is the same statement as "$H$, or else not-$B_1$, or else not-$B_2$," that is $H \vee \neg B_1 \vee \neg B_2$. A clause of this shape, with exactly one positive atom $H$, is a definite clause (a Horn clause), and every rule in kb.py is one.

A goal, or query, is written $\leftarrow G_1 \wedge \cdots \wedge G_m$ with an empty head. Read logically it is the flat denial $\neg(G_1 \wedge \cdots \wedge G_m)$: "these cannot all hold at once." That framing is the key to resolution. To prove that the program $P$ entails the goal, written $P \models G_1 \wedge \cdots \wedge G_m$ (the double turnstile $\models$ reads "logically entails," meaning true in every model of $P$), we assume the denial and hunt for a contradiction. If adding $\neg(G_1 \wedge \cdots)$ to $P$ lets us derive the always-false empty clause, written $\square$, then $P$ together with the denial is unsatisfiable, so $P \models G_1 \wedge \cdots \wedge G_m$ after all. This is proof by refutation, and the foundational insight is that a single inference rule, resolution, suffices to drive it [2]. We write $P \vdash G$ (the single turnstile $\vdash$ reads "derives," a fact about the procedure) when the procedure finds such a refutation, and soundness is the guarantee that $P \vdash G$ implies $P \models G$.

The SLD step is this. Take the current goal list (the resolvent) $\leftarrow A_1 \wedge \cdots \wedge A_m$, select one atom $A_i$ (Prolog and sld.py always select the leftmost, $A_1$; this leftmost choice is the S, the Selective part of the name, its selection function), and pick a rule $H \leftarrow B_1 \wedge \cdots \wedge B_n$ whose head unifies with it, $\sigma = \text{unify}(H, A_i)$. The L, Linear, names something else entirely: the shape of the derivation, in which each new resolvent is obtained by resolving the previous one against a single program clause, a chain rather than a branching combination of clauses. Replace the selected atom by the rule's body and apply the unifier to everything:

$$\leftarrow (A_1 \wedge \cdots \wedge A_{i-1}\ \wedge\ B_1 \wedge \cdots \wedge B_n\ \wedge\ A_{i+1} \wedge \cdots \wedge A_m)\,\sigma.$$

Each such step is a sound logical inference, and the one-line reason is worth showing rather than merely citing. Recall a resolvent is a denial: the old one asserts the clause $\neg A_1 \vee \cdots \vee \neg A_m$, the rule asserts $H \vee \neg B_1 \vee \cdots \vee \neg B_n$, and we chose $\sigma$ so that $H\sigma = A_i\sigma$. Take any model $M$ (any assignment of truth to the ground atoms) that satisfies both, after $\sigma$ is applied. Split on the selected atom. Either $M$ makes $A_i\sigma$ true, in which case the disjunct $\neg A_i\sigma$ of the old denial is false, so the old denial can hold only because some other $\neg A_j\sigma$ is true; or $M$ makes $A_i\sigma$, hence $H\sigma$, false, in which case the rule can hold only because some $\neg B_k\sigma$ is true. Either surviving disjunct is itself a disjunct of the new resolvent, so $M$ satisfies the new resolvent as well: the new resolvent is entailed by the old one together with the rule [2]. A fact is a rule with $n = 0$ body atoms, so resolving against a fact simply deletes the selected atom (there is no body to splice in). When the resolvent becomes empty, every atom has been deleted, and that empty resolvent is the empty clause $\square$: the refutation is complete and the goal is proved. The substitution you accumulate along the way, the composition $\sigma = \sigma_k \circ \cdots \circ \sigma_1$ of the unifiers used at each step (the ring $\circ$ reads "composed with," meaning apply the earlier binding, then the later one), is the answer: the bindings that make the original goal true.

Now the engine, and every clause of the definition above appears in it. Given the current list of goals, sld.py takes the first one and tries each rule in turn:

    goal, rest = goals[0], goals[1:]
    g = apply_sub(goal, sub)
    ...
    for rule in rules:
        head, body = rename(rule, counter)
        s = unify(head, g, sub)
        if s is None:
            continue
        for s_body, body_proofs in _solve(body, s, rules, counter):
            this = Proof(apply_sub(g, s_body), body_proofs)
            for s_rest, rest_proofs in _solve(rest, s_body, rules, counter):
                yield s_rest, [this] + rest_proofs

Match this against the derivation. goal, rest = goals[0], goals[1:] (line 42) is leftmost selection: $A_1$ is goal, and $A_2 \wedge \cdots \wedge A_m$ is rest. unify(head, g, sub) (line 54) computes the unifier $\sigma$, returning None exactly when no step is possible with this rule, in which case continue moves to the next rule (that is backtracking). _solve(body, s, ...) (line 57) proves the spliced-in body $B_1 \wedge \cdots \wedge B_n$, and _solve(rest, s_body, ...) (line 59) proves the leftover goals $A_2 \wedge \cdots \wedge A_m$, both under the extended substitution: together they are the new resolvent. And the base case that stops the recursion is the empty clause itself:

def _solve(goals: list, sub: dict, rules: list, counter: list):
    """Yield ``(substitution, [proofs])`` for every way to prove all ``goals``."""
    if not goals:
        yield sub, []
        return

if not goals: (lines 39–41) is the line "$\square$, success": no goals remain, so yield the accumulated substitution and an empty list of proofs. One more piece earns its keep. Before each use, rename (lines 51–64 of unify.py) stamps a fresh numeric suffix onto every variable in the rule, turning the file's X into X_1, X_2, and so on. This is the standardize-apart discipline, and it is not cosmetic: without it, two uses of the same rule in one proof (or a recursive rule invoking itself) would accidentally share a variable, and a binding forced on one use would wrongly constrain the other [1]. One caveat on notation: the suffix _1 written throughout the traces here (and the _2 distinguishing R1 from R2 below) is illustrative, not a captured value. Because rename shares one counter across every rule and fact it tries, the actual integer is order-dependent and usually larger. In a real run of grandAdvisor(alice, carol), the counter has already been bumped past the 23 facts and the earlier rules skipped on the way in, so the head is stamped X_27, Z_27. Only the freshness of the name matters, never the particular number, which is why the traces write the simplest _1.

A proof as a resolvent sequence

Here is the full derivation for grandAdvisor(alice, carol), written the way the definition prescribes: a sequence of resolvents, starting from the query and collapsing to $\square$. Facts are folded into the rule set as empty-body clauses (line 72 of sld.py: all_rules = [(fact, []) for fact in facts] + list(rules)), so a fact match is just an SLD step with $n = 0$.

#	resolvent (goals still to prove)	selected atom	clause used (renamed)	MGU at this step	answer $\sigma$ so far
0	$\leftarrow \text{grandAdvisor}(\text{alice}, \text{carol})$	grandAdvisor(alice, carol)	$\text{grandAdvisor}(X_1, Z_1) \leftarrow \text{advises}(X_1, Y_1) \wedge \text{advises}(Y_1, Z_1)$	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$
1	$\leftarrow \text{advises}(\text{alice}, Y_1) \wedge \text{advises}(Y_1, \text{carol})$	advises(alice, $Y_1$)	$\text{advises}(\text{alice}, \text{bob}) \leftarrow$ (fact)	$\{Y_1 \mapsto \text{bob}\}$	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol},\ Y_1 \mapsto \text{bob}\}$
2	$\leftarrow \text{advises}(\text{bob}, \text{carol})$	advises(bob, carol)	$\text{advises}(\text{bob}, \text{carol}) \leftarrow$ (fact)	$\{\}$ (already ground)	unchanged
3	$\square$ (empty)	—	—	—	success

Step 0 is the rule loop firing on the only rule whose head unifies. Step 1 splices in the body and immediately resolves its first atom against a fact, binding $Y_1 \mapsto \text{bob}$; note how that binding propagates, so the second body atom, still advises(Y_1, carol) at step 1, has become the ground advises(bob, carol) by step 2. Step 3 is the base case if not goals. The proof visited exactly the three atoms grandAdvisor(alice, carol), advises(alice, bob), advises(bob, carol), against the two dozen forward chaining would have built.

The proof tree: an auditable trace

Because a success is built as a tree of Proof nodes (the class at lines 19–34 of sld.py) rather than a single boolean, we can print the reasoning. A Proof stores the goal it proved and the list of sub-proofs of the body that established it; render (lines 29–34) walks it with increasing indentation. Running sld.py proves the goal and renders it:

p = prove(("grandAdvisor", "alice", "carol"))
print("proof of grandAdvisor(alice, carol):")
print(p.render(1) if p else "  (unprovable)")

proof of grandAdvisor(alice, carol):
  grandAdvisor(alice, carol)
    advises(alice, bob)
    advises(bob, carol)

That is the resolvent sequence above, folded back into a tree: the goal at the root, and its two indented children the facts that established it, which are precisely the two body atoms after $\sigma$ was applied. This is a faithful proof trace: every step is a real unification against a real rule or fact, so the conclusion is auditable, not asserted [3].

The proof tree SLD resolution builds for grandAdvisor(alice, carol): the goal at the root, the rule that concludes it with its unifying substitution, and two body goals that bottom out in base facts — an auditable trace, not just a yes. Original diagram by the authors, created with AI assistance.

Recursion and backtracking, traced

The tree grows taller when a rule's body invokes the same rule. The citation rules at lines 86–88 of kb.py are the interesting case, because the second one calls citesTransitively in its own body:

$$\begin{aligned} &\text{R1:}\quad \text{citesTransitively}(A, B) \leftarrow \text{cites}(A, B),\\ &\text{R2:}\quad \text{citesTransitively}(A, C) \leftarrow \text{cites}(A, B)\ \wedge\ \text{citesTransitively}(B, C). \end{aligned}$$

Proving citesTransitively(p3, p1) shows both recursion and a dead branch that forces backtracking. The engine tries clauses in order:

1. R1 (renamed), fails. Unify $\text{citesTransitively}(A_1, B_1)$ with the goal: $\{A_1 \mapsto \text{p3},\ B_1 \mapsto \text{p1}\}$. Body becomes cites(p3, p1). But the citation facts are only cites(p2, p1) and cites(p3, p2) (lines 57–58 of kb.py); there is no cites(p3, p1). The single body atom cannot resolve, so this branch dies and continue (line 56) backtracks.
2. R2 (renamed), succeeds. Unify $\text{citesTransitively}(A_2, C_2)$ with the goal: $\{A_2 \mapsto \text{p3},\ C_2 \mapsto \text{p1}\}$. Body becomes cites(p3, B_2) $\wedge$ citesTransitively(B_2, p1).
   • cites(p3, B_2) resolves against the fact cites(p3, p2), binding $\{B_2 \mapsto \text{p2}\}$.
   • citesTransitively(p2, p1) recurses. This time R1 fires: its body cites(p2, p1) is a fact, so the sub-goal closes at once.

The rendered tree is exactly one level taller than the grand-advisor tree, matching the real output:

  citesTransitively(p3, p1)
    cites(p3, p2)
    citesTransitively(p2, p1)
      cites(p2, p1)

The dead R1 attempt on cites(p3, p1) does not appear in the printed tree, because only the successful path is recorded, but it is real work the search did and undid. That interplay, try a clause, fail, back up, try the next, is the whole of backward-chaining control flow, and it lives in the two lines if s is None: continue.

Query answering: enumerate every binding

Leaving a variable unbound in the goal turns a yes-or-no proof into a query: "for which values is this provable?" The answers function (lines 82–93) collects every substitution that proves the goal and reports the resulting ground atoms, each solution a binding of the goal's variables [3]. The companion asks for alice's colleagues:

print("colleagues of alice:", answers(("colleague", "alice", "Who")))

colleagues of alice: [('colleague', 'alice', 'bob')]

One answer, bob, and the search tree explains why exactly one survives. The rule (lines 82–83 of kb.py) is $\text{colleague}(X, Y) \leftarrow \text{affiliated}(X, I) \wedge \text{affiliated}(Y, I) \wedge \text{neq}(X, Y)$. Unifying its head with the goal colleague(alice, Who) binds $\{X_1 \mapsto \text{alice},\ Y_1 \mapsto \text{Who}\}$, so the body becomes three sub-goals: affiliated(alice, I_1), affiliated(Who, I_1), neq(alice, Who). Trace them left to right:

• affiliated(alice, I_1): alice's only affiliation fact is affiliated(alice, mit), so $\{I_1 \mapsto \text{mit}\}$.
• affiliated(Who, mit): two facts have mit as their second argument, affiliated(alice, mit) and affiliated(bob, mit), so the search branches into $Who \mapsto \text{alice}$ and $Who \mapsto \text{bob}$.
  • Branch $Who \mapsto \text{alice}$: the guard neq(alice, alice) is checked. In the code the guard fires only when both sides are non-variable and unequal; here they are equal, so the condition x != y is false, nothing is yielded, and the branch dies.
  • Branch $Who \mapsto \text{bob}$: the guard neq(alice, bob) passes ($\text{alice} \ne \text{bob}$), the resolvent empties, and colleague(alice, bob) is recorded.

That guard, neq, is the one non-fact predicate: it is not looked up in the knowledge base but checked by the engine, at lines 45–50 of sld.py:

    if g[0] == "neq":  # built-in inequality guard
        x, y = walk(g[1], sub), walk(g[2], sub)
        if not is_var(x) and not is_var(y) and x != y:
            for s2, proofs in _solve(rest, sub, rules, counter):
                yield s2, [Proof(g, [])] + proofs
        return

Backward chaining did not enumerate every pair of people; it started from alice, fixed her institution, and walked only the affiliations at mit that could satisfy the rule, pruning the reflexive pair the moment the guard saw it. The symmetry checks out: answers(("colleague", "bob", "Who")) returns [('colleague', 'bob', 'alice')], alice and bob being the only two at mit. The same machinery enumerates a fully open query. Asking answers(("grandAdvisor", "alice", "Z")) returns both grandAdvisor(alice, carol) and grandAdvisor(alice, dave), because alice advises bob, and bob advises both carol and dave; opening both arguments, answers(("grandAdvisor", "A", "B")), adds grandAdvisor(bob, erin) (bob advises carol, carol advises erin) for three grand-advising pairs in all. Each is a distinct successful branch of the same search, distinguished only by which facts its unifications landed on.

Forward versus backward: two directions, one meaning

We now have both engines, and they compute the same truths from opposite ends. Forward chaining pushes from the facts toward all conclusions; on the academic world it reaches the full model in three waves, the sizes growing and then holding steady:

least fixpoint reached in 3 rounds; sizes per round: [23, 41, 47, 47]
47 atoms total, 24 derived.

Every one of the 24 derived atoms is materialized whether or not anyone wants it. Backward chaining does the opposite: the proof it builds for grandAdvisor(alice, carol) depends on just three atoms, and it bottoms out there. The trade is clear. Forward chaining wins when you will ask many questions against a stable set of facts, since you derive everything once and then answer each query by lookup, which is exactly how a Datalog database materializes its rules. Backward chaining wins when you have one goal, or a goal with variables to fill, and no wish to compute the rest of the universe to answer it; it is also what naturally yields a proof tree, since it records why each goal held [1].

Both directions terminate on this program, but for different reasons, a distinction worth getting right. Forward chaining stops because the finite Herbrand base caps its monotone operator: a set that cannot grow past a fixed finite ceiling forces the iteration to a halt, which is exactly what [23, 41, 47, 47] shows, growth then a fixed point. Backward SLD carries no such guarantee in general. The engine in sld.py keeps no memory of goals it has already attempted, so a recursive rule over cyclic data could re-derive the same finite atoms forever and never return; a finite Herbrand base does not by itself prevent that loop. (Real Prolog systems add tabling, also called SLG resolution, precisely to catch it, by remembering already-tried goals.)

So why does the backward search terminate here? Because the recursion has a well-founded measure that strictly decreases at every recursive call. The relation cites is acyclic: the citation facts form the chain $\text{p3} \to \text{p2} \to \text{p1}$ with no way back. Assign each paper a rank equal to the length of the longest citation path leading out of it:

$$\text{rank}(\text{p1}) = 0, \qquad \text{rank}(\text{p2}) = 1, \qquad \text{rank}(\text{p3}) = 2.$$

Because a longest path out of $B$, prefixed by an edge $A \to B$, is a path out of $A$, any citation edge forces $\text{rank}(B) \lt \text{rank}(A)$. Rule R2 recurses only on citesTransitively(B, C) where cites(A, B) was just established, so the first argument's rank drops by at least one on every recursive step. A strictly decreasing sequence of non-negative integers cannot be infinite, so the recursion depth is bounded (here by $\text{rank}(\text{p3}) = 2$, which is why the deepest tree in this chapter is three atoms tall), and the backward search halts. Acyclic data, not the finite Herbrand base, is what saves plain SLD on this program.

The unsolved part

SLD resolution is only as good as its matching, and its matching is brittle by design. Unification succeeds only on an exact symbolic match: advises unifies with advises, never with mentors or supervises, even though a human sees those as near-synonyms, and two distinct constants simply clash, as we watched carol and bob do. If a fact is phrased a hair differently from the rule, or is missing from the knowledge base entirely, the proof branch dies, and no near-miss can rescue it. That is the price of certainty: every proof is airtight, but only over exactly the symbols written down. The open question the later volumes take up is whether a machine can keep the shape of this reasoning, goals, rules, recursion, proof trees, while relaxing the all-or-nothing match. Volume 4's neural theorem proving answers with soft unification: represent each symbol as a vector, and replace the hard equality test x == y on line 35 of unify.py with a similarity score, so advises and mentors can match to the degree their embeddings are close. The proof tree survives, but it now carries a confidence rather than a guarantee, trading the certainty of exact matching for the ability to prove things across the near-misses and gaps that defeat a purely symbolic engine.

Why it matters

SLD resolution is the crisp target that every "differentiable prover" in this series is trying to imitate. Neuro-symbolic systems are, in large part, attempts to keep the two virtues on display here, goal-directedness (chase only what the question needs) and auditability (leave a proof tree, not just an answer), while surviving the noise, synonymy, and incompleteness that break exact matching. You cannot tell whether a neural prover is faithful without knowing what the symbolic proof should have been, and this chapter is that reference: the exact substitution unification finds, the exact resolvent sequence resolution walks, the exact bindings a query returns. When Volume 4 softens unify into vector similarity, the thing it is softening is the twenty lines you just traced.

Key terms

• Backward chaining — proving a goal by asking which rule could conclude it and recursing on that rule's body, stopping when every branch reaches a fact; the opposite direction from forward chaining.
• SLD resolution — Selective Linear resolution for Definite clauses: Robinson's resolution rule specialized to Horn clauses, the proof procedure behind Prolog.
• Definite (Horn) clause — a rule $H \leftarrow B_1 \wedge \cdots \wedge B_n$ with exactly one positive head atom; logically $H \vee \neg B_1 \vee \cdots \vee \neg B_n$.
• Goal / query — a headless clause $\leftarrow G_1 \wedge \cdots \wedge G_m$, read as the denial of what we want to prove; leaving a variable in it enumerates every binding that proves it.
• Resolvent — the current list of goals still to prove; each SLD step replaces the selected atom by an instantiated rule body, and reaching the empty resolvent $\square$ completes the refutation.
• Refutation ($P \vdash G$, $P \models G$) — proving $G$ by assuming its denial and deriving the empty clause; soundness is that a derivation ($\vdash$) implies entailment ($\models$).
• Unification / unifier / MGU — the operation that finds the most general substitution making two atoms identical, or fails (a clash) when it cannot.
• Substitution — a map from variables to terms, written with $\mapsto$; a binding is one such variable-to-term entry, and $\circ$ composes substitutions along a proof branch.
• Occurs-check — the guard, needed only with function symbols, that stops a variable from being bound to a term containing it; unnecessary in function-free Datalog.
• Standardize apart (rename) — stamping a rule's variables with fresh names before use so two applications of one rule never share a variable.
• Proof tree — the nested record of goals and the sub-goals that established them; an auditable trace, not just a truth value.
• Herbrand base — the finite set of ground atoms formable from a program's constants; its finiteness is why forward chaining terminates, while backward SLD relies on acyclic data (a well-founded rank) or tabling instead.
• Tabling (SLG resolution) — the loop-checking discipline real Prolog adds to plain SLD, remembering already-tried goals so recursive rules over cyclic data cannot spin forever.
• Soft unification — Volume 4's replacement of exact symbol equality with vector similarity, so near-synonyms match to a degree, trading certainty for reach.

Where this leads

We have watched reasoning run both directions, forward to the whole model, backward to a single proof, and both times something settled: the forward chase stopped growing at 47 atoms, and the backward search bottomed out in facts once its rank could fall no further. The next chapter, Fixpoints: Reasoning as Reaching a Limit, names the mathematics under that settling: the immediate-consequence operator, the least fixpoint it climbs to, and the order-and-lattice theory that guarantees such a limit always exists and is unique. It is the formal reason "keep applying the rules until nothing changes" is not a hope but a theorem, and the shape Volume 2's description-logic reasoner will reuse.