---
title: Inference in First-Order Logic
module: Logic and Planning
moduleNumber: 3
lessonNumber: 5
order: 305
summary: >
  Propositional inference lifts to first-order logic once we can make terms
  match. Unification is that machinery: the algorithm that finds the substitution
  making two expressions identical, and the basis of generalized modus
  ponens. This first part builds the lifted inference rules and the two chaining
  algorithms they drive — forward chaining, the data-driven procedure behind
  production systems and Datalog, and backward chaining, the goal-driven
  procedure behind Prolog.
topics: [Logic]
sources:
  - book: AIMA
    ref: "Ch. 9 — Inference in First-Order Logic; §9.1 Propositional vs. First-Order Inference; §9.2 Unification and Lifting"
  - book: AIMA
    ref: "§9.3 Forward Chaining; §9.4 Backward Chaining"
---


[First-order logic](/artificial-intelligence/logic-and-planning/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.[^aima-intro] 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,

$$
\forall x \; King(x) \land Greedy(x) \implies Evil(x),
$$

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.

> **Definition (Universal Instantiation).** From $\forall v \; \alpha$ we may
> infer $\textsc{Subst}(\{v/g\}, \alpha)$ for any ground term $g$ — a term with
> no variables. A universally quantified sentence licenses _every_ instance
> obtained by plugging a ground term in for the variable.

Substituting $\{x/John\}$ turns the axiom into the propositional implication
$King(John) \land Greedy(John) \implies 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.

> **Definition (Existential Instantiation).** From $\exists v \; \alpha$ we may
> infer $\textsc{Subst}(\{v/k\}, \alpha)$ where $k$ is a constant symbol that
> appears nowhere else in the knowledge base — a **Skolem constant**. The
> existential says some object satisfies $\alpha$; instantiation names that
> object, and the name must not already be taken.

From $\exists x \; Crown(x) \land OnHead(x, John)$ we may infer $Crown(C_1) \land
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.[^aima-inst] 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.[^aima-prop] 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.

$$
% caption: Propositionalization instantiates a quantified axiom at every ground
% term. With a function symbol $Father$ the set of ground terms is infinite —
% $John$, $Father(John)$, $Father(Father(John))$, ... — so the propositional KB
% never finishes generating.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  ax/.style={draw, minimum width=42mm, minimum height=9mm, align=center},
  gr/.style={draw, minimum width=30mm, minimum height=7mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \node[ax, draw=acc, text=acc] (a) at (0,2.4) {for all x: King(x) and Greedy(x) $\Rightarrow$ Evil(x)};
  \node[gr] (g1) at (-3.3,0.7) {x = John};
  \node[gr] (g2) at (0,0.7)    {x = Father(John)};
  \node[gr] (g3) at (3.3,0.7)  {x = Father(Father(John))};
  \node[font=\large] (dots) at (5.6,0.7) {...};
  \draw[->, acc, thick] (a) -- (g1);
  \draw[->, acc, thick] (a) -- (g2);
  \draw[->, acc, thick] (a) -- (g3);
  \draw[->, acc, thick] (a.east) -- (dots);
  \node[anchor=north, text=black, font=\scriptsize] at (0,0.15) {infinitely many ground terms once a function symbol appears};
\end{tikzpicture}
$$

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**.[^aima-semi] 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) \land Greedy(Richard) \implies Evil(Richard)$ and every other
irrelevant instance. A human never does this. A human matches the _pattern_
$King(x) \land 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.

> **Definition (Unification).** A **unifier** of two expressions $p$ and $q$ is a
> substitution $\theta$ making them identical: $\textsc{Subst}(\theta, p) =
> \textsc{Subst}(\theta, q)$. The algorithm $\textsc{Unify}(p, q)$ returns such a
> $\theta$ if one exists and fails otherwise.

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:[^aima-unify]

$$
\begin{aligned}
\textsc{Unify}(Knows(John, x),\; Knows(John, Jane)) &= \{x/Jane\} \\
\textsc{Unify}(Knows(John, x),\; Knows(y, Bill)) &= \{x/Bill,\; y/John\} \\
\textsc{Unify}(Knows(John, x),\; Knows(y, Mother(y))) &= \{y/John,\; x/Mother(John)\} \\
\textsc{Unify}(Knows(John, x),\; Knows(x, Elizabeth)) &= fail.
\end{aligned}
$$

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.[^aima-standard]

### The most general unifier

When a pair unifies at all, it usually unifies in many ways.
$\textsc{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 $\textsc{Unify}$ returns.

$$
% caption: The most general unifier of $Knows(John, x)$ and $Knows(y, z)$ is
% $\{y/John,\, x/z\}$, sitting above every other unifier — each of which
% (like the fully-ground $\{y/John,\, x/John,\, z/John\}$) is obtained from it by
% a further substitution.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  u/.style={draw, minimum width=34mm, minimum height=8mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \node[u, draw=acc, text=acc] (mgu) at (0,2.0) {mgu: y = John, x = z};
  \node[u] (s1) at (-3.2,0) {y = John, x = z, z = John};
  \node[u] (s2) at (3.2,0)  {y = John, x = Bill, z = Bill};
  \draw[->, acc, thick] (mgu) -- (s1) node[midway, left, font=\scriptsize, text=black] {+ z=John};
  \draw[->, acc, thick] (mgu) -- (s2) node[midway, right, font=\scriptsize, text=black] {+ z=Bill};
  \node[anchor=south, text=black, font=\scriptsize] at (0,2.5) {fewest restrictions};
\end{tikzpicture}
$$

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.[^aima-algo] 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.

```algorithm
caption: $\textsc{Unify}(x, y, \theta)$ — return an MGU of $x$ and $y$, or failure
input: $x$, $y$, expressions (variable, constant, list, or compound)
input: $\theta$, the substitution built so far (defaults to empty)
if $\theta = failure$ then return failure
else if $x = y$ then return $\theta$
else if $x$ is a variable then return $\textsc{Unify-Var}(x, y, \theta)$
else if $y$ is a variable then return $\textsc{Unify-Var}(y, x, \theta)$
else if $x$ and $y$ are compound then
  return $\textsc{Unify}(\text{Args}(x), \text{Args}(y), \textsc{Unify}(\text{Op}(x), \text{Op}(y), \theta))$
else if $x$ and $y$ are lists then
  return $\textsc{Unify}(\text{Rest}(x), \text{Rest}(y), \textsc{Unify}(\text{First}(x), \text{First}(y), \theta))$
else return failure

function $\textsc{Unify-Var}(var, x, \theta)$
  if $\{var/val\} \in \theta$ then return $\textsc{Unify}(val, x, \theta)$
  else if $\{x/val\} \in \theta$ then return $\textsc{Unify}(var, val, \theta)$
  else if $\textsc{Occur-Check}(var, x)$ then return failure
  else return $\theta$ with $\{var/x\}$ added
```

To see the recursion concretely, trace $\textsc{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.** $\textsc{Unify}(John, y, \{\,\})$. Here $y$ is a
   variable and $John$ is not, so $\textsc{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.** $\textsc{Unify}(x, Mother(y), \{y/John\})$. Now $x$
   is a variable, so $\textsc{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 $\textsc{Unify-Var}(x, S(x), \{\,\})$; $x$
is unbound and $S(x)$ is not in $\theta$, but $\textsc{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.

$$
% caption: The recursion of $\textsc{Unify}(Knows(John, x), Knows(y,
% Mother(y)))$. The top call splits into operator and two argument
% unifications; $\theta$ grows left to right, $\{y/John\}$ established at the
% first argument feeding into the second, where $x$ binds to $Mother(y)$. The
% inset shows the occur check rejecting $x$ against $S(x)$.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  nd/.style={draw, minimum height=6mm, inner sep=3pt, font=\scriptsize, align=center},
  hd/.style={draw=acc, text=acc, minimum height=6mm, inner sep=3pt, font=\scriptsize, align=center},
  th/.style={text=black, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \definecolor{red}{HTML}{C0392B}
  \node[hd] (top) at (0,3.1) {Unify(Knows(John,x), Knows(y,Mother(y)))};
  \node[nd] (op)  at (-3.6,1.5) {Op: Knows = Knows};
  \node[nd] (a1)  at (0,1.5)    {Arg 1: Unify(John, y)};
  \node[nd] (a2)  at (3.6,1.5)  {Arg 2: Unify(x, Mother(y))};
  \node[nd] (b1)  at (0,0.1)    {bind y = John};
  \node[nd] (b2)  at (3.6,0.1)  {bind x = Mother(y)};
  \draw[->, acc, thick] (top) -- (op);
  \draw[->, acc, thick] (top) -- (a1);
  \draw[->, acc, thick] (top) -- (a2);
  \draw[->, acc, thick] (a1) -- (b1);
  \draw[->, acc, thick] (a2) -- (b2);
  \draw[->, dashed, acc] (b1.east) to[out=0, in=180] node[pos=0.35, below, th] {theta} (a2.west);
  % occur-check inset
  \node[nd, draw=red, text=red] (oc) at (0,-1.5) {Unify(x, S(x)): occur check f\/inds x in S(x) $\Rightarrow$ fail};
\end{tikzpicture}
$$

### 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 $\textsc{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.[^aima-store]

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.

$$
% caption: The subsumption lattice for $Employs(IBM, Richard)$. The most
% general pattern $Employs(w, z)$ sits at the top; each downward edge
% instantiates one argument, until the fully ground fact sits at the bottom.
% A query is one node of this lattice, and its matches are the facts filed at
% or below it.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  ltx/.style={draw, minimum height=6mm, inner sep=3pt, font=\scriptsize, align=center},
  top/.style={draw=acc, text=acc, minimum height=6mm, inner sep=3pt, font=\scriptsize},
  bot/.style={draw=acc, text=acc, thick, minimum height=6mm, inner sep=3pt, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \node[top] (t)  at (0,3.0)     {Employs(w, z)};
  \node[ltx] (l)  at (-2.9,1.5)  {Employs(IBM, z)};
  \node[ltx] (r)  at (2.9,1.5)   {Employs(w, Richard)};
  \node[bot] (b)  at (0,0)       {Employs(IBM, Richard)};
  \draw[->, acc, thick] (t) -- (l);
  \draw[->, acc, thick] (t) -- (r);
  \draw[->, acc, thick] (l) -- (b);
  \draw[->, acc, thick] (r) -- (b);
  \node[anchor=west, text=black, font=\scriptsize] at (3.7,3.0) {most general};
  \node[anchor=north, text=black, font=\scriptsize] at (0,-0.7) {the stored fact};
\end{tikzpicture}
$$

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)
\land Greedy(x) \implies Evil(x)$ and we know $King(John)$ and — being more ambitious
— $\forall y \; Greedy(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$.

> **Algorithm (Generalized Modus Ponens).** For atomic sentences $p_i$, $p_i'$, and
> $q$, if there is a substitution $\theta$ with $\textsc{Subst}(\theta, p_i') =
> \textsc{Subst}(\theta, p_i)$ for all $i$, then from $p_1', \ldots, p_n'$ and
> $(p_1 \land \cdots \land p_n \implies q)$ infer $\textsc{Subst}(\theta, q)$.

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 \textsc{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.[^aima-fc] 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.[^aima-crime]

> 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):

$$
\begin{aligned}
&American(x) \land Weapon(y) \land Sells(x, y, z) \land Hostile(z) \implies Criminal(x) &&(9.3)\\
&Missile(x) \land Owns(Nono, x) \implies Sells(West, x, Nono) &&(9.6)\\
&Missile(x) \implies Weapon(x) &&(9.7)\\
&Enemy(x, America) \implies Hostile(x) &&(9.8)
\end{aligned}
$$

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**.

$$
% caption: The proof tree forward chaining builds for the crime example. Initial
% facts sit at the bottom; facts inferred on the first iteration in the middle;
% $Criminal(West)$, inferred on the second, at the top. Each node is joined to
% the premises that produced it.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  fact/.style={draw, minimum height=6.5mm, inner sep=3.5pt, font=\scriptsize, align=center},
  goal/.style={draw=acc, text=acc, thick, minimum height=6.5mm, inner sep=3.5pt, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  % bottom row, spread wide
  \node[fact] (amer)  at (0,0)     {American(West)};
  \node[fact] (miss)  at (3.7,0)   {Missile(M1)};
  \node[fact] (owns)  at (6.9,0)   {Owns(Nono,M1)};
  \node[fact] (enemy) at (10.5,0)  {Enemy(Nono,America)};
  % middle row, each above its supports
  \node[fact] (weap) at (3.4,1.9)  {Weapon(M1)};
  \node[fact] (sell) at (5.9,1.9)  {Sells(West,M1,Nono)};
  \node[fact] (host) at (10.5,1.9) {Hostile(Nono)};
  % top
  \node[goal] (crim) at (5.6,3.7)  {Criminal(West)};
  % edges into middle row
  \draw (weap) -- (miss);
  \draw (sell) -- (miss);
  \draw (sell) -- (owns);
  \draw (host) -- (enemy);
  % edges to Criminal (route to American around the left of Weapon)
  \draw (crim.west) to[out=180, in=90] (amer.north);
  \draw (crim) -- (weap);
  \draw (crim) -- (sell);
  \draw (crim) -- (host);
\end{tikzpicture}
$$

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))), \ldots$ forever), so completeness again bumps into
semidecidability.

```algorithm
caption: $\textsc{FOL-FC-Ask}(KB, \alpha)$ — data-driven forward chaining
input: $KB$, a set of first-order definite clauses; $\alpha$, the atomic query
$local$: $new$, the sentences inferred on each iteration
repeat
  $new \gets \{\,\}$
  for each rule $(p_1 \land \cdots \land p_n \implies q)$ in $KB$ do
    standardize the variables of the rule apart
    for each $\theta$ with $\textsc{Subst}(\theta, p_1 \land \cdots \land p_n) = \textsc{Subst}(\theta, p_1' \land \cdots \land p_n')$ do
      for some $p_1', \ldots, p_n'$ already in $KB$
      $q' \gets \textsc{Subst}(\theta, q)$
      if $q'$ does not unify with any sentence in $KB$ or $new$ then
        add $q'$ to $new$
        $\phi \gets \textsc{Unify}(q', \alpha)$
        if $\phi \ne failure$ then return $\phi$
  add $new$ to $KB$
until $new$ is empty
return false
```

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](/artificial-intelligence/search/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.[^aima-bc] 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.

$$
% caption: The goal tree backward chaining builds to prove $Criminal(West)$, read
% depth-first, left to right. Each conjunct of rule $(9.3)$ is a subgoal; the
% binding found for one is threaded into the next, so by the time $Hostile(z)$ is
% reached, $z$ is already bound to $Nono$. Braces show the substitution returned.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  gl/.style={draw, minimum height=6mm, inner sep=3pt, font=\scriptsize, align=center},
  goal/.style={draw=acc, text=acc, thick, minimum height=6mm, inner sep=3pt, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \node[goal] (crim) at (4.4,3.4) {Criminal(West)};
  % four subgoals
  \node[gl] (amer) at (0.3,1.7)  {American(West)};
  \node[gl] (weap) at (2.9,1.7)  {Weapon(y)};
  \node[gl] (sell) at (5.4,1.7)  {Sells(West,M1,z)};
  \node[gl] (host) at (8.1,1.7)  {Hostile(Nono)};
  % leaves
  \node[gl] (miss) at (2.9,0)    {Missile(M1)};
  \node[gl] (owns) at (5.4,0)    {Owns(Nono,M1)};
  \node[gl] (enemy) at (8.1,0)   {Enemy(Nono,America)};
  \draw (crim) -- (amer);
  \draw (crim) -- (weap);
  \draw (crim) -- (sell);
  \draw (crim) -- (host);
  \draw (weap) -- (miss);
  \draw (sell) -- (miss);
  \draw (sell) -- (owns);
  \draw (host) -- (enemy);
  % substitution annotations
  \node[text=black, font=\scriptsize, anchor=north] at (0.3,1.35) {\{ \}};
  \node[text=black, font=\scriptsize, anchor=north] at (2.9,-0.35) {y = M1};
  \node[text=black, font=\scriptsize, anchor=north] at (5.4,1.35) {z = Nono};
\end{tikzpicture}
$$

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.

```algorithm
caption: $\textsc{FOL-BC-Ask}(KB, query)$ — goal-driven backward chaining
input: $KB$, definite clauses; $query$, the atomic goal
return $\textsc{FOL-BC-Or}(KB, query, \{\,\})$

function $\textsc{FOL-BC-Or}(KB, goal, \theta)$ // yields substitutions
  for each rule $(lhs \implies rhs)$ in $\textsc{Fetch-Rules}(KB, goal)$ do
    standardize $(lhs, rhs)$ apart
    for each $\theta'$ in $\textsc{FOL-BC-And}(KB, lhs, \textsc{Unify}(rhs, goal, \theta))$ do
      yield $\theta'$

function $\textsc{FOL-BC-And}(KB, goals, \theta)$ // yields substitutions
  if $\theta = failure$ then return
  else if $goals$ is empty then yield $\theta$
  else
    $first, rest \gets \textsc{First}(goals), \textsc{Rest}(goals)$
    for each $\theta'$ in $\textsc{FOL-BC-Or}(KB, \textsc{Subst}(\theta, first), \theta)$ do
      for each $\theta''$ in $\textsc{FOL-BC-And}(KB, rest, \theta')$ do
        yield $\theta''$
```

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,

$$
Algorithm = Logic + Control.
$$

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

```prolog
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](/artificial-intelligence/logic-and-planning/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.

[^aima-intro]: **Russell & Norvig**, _AIMA_, Ch. 9 — introduction: Chapter 7 established sound and complete propositional inference; Chapter 9 extends it to first-order logic via inference rules for quantifiers, unification, and the forward-chaining, backward-chaining, and resolution families.
[^aima-inst]: **Russell & Norvig**, _AIMA_, §9.1.1 — Inference rules for quantifiers: universal instantiation over ground terms, existential instantiation with a fresh Skolem constant, and inferential (not logical) equivalence of the resulting knowledge base.
[^aima-prop]: **Russell & Norvig**, _AIMA_, §9.1.2 — Reduction to propositional inference: replacing a universally quantified sentence by all its ground instances, propositionalization, and Herbrand's theorem guaranteeing a finite sufficient subset.
[^aima-semi]: **Russell & Norvig**, _AIMA_, §9.1.2 — the semidecidability of first-order entailment: algorithms say yes to every entailed sentence but none says no to every non-entailed one, the analogue of Turing's and Church's 1936 undecidability results.
[^aima-unify]: **Russell & Norvig**, _AIMA_, §9.2.2 — Unification: $\textsc{Unify}$ returning a substitution $\theta$ with $\textsc{Subst}(\theta, p) = \textsc{Subst}(\theta, q)$, the four $Knows(John, x)$ examples, and the occur check making the algorithm quadratic.
[^aima-store]: **Russell & Norvig**, _AIMA_, §9.2.3 — Storage and retrieval: predicate and argument indexing over $\textsc{Store}$/$\textsc{Fetch}$, the tradeoff between index keys and update cost, and the subsumption lattice with its $2^n$ subsumers for an $n$-argument literal.
[^aima-standard]: **Russell & Norvig**, _AIMA_, §9.2.2 — standardizing apart to avoid variable-name clashes, and the most general unifier being unique up to renaming for every unifiable pair.
[^aima-algo]: **Russell & Norvig**, _AIMA_, §9.2.2, Figure 9.1 — the recursive $\textsc{Unify}$ / $\textsc{Unify-Var}$ algorithm comparing structures element by element, consulting $\theta$ for consistency, with the occur check on variable-to-compound bindings.
[^aima-fc]: **Russell & Norvig**, _AIMA_, §9.3 — Forward Chaining: first-order definite clauses, Datalog and its decidability, FOL-FC-ASK (Figure 9.3), soundness and completeness, the fixed point, renaming, pattern matching, conjunct ordering, and rete/production systems.
[^aima-crime]: **Russell & Norvig**, _AIMA_, §9.3.1–9.3.2 — the crime/Colonel West example: the definite-clause encoding (9.3)–(9.10), skolemizing "Nono has missiles" into $M_1$, the two forward-chaining iterations, and the proof tree of Figure 9.4.
[^aima-bc]: **Russell & Norvig**, _AIMA_, §9.4.1 — Backward Chaining: the AND–OR search, FOL-BC-ASK as a generator (Figure 9.6), threading substitutions through conjuncts, the goal tree of Figure 9.7, and depth-first incompleteness on repeated subgoals.