The Logic Paradigm

A logic program is built from terms: constants (`tom`, `42`), variables (`X`, `Y`), and compound terms (`parent(tom, bob)`, `f(X, g(Y))`). A fact is a clause with no body, asserting something unconditionally true, e.g. `parent(tom, bob).` A rule has a head and a body, read as "head holds if body holds," e.g. `grandparent(X, Z) :- parent(X, Y), parent(Y, Z).` Facts and rules are both special cases of Horn clauses: at most one positive literal (the head), plus zero or more negative literals (the body), written in clausal form as `H :- B1, B2, ..., Bn`. A query (or goal) asks whether some statement follows from the program, e.g. `?- grandparent(tom, ann).`, possibly containing variables to be bound in the answer. The two central mechanisms that make this declarative reading executable are unification and resolution. Unification is the algorithm that decides whether two terms can be made syntactically identical by substituting terms for variables, and if so computes the most general unifier (mgu) — the least-committal such substitution. Resolution is the inference rule that, given a goal matching the head of a clause (via unification), replaces the goal with the clause's body, carrying the unifier forward. Repeated resolution steps, restricted to the specific strategy called SLD-resolution (Selective Linear Definite clause resolution), form a derivation; a derivation ending in the empty goal is a proof, and the composed substitutions along the way give the answer. Because a goal can unify with more than one clause head, resolution is nondeterministic: at each step there may be several applicable clauses. Real implementations resolve this with backtracking search, conventionally depth-first and left-to-right (try clauses in program order, subgoals in body order), which turns the search space into an explicit tree — the SLD-tree — that the interpreter explores, retreating on failure to try the next alternative. This combination of unification, resolution, and chronological backtracking is what a Prolog-like system actually executes; understanding it precisely is the payoff of this article.

Unification. Two terms unify if there is a substitution σ (a finite mapping from variables to terms) such that applying σ to both terms yields syntactically identical results. The classical algorithm (Robinson's algorithm, refined by Martelli–Montanari into a near-linear version) works by maintaining a set of equations to solve and a substitution built so far. ``` function UNIFY(t1, t2):

# returns a substitution (mgu) or FAIL stack = [(t1, t2)] subst = {} # empty substitution while stack is not empty: (a, b) = stack.pop() a = APPLY(subst, a) b = APPLY(subst, b) if a == b: # identical constants/variables/atoms continue else if a is a variable: if a occurs in b: # occurs check (optional; see below) return FAIL subst = COMPOSE(subst, {a -> b}) else if b is a variable: stack.push((b, a)) # swap and retry else if a and b are compound terms: if FUNCTOR(a) != FUNCTOR(b) or ARITY(a) != ARITY(b): return FAIL for i in 1 .. ARITY(a): stack.push((ARG(a, i), ARG(b, i))) else: return FAIL # e.g. two different constants return subst ``` `COMPOSE` applies the new binding to the existing substitution's range and adds the new pair; `APPLY` substitutes a term's variables according to the current substitution. Standard Prolog implementations skip the occurs check by default for efficiency, trading soundness (you can build a term that "contains itself", e.g. unifying `X` with `f(X)`) for speed; this is a documented, deliberate design tradeoff.

SLD-resolution and the interpreter loop. Given a goal list (initially the query's literals) and a program (an ordered list of clauses), the interpreter repeatedly picks the leftmost goal, tries clauses in program order, and on a unifying clause replaces that goal with the clause's body (renamed with fresh variables to avoid name clashes), applying the mgu to the rest of the goal list. ``` function SOLVE(goals, program, subst): if goals is empty: yield subst # success: report this answer return goal = FIRST(goals) rest = REST(goals) for clause in program: # try clauses in program order (head, body) = RENAME_FRESH(clause) # fresh variables per attempt mgu = UNIFY(goal, head) if mgu != FAIL: newGoals = APPEND(body, rest) newSubst = COMPOSE(subst, mgu) yield from SOLVE(newGoals, program, newSubst)

# on backtracking, control returns here and the loop tries

# the NEXT clause -- this is exactly what gives multiple answers ``` `RENAME_FRESH` is essential: each use of a clause must get its own copy of its variables, so that resolving `parent(X, Y)` against two different subgoals does not accidentally conflate unrelated `X`s. The `yield`/backtrack structure is depth-first, left-to-right: it explores the first successful branch fully (and any branches nested inside it) before returning to try the next sibling clause — precisely the standard Prolog search order. The cut operator (`!`), found in real Prolog systems, prunes this search: once execution passes a cut, the interpreter commits to the choices made so far in the current clause and discards remaining alternative clauses for the enclosing goal. It is an operational, non-logical escape hatch layered on top of the pure declarative model, added for efficiency and control — and a classic source of subtle bugs, discussed below.

Unification complexity. The naive algorithm above, without the occurs check, has worst-case time complexity that depends on term representation. A structure-sharing (DAG) representation, together with the Martelli–Montanari refinement, achieves O(n) where n is the combined size of the two terms — each equation is processed once and substitutions are represented implicitly via union-find-like binding rather than eagerly rewritten. Naive substitution-based implementations that apply bindings eagerly by copying terms can degrade to O(n²) or worse, because a single variable binding can force rewriting of exponentially large terms if done carelessly. The occurs check, which guarantees soundness by rejecting circular bindings like `X = f(X)`, adds an extra traversal per variable binding; in the worst case this makes full-generality unification O(n²) (or with sophisticated shared structures, still roughly linear, but real Prolog systems mostly just omit it, trading soundness for the common case's speed).

Why omitting the occurs check is dangerous but usually harmless. Without the check, unifying `X` with `f(X)` succeeds and produces a rational tree (an infinite, cyclic term), which most operations never need to traverse fully; it becomes a correctness hazard only when a program explicitly ever tries to print, compare structurally, or otherwise traverse such a term to a fixpoint. Most useful logic programs never generate self-referential unifications, so in practice this optimization is safe; it is a documented unsoundness in the standard semantics, not a bug.

Correctness of SLD-resolution. The precise correctness statement is a soundness and completeness theorem relating the operational semantics (the SOLVE algorithm) to the declarative semantics (logical entailment in the least Herbrand model of the program, viewed as a first-order theory of Horn clauses).

• Soundness: if `SOLVE` succeeds on goal G with substitution σ, then Gσ is a logical consequence of the program P, i.e. P ⊨ Gσ. This holds because every resolution step is a valid instance of the resolution inference rule from first-order logic, which is itself sound.
• Completeness: if P ⊨ Gσ for some ground instance, then there exists an SLD-derivation (some sequence of clause choices) that succeeds and produces a substitution at least as general as σ. This is the SLD-resolution completeness theorem (a consequence of the general completeness of resolution for Horn-clause logic).

The crucial subtlety is that completeness is a statement about the existence of a successful branch in the SLD-tree, not about the specific depth-first, left-to-right search strategy finding it in finite time. Depth-first search can dive into an infinite branch (e.g., a recursive rule with no terminating case reachable) and never backtrack to a finite successful branch that lies to its right. So: SLD-resolution as a proof system is sound and complete; Prolog's specific search strategy is sound but not complete — it can loop forever even when a proof exists elsewhere in the tree. This is exactly analogous to how a sound and complete type system can still have an undecidable or non-terminating inference algorithm if implemented with the wrong search order, a tension familiar from Evaluation and Reduction of Expressions where reduction strategy (call-by-value vs. normal order) affects termination even when a normal form exists.

Complexity of query answering is therefore not a single number: it depends on the size of the SLD-tree actually explored, which depends on clause ordering, goal ordering, and backtracking depth — in the worst case exponential in the number of subgoals, since each may spawn multiple clause choices whose combinations multiply. This mirrors backtracking search generally: the branching factor is bounded by the number of clauses matching a predicate, and the depth is bounded by the recursion depth of the derivation, giving a worst-case bound of O(bᵈ) tree nodes for branching factor b and depth d, with the usual caveats that cuts and indexing can prune this dramatically in practice.

Consider this small program: ```prolog parent(tom, bob). parent(tom, liz). parent(bob, ann). parent(bob, pat). grandparent(X, Z) :- parent(X, Y), parent(Y, Z). ?- grandparent(tom, Z). ``` We trace `SOLVE([grandparent(tom, Z)], program, {})` by hand, showing each step's goal list, the clause tried, the resulting unifier, and the outcome.

Reading the trace: the interpreter first commits to `Y = bob` (Tom's first-listed child), finds `ann` as a grandchild, reports it, and — if the caller asks for more solutions (`;` in a Prolog REPL) — backtracks to find `pat` via the same `Y = bob` branch, then backtracks further to try `Y = liz`, which yields no grandchildren since `liz` has no listed children, and the whole search terminates having found exactly `{Z = ann, Z = pat}`. This demonstrates unification producing different bindings on each branch (not a "trivial symmetric" single-answer case), and shows backtracking recovering from the dead-end at `liz` rather than crashing or looping. Now trace unification itself on the first clause application, to see the algorithm's internal state:

This matches step 1's claimed unifier exactly, confirming the hand-trace is consistent with the formal `UNIFY` procedure.

The logic paradigm grew out of automated theorem proving research seeking to make resolution — a general inference rule for first-order logic discovered in the early 1960s — practical as a programming mechanism rather than just a proof-search technique.

Warren's abstract machine deserves particular note: it showed that the elegant but seemingly slow unification-and-backtracking model could be compiled to an efficient low-level instruction set, much as the Evaluation and Reduction of Expressions machinery for functional languages was later compiled to abstract machines like the SECD or STG machine — a recurring theme that declarative elegance and efficient execution are not in tension once the right intermediate representation is found.

Prolog and its descendants remain the direct ancestors of modern constraint logic programming systems used in scheduling, planning, and combinatorial optimization, where facts and rules naturally express constraints and the solver's search is the constraint propagation engine. Datalog, a terminating, function-symbol-free fragment of the same paradigm, is the logical core of modern deductive database query optimizers and, notably, of large-scale static analysis and security tools that express points-to analysis, taint tracking, and access-control policies as sets of Datalog rules evaluated over enormous fact databases. Rule-based expert systems and business-rule engines used in finance, insurance, and healthcare compliance are direct descendants of the fact-and-rule model. Prolog-style unification is also embedded, in disguise, inside every language with algebraic pattern matching and inside type inference algorithms — Hindley–Milner type inference is itself, at its core, a unification algorithm over type terms, tying this paradigm directly back to Type Systems. Even SQL query planners and modern build systems that resolve dependency graphs by declarative rule satisfaction owe a conceptual debt to SLD-resolution's model of goal-directed proof search.

Ask the tutor: How does Prolog's Warren Abstract Machine compile unification and backtracking into efficient low-level instructions?