Resolution

Origin. Robinson (1965). Refutation-complete for first-order logic. Clause form reasoning. Single inference rule. Foundation for Prolog and SAT solvers.

Models. Formulas in CNF (clauses). Resolution rule combines clauses. Refutation: derive empty clause. Unification for first-order.

Formalism.

Clause: Disjunction of literals: L₁ ∨ L₂ ∨ ... ∨ Lₙ Literal: atom A or negation ¬A.

CNF (Conjunctive Normal Form): Conjunction of clauses. ∀∃ prenex, Skolemization for first-order.

Resolution rule (propositional): A ∨ C₁ ¬A ∨ C₂ ─────────────────── resolve on A C₁ ∨ C₂

Resolvent: C₁ ∨ C₂ with A, ¬A removed. If C₁ = C₂ = ∅: empty clause □.

First-order resolution: P(t̄) ∨ C₁ ¬P(s̄) ∨ C₂ σ = mgu(t̄, s̄) ────────────────────────────────────────── (C₁ ∨ C₂)σ

MGU: most general unifier.

Refutation completeness: Γ ⊨ φ iff Γ ∪ {¬φ} derives □.

Strategies: Set-of-support: restrict resolution pairs. Ordered resolution: fixed literal order. Hyperresolution: multiple steps. Paramodulation: equality handling.

Symbols.

Symbol	Unicode	Name	Meaning
∨	U+2228	Disjunction	Clause
□	U+25A1	Empty clause	Contradiction
σ	U+03C3	Substitution	Unifier
mgu	—	MGU	Most general unifier

Metatheory. Refutation complete. Semi-decidable for FOL. Decidable fragments. SLD-resolution for logic programming.

Applies to. Automated theorem proving. SAT/SMT solvers. Prolog execution. Verification. Answer extraction.

Limitations. Only refutation. CNF conversion blowup. Search space exponential. Strategy crucial.