Resolution Is Refutation-Complete
Claim
If a finite set of propositional clauses \(S\) is unsatisfiable, then resolution can derive the empty clause \(\square\) from \(S\) in finitely many steps (Robinson 1965).
Proof
By induction on \(n\), the number of distinct propositional symbols in \(S\).
Base case (\(n = 0\)). If \(S\) contains no propositional symbols, the only clause it can contain is \(\square\). Since \(S\) is unsatisfiable it must contain \(\square\), and we are done.
Inductive step. Assume the claim holds for all unsatisfiable clause sets with fewer than \(n\) symbols. Let \(S\) have \(n\) symbols; pick one, call it \(p\).
Define two derived sets by unit propagation on \(p\):
- \(S_p\): delete every clause containing \(p\) (satisfied when \(p\) is true), and delete \(\lnot p\) from every remaining clause.
- \(S_{\lnot p}\): delete every clause containing \(\lnot p\) (satisfied when \(p\) is false), and delete \(p\) from every remaining clause.
Since \(S\) is unsatisfiable, both \(S_p\) and \(S_{\lnot p}\) are unsatisfiable (any assignment either sets \(p\) true or false, and neither satisfies \(S\)). Both contain at most \(n - 1\) symbols. By the inductive hypothesis, resolution derives \(\square\) from \(S_p\) via derivation \(D_p\), and derives \(\square\) from \(S_{\lnot p}\) via derivation \(D_{\lnot p}\).
Lifting \(D_p\) to \(S\).
Each axiom clause \(C'\) used in \(D_p\) came from some clause \(C \in S\) by one of two operations:
- \(C' = C\) (clause did not contain \(p\) or \(\lnot p\)): use \(C\) directly.
- \(C' = C \setminus \{\lnot p\}\) (the \(\lnot p\) literal was deleted): replace \(C'\) with the original \(C = C' \cup \{\lnot p\}\).
Resolution steps in \(D_p\) that resolve on literals other than \(p\) remain valid in \(S\) (adding \(\lnot p\) to a clause does not prevent resolving on a different literal; it only adds \(\lnot p\) to the resolvent). After lifting, \(D_p\) becomes a derivation \(D_p'\) from \(S\) whose final clause is either \(\square\) or the unit clause \((\lnot p)\) (if \(\lnot p\) accumulated in the resolvents without being eliminated).
Similarly, lifting \(D_{\lnot p}\) to \(S\) yields a derivation \(D_{\lnot p}'\) from \(S\) whose final clause is either \(\square\) or \((p)\).
Combining. There are three cases:
- \(D_p'\) ends in \(\square\): done.
- \(D_{\lnot p}'\) ends in \(\square\): done.
- \(D_p'\) ends in \((\lnot p)\) and \(D_{\lnot p}'\) ends in \((p)\): resolve \((\lnot p)\) and \((p)\) to obtain \(\square\).
In every case, resolution derives \(\square\) from \(S\). \(\blacksquare\)
Extension to First-Order Logic
The first-order result follows from two additional facts:
- Herbrand’s theorem: a set of first-order clauses \(S\) is unsatisfiable if and only if some finite set of ground instances of \(S\) is propositionally unsatisfiable.
- Lifting lemma: any propositional resolution step on ground instances can be lifted to a first-order resolution step on the original clauses using the most general unifier, with the ground step being an instance of the lifted step.
Together these show that whenever a finite unsatisfiable set of ground instances exists (Herbrand), a refutation of the ground instances exists (propositional completeness above), and that refutation lifts to a first-order refutation (lifting lemma). Therefore first-order resolution is also refutation-complete.