---
title: First-Order Resolution
module: Logic and Planning
moduleNumber: 3
lessonNumber: 6
order: 306
summary: >
  Chaining is complete only for Horn knowledge bases. General first-order
  sentences — with disjunctive conclusions and negations — need a single sound and
  complete rule: resolution. This part converts arbitrary sentences to CNF by
  skolemizing away the existentials, lifts the resolution rule with unification,
  and proves entailment by refuting the negated goal. The result is the proof
  procedure Gödel's completeness theorem guarantees will find any entailment,
  together with the search strategies that make it usable.
topics: [Logic]
sources:
  - book: AIMA
    ref: "Ch. 9 — Inference in First-Order Logic; §9.5 Resolution"
---

This builds on
[Inference in First-Order Logic](/artificial-intelligence/logic-and-planning/inference-and-resolution),
which lifted propositional inference to first order through unification and built
the forward- and backward-chaining algorithms for Horn knowledge bases. Here we
drop the Horn restriction and give a single complete rule for all of first-order
logic.

## Resolution

Chaining is complete only for definite clauses — Horn knowledge bases. General
first-order sentences, with disjunctive conclusions and negations, need a single
sound and complete rule: **resolution**.[^aima-res] It proves $KB \models \alpha$ by
_refutation_ — showing $KB \land \lnot\alpha$ unsatisfiable — and it operates on
sentences in conjunctive normal form.

### Conversion to CNF

Every first-order sentence has an inferentially equivalent **conjunctive normal
form** (CNF): a conjunction of **clauses**, each a disjunction of literals, with
variables understood as universally quantified. The rule $(9.3)$ becomes the single
clause

$$
\lnot American(x) \lor \lnot Weapon(y) \lor \lnot Sells(x, y, z) \lor \lnot Hostile(z) \lor Criminal(x).
$$

The conversion is mechanical but has one first-order-specific step. Consider
"everyone who loves all animals is loved by someone,"

$$
\forall x \; [\forall y \; Animal(y) \implies Loves(x, y)] \implies [\exists y \; Loves(y, x)].
$$

We eliminate implications ($\alpha \implies \beta$ becomes $\lnot\alpha \lor \beta$);
push negations inward, using $\lnot\forall x\, p \equiv \exists x\, \lnot p$ and
$\lnot\exists x\, p \equiv \forall x\, \lnot p$; and standardize apart any reused
quantifier variables. The remaining step has no propositional analogue.

> **Definition (Skolemization).** Removing existential quantifiers by replacing each
> existentially quantified variable with a **Skolem function** of the universally
> quantified variables in whose scope it lies. If the existential stands alone the
> function is a constant; nested inside universals, it must _depend_ on them.

Naively replacing the two existentials with constants $A$ and $B$ would assert that
_everyone_ fails to love one particular animal $A$ or is loved by one particular
entity $B$ — the wrong meaning. Because the object depends on $x$, the Skolem entity
must too, giving Skolem functions $F(x)$ and $G(x)$:

$$
\forall x \; [Animal(F(x)) \land \lnot Loves(x, F(x))] \lor Loves(G(x), x).
$$

Now every remaining variable is universal, so we drop the quantifiers, distribute
$\lor$ over $\land$, and read off the clauses. Skolemization is the general form of
the existential-instantiation trick from the start of the lesson; the Skolemized
sentence is satisfiable exactly when the original is, which is all refutation needs.

Run all six stages on that sentence in full, so no step is left implicit.
The starting point is

$$
\forall x \; [\forall y \; Animal(y) \implies Loves(x, y)] \implies [\exists y \;
Loves(y, x)].
$$

1. **Eliminate implications.** Rewrite each $\alpha \implies \beta$ as
   $\lnot\alpha \lor \beta$, both the outer one and the inner one:

   $$
   \forall x \; \lnot[\forall y \; \lnot Animal(y) \lor Loves(x, y)] \lor
   [\exists y \; Loves(y, x)].
   $$

2. **Move negation inward.** Push the leading $\lnot$ through the universal,
   turning $\lnot\forall y$ into $\exists y$ and negating the disjunction under
   it with De Morgan, so $\lnot(\lnot Animal(y) \lor Loves(x,y))$ becomes
   $Animal(y) \land \lnot Loves(x,y)$:

   $$
   \forall x \; [\exists y \; Animal(y) \land \lnot Loves(x, y)] \lor
   [\exists y \; Loves(y, x)].
   $$

3. **Standardize apart.** The two $\exists y$ quantifiers bind unrelated
   variables reusing the name $y$; rename the second to $z$ so no later step
   confuses them:

   $$
   \forall x \; [\exists y \; Animal(y) \land \lnot Loves(x, y)] \lor
   [\exists z \; Loves(z, x)].
   $$

4. **Skolemize.** Both existentials lie inside $\forall x$, so the witnesses
   depend on $x$. Replace $y$ by the Skolem function $F(x)$ and $z$ by $G(x)$,
   and drop the existentials:

   $$
   \forall x \; [Animal(F(x)) \land \lnot Loves(x, F(x))] \lor Loves(G(x), x).
   $$

5. **Drop universal quantifiers.** Only $\forall x$ remains, and every free
   variable is now understood as universally quantified, so erase it:

   $$
   [Animal(F(x)) \land \lnot Loves(x, F(x))] \lor Loves(G(x), x).
   $$

6. **Distribute $\lor$ over $\land$.** The final form is a conjunction of
   clauses. Distributing the trailing disjunct across the conjunction splits
   the sentence into two clauses:

   $$
   [Animal(F(x)) \lor Loves(G(x), x)] \;\land\; [\lnot Loves(x, F(x)) \lor
   Loves(G(x), x)].
   $$

Those two clauses are the input resolution will use later. Nothing in the
sequence changed the sentence's satisfiability, and only stage 4 has no
propositional counterpart.

$$
% caption: The CNF pipeline for first-order sentences. Every stage is mechanical;
% only skolemization is new — it replaces an existential with a Skolem function
% of the enclosing universals, so the witness can depend on them, then the bare
% universals are dropped.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  st/.style={draw, minimum width=32mm, minimum height=8mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \node[st] (s1) at (0,0)     {eliminate $\Rightarrow$};
  \node[st] (s2) at (0,-1.15) {push not inwards};
  \node[st] (s3) at (0,-2.3)  {standardize apart};
  \node[st, draw=acc, text=acc, thick] (s4) at (0,-3.45) {skolemize (drop exists)};
  \node[st] (s5) at (0,-4.6)  {drop universals};
  \node[st] (s6) at (0,-5.75) {distribute or over and};
  \foreach \a/\b in {s1/s2, s2/s3, s3/s4, s4/s5, s5/s6}
    \draw[->, acc, thick] (\a) -- (\b);
  \node[anchor=west, text=black, font=\scriptsize] at (2.1,-3.45) {the one first-order-only step};
  \node[anchor=west, text=black, font=\scriptsize] at (2.1,-5.75) {result is a set of clauses};
\end{tikzpicture}
$$

### The resolution rule

The first-order resolution rule is the lifted version of propositional resolution.
Two clauses standardized apart can be resolved if one has a literal that unifies with
the negation of a literal in the other; the resolvent is the union of the remaining
literals with the unifier applied.

> **Algorithm (Binary resolution).** From $\ell_1 \lor \cdots \lor \ell_k$ and
> $m_1 \lor \cdots \lor m_n$, if $\textsc{Unify}(\ell_i, \lnot m_j) = \theta$, infer
> the resolvent $\textsc{Subst}(\theta, \ell_1 \lor \cdots \lor \ell_{i-1} \lor
> \ell_{i+1} \lor \cdots \lor \ell_k \lor m_1 \lor \cdots \lor m_{j-1} \lor m_{j+1}
> \lor \cdots \lor m_n)$.

For instance, $[Animal(F(x)) \lor Loves(G(x), x)]$ and $[\lnot Loves(u, v) \lor
\lnot Kills(u, v)]$ resolve on the complementary $Loves(G(x), x)$ and $\lnot Loves(u,
v)$ under $\theta = \{u/G(x),\; v/x\}$, producing $[Animal(F(x)) \lor \lnot
Kills(G(x), x)]$. Binary resolution alone is not quite complete; it must be paired
with **factoring**, which collapses two literals in a clause to one when they are
unifiable. The two together are complete.

### Refutation

To prove $KB \models \alpha$, add $\lnot\alpha$ to the knowledge base, convert
everything to clauses, and resolve until the **empty clause** — a disjunction of no
literals, denoting a contradiction — appears. On the crime example, negating the goal
to $\lnot Criminal(West)$ and resolving against the clause forms of $(9.3)$–$(9.10)$
produces a proof with a characteristic shape: a single **spine**, the goal clause
resolving against one knowledge-base clause at a time until the empty clause drops
out.

$$
% caption: The resolution refutation of the crime example. Beginning from the
% negated goal $\lnot Criminal(West)$, each step resolves the current clause on
% the spine against one KB clause, shrinking it, until the empty clause (box)
% signals contradiction. This single spine is the mark of resolution on Horn
% clauses; it mirrors backward chaining's goals exactly.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  cl/.style={draw, minimum height=6mm, inner sep=3pt, font=\scriptsize, align=center},
  sp/.style={draw=acc, text=acc, minimum height=6mm, inner sep=3pt, font=\scriptsize, align=center}]
  \definecolor{acc}{HTML}{2348F2}
  % spine on the right, KB clauses on the left
  \node[sp] (g0) at (5.6,4.2)  {not Criminal(West)};
  \node[sp] (g1) at (5.6,3.15) {not Amer / not Weap / not Sells / not Host};
  \node[sp] (g2) at (5.6,2.1)  {not Weap / not Sells / not Host};
  \node[sp] (g3) at (5.6,1.05) {not Sells / not Host};
  \node[sp] (g4) at (5.6,0.0)  {not Host};
  \node[draw=acc, text=acc, minimum size=4mm, inner sep=1pt] (box) at (5.6,-1.05) {\ };
  % KB clauses feeding in from the left
  \node[cl] (k1) at (0.6,3.15) {rule (9.3), clause form};
  \node[cl] (k2) at (0.6,2.1)  {American(West)};
  \node[cl] (k3) at (0.6,1.05) {Weapon(M1)};
  \node[cl] (k4) at (0.6,0.0)  {Sells(West,M1,Nono)};
  \node[cl] (k5) at (0.6,-1.05){Hostile(Nono)};
  % spine arrows
  \draw[->, acc, thick] (g0) -- (g1);
  \draw[->, acc, thick] (g1) -- (g2);
  \draw[->, acc, thick] (g2) -- (g3);
  \draw[->, acc, thick] (g3) -- (g4);
  \draw[->, acc, thick] (g4) -- (box);
  % KB feeds
  \draw[->] (k1) -- (g1);
  \draw[->] (k2) -- (g2);
  \draw[->] (k3) -- (g3);
  \draw[->] (k4) -- (g4);
  \draw[->] (k5) -- (box);
\end{tikzpicture}
$$

On Horn knowledge bases the clauses along the spine correspond exactly to the
successive goals of backward chaining: backward chaining is resolution with a fixed
strategy for choosing the next step. General knowledge bases give bushier proofs.

#### Curiosity killed the cat, in full

The "Curiosity killed the cat" puzzle is the standard example of a proof that
is not a single spine. In English: everyone who loves all animals is loved by
someone; anyone who kills an animal is loved by no one; Jack loves all
animals; either Jack or Curiosity killed the cat, who is named Tuna; and Tuna
is a cat while all cats are animals. Does Curiosity kill Tuna? Converting
every sentence to clauses gives the knowledge base (variables universal, $F$
and $G$ the Skolem functions from the CNF trace above):[^aima-cat]

$$
\begin{aligned}
&\text{A: } Animal(F(x)) \lor Loves(G(x), x) \\
&\text{B: } \lnot Loves(x, F(x)) \lor Loves(G(x), x) \\
&\text{C: } \lnot Animal(y) \lor \lnot Kills(x, y) \lor \lnot Loves(z, x) \\
&\text{D: } Animal(Tuna) \\
&\text{E: } Kills(Jack, Tuna) \lor Kills(Curiosity, Tuna) \\
&\text{F: } Loves(Jack, w) \quad (\text{Jack loves all animals})
\end{aligned}
$$

Clauses A and B come from "loves all animals is loved by someone"; C from
"kills an animal, loved by no one"; and to refute the query we add its
negation, $\lnot Kills(Curiosity, Tuna)$. Now resolve, tracking each
resolvent and the unifier that produced it.

1. Resolve E with the negated goal on $Kills(Curiosity, Tuna)$, unifier
   $\{\,\}$: the two $Curiosity$ literals are already ground and
   complementary, leaving $Kills(Jack, Tuna)$.
2. Resolve that with C on $Kills(x, y)$, unifier $\{x/Jack,\; y/Tuna\}$,
   giving $\lnot Animal(Tuna) \lor \lnot Loves(z, Jack)$.
3. Resolve with D $= Animal(Tuna)$, unifier $\{\,\}$, discharging the first
   disjunct and leaving $\lnot Loves(z, Jack)$: no one loves Jack.
4. Resolve with B on $Loves(G(x), x)$ against $\lnot Loves(z, Jack)$, unifier
   $\{z/G(Jack),\; x/Jack\}$, giving $\lnot Loves(Jack, F(Jack))$.
5. Resolve with F $= Loves(Jack, w)$, unifier $\{w/F(Jack)\}$: the two
   $Loves(Jack, \cdot)$ literals are complementary, and the resolvent is the
   **empty clause**.

The empty clause closes the proof, so $KB \models Kills(Curiosity, Tuna)$. The
paraphrase reads as ordinary deduction: if Curiosity did not kill Tuna, Jack
did (step 1); Tuna is an animal, so whoever killed it is loved by no one, in
particular Jack (steps 2–3); but Jack loves all animals, so someone loves Jack
(steps 4–5) — a contradiction. Step 4 uses clause B, which skolemization
produced, and the general accounting also needs **factoring**; the version
above threads a single lineage for readability.

$$
% caption: The resolution refutation of "Curiosity killed the cat." Unlike the
% Horn spine, this proof branches: the negated goal and several KB clauses
% (E, C, D, B, F) each feed resolvents, unifiers shown on the edges, down to
% the empty clause (box). Skolem functions $F$, $G$ appear because the source
% sentences were existentially quantified.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  cl/.style={draw, minimum height=6mm, inner sep=3pt, font=\scriptsize, align=center},
  rv/.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}
  % KB clauses (left column)
  \node[cl] (E) at (0,4.2)   {E: Kills(Jack,Tuna) or Kills(Curiosity,Tuna)};
  \node[cl] (ng) at (0,5.4)  {not Kills(Curiosity,Tuna)};
  \node[cl] (C) at (0,2.6)   {C: not Animal(y) or not Kills(x,y) or not Loves(z,x)};
  \node[cl] (D) at (0,1.2)   {D: Animal(Tuna)};
  \node[cl] (B) at (0,-0.2)  {B: not Loves(x,F(x)) or Loves(G(x),x)};
  \node[cl] (F) at (0,-1.6)  {F: Loves(Jack,w)};
  % resolvents (right column)
  \node[rv] (r1) at (6.3,4.8) {Kills(Jack,Tuna)};
  \node[rv] (r2) at (6.3,2.6) {not Animal(Tuna) or not Loves(z,Jack)};
  \node[rv] (r3) at (6.3,1.2) {not Loves(z,Jack)};
  \node[rv] (r4) at (6.3,-0.2) {not Loves(Jack,F(Jack))};
  \node[draw=acc, text=acc, thick, minimum size=4.5mm, inner sep=1pt] (box) at (6.3,-1.6) {\ };
  % edges
  \draw[->, acc, thick] (ng) -- (r1);
  \draw[->, acc, thick] (E)  -- (r1);
  \draw[->, acc, thick] (r1) -- node[right, th] {x=Jack, y=Tuna} (r2);
  \draw[->, acc, thick] (C)  -- (r2);
  \draw[->, acc, thick] (r2) -- (r3);
  \draw[->, acc, thick] (D)  -- (r3);
  \draw[->, acc, thick] (r3) -- node[right, th] {z=G(Jack), x=Jack} (r4);
  \draw[->, acc, thick] (B)  -- (r4);
  \draw[->, acc, thick] (r4) -- node[right, th] {w=F(Jack)} (box);
  \draw[->, acc, thick] (F)  -- (box);
\end{tikzpicture}
$$

One subtlety: for _existential_ queries like "who killed the cat?" resolution can
return a **nonconstructive** proof, deriving $\exists w \; Kills(w, Tuna)$ without
committing to a single $w$. Tracking an **answer literal** through the proof recovers
the actual binding.

### Completeness

Resolution is **refutation-complete**: if a set of clauses is unsatisfiable, a finite
number of resolution steps derives the empty clause.[^aima-complete] The proof
threads three results. Any unsatisfiable clause set has an unsatisfiable finite set of
_ground instances_ (Herbrand's theorem); propositional resolution is complete on
those ground clauses (the ground resolution theorem); and a **lifting lemma** shows
every ground resolution proof is the shadow of a first-order one, obtained by
instantiating the MGU. So the empty clause reachable at the ground level is reachable
with the original first-order clauses. Instantiating variables only as far as a
proof requires, rather than exhaustively as propositionalization did, is resolution's
advantage.

This refutation-completeness is the first-order side of a deep result. In 1930 Gödel
proved that first-order logic has a complete proof procedure — every valid sentence is
provable — and a refutation-complete resolution system is one way to realize it.

> **Theorem (Gödel's completeness).** First-order logic is complete: for any set of
> sentences $KB$ and any sentence $\alpha$, if $KB \models \alpha$ then there is a
> finite proof of $\alpha$ from $KB$.

The result is not a promise of decidability — completeness says every entailment _has_
a proof, while semidecidability says we cannot always tell when one is absent. And
Gödel's later **incompleteness** theorem draws the boundary: extend the language with
arithmetic and induction, and there are true sentences no proof system can reach. The
completeness that resolution enjoys is a property of pure first-order logic, before
that extension.

### Resolution strategies

Refutation-completeness guarantees a proof exists; it says nothing about how
long the search for it takes. Applying resolution to every pair of clauses
generates a combinatorial flood of resolvents, most of them useless. A
**strategy** is a rule restricting which pairs to resolve, chosen so the
search reaches the empty clause sooner while keeping completeness.[^aima-strat]

> **Definition (Unit preference).** Prefer resolutions in which one clause is a
> **unit clause** — a single literal. Resolving with a unit shortens the other
> clause by one literal, and since the target is the empty (zero-literal)
> clause, shrinking clauses moves toward it. On Horn bases, unit resolution is
> not only a heuristic but complete on its own.

> **Definition (Set of support).** Fix a subset of clauses — the **support
> set** — and permit a resolution only when at least one parent is in it or
> descends from it. Taking the negated query as the initial support set keeps
> every resolution connected to the goal, ruling out inferences among
> background axioms that could never contribute. It stays complete provided the
> clauses outside the support set are satisfiable.

> **Definition (Input resolution).** Require every resolution to use at least
> one clause from the original input set — an axiom or the negated goal —
> rather than two derived clauses, giving the spine shape seen on the crime
> example. It is complete for Horn knowledge bases but not in general; the
> **linear** strategy, allowing a clause to resolve with one of its own
> ancestors, restores completeness.

Two more devices prune rather than direct. **Subsumption** discards any clause
already subsumed by one in the base — if $P(x)$ is known, the more specific
$P(A)$ carries no new information and can be deleted, keeping the clause set
free of redundancy. And clauses can be simplified by removing tautologies and
duplicated literals before they ever enter the pool.

$$
% caption: Four resolution strategies as restrictions on which clause pairs may
% be resolved. Unit preference and set of support steer the search toward the
% empty clause; input resolution constrains proof shape; subsumption deletes
% redundant clauses. Each keeps completeness under the stated conditions.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  bx/.style={draw, minimum width=54mm, minimum height=12mm, align=left, inner sep=4pt, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \node[bx, draw=acc] (u) at (0,0)     {\textbf{Unit pre\/ference}\\ prefer a unit-clause parent;\\ shrinks clauses toward empty};
  \node[bx] (s) at (6.4,0)             {\textbf{Set of support}\\ one parent from the\\ goal-linked support set};
  \node[bx] (i) at (0,-1.9)            {\textbf{Input resolution}\\ one parent from the\\ original clauses};
  \node[bx] (b) at (6.4,-1.9)          {\textbf{Subsumption}\\ delete clauses a more\\ general one covers};
\end{tikzpicture}
$$

### Handling equality

Resolution as stated treats $=$ as one more predicate, which is not enough:
from $A = B$ and $P(A)$ it will not derive $P(B)$ without help, because the two
$A$ terms never meet a complementary literal to resolve on. One remedy is to
add the axioms of equality — reflexivity, symmetry, transitivity, and a
substitution axiom for every function and predicate — but these generate large
numbers of resolvents. The alternatives build equality reasoning into the
inference rule.[^aima-eq]

> **Definition (Demodulation).** Given a unit equation $s = t$ and a clause
> containing a term $u$ that unifies with $s$ under $\theta$, replace $u$ by
> $\textsc{Subst}(\theta, t)$. Demodulation rewrites terms in one direction,
> normally toward a simpler canonical form.

**Paramodulation** is the more general rule: it resolves on an equation
without requiring it to be a separate unit clause, so equality reasoning
interleaves with the rest of the proof. Resolution with paramodulation is
refutation-complete for first-order logic with equality, and it is the
equality machinery inside modern provers.

## Modern automated theorem provers

The resolution and unification machinery in this lesson still runs inside the
automated reasoning tools used today, though the winning provers refine it
well past binary resolution. The dominant calculus is **superposition**, an
ordered combination of resolution and paramodulation that uses term orderings
to restrict which inferences are allowed. **E**, described by Stephan Schulz
(2002, in the _Journal of the AI Communications_), and **Vampire**, described
by Laura Kovács and Andrei Voronkov (2013, in _Computer Aided Verification_,
CAV), are two saturation-based superposition provers built on this calculus;
both take a first-order problem, saturate the clause set under the inference
rules with the redundancy elimination and indexing sketched above, and search
for the empty clause. These systems are compared each year at **CASC**, the CADE
ATP System Competition, organized by Geoff Sutcliffe on the TPTP problem
library.[^byb-provers]

A second line handles logic with background theories. **SMT** solvers —
satisfiability modulo theories — pair a propositional SAT core with dedicated
decision procedures for theories like linear arithmetic, arrays, and
bit-vectors, so the Boolean search delegates theory-specific facts to a
specialist rather than encoding them as clauses. **Z3**, described by Leonardo
de Moura and Nikolaj Bjørner (2008, in _Tools and Algorithms for the
Construction and Analysis of Systems_, TACAS), is one such solver, used widely
in program verification and symbolic execution. The division of labor echoes
this lesson's split between a general search procedure and specialized handling
of equality: SMT generalizes that idea to a whole catalog of theories.

$$
% caption: Two descendants of first-order resolution. Left: saturation provers
% (E, Vampire) run superposition — ordered resolution plus paramodulation —
% over a clause set toward the empty clause. Right: SMT solvers (Z3) split the
% work between a SAT core and theory solvers. Both build on the resolution and
% equality machinery of this lesson.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  bx/.style={draw, minimum width=44mm, minimum height=9mm, align=center, inner sep=4pt, font=\scriptsize},
  sm/.style={draw, minimum width=30mm, minimum height=8mm, align=center, inner sep=3pt, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \definecolor{red}{HTML}{C0392B}
  \node[bx, draw=acc, text=acc] (sup) at (0,1.2) {Saturation prover\\ (E, Vampire)};
  \node[sm] (calc) at (0,-0.4) {superposition:\\ ordered resolution\\ + paramodulation};
  \draw[->, acc, thick] (sup) -- (calc);
  \node[anchor=north, text=black, font=\scriptsize] at (0,-1.5) {toward the empty clause};
  % SMT side
  \node[bx, draw=red, text=red] (smt) at (7.2,1.2) {SMT solver (Z3)};
  \node[sm] (sat) at (5.7,-0.4) {SAT core};
  \node[sm] (theory) at (8.9,-0.4) {theory solvers:\\ arithmetic, arrays};
  \draw[->, red, thick] (smt) -- (sat);
  \draw[->, red, thick] (smt) -- (theory);
  \draw[<->, dashed, black] (sat) -- (theory);
\end{tikzpicture}
$$

The heritage runs back through Prolog. The **answer-set programming** family
and modern **Datalog** engines descend from the logic-programming and
resolution tradition, with declarative languages whose execution is inference
over Horn-like rules. What began as a proof procedure for pure first-order
logic became a set of engines that verify programs, solve constraints, and
answer database queries.

## Where inference leads

Unification underlies everything here. It turns universal
instantiation from an infinite enumeration into a targeted match; it lifts modus
ponens into generalized modus ponens, which drives forward and backward chaining and
underwrites Prolog; and lifted into the resolution rule, it makes a single complete
proof procedure possible. The rest is strategy — data-driven versus goal-driven,
Horn-restricted chaining versus general refutation. What all of it computes is
_entailment_: what follows, with certainty, from what is known. The next module turns
that capability outward, using logical representation and inference to choose actions
rather than merely deduce facts, in
[classical planning](/artificial-intelligence/logic-and-planning/classical-planning).

[^aima-res]: **Russell & Norvig**, _AIMA_, §9.5.1–9.5.2 — Resolution: CNF for first-order logic, the conversion procedure with skolemization and Skolem functions, the lifted binary resolution rule, and factoring for completeness.
[^aima-cat]: **Russell & Norvig**, _AIMA_, §9.5.3, Figure 9.12 — the "Curiosity killed the cat" refutation using skolemization and factoring, and the nonconstructive-proof issue for existential goals resolved by answer literals.
[^aima-complete]: **Russell & Norvig**, _AIMA_, §9.5.4 — Completeness of resolution: refutation-completeness via Herbrand's theorem, the ground resolution theorem, and the lifting lemma; and Gödel's 1930 completeness theorem for first-order logic.
[^aima-eq]: **Russell & Norvig**, _AIMA_, §9.5.5 — Equality: the equality axioms, demodulation rewriting a term using a unit equation $s = t$, and paramodulation as the complete equality-resolution rule for first-order logic with equality.
[^aima-strat]: **Russell & Norvig**, _AIMA_, §9.5.6 — Resolution strategies: unit preference, set of support with the negated query as initial support, input and linear resolution and their completeness limits, and subsumption for eliminating redundant clauses.