Mathematicsproof theory
Resolution and Unification
You should know: propositional logic, predicate logic
Overview
Resolution, introduced by John Alan Robinson in 1965, is a single, uniform inference rule that is refutation-complete for both propositional and first-order logic, meaning it can, in principle, detect the unsatisfiability of any inconsistent set of clauses. A clause is a disjunction of literals; the resolution rule takes two clauses that contain complementary literals (one has p, the other ¬p) and produces a new clause — the resolvent — consisting of the remaining literals of both, with the complementary pair removed. To prove a first-order sentence φ follows from a set of premises, resolution theorem provers negate φ, convert everything to clausal (conjunctive normal) form, and repeatedly resolve clauses looking for the empty clause □ (a contradiction); reaching □ certifies that the premises plus ¬φ are unsatisfiable, hence the premises entail φ. In first-order logic, resolving clauses with variables requires unification — the process of finding a substitution that makes two terms syntactically identical — and Robinson's unification algorithm computes a most general unifier (mgu), the least-committal substitution that works, from which every other unifying substitution can be obtained by further instantiation. This combination of resolution and unification is the theoretical engine behind automated theorem provers and the logic programming language Prolog.
Intuition
Resolution is 'cutting' two disjunctive facts against each other: if you know 'p or q' and separately 'not-p or r,' then whichever way p turns out, one of q or r must be true, so you can conclude 'q or r' and throw away the p / not-p pair entirely — that's the whole rule, applied repeatedly until either nothing new emerges or you squeeze out an outright contradiction (the empty clause, meaning 'false'). Unification is the first-order version of pattern matching: to resolve Loves(x, Mary) against ¬Loves(John, y), you need x = John and y = Mary simultaneously, and the most general unifier is the 'laziest' substitution achieving this — it commits to exactly what's forced (x↦John, y↦Mary) and nothing more, so the resulting clause stays as general as possible for future resolution steps.
Formal Definition
Clauses are sets/disjunctions of literals. The resolution rule and unification are defined as follows:
Worked Examples
Identify the complementary literals: p in the first clause, ¬p in the second.
Remove the complementary pair and union the remaining literals from both clauses.
Answer: The resolvent is {q, r} — i.e., q ∨ r.
Practice Problems
What is the resolvent of the clauses {¬p, q} and {p}?
What does it mean for σ to be a 'most general unifier' rather than just 'a unifier'?
Use propositional resolution to derive the empty clause from {p ∨ q, ¬p ∨ r, ¬q ∨ r, ¬r}.
Quiz
Summary
- Resolution is a single inference rule: from clauses C₁ ∪ {p} and C₂ ∪ {¬p}, derive the resolvent C₁ ∪ C₂; it is refutation-complete for propositional and first-order logic.
- A refutation proof negates the goal, clausifies everything, and repeatedly resolves clauses, looking for the empty clause □ (a contradiction).
- In first-order logic, resolving clauses with variables requires unification: computing a most general unifier (mgu), the least-committal substitution making two literals identical — the algorithmic core of Prolog and automated theorem provers.