Inference in First-Order Logic

First-order logic gave us a language with variables, quantifiers, functions, and relations — enough to say all greedy kings are evil in one sentence instead of one per king. The question this lesson answers is procedural: given a knowledge base written in that language and a query, how does a machine decide whether the query follows? The propositional machinery of the previous module already gives sound and complete inference for the quantifier-free case.¹ The whole task is to lift it to sentences that quantify over objects — and the single piece of new machinery that makes the lift work is unification, the algorithm that makes two terms match.

Lifting propositional inference

Start with the standard folkloric axiom, that greedy kings are evil,

together with the facts $King(John)$ and $Greedy(John)$. A human sees at once that $Evil(John)$ follows. To make a machine see it, the first idea is to strip the quantifier by substituting ground terms for the variable.

Substituting $\{x/John\}$ turns the axiom into the propositional implication $King(John)\wedge Greedy(John)⟹Evil(John)$, and now propositional modus ponens finishes the job. Existentials are handled by a dual rule, but with a twist: the object the existential asserts must be given a fresh name.

From $\exists xCrown(x)\wedge OnHead(x,John)$ we may infer $Crown(C_1)\wedge OnHead(C_1,John)$ as long as $C_1$ is new. Giving the object the name of an existing constant — say $\pi$, when we only know some number just above $2.71828$ exists — would assert a falsehood.² Universal instantiation can be applied repeatedly and the original kept; existential instantiation is applied once and the existential discarded. The result is not logically equivalent to the original, but it is inferentially equivalent: satisfiable exactly when the original is.

Applying universal instantiation to every ground term reduces first-order inference to propositional inference — a technique called propositionalization. Replace each universally quantified sentence by the set of all its ground instances, view each ground atom like $King(John)$ as a propositional symbol, and run any complete propositional algorithm.³ It works, and by a theorem of Herbrand (1930) any entailed sentence has a proof using only a finite subset of the instantiations, so we can enumerate ground terms by increasing nesting depth until the proof appears. But there is a catch.

The moment the knowledge base mentions a function symbol like $Father$, the set of ground terms is infinite, and the propositional knowledge base never finishes generating. Worse, if the query is not entailed, the procedure can run forever without ever knowing whether it is stuck or one step from a proof. This is a fundamental limit: entailment in first-order logic is semidecidable.⁴ There is an algorithm that says yes to every entailed sentence, but none that also says no to every non-entailed one — the first-order analogue of the halting problem, proved independently by Turing and Church in 1936.

Unification

Propositionalization is also wasteful. To prove $Evil(John)$ from the axiom and the two facts about John, it generates $King(Richard)\wedge Greedy(Richard)⟹Evil(Richard)$ and every other irrelevant instance. A human never does this. A human matches the pattern$King(x)\wedge Greedy(x)$ against the known facts, reads off that $x$ must be $John$, and infers only $Evil(John)$. Unification is that matching step made precise.

The substitution $\theta =\{x/John\}$ unifies $King(x)$ with $King(John)$. A substitution binds variables to terms; applying it replaces each variable by its bound term throughout the expression. Some queries have richer answers. To answer $Knows(John,x)$ — whom does John know? — we unify it against every $Knows$ fact in the base:⁵

The last one fails, and the reason is instructive: $x$ is asked to be $John$ (to match the first argument) and $Elizabeth$ (to match the second) at once. Yet $Knows(x,Elizabeth)$ means everyone knows Elizabeth, so John surely knows her — the failure is an accident of the two sentences reusing the variable name $x$. The fix is standardizing apart: rename one sentence's variables before unifying, turning the second into $Knows(x_{17},Elizabeth)$, after which $\{x/Elizabeth,x_{17}/John\}$ succeeds.⁶

The most general unifier

When a pair unifies at all, it usually unifies in many ways. $\text{Unify}(Knows(John,x),Knows(y,z))$ admits $\{y/John,x/z\}$, which leaves the result as $Knows(John,z)$, and also $\{y/John,x/John,z/John\}$, which pins everything to $John$. The first is more general: it constrains the variables less, and every other unifier is an instance of it. For any unifiable pair there is a single most general unifier (MGU), unique up to renaming, and it is what $\text{Unify}$ returns.

The algorithm walks the two expressions in step, side by side. Constants must match; a variable matched against a term binds to it (consulting $\theta$ so earlier bindings stay consistent); two compound expressions recurse on their function symbol and argument lists.⁷ One step has its own name. When binding a variable to a compound term, we must check that the variable does not occur inside that term: $S(x)$ cannot unify with $S(S(x))$, because no finite substitution makes $x$ equal to $S(x)$. This is the occur check, and it is what makes unification's cost quadratic rather than linear in the size of the terms. Most Prolog systems omit it for speed, at the price of occasionally unsound inferences.

To see the recursion concretely, trace $\text{Unify}(Knows(John,x),Knows(y,Mother(y)))$ from the empty substitution. The two expressions are compound, so the top call recurses on operator and arguments. The operator $Knows$ unifies with itself, leaving $\theta$ empty; then the argument lists are unified element by element, threading $\theta$ through each step.

1. First arguments. $\text{Unify}(John,y,\{\})$. Here $y$ is a variable and $John$ is not, so $\text{Unify-Var}(y,John,\{\})$ runs; $y$ is unbound, $John$ is not a variable, the occur check on a constant is vacuous, and the binding $\{y/John\}$ is added. Now $\theta =\{y/John\}$.
2. Second arguments. $\text{Unify}(x,Mother(y),\{y/John\})$. Now $x$ is a variable, so $\text{Unify-Var}(x,Mother(y),\{y/John\})$ runs. $x$ is unbound and $Mother(y)$ is not in the domain of $\theta$. The occur check asks whether $x$ appears inside $Mother(y)$; it does not, so the binding $\{x/Mother(y)\}$ is added.

The returned substitution is $\{y/John,x/Mother(y)\}$, matching the third line of the table above. Applying it to either expression yields $Knows(John,Mother(John))$.

Now trace the occur check on a failing pair. Unifying $x$ with $S(x)$ — a variable against a term that contains it — reaches $\text{Unify-Var}(x,S(x),\{\})$; $x$ is unbound and $S(x)$ is not in $\theta$, but $\text{Occur-Check}(x,S(x))$ walks into the argument of $S$, finds $x$, and returns true, so the whole call returns failure. No finite term equals $S(S(S(\cdots )))$, and the check is what prevents the algorithm from binding $x$ to an infinite structure.

Storing and retrieving clauses

Every inference step above ends by asking the knowledge base a question: which stored facts unify with this pattern? Done naively, answering it means attempting $\text{Unify}$ against every sentence in the base, and for a large base that scan dominates the running time. The fix is to index the clauses so that only plausible matches are ever tested.⁸

The coarsest useful scheme is predicate indexing: keep a separate bucket per predicate symbol, so a query on $Knows$ never touches the $Employs$ facts. When a single predicate holds most of the base — $Employs(x,y)$ for every employee in a company, queried both by employer and by employee — a finer index on argument positions helps, at the cost of maintaining more index keys. The tradeoff is the standard database one: more keys make retrieval faster and updates slower.

The general structure behind such schemes is the subsumption lattice. A literal $p$ subsumes $q$ when some substitution turns $p$ into $q$, so $p$ is the more general pattern. The queries that could match a stored fact $Employs(IBM,Richard)$ are exactly its subsumers, and they form a lattice ordered by generality: the fact itself at the bottom, the all-variables pattern $Employs(w,z)$ at the top, and partially-instantiated patterns in between. To answer a query, walk down from the query pattern collecting the facts filed beneath it.

The lattice grows quickly: a fact with $n$ arguments has $2^n$ subsumers, so indexing every fact under all of them is only worthwhile when $n$ is small, which for most predicates it is.

Generalized modus ponens

Unification lets us state a single inference rule that does all the work of matching and firing an implication in one lifted step. Suppose the axiom is $King(x)\wedge Greedy(x)⟹Evil(x)$ and we know $King(John)$ and — being more ambitious — $\forall yGreedy(y)$, that everyone is greedy. We want $Evil(John)$. The substitution $\theta =\{x/John,y/John\}$ makes the premises $King(x)$ and $Greedy(x)$ identical to the known $King(John)$ and $Greedy(y)$ at once, so we may assert the conclusion under $\theta$.

This is a lifted rule — it raises ordinary modus ponens from ground propositional logic to first-order logic. Its soundness is quick: for any sentence $p$ with universally quantified variables, $p\models \text{Subst}(\theta ,p)$ by universal instantiation, so the lifted step is just a ground modus ponens hiding behind the substitution. What it gains over propositionalization is that it makes only the substitutions the proof needs, never the irrelevant ones.

Forward chaining

Generalized modus ponens is the atom of inference; the two chaining algorithms are strategies for applying it. Forward chaining is data-driven: start from the known facts, fire every rule whose premises are satisfied, add the conclusions, and repeat until the query appears or nothing new can be derived.⁹ It works on definite clauses — disjunctions of literals with exactly one positive, written as an implication whose premise is a conjunction of positive literals and whose conclusion is a single positive literal. When the clauses also contain no function symbols, the language is called Datalog, and inference is not merely semidecidable but decidable, because the set of ground facts is finite.

The crime example

The canonical worked problem: prove that Colonel West is a criminal.¹⁰

The law says it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American.

Rendered as definite clauses (universal quantifiers on variables left implicit):

The existential in Nono has some missiles is skolemized into two ground facts by existential instantiation, introducing a new constant $M_1$: $Owns(Nono,M_1)$ and $Missile(M_1)$. The rest are already ground: $American(West)$ and $Enemy(Nono,America)$. Forward chaining now sweeps the rules. On the first iteration $(9.6)$ fires with $\{x/M_1\}$ to add $Sells(West,M_1,Nono)$; $(9.7)$ adds $Weapon(M_1)$; $(9.8)$ adds $Hostile(Nono)$. On the second iteration rule $(9.3)$ finally fires, with $\{x/West,y/M_1,z/Nono\}$, concluding $Criminal(West)$. A third pass adds nothing — the knowledge base has reached a fixed point.

FOL-FC-ASK is easy to characterize. It is sound, being nothing but repeated generalized modus ponens, and it is complete for definite-clause knowledge bases: it derives every fact those clauses entail. For Datalog it terminates in polynomial time. A new fact is not counted as new if it is merely a renaming of an existing one — $Likes(x,IceCream)$ and $Likes(y,IceCream)$ say the same thing. With function symbols the fixed point can be infinite (the Peano axioms generate $NatNum(S(0)),NatNum(S(S(0))),\dots$ forever), so completeness again bumps into semidecidability.

The inner loop's cost is the matching of a rule's premise against the facts, called pattern matching, and it is where forward chaining spends its time. Ordering the conjuncts to test the most constrained one first — the conjunct ordering problem, solved heuristically much as the minimum-remaining-values rule solves constraint satisfaction — and incremental schemes like the rete network, which retains partial matches across iterations instead of recomputing them, are what make production systems run large rule sets in real time. Because forward chaining draws every entailed conclusion, including ones irrelevant to the query, it suits systems that react to newly arrived data — but wastes effort when the goal is specific.

Backward chaining

Backward chaining inverts the direction. It is goal-driven: to prove the query, find rules whose conclusion unifies with it, and recursively prove their premises.¹¹ The search has the shape of an AND–OR tree. The OR branching is over rules: a goal can be established by any clause whose head unifies with it. The AND branching is within a rule: all of the conjuncts in its premise must be proved. On the crime knowledge base, proving $Criminal(West)$ unifies with the head of $(9.3)$ and spawns four subgoals — $American(West)$, $Weapon(y)$, $Sells(West,y,z)$, $Hostile(z)$ — each pursued in turn, the substitution from each success carried into the next.

Because a query can succeed in several ways — $Person(x)$ might hold with $x/John$ and with $x/Richard$ — backward chaining is implemented as a generator that yields substitutions one at a time. FOL-BC-OR fetches each candidate rule, stands its variables apart, unifies its head with the goal, and proves the premise conjuncts through FOL-BC-AND, which threads the accumulated substitution from one conjunct to the next.

Backward chaining is a depth-first search, so its space cost is linear in the proof size, but — unlike forward chaining — it can loop on repeated subgoals and is incomplete when a branch recurses without end. Its advantage is directedness: it touches only rules relevant to the goal.

Logic programming

Backward chaining is the execution model of logic programming, and Prolog is its most widely used language. Kowalski's slogan captures the idea: a program is knowledge plus a control strategy for running inference over it,

A Prolog clause is written head-first with the implication reversed and conjuncts comma-separated, uppercase for variables and lowercase for constants — the crime rule reads criminal(X) :- american(X), weapon(Y), sells(X,Y,Z), hostile(Z). The appeal is that a single relational definition runs in every direction. Given

append([], Y, Y).
append([A|X], Y, [A|Z]) :- append(X, Y, Z).

the query append(X, Y, [1,2]) asks not what is the result of appending but "which two lists append to give [1,2]," and yields all three splits. Prolog departs from pure logic in ways that buy speed: it uses depth-first search with no loop check (fast when the axioms are ordered well, incomplete otherwise), omits the occur check (occasionally unsound), and treats negation as failure to prove. These are the compromises between declarativeness and efficiency that make it a practical language rather than a theorem prover.

Where this continues

Forward and backward chaining are complete only for definite clauses — Horn knowledge bases, where every rule has a single positive conclusion. Real first-order knowledge has disjunctions and negations that Horn form cannot express, and for those we need one more inference rule: a single sound and complete procedure for all of first-order logic.

This continues in First-Order Resolution, which converts arbitrary sentences to CNF by skolemizing away the existentials, lifts the resolution rule with unification, and refutes the negated goal — the proof system Gödel showed is complete for first-order entailment.