Textbook of AI

Resolution is the inference rule introduced by J. A. Robinson in 1965. Stated in its simplest propositional form: from clauses (A ∨ B) and (¬A ∨ C) infer (B ∨ C). Iterated resolution between clauses, with unification to find compatible variable bindings in the first-order case, eventually derives the empty clause from any unsatisfiable set, proving the negation of any theorem. Resolution is refutation-complete for first-order logic: if a formula is unsatisfiable, resolution will derive the empty clause in finite time.

Resolution requires that formulas first be converted to clausal normal form (a conjunction of disjunctions of literals), a transformation that can in principle blow up the formula exponentially. Skolemisation removes existential quantifiers by introducing Skolem functions before clausification.

Practical resolution provers use various refinements: set-of-support strategy (resolve only with descendants of the negated goal), input resolution (every step uses an input clause), linear resolution, and paramodulation for equality reasoning. The most influential restricted form is SLD-resolution (Linear resolution with Selection function for Definite clauses), which is the execution mechanism of Prolog and the basis of all logic programming.

Resolution dominated automated theorem proving for thirty years. Modern provers (Vampire, E, Spass) still use it as their core inference rule, supplemented by extensive heuristics for clause selection and an extensive armoury of pre-processing transformations.