Resolution and Unification
Motivation
Resolution is a single inference rule that is sufficient for complete automated theorem proving (Robinson 1965). Combined with unification — the algorithm for matching terms with variables — it underlies both logical refutation provers and logic programming languages such as Prolog (Russell and Norvig 2020).
Where forward chaining and backward chaining work on the restricted definite Horn clauses, resolution handles arbitrary first-order clauses and is complete for entailment in first-order logic.
Problem
Given a knowledge base \(KB\) (a set of first-order sentences) and a query sentence \(\phi\), decide whether \(KB \models \phi\) (the KB entails \(\phi\)).
Resolution attacks this by refutation: prove \(KB \models \phi\) by showing that \(KB \cup \{\lnot \phi\}\) is unsatisfiable.
Key Ideas
Propositional resolution
A clause is a disjunction of literals, e.g., \((\lnot p \lor q \lor r)\). Given two clauses that contain complementary literals \(\ell\) and \(\lnot \ell\), the resolution rule produces their resolvent:
\[\frac{\ell \lor C_1 \qquad \lnot \ell \lor C_2}{C_1 \lor C_2}\]
The resolvent \(C_1 \lor C_2\) is a logical consequence of both parent clauses. The literal \(\ell\) is resolved away. Example: from \((\lnot p \lor q)\) and \((p \lor r)\), resolve on \(p\) to get \((q \lor r)\).
Refutation as proof by contradiction
To prove \(KB \models \phi\), resolution proceeds by contradiction:
- Convert \(KB \cup \{\lnot \phi\}\) to conjunctive normal form (CNF).
- Repeatedly apply resolution to derive new clauses.
- If the empty clause \(\square\) (contradiction) is derived, then \(KB \cup \{\lnot \phi\}\) is unsatisfiable, so \(KB \models \phi\).
The empty clause is unsatisfiable by definition (a disjunction of zero literals has no satisfying valuation). Deriving it from \(KB \cup \{\lnot \phi\}\) proves the set is unsatisfiable.
Unification: matching terms with variables
In first-order logic, clause literals may contain variables. Unification finds a substitution that makes two terms syntactically identical.
A substitution \(\theta = \{x_1 \mapsto t_1, \ldots, x_n \mapsto t_n\}\) replaces variables with terms. Substitution \(\theta\) unifies terms \(s\) and \(t\) if \(\theta(s) = \theta(t)\).
The most general unifier (MGU) \(\theta^*\) of \(s\) and \(t\) is a unifier such that every other unifier \(\sigma\) factors as \(\sigma = \rho \circ \theta^*\) for some substitution \(\rho\). The MGU is unique up to variable renaming.
The standard unification algorithm operates on sets of equations \(\{s_i = t_i\}\):
- Decompose: \(f(s_1, \ldots, s_n) = f(t_1, \ldots, t_n)\) → replace with \(\{s_1 = t_1, \ldots, s_n = t_n\}\).
- Eliminate: \(x = t\) with \(x\) a variable → apply \(x \mapsto t\) everywhere; add to \(\theta\).
- Occurs check: if \(x = t\) with \(x \in \text{vars}(t)\) and \(x \neq t\), fail (circular).
- Clash: \(f(\ldots) = g(\ldots)\) with \(f \neq g\), fail.
First-order resolution
Given clauses \(C_1\) and \(C_2\) (with no shared variables; rename apart if needed), if literal \(L_1 \in C_1\) and \(\lnot L_2 \in C_2\) have MGU \(\theta = \text{MGU}(L_1, L_2)\), the first-order resolvent is:
\[\theta(C_1 \setminus \{L_1\}) \cup \theta(C_2 \setminus \{\lnot L_2\}).\]
The substitution \(\theta\) is applied to both clauses before forming the resolvent. Example: from \(P(x) \lor Q(x)\) and \(\lnot P(f(a)) \lor R(y)\), unify \(P(x)\) and \(P(f(a))\) with \(\theta = \{x \mapsto f(a)\}\), giving resolvent \(Q(f(a)) \lor R(y)\).
Algorithm
function REFUTE(KB, φ):
S ← CNF(KB ∪ {¬φ}) # set of clauses
new ← ∅
repeat:
for each pair of clauses (C₁, C₂) in S with C₁ ≠ C₂:
for each complementary literal pair (L₁ in C₁, ¬L₂ in C₂):
θ ← MGU(L₁, L₂)
if θ succeeds:
R ← θ(C₁ \ {L₁}) ∪ θ(C₂ \ {¬L₂})
if R = □: return SUCCESS # entailed
new ← new ∪ {R}
if new ⊆ S: return FAILURE # no new resolvents
S ← S ∪ newIn practice, the all-pairs enumeration is replaced by strategies (set of support, linear resolution, ordered resolution) that prune most resolutions while preserving completeness.
Walkthrough
Refuting a first-order goal
Knowledge base:
- \(\forall x.\, Q(x) \Rightarrow P(x)\)
- \(Q(a)\)
Goal: \(P(a)\).
Step 1 — convert to CNF. The implication becomes \(\lnot Q(x) \lor P(x)\), and the negated goal \(\lnot P(a)\) is added:
\[ S = \{\, \lnot Q(x) \lor P(x), \quad Q(a), \quad \lnot P(a) \,\}. \]
Step 2 — apply resolution:
| Step | Resolve | Unifier | Resolvent |
|---|---|---|---|
| 1 | \(\lnot Q(x) \lor P(x)\) with \(\lnot P(a)\) on \(P\) | \(\theta = \{x \mapsto a\}\) | \(\lnot Q(a)\) |
| 2 | \(\lnot Q(a)\) with \(Q(a)\) on \(Q\) | empty | \(\square\) |
The empty clause is derived, so \(KB \cup \{\lnot P(a)\}\) is unsatisfiable: \(KB \models P(a)\).
Notice that resolution used the rule \(\lnot Q(x) \lor P(x)\) backward (matching \(P(x)\) to the negated goal) and forward (matching \(\lnot Q(x)\) against \(Q(a)\)) in a single proof — there is no distinction in resolution between premise and conclusion.
Correctness
Soundness. Each resolution step produces a clause that is a logical consequence of its two parents — the resolvent holds in every model where both parents hold. So if the empty clause is derived, the original clause set has no model and is unsatisfiable.
Refutation completeness (Robinson 1965). If a set of clauses \(S\) is unsatisfiable, resolution will derive \(\square\) in finitely many steps. (proof) Combined with the reduction to CNF, this makes resolution a complete procedure for first-order logical entailment — every entailed sentence has a finite resolution refutation.
Resolution is refutation-complete, not generation-complete: it can prove any logical consequence but does not enumerate all consequences directly.
Complexity and Tradeoffs
First-order resolution is semidecidable: if \(KB \models \phi\) the procedure terminates with a proof, but if \(KB \not\models \phi\) it may run forever. This is unavoidable — first-order entailment itself is semidecidable (Church–Turing).
Naive resolution enumerates all pairs of clauses at each step, growing the clause set super-linearly. Practical theorem provers depend on search strategies to control the explosion (see Variants), and the empirical performance of state-of-the-art provers on theorems like the TPTP problem library reflects decades of strategy and data-structure engineering.
When to Use It
| Situation | Approach |
|---|---|
| Full first-order theorem proving | Resolution-based prover (Vampire, E, SPASS). |
| Horn-clause KB with focused query | Backward chaining (Prolog) — a special case of resolution that’s much cheaper. |
| Horn-clause KB with streaming facts | Forward chaining (Datalog) — also a special case. |
| Propositional SAT | Use DPLL/CDCL — purpose-built for propositional logic. |
| Decidable fragments (description logic, etc.) | Use a tableau-based decision procedure tailored to the fragment. |
Variants
- Set of support strategy. Restrict at least one parent of every resolution to a clause derived (transitively) from the negated goal. Preserves completeness, prunes irrelevant directions of search.
- Linear resolution. Each step uses the most recent resolvent as one parent. Used by Prolog under the name SLD resolution for Horn clauses.
- Hyper-resolution. Combine multiple resolution steps into one, eliminating all negative literals of a “nucleus” clause in a single inference. Reduces the proof length.
- Paramodulation. Adds an inference rule for equality, replacing equals with equals. Essential for theorem proving in theories with equality.
- Ordered resolution. Only resolve on literals maximal in some term ordering. Drastically reduces redundant inferences; standard in modern provers.