Horn clauses & the Prolog interpreter

From general resolution to something fast

General resolution is complete but exponential. Prolog buys tractability by restricting the language to Horn clauses, and this single restriction is the design decision that turns logic into a programming language.

What a Horn clause is

A Horn clause contains at most one positive literal. That restriction yields exactly three shapes, which map one-to-one onto Prolog:

• Fact — a single positive literal, no body: $a\leftarrow$. In Prolog: parent(tom, bob). An unconditional assertion.
• Rule — one positive head, one or more body conditions: $a\leftarrow b_1\wedge \cdots \wedge b_n$. In Prolog: grandparent(X,Z) :- parent(X,Y), parent(Y,Z). Read declaratively: "$a$ is true if all of $b_1\dots b_n$ are."
• Goal (headless clause) — no positive literal, a conjunction of goals to satisfy: $\leftarrow b_1\wedge \cdots \wedge b_n$. In Prolog: ?- grandparent(tom, ann). This is the negated query — exactly the negated goal you add in resolution refutation.

Not everything fits: $p\vee q$ has two positive literals and no Horn form. But most practical knowledge does, and the payoff is huge — Horn-clause databases support an efficient linear input form, unit preference, left-to-right, depth-first refutation that is refutation-complete (van Emden & Kowalski, 1976).

How the interpreter runs

Given a goal clause $\leftarrow a_1\wedge \cdots \wedge a_n$, the Prolog interpreter:

1. Selects the leftmost goal $a_1$ (left-to-right).
2. Scans the program top-to-bottom for the first clause whose head unifies with $a_1$.
3. On a match, replaces $a_1$ with that clause's body (its subgoals go to the front of the goal list). The goal list behaves as a stack, which is what makes the search depth-first.
4. On failure, backtracks to the most recent choice point and tries the next matching clause.

So Prolog is resolution: unifying a goal with a clause head and replacing it with the body is one linear-input resolution step. Clause order and goal order are not logically meaningful in pure logic — but in Prolog they control the search, which is why "the same program in a different clause order" can loop forever or terminate.

Three things Prolog assumes (and the cut)

Prolog quietly enforces three axioms: the unique name axiom (distinct names = distinct individuals), the closed-world axiom (anything not provable is taken to be false — this is negation as failure, \+), and the domain closure axiom (the only individuals are those named in the database). The closed-world assumption is powerful but dangerous: unknown gets treated as false.

The cut (!) prunes backtracking — once crossed, it commits to the current clause choice and all bindings made before it. Cut makes programs faster and lets you express "don't reconsider," but it sacrifices the guarantee of finding all solutions (or even an alternative solution that exists down another path).