## Definition **Resolution** is a single inference rule that, combined with unification, is *refutation-complete* for propositional and first-order logic in clausal form. Introduced by John Alan Robinson in 1965 — the breakthrough that made automated theorem proving practical. ## The Rule In clausal form: $\frac{C_1 \lor \ell, \quad C_2 \lor \neg \ell}{C_1 \lor C_2}$ Two clauses containing complementary literals ($\ell$ and $\neg \ell$) produce a new clause (the *resolvent*) consisting of the remaining literals. ## Proof by Contradiction To prove $KB \models \alpha$, one shows $KB \cup \{\neg \alpha\}$ is unsatisfiable: 1. Convert $KB \cup \{\neg \alpha\}$ to CNF. 2. Apply resolution repeatedly. 3. If the empty clause $\bot$ is derived, $KB \models \alpha$. This is the standard proof-by-contradiction shape. ## First-Order Resolution Adds **unification** to handle variables. Two literals $P(x)$ and $\neg P(a)$ aren't directly complementary, but unifying $\{x/a\}$ makes them so. The unified clause $C_1 \lor C_2$ has the substitution applied. ## Refutation Completeness If $\alpha$ is unsatisfiable, resolution eventually derives $\bot$. (Not the same as completeness for arbitrary inference; resolution can't derive every entailment, only test unsatisfiability.) ## Strategies Naive resolution explores too many derivations. Search strategies prune: - **Unit preference** — prefer clauses that resolve to shorter clauses. - **Set-of-support** — at least one parent must come from the negated goal or its descendants. - **Linear resolution** — every step uses the most recent resolvent. - **Subsumption** — discard clauses subsumed by simpler ones. ## Limitations - **Undecidability of FOL.** Resolution semi-decides — it confirms unsatisfiability when it holds, but may not halt otherwise. - **Combinatorial explosion** in practice on non-trivial knowledge bases. Most modern systems use specialised SAT solvers (CDCL — Conflict-Driven Clause Learning) on propositional encodings rather than full FOL resolution. SMT solvers extend SAT with theory reasoning (arithmetic, arrays, etc.). ## Related - [[Propositional Logic]] - [[First-Order Logic]] - [[Inference Rules]]