Resolution (logic)

Resolution is a rule of inference used in propositional logic and first-order logic. It derives a new clause, called a resolvent, from two clauses containing complementary literals. Resolution is primarily a refutation method: the negation of a conjecture is combined with the premises, and derivation of the empty clause establishes that the resulting clause set is unsatisfiable.

The rule occupies a central position in automated theorem proving because a single inference schema can replace a larger collection of logical rules after formulas have been converted into clausal form. Its first-order version incorporates unification, allowing complementary literals containing variables to be matched by substitution. Resolution is refutationally complete for both propositional clauses and first-order clauses, although unrestricted application generates many clauses that do not contribute to a refutation.

Propositional resolution

A propositional clause is a finite disjunction of literals. If two clauses contain a proposition with opposite polarity, their resolvent is obtained by removing the complementary literals and combining the remaining disjuncts. In schematic form, the binary resolution rule is

[ \frac{C \lor p \qquad D \lor \neg p}{C \lor D}, ]

where (C) and (D) denote disjunctions that do not include the displayed occurrences of (p) and (\neg p). In the equivalent set representation of clauses, the rule has the form

[ \frac{C \cup {p} \qquad D \cup {\neg p}} {C \cup D}. ]

The rule is sound because every interpretation satisfying both parent clauses also satisfies the resolvent. When (p) is true, the second parent can be satisfied only through (D); when (p) is false, the first parent can be satisfied only through (C). Consequently, at least one literal in (C \lor D) is true under every interpretation satisfying both parents.

For example, the clauses

[ a \lor b ]

and

[ \neg b \lor c ]

have the resolvent

[ a \lor c. ]

A resolvent containing both a literal and its negation is a tautological clause. Such a clause is logically valid and ordinarily contributes no restriction to the clause set, although its removal is an implementation-level simplification rather than part of the resolution rule itself.

The empty clause, conventionally written (\Box), contains no literals and is false under every interpretation. A derivation of (\Box) therefore constitutes a resolution refutation. For the clause set

[ {p \lor q,; \neg p,; \neg q}, ]

resolution of (p \lor q) with (\neg p) produces (q), after which resolution with (\neg q) produces (\Box). The original clause set is consequently unsatisfiable.

Clausal representation and refutation

Resolution operates on formulas in conjunctive normal form, where a formula is represented as a conjunction of clauses. Propositional formulas can be transformed into an equivalent conjunctive normal form, although direct distribution can cause exponential growth. Definitional transformations such as the Tseytin transformation instead introduce auxiliary propositions and produce an equisatisfiable clause set of linear size.

For first-order formulas, clausal transformation includes elimination of implications, movement of negation to atomic formulas, standardization of bound variables, and removal of existential quantifiers by Skolemization. Skolemization preserves satisfiability rather than logical equivalence: the Skolemized formula has a model exactly when the relevant quantified formula has a model, but the formulas need not have identical meanings in every structure.

A theorem (F) follows from premises (\Gamma) precisely when

[ \Gamma \cup {\neg F} ]

is unsatisfiable. Resolution theorem proving therefore represents the premises together with a clausal form of the negated conclusion and attempts to derive the empty clause. A terminating derivation without the empty clause does not by itself establish satisfiability unless the employed calculus and termination condition provide an appropriate saturation result.

First-order resolution

First-order clauses may contain variables, function symbols, and predicate symbols. Complementary literals need not be syntactically identical before a resolution step, because a substitution can make their atomic parts identical. Given clauses

[ C \lor L ]

and

[ D \lor \neg L', ]

a substitution (\sigma) that unifies (L) and (L') yields the resolvent

[ (C \lor D)\sigma. ]

Resolution calculi generally use a most general unifier, which imposes no identifications beyond those required to match the selected literals. Any other unifier of the same literals can then be expressed as an instance of the most general unifier.

For example, the clauses

[ P(x) \lor R(x) ]

and

[ \neg P(f(y)) \lor S(y) ]

contain literals unified by the substitution

[ \sigma = {x \mapsto f(y)}. ]

Their resolvent is

[ R(f(y)) \lor S(y). ]

Variables belonging to different clauses are standardized apart before their interaction is represented, so an identically written variable in separate clauses does not accidentally denote the same quantified variable. This convention reflects the implicit universal quantification of variables in clauses.

First-order resolution is accompanied by factoring. If two literals within one clause are unifiable, factoring applies a unifier and removes the resulting duplicate. Thus a clause of the form

[ P(x) \lor P(f(y)) \lor C ]

can be factored when the displayed atoms admit a unifier. Factoring is required in the standard completeness analysis because a ground refutation can depend on multiple instances of literals that originate in a single non-ground clause.

Completeness

Propositional resolution is refutationally complete: every unsatisfiable finite set of propositional clauses has a resolution derivation of the empty clause. One proof interprets resolution as elimination of propositional variables. Clauses containing a positive occurrence of a selected variable are resolved with clauses containing its negative occurrence, after which the original clauses involving that variable can be removed. Repetition reduces the problem to a variable-free clause set whose unsatisfiability is represented by the empty clause.

First-order completeness connects resolution with Herbrand's theorem. If a first-order clause set is unsatisfiable, a finite set of its ground instances is already propositionally unsatisfiable. Propositional completeness supplies a refutation of those instances, while lifting reconstructs corresponding inferences at the first-order level through unification. The resulting statement is the lifting theorem, which explains why resolution does not require explicit enumeration of every ground instance appearing in a Herbrand universe.

Completeness does not imply termination. First-order validity is semidecidable: a fair complete resolution procedure eventually derives the empty clause for an unsatisfiable clause set, but it can continue indefinitely when the clause set is satisfiable. Propositional resolution concerns a decidable problem, although the number and size of generated clauses can still be exponential.

Historical development

Early antecedents of resolution appeared in work on canonical representations of Boolean functions. Archie Blake’s 1937 analysis of prime implicates described an operation closely related to propositional resolution, while Willard Van Orman Quine later developed consensus methods for simplifying Boolean expressions. These approaches treated the elimination of complementary variables as part of the algebraic analysis of propositional formulas.

Martin Davis and Hilary Putnam incorporated a resolution-style variable-elimination operation into their 1960 decision procedure for first-order logic, applied after grounding over finite portions of a Herbrand universe. The propositional component of this method subsequently formed part of the conceptual background of the Davis–Putnam–Logemann–Loveland algorithm, although DPLL replaces exhaustive retention of resolvents with a search based on assignments and propagation.

J. Alan Robinson presented the first-order resolution principle in 1965 and combined it explicitly with a general unification algorithm. His formulation established a uniform refutation calculus for first-order clauses and supplied the lifting argument connecting ground resolution to non-ground inference. This development consolidated clausal transformation, unification, and refutation completeness into the form used by later automated deduction systems.

Refinements of the calculus

Unrestricted resolution permits every complementary pair of literals to generate a resolvent. The resulting search space contains redundant clauses, repeated variants, and inferences unrelated to any minimal refutation. Resolution refinements restrict the admissible inferences while preserving refutational completeness under specified conditions.

In 1967, You Watanabe formulated a selection discipline in which designated negative literals controlled the admissibility of first-order resolution steps. Her completeness analysis connected literal selection with factoring and showed that the selection condition had to remain compatible with the ordering used to compare instantiated literals. The resulting formulation became an early instance of the general method now described as resolution with selection.

Ordered resolution admits an inference only when the resolved literals are maximal according to a suitable ordering. Selection functions can override maximality by designating particular negative literals, thereby imposing a structured dependence among possible inferences. Modern saturation calculi commonly combine ordering and selection with redundancy criteria that identify clauses already entailed in an appropriately smaller form.

Donald Loveland developed model elimination as a goal-directed refinement related to linear resolution. Robert Kowalski and Donald Kuehner established completeness results for linear resolution, in which one parent of each inference belongs to the evolving main derivation. These systems reduced the freedom of unrestricted resolution by organizing a refutation around a sequence of connected subgoals.

Subsumption provides a separate form of redundancy control. A clause (C) subsumes a clause (D) when a substitution makes (C) a subset of (D), so the instances represented by (C) are at least as general as those represented by (D). Tautology deletion and subsumption do not alter the logical consequences relevant to refutation, provided that their use satisfies the conditions of the underlying saturation calculus.

Horn clauses and logic programming

A Horn clause contains at most one positive literal. Definite Horn clauses can be written as implications whose antecedent is a conjunction of atoms and whose consequent is a single atom. Their restricted structure supports specialized forms of resolution with a more directed operational interpretation.

SLD resolution applies linear resolution to definite clauses using a selection rule for choosing an unresolved goal literal. A query is represented as a negative goal clause, and successful refutation derives the empty clause while composing the unifiers generated during the derivation. The restriction to definite programs makes the resulting calculus the standard operational basis of Prolog and related forms of logic programming.

The logical completeness of SLD resolution is stated relative to definite programs and appropriate fairness conditions. Its operational behavior also depends on clause order, literal selection, and the treatment of infinite terms, which are properties of a particular execution model rather than changes to the underlying logical consequence relation.

Relation to other proof systems

Resolution represents formulas primarily as clauses and treats proof construction as saturation or refutation. In contrast, natural deduction retains the connective structure of formulas and uses introduction and elimination rules. Sequent calculus similarly manipulates structured sequents and makes assumptions and conclusions explicit within each judgment.

Propositional resolution can be interpreted as a proof system for implicates, since each derived clause is a logical consequence of the initial set. It is also closely related to clause learning in modern Boolean satisfiability solvers. A conflict clause learned by a conflict-driven solver has a resolution derivation from clauses responsible for the conflict, although the solver organizes those derivations through assignments and implication graphs rather than unrestricted pairwise saturation.

First-order resolution forms part of broader saturation frameworks that include paramodulation and superposition calculus. Pure resolution treats equality as an ordinary predicate unless additional equality axioms are supplied. Paramodulation and superposition instead incorporate equality reasoning into the inference system, avoiding the large and redundant search spaces produced by unrestricted use of general equality axioms.