Resolution principle

The resolution principle is a single inference rule for first-order logic proposed by J. A. Robinson in 1965, which provides a refutation-complete method for automated theorem proving. The rule is deceptively simple: from two clauses containing complementary literals, derive a new clause (the resolvent) containing all literals except the complementary pair. A clause is a disjunction of literals; a literal is an atomic formula or its negation. The process of resolving clauses continues until the empty clause — a contradiction — is derived, or until the search space is exhausted.

Resolution is complete for first-order logic: if a set of clauses is unsatisfiable, resolution will eventually derive the empty clause. This completeness made it the foundation of the first generation of ATP systems and remains the basis of modern saturation provers like Vampire and E. However, resolution is not efficient without guidance. The search space grows exponentially, and the art of resolution-based proving lies in clause selection, term indexing, and redundancy elimination — strategies that prune the search without sacrificing completeness.

The resolution principle also depends on unification, the process of finding a most general substitution that makes two atomic formulas identical. Unification is the computational engine beneath resolution; without it, resolution could not instantiate variables to match complementary literals across different clauses. Together, resolution and unification form the backbone of classical ATP.

Resolution reduced theorem proving to a search problem, and in doing so revealed that the difficulty of proof is not the scarcity of inference rules but the abundance of possible inferences. The challenge of ATP is not finding a proof; it is finding a proof before the combinatorics bury it.