Resolution (logic)

• 1. Introduction

  ›

  Resolution, the logical inference rule, sits at the heart of nearly every automated theorem-proving system built since the 1960s. On the surface it looks like a single, clean operation: take two logical clauses, find a pair of complementary literals, cancel them out, and merge what remains into a new clause. That modest description hides an extraordinary ambition. The researchers who developed resolution wanted a machine to be able to prove mathematical truths on its own, without human guidance at each step. What makes that goal so difficult, and what makes resolution so powerful, is the question the rest of this documentary will pursue.

• 2. Davis, Putnam, and the Explosion Problem

  ›

  Davis and Putnam traced the earliest form of the resolution rule back to their work in 1960. Their algorithm could, in principle, decide whether a logical formula was unsatisfiable, but it came at a heavy price. To use their method, a machine had to try all possible ground instances of the formula being tested. That means substituting every possible concrete value for every variable and checking each combination separately. For even modestly complex formulas, the number of combinations balloons so rapidly that the method becomes unworkable. This is what logicians call combinatorial explosion, and it was the central obstacle standing between the ambition of automated proof and anything resembling practical computation. The Davis-Putnam algorithm was later refined into the DPLL algorithm, which removed the need to explicitly represent the resolvents produced along the way.

• 3. Robinson's Unification Breakthrough

  ›

  John Alan Robinson solved the explosion problem in 1965 with a technique called syntactical unification. Rather than substituting all possible values at the start and then checking every case, Robinson's algorithm waits. It instantiates variables only when the proof actually needs them, and only as far as necessary to maintain what he called refutation completeness. That phrase means the system will always find a contradiction if one is genuinely there to be found. The clause produced by a single application of the resolution rule is called a resolvent. When Robinson defined the rule, he also incorporated a step called factoring, which unifies two literals within the same clause before or during resolution. This addition turned out to be essential: there are sets of unsatisfiable clauses for which the empty clause, the target that signals a contradiction, can never be obtained by resolution alone without factoring.

• 4. How Refutation Works

  ›

  Resolution proves things by contradiction. If you want to verify that a conjecture follows from a set of axioms, you begin by assuming the conjecture is false. You then add that negation to the knowledge base, convert all the sentences into a standard form called conjunctive normal form, and collect all the resulting clauses into a set. From there, the machine systematically applies the resolution rule to every possible pair of clauses that share complementary literals. Any clause that turns out to be a tautology, meaning it contains a literal alongside its own negation, is discarded. New, non-redundant clauses get added to the set and become candidates for further resolution. If this process ever produces the empty clause, a clause with no literals at all, the original assumption was contradictory, which means the conjecture is true. If the process runs dry without producing the empty clause and no new clauses can be generated, the conjecture is not a theorem.

• 5. Resolution Meets First-Order Logic

  ›

  Propositional logic deals with fixed, unchanging statements, but first-order logic allows variables, predicates, and quantifiers. Robinson generalized resolution to cover this richer setting by incorporating the most general unifier into the rule. A most general unifier is a substitution that makes two expressions identical while committing as little as possible, leaving the maximum flexibility for the rest of the proof. The source text illustrates this with the syllogism about Homer: all Greeks are Europeans, Homer is a Greek, therefore Homer is a European. To apply resolution, both premises are converted into conjunctive normal form, with universal quantifiers simply omitted as implicitly understood and existentially quantified variables replaced by what are called Skolem functions. The predicate for being Greek appears in negated form in one clause and non-negated in the other. Unifying them binds the variable X to the constant a, the name for Homer, and combining the remaining predicates produces the conclusion directly. The Cretans-and-liars example in the source shows the same process applied to a chain of two implications, where a variable rename in the second clause keeps the two sets of variables distinct before unification.

• 6. Beyond Clausal Form

  ›

  Clausal normal form is convenient for machines but hostile to human readers. Researchers Murray, Manna, Waldinger, and Traugott each developed generalizations of the resolution rule that work directly on formulas that have not been converted to clause form. These non-clausal approaches matter most in interactive theorem proving, where a mathematician works alongside the machine and needs to read intermediate results. Avoiding the conversion to clause form also sidesteps some of the combinatorial growth that can occur during that transformation and sometimes reduces the total number of resolution steps. Traugott's rule is stronger than Murray's in a specific technical sense: comparing their results on the same example, Traugott's rule introduced no new binary junction symbols while Murray's introduced three. Because Traugott's intermediate formulas retain the structure of the user's own notation more faithfully, they can exploit implications in the original assumptions in ways that Murray's syntactically equivalent but differently shaped formulas cannot.

• 7. Paramodulation and Equality

  ›

  Standard resolution cannot reason directly about equality. Paramodulation is the technique developed to fill that gap. It applies when one of the clauses contains a positive equality literal, meaning a statement that two terms are the same. The operation finds a subterm in a second clause that can be unified with one side of that equality, then replaces that subterm with the other side, generating a new clause that reflects the substitution. The general aim is to reduce the system toward atoms, shrinking the size of terms as substitutions accumulate. Reflexive identities, statements of the form that something equals itself, are excluded from the generated clauses as useless. Seven theorem-proving systems are listed in the source as implementations that draw on these techniques: CARINE, GKC, Otter, Prover9, SNARK, SPASS, Vampire, and Logictools online prover, a range that spans from research prototypes to actively maintained solvers used in formal verification today.