Resolution in First-Order Logic

Goal: Complete Refutation in FOL

Resolution (Ch.7) works on propositional CNF. FOL resolution extends it to handle variables via unification.

Strategy: prove KB ⊨ α by showing KB ∧ ¬α is unsatisfiable using resolution.

Step 1: Conversion to CNF for FOL

Converting a FOL sentence to CNF requires additional steps beyond propositional CNF conversion.

Full FOL → CNF Algorithm

Eliminate implications and biconditionals (same as propositional)
Move ¬ inward (De Morgan, quantifier duality: ¬∀x P → ∃x ¬P)
Standardize variables apart — rename so each ∀ uses a unique variable name
Skolemize — eliminate existential quantifiers
Drop universal quantifiers — all remaining variables are implicitly universal
Distribute ∨ over ∧ — convert to CNF

Step 2: Skolemization

Skolemization eliminates ∃ by introducing Skolem functions (or Skolem constants).

Simple case: no enclosing ∀

∃x P(x)  →  P(SK1)    -- SK1 is a new constant (Skolem constant)

∃ inside ∀

∀x ∃y Loves(x, y)  →  ∀x Loves(x, F(x))    -- F is a Skolem function

The Skolem function F(x) represents “the object that x loves” — it depends on x because the ∃ is inside ∀x.

Why Skolemization Preserves Satisfiability

Original: there exists some y (possibly depending on x). Skolemized: introduce a function F that names that y.

The two sentences are equisatisfiable (not equivalent — but SAT/UNSAT status is preserved), which is sufficient for refutation.

Step 3: FOL Resolution Rule

After CNF, resolution in FOL applies the standard resolution rule but uses unification to match complementary literals:

Given clauses:
   l₁ ∨ ... ∨ lₖ ∨ p
   m₁ ∨ ... ∨ mₙ ∨ ¬q

If UNIFY(p, q) = θ:
   Resolvent: SUBST(θ, l₁ ∨ ... ∨ lₖ ∨ m₁ ∨ ... ∨ mₙ)

The key difference from propositional: p and q need not be identical — they must unify via θ.

Example

Clauses:
   (1) ¬King(x) ∨ ¬Greedy(x) ∨ Evil(x)
   (2) King(John)
   (3) Greedy(John)
   (4) ¬Evil(John)           -- negated goal

Resolve (1) with (2): UNIFY(King(x), King(John)) = {x/John} → ¬Greedy(John) ∨ Evil(John)
Resolve with (3): → Evil(John)
Resolve with (4): → empty clause ⊥

Contradiction — KB ⊨ Evil(John) proved.

FOL Resolution: Properties

Property	Value
Sound	Yes
Refutation-complete	Yes — if KB ⊨ α, resolution will derive the empty clause
Complete for non-theorems	No — may loop (FOL undecidable)
Terminates	No in general (semi-decidable)

Completeness theorem (Gödel, 1930 / Robinson, 1965): FOL resolution is refutation-complete. If KB ∧ ¬α is unsatisfiable, resolution will eventually derive the empty clause.

Equality

Standard resolution doesn’t handle equality well (needs infinite axioms like ∀x x=x, ∀x,y x=y → y=x).

Paramodulation: special inference rule for equality:

If t₁ = t₂ is in KB and α[t₁] is in KB:
   Derive α[t₂]

Equational reasoning is built into modern FOL theorem provers (E, Vampire, Prover9).

Practical FOL Inference

Modern FOL theorem provers (Prover9, Vampire, E): - CNF + resolution + paramodulation + learning (clause selection heuristics) - Used for: mathematical theorem proving, formal verification, ontology reasoning

FOL inference = the gold standard reasoning framework, with propositional SAT/resolution as a special case.