A proof method that demonstrates the unsatisfiability of a set of clauses by repeatedly applying the resolution rule to produce new clauses until the empty clause is derived, indicating a contradiction.

Principle

Use the binary resolution rule to combine clauses containing complementary literals, optionally with unification in the first-order case, and control the search (selection, ordering, subsumption) so that derivation of the empty clause is reachable if the clause set is unsatisfiable.

Demonstration

Starting from clauses {p ∨ q, ¬q ∨ r, ¬r, ¬p}, resolve p ∨ q with ¬p to derive q, resolve q with ¬q ∨ r to derive r, resolve r with ¬r to derive the empty clause, thereby refuting the original set.

Misapplication

Applying propositional resolution procedures verbatim to unconstrained first-order clause sets without unification or without strategies for termination, or assuming resolution always produces short or human-readable proofs; naive expansion can explode combinatorially.

Consequence

Resolution refutation is sound and, for propositional logic and appropriately configured first-order settings, refutation-complete: if the clause set is unsatisfiable, a refutation exists; it underpins many automated theorem provers and SAT solvers (after CNF transformation and sometimes with additional mechanisms).

Reversal

The inversion is constructive proof search (e.g., tableau or natural deduction producing a direct derivation of the formula) rather than refutation by contradiction; in the reversed approach one attempts to build a model or direct proof instead of deriving a contradiction.

Boundary

Applicable to clause form (CNF) representations; pure resolution does not by itself construct models for satisfiable sets and, in first-order logic, may not terminate without suitable strategies or restrictions (e.g., ordering, selection, or loop check).

Semantic Tension

There is tension between resolution refutation and sequent or natural deduction styles: resolution is oriented towards refutation and algorithmic search over clauses, while other styles emphasize constructive witness extraction and different proof shapes and normal forms.

Synthesis

Resolution refutation combines the local inference rule of resolution with unification (in first-order) and global search control so that contradictions are derived from clause sets; it transforms the task of proving validity into a systematic clause-elimination search that either yields the empty clause or fails to refute.