Resolution in FOL

Mathematical Logic · Axiom Academy

LESSON Resolution in First-Order Logic Master resolution theorem proving for first-order logic through unification and refutation. Resolution is a complete inference rule that forms the foundation of automated theorem proving. 1. Review: Propositional Resolution In propositional logic, resolution works with clauses —disjunctions of literals. The resolution rule states: if we have a clause containing literal L and another clause containing ¬L, we can combine them by removing both L and ¬L. 2. Clausal Form in First-Order Logic To apply resolution in FOL, we must first convert formulas to clausal form. This involves several steps: eliminate implications, move negations inward, standardize variables, eliminate existential quantifiers (Skolemization), and distribute disjunctions over conjunctions. Eliminate → and ↔ using logical equivalences Move ¬ inward using De Morgan's laws Standardize variables (rename to avoid conflicts) Skolemize: Replace ∃x with Skolem functions Move universal quantifiers to the front Distribute ∨ over ∧ to get CNF Drop universal quantifiers (implicitly universal) Eliminate →: ∀x(¬P(x) ∨ ∃y Q(x,y)) Skolemize ∃y: ∀x(¬P(x) ∨ Q(x,f(x))) Result: Single clause ¬P(x), Q(x,f(x)) 3. Unification: Matching Terms Unlike propositional resolution which requires exact matches, FOL resolution needs unification to match terms containing variables. A substitution θ is a mapping from variables to terms, written x₁/t₁, x₂/t₂, ... .

This is the written version of the interactive lesson above. See the full Mathematical Logic course.