Resolution

Origin. J. A. Robinson, "A Machine-Oriented Logic Based on the Resolution Principle" (JACM, 1965), which fused Herbrand's theorem with a single inference rule and made the instantiation step computable by syntactic unification. It replaced the ground enumeration of Davis and Putnam (1960) and of Gilmore (1960), where every proof had to guess Herbrand instances in advance. Kowalski and Kuehner's SL-resolution (1971) and the SLD restriction to Horn clauses gave Prolog its execution model; Robinson and Wos added paramodulation (1969) for equality, which later became superposition.

Models. A formula is refuted, not proved. Everything is first put in clausal form — a conjunction of disjunctions of literals — after prenexing and Skolemization, which preserves satisfiability but not equivalence. Resolution then closes the clause set under one rule until the empty clause appears, and the empty clause is unsatisfiable, so its derivation refutes the original set. Unification supplies the substitution that makes two literals complementary, so the Herbrand instances are found rather than enumerated.

Formalism.

Clause: Disjunction of literals: L₁ ∨ L₂ ∨ ... ∨ Lₙ Literal: atom A or negation ¬A.

CNF (Conjunctive Normal Form): Conjunction of clauses. ∀∃ prenex, Skolemization for first-order.

Resolution rule (propositional): A ∨ C₁ ¬A ∨ C₂ ─────────────────── resolve on A C₁ ∨ C₂

Resolvent: C₁ ∨ C₂ with A, ¬A removed. If C₁ = C₂ = ∅: empty clause □.

First-order resolution: P(t̄) ∨ C₁ ¬P(s̄) ∨ C₂ σ = mgu(t̄, s̄) ────────────────────────────────────────── (C₁ ∨ C₂)σ

MGU: most general unifier.

Factoring: P(t̄) ∨ P(s̄) ∨ C σ = mgu(t̄, s̄) ────────────────────────────────── (P(t̄) ∨ C)σ Needed for completeness. Binary resolution alone is incomplete: {P(x) ∨ P(y), ¬P(u) ∨ ¬P(v)} is unsatisfiable but has no binary refutation.

Herbrand and lifting: Herbrand: an unsatisfiable clause set has an unsatisfiable finite set of ground instances. Lifting lemma: a ground resolution step lifts to a general one whose instance it is. Together these give completeness at the general level from completeness at the ground level.

Refutation completeness: Γ ⊨ φ iff Γ ∪ {¬φ} derives □.

Redundancy: Subsumption, tautology deletion, and ordering restrictions prune the search without losing completeness — provided the deletion criterion is redundancy-based.

Strategies: Set-of-support: restrict resolution pairs. Ordered resolution: fixed literal order. Hyperresolution: multiple steps. Paramodulation: equality handling.

Symbols.

Symbol	Unicode	Name	Meaning
∨	U+2228	Disjunction	Joins the literals of a clause
¬	U+00AC	Negation	Forms the negative literal ¬A
□	U+25A1	White square / Empty clause	The unsatisfiable clause ending a refutation
∅	U+2205	Empty set	The clause with no literals, written □
σ	U+03C3	Sigma / Substitution	The unifier applied to the resolvent
⊨	U+22A8	Entailment	Semantic consequence Γ ⊨ φ
∀	U+2200	Universal quantifier	Implicit over clause variables
∃	U+2203	Existential quantifier	Removed by Skolemization
t̄, s̄	—	Argument tuples	Term vectors unified by the mgu
mgu	—	Most general unifier	Every unifier factors through it
CNF	—	Conjunctive normal form	Clausal input format
SLD	—	Linear resolution with selection	Prolog's restriction to Horn clauses

Metatheory. Robinson (1965) proved refutation completeness: a clause set is unsatisfiable iff resolution together with factoring derives the empty clause. The proof is Herbrand's theorem plus the lifting lemma — completeness at the ground level lifts to the general level because every general resolvent has the ground resolvent as an instance. Factoring is not optional: binary resolution alone is incomplete, as {P(x) ∨ P(y), ¬P(u) ∨ ¬P(v)} shows. Refinements that preserve completeness include set-of-support (Wos), hyperresolution (Robinson), ordered and semantic resolution, and SL-resolution (Kowalski and Kuehner); SLD-resolution is complete for Horn clauses and is the operational semantics of Prolog. As a propositional proof system in the Cook–Reckhow sense, resolution is sound and complete for refuting CNF but is not polynomially bounded: Haken (1985) proved that refutations of the pigeonhole principle require size 2^Ω(n), and Urquhart (1987) proved exponential lower bounds for Tseitin formulas over expander graphs. Conflict-driven clause learning p-simulates general resolution, so those bounds bound SAT solvers too.

Applies to. Automated theorem proving. SAT/SMT solvers. Prolog execution. Verification. Answer extraction.

Limitations. Resolution refutes and does not prove: there is no derivation of φ, only a demonstration that ¬φ is inconsistent with the premises, and any answer must be read back off the refutation. It requires clausal form, so the input must first be prenexed and Skolemized — which preserves satisfiability but not logical equivalence and destroys the original formula's structure — and converted to CNF, where the distributive conversion is exponential and the Tseitin encoding avoids that only by introducing new variables. Equality is outside the rule: resolution with the equality axioms is complete but unusable, and paramodulation or superposition must be added. At first order the method is only semi-decidable, and on satisfiable clause sets saturation need not terminate; termination is a property of particular decidable fragments under particular orderings, not of the calculus. Haken's lower bound is unconditional, so no ordering, no strategy and no heuristic makes resolution polynomial on the pigeonhole principle. And completeness rests on classical prenexing and Skolemization, so the method does not transfer to intuitionistic or modal logic without substantial reworking.