Source Summary: Robinson 1965 — Resolution Principle
Full title: A Machine-Oriented Logic Based on the Resolution Principle
Authors: J. A. Robinson
Affiliation: Argonne National Laboratory / Rice University
Venue: Journal of the ACM, 12(1), pp. 23–41 (January 1965)
PDF: papers/robinson-1965-a-machine-oriented-logic-based-on.pdf
Contributions
- Resolution principle — a single inference rule that is both sound and complete for first-order logic. Replaces the combinatorial explosion of prior Herbrand-based methods.
- Unification algorithm — an efficient procedure for finding the most general substitution that makes two logical expressions identical.
- Refutation completeness — to prove a theorem P, assume ¬P and derive contradiction (the empty clause). Resolution is complete for this task.
- Foundation of automated theorem proving and logic programming — Prolog, CHR, and all logic programming descend directly from this paper.
The Problem (from PDF)
Prior theorem provers (based on Herbrand’s theorem) worked by:
- Generate substitutions of terms for variables (substitution stage)
- Check if the result is truth-functionally unsatisfiable (analysis stage)
- Repeat with more complex substitutions
The problem: the two stages are interleaved in an exponentially explosive cycle. Robinson’s key insight: both stages can be combined into a single new process — resolution.
Resolution: The Inference Rule
Clausal form
First, convert all sentences to clausal normal form: a conjunction of clauses, where each clause is a disjunction of literals (atoms or their negations).
Any first-order sentence can be converted to this form (Skolemization + CNF transformation).
Unification
Two atoms P(t₁,…,tₙ) and P(s₁,…,sₙ) unify if there exists a substitution θ such that:
P(t₁θ,...,tₙθ) = P(s₁θ,...,sₙθ)
The most general unifier (MGU) is the least committal such substitution.
The Resolution Rule
Given:
- Clause C₁ containing literal L
- Clause C₂ containing literal ¬L’ where L and L’ unify via MGU θ
Derive the resolvent:
(C₁ − {L}) ∪ (C₂ − {¬L'}) [after applying θ]
Example:
- C₁ = {P(x), Q(x)} (meaning: P(x) ∨ Q(x))
- C₂ = {¬P(a)}
- MGU: x = a
- Resolvent: {Q(a)}
Completeness
If a set of clauses S is unsatisfiable, then resolution will eventually derive the empty clause □.
This gives a refutation procedure: to prove theorem T from axioms A, show A ∪ {¬T} is unsatisfiable.
Why It Was Revolutionary
Before resolution, mechanical theorem proving required separate substitution + truth-functional analysis cycles — exponentially slow in practice.
Resolution:
- Reduces all of first-order logic to one inference rule
- Each resolution step simultaneously instantiates variables AND simplifies the clause set
- The search space is still large, but the per-step cost is dramatically lower
Result: for the first time, mechanical proofs of non-trivial theorems became practical.
Impact
| Descendant | Year | Connection |
|---|---|---|
| SL-resolution | 1971 | Linear restriction for efficiency |
| Prolog | 1972 | Logic programming = resolution + depth-first search |
| Otter / Vampire | 1980s–90s | High-performance resolution theorem provers |
| CHR | 1991 | Constraint handling via resolution |
| SAT solvers (DPLL) | 1960–present | Propositional resolution with learning |
Key References (from paper)
- Herbrand 1930 — Fundamental theorem (the problem resolution solves)
- Davis & Putnam 1960 — Earlier incomplete procedure
- Gilmore 1960 — First Herbrand-based theorem prover