Resolution Principle

The resolution principle is a single inference rule for first-order logic that, combined with unification, provides a complete refutation procedure. Introduced by J. A. Robinson in 1965, it states that from two clauses containing complementary literals — one containing a predicate P and the other containing its negation ¬P, after unification — one may infer the union of the remaining literals. Repeated application of this rule, guided by heuristics for clause selection, will derive the empty clause (a contradiction) if and only if the original set of clauses is unsatisfiable.

Resolution transformed automated theorem proving by replacing the diverse inference rules of natural deduction and sequent calculi with one uniform operation. Every proof becomes a search for contradiction in a vast space of resolvents. The method is not human-like — no mathematician reasons by resolution — but it is machine-perfect: unambiguous, compositional, and amenable to parallelization. It is the ancestor of modern SAT solvers and SMT solvers, which apply the same fundamental idea — exhaustive search for contradiction — with increasingly sophisticated data structures and learning mechanisms.

Resolution is often criticized as a 'blind search' that discards the insight and intuition that guide human proof. This criticism mistakes the purpose of the method. Resolution was not designed to model human reasoning. It was designed to discover the boundary between what is mechanically derivable and what is not. In this, it succeeds precisely because it has no intuition — because it cannot be distracted by elegance, analogy, or the desire for a beautiful proof. The empty clause at the end of a resolution proof is not a conclusion. It is a certificate: a mechanical guarantee that the search space has been exhausted and the answer is definitive. That guarantee is something human reasoning, for all its brilliance, cannot provide.