The Resolution Method and Unification

Motivation: Automated Theorem Proving

How can a computer prove mathematical theorems? The resolution method (Robinson, 1965) is an algorithm that reduces checking logical consequence to searching for a contradiction: we negate the conclusion, add it to the premises, and try to derive the empty disjunct ☐. This is the foundation of the Prolog language and modern ATP systems.

Conversion to Clausal Form

Steps:

1. Eliminate → and ↔.
2. Push ¬ inward (De Morgan's laws, elimination of double negation).
3. Rename variables (each quantifier gets its own variable).
4. Move quantifiers to the front (convert to prenex form).
5. Skolemization: eliminate ∃. ∃x P(x) → P(c) (new Skolem constant); ∀y ∃x P(x,y) → ∀y P(f(y),y) (new Skolem function f).
6. Remove ∀ (variables are assumed universally quantified).
7. Distribute ∨ over ∧ → CNF (set of disjuncts).

Skolemization preserves satisfiability (but not logical equivalence).

Unification

A substitution σ is a mapping of variables → terms. σ(t) is the result of applying σ to term t.

A unifier for a set of pairs {(s₁,t₁),...,(sₙ,tₙ)}: σ such that σ(sᵢ) = σ(tᵢ) for all i.

Most General Unifier (MGU): σ such that any other unifier τ = τ' ∘ σ. The MGU is unique up to variable renaming.

Unification algorithm:

• If s = x (a variable): check the occur check (x does not occur in t) → σ = {x↦t}.
• If s = f(s₁,...,sₙ) and t = f(t₁,...,tₙ): unify pairwise.
• If s and t are different constants or functors of different arity → failure.

The Resolution Rule

Propositional resolution: from (D₁ ∨ l) and (D₂ ∨ ¬l) → resolvent D₁ ∨ D₂.

First-order resolution: from clauses C₁ (with literal l₁) and C₂ (with literal ¬l₂), if σ = MGU(l₁, l₂): Resolvent = σ(C₁ {l₁}) ∨ σ(C₂ {l₂}).

Robinson's Theorem (completeness of resolution): A set of clauses S is unsatisfiable ⟺ the empty disjunct ☐ is derived from S by a finite chain of resolutions.

Numerical Example

Problem: Prove "Socrates is mortal" from "All men are mortal" and "Socrates is a man".

Step 1. Formalization:

• ∀x (Human(x) → Mortal(x)) → clause: {¬Human(x) ∨ Mortal(x)}
• Human(Socrates) → clause: {Human(Socrates)}
• Negation of the conclusion: ¬Mortal(Socrates) → clause: {¬Mortal(Socrates)}

Step 2. Unification x ↦ Socrates for the first clause and {Human(Socrates)}: MGU: {x ↦ Socrates}. Resolvent from {¬Human(x) ∨ Mortal(x)} and {Human(Socrates)}: {Mortal(Socrates)}.

Step 3. Resolution of {Mortal(Socrates)} and {¬Mortal(Socrates)} (MGU = ε): Resolvent: ☐ (empty disjunct).

Conclusion: The set of clauses is unsatisfiable → the conclusion follows from the premises ✓.

Real-World Application

Prolog is a programming language based on resolution. The query ?- mortal(X). is solved by searching for a unifier and resolution with the knowledge base. Used in expert systems, NLP, and planning.

Additional Aspects

The resolution method is the only inference rule sufficient for refutation of inconsistent sets of clauses (resolution completeness theorem). In combination with the unification algorithm, it provides an efficient mechanical method for theorem proving in predicate logic. Robinson's algorithm (1965) finds the most general unifier in linear time given an appropriate representation. Modern systems (Vampire, E) use resolution plus hundreds of clause selection heuristics: literal selection, term ordering (KBO/LPO), redundancy elimination. This allowed, in 1996, for a computer to prove the Robbins conjecture on Boolean algebra—the first significant open theorem proved by an ATP system.

Connection with Other Areas of Mathematics

Resolution and unification, as tools of first-order logic, intersect with a number of "pure mathematical" disciplines through model-theoretic and computational aspects. Skolemization relies on results of Löwenheim and Skolem on normal forms and is closely related to the Löwenheim–Skolem lemma: every countably axiomatizable theory with an infinite model has a countable model. The existence of Skolem functions is interpreted as the selection of concrete "witnesses" for quantifiers in models.

In universal algebra and rewriting theory, unification appears as solving equations in free algebras: the classical result of Martelli–Montanari (1976) formalizes unification in terms of rewriting systems. Here, bridges are also built to commutative algebra via unification modulo equivalence (unification modulo theories), for example modulo associativity and commutativity; this echoes Gröbner basis techniques (Buchberger) in solving polynomial equations.

In proof theory, the resolution method is compared with Gentzen's sequent calculus: the completeness theorem for resolution can be interpreted as the existence of a certain class of cuts in LK calculus. The works of Smullyan, Schütte, and later Buchberger and Baumgart point to connections between resolution strategies and normal forms of proofs.

In applied mathematics and numerical methods, resolution techniques are used indirectly via SMT solvers (Z3, CVC4), where the logical parts of hybrid optimization and differential equation problems (e.g., in invariant verification for ODE systems) are handled by logical engines based on unification and resolution. In probabilistic logic and Markov/halpern Bayesian networks, generalizations of resolution are used to derive conditional probabilities in symbolic form.

Historical Background and Development of the Idea

The roots of the resolution method trace back to the classic work of David Hilbert and Paul Bernays "Grundlagen der Mathematik" (1934–1939), where proofs in first-order logic were formalized. The idea of normal forms and the elimination of quantifiers via functions was developed by Thoralf Skolem in the 1920s, laying the groundwork for Skolemization. The modern form of the resolution rule was introduced by John Alan Robinson in his article "A Machine-Oriented Logic Based on the Resolution Principle" (Journal of the ACM, 1965). Robinson combined two traditions: Gentzen's sequent methods and the practical problem of proof automation. His motivation was to implement an efficient, essentially unique inference rule suitable for machine implementation, unlike the cumbersome natural deduction systems. In the 1970s–1980s, resolution methods became the core of automatic theorem-proving systems: works by Loveland, Luckham, Wos, and the joint Boyer–Moore project shaped a culture of "machine proofs". In parallel, unification theory progressed: the work of Herbrand, then P. Martelli and U. Montanari (Journal of the ACM, 1982), provided a general algorithm and proved the uniqueness of the most general unifier. A breakthrough was the creation of the Prolog language (Colmerauer, Roussel, 1972) and the monographs by Clocksin and Lloyd, where SLD-resolution became the foundation of logic programming. By the late 20th century, resolution had evolved into powerful ATP systems: Otter (McCune), later Vampire (Rashkovich, Voronkov, 1990s), and E (Schulz). In 1996 Larry Wos and colleagues confirmed the Robbins hypothesis on Boolean algebra using EQP, symbolizing the maturity of resolution methods.