Resolution theorem proving, with a worked example

The resolution rule in one line

Resolution works on clauses, which are disjunctions of literals. A literal is an atomic statement or its negation. If one clause contains a literal L and another contains the negation of L, the rule lets you merge the two clauses and drop the clashing pair. From (A or L) and (B or not L) you may conclude (A or B).

The rule was published by J. A. Robinson in 1965, in a paper titled A Machine-Oriented Logic Based on the Resolution Principle. The title is the point: the rule is simple enough to be applied mechanically, with no human choosing clever steps.

Proof by refutation and the empty clause

A resolution prover does not try to build a proof of the goal directly. It adds the negation of the goal to the premises and looks for a contradiction. If the combined set of clauses can be shown to be unsatisfiable, the original goal follows from the premises.

A contradiction shows up as the empty clause, written as a small empty box. It appears when two unit clauses clash, for example P and not P. Resolving them leaves nothing: no literals, and therefore no way to make the clause true. Once the empty clause is derived, the search is over.

Resolution is refutation complete for first-order logic. If a clause set is unsatisfiable, some sequence of resolution steps (together with factoring, which merges identical literals in one clause) reaches the empty clause. The converse also holds: the rule is sound, so it never derives the empty clause from a satisfiable set.

A worked resolution example

Take three statements. Every human is mortal, written as the clause not Human(x) or Mortal(x). Socrates is human, written as Human(Socrates). The goal is that Socrates is mortal, so its negation not Mortal(Socrates) joins the set.

Resolving the first two clauses, with x replaced by Socrates, gives Mortal(Socrates). Resolving that with the negated goal gives the empty clause. The set is contradictory, so the goal is proved. The pinned section on the home page replays exactly this derivation.

The unification algorithm, with an example

In first-order logic literals contain variables, so two literals rarely match letter for letter. The prover finds a substitution that makes them identical, called a unifier. Robinson's paper also gave an algorithm for computing a most general unifier, the substitution that commits to as little as possible.

Unification is why the Socrates step works: replacing x by Socrates makes Human(x) and Human(Socrates) the same literal. A second example: to unify Loves(x, Mary) with Loves(John, y) the algorithm binds x to John and y to Mary, giving Loves(John, Mary). To unify P(x) with P(f(x)) it fails, because x would have to contain itself, and the check that catches this is called the occurs check.

Why a resolution theorem prover needs a search strategy

Applying the rule is easy. Deciding which clauses to combine is hard, because the number of derivable clauses grows quickly. Practical provers use a given-clause loop, simplification rules such as subsumption (deleting a clause that is implied by a more general one), term orderings that restrict which literals may be resolved, and strategies such as the set of support, introduced in the 1960s.

Modern provers that handle equality usually rely on superposition, a refinement that builds equational reasoning into the calculus. The core remains the same: derive new clauses until the empty clause appears or time runs out.