Inference and Proof by Resolution

Proof by Refutation

Goal: prove KB ⊨ α.

Strategy: assume the negation. Show KB ∧ ¬α is unsatisfiable (derives a contradiction).

Theoretical basis: KB ⊨ α iff KB ∧ ¬α is unsatisfiable.

This converts theorem proving into unsatisfiability checking — and resolution is the tool for that.

Conjunctive Normal Form (CNF)

Resolution operates on sentences in Conjunctive Normal Form:

A sentence is in CNF iff it is a conjunction of clauses, where each clause is a disjunction of literals.

CNF: (L₁₁ ∨ L₁₂ ∨ ...) ∧ (L₂₁ ∨ ...) ∧ ...

Every propositional sentence can be converted to CNF.

CNF Conversion Algorithm (4 Steps)

1. Eliminate biconditionals: α ↔︎ β → (α → β) ∧ (β → α)
2. Eliminate implications: α → β → ¬α ∨ β
3. Move ¬ inward (to atoms only):
   • ¬¬α → α
   • ¬(α ∧ β) → ¬α ∨ ¬β (De Morgan)
   • ¬(α ∨ β) → ¬α ∧ ¬β (De Morgan)
4. Distribute ∨ over ∧:
   • α ∨ (β ∧ γ) → (α ∨ β) ∧ (α ∨ γ)

Worked Example

Convert B₁₁ ↔︎ (P₁₂ ∨ P₂₁):

Step 1: (B₁₁ → (P₁₂ ∨ P₂₁)) ∧ ((P₁₂ ∨ P₂₁) → B₁₁)

Step 2: (¬B₁₁ ∨ P₁₂ ∨ P₂₁) ∧ (¬(P₁₂ ∨ P₂₁) ∨ B₁₁)

Step 3: (¬B₁₁ ∨ P₁₂ ∨ P₂₁) ∧ ((¬P₁₂ ∧ ¬P₂₁) ∨ B₁₁)

Step 4 (distribute): (¬B₁₁ ∨ P₁₂ ∨ P₂₁) ∧ (¬P₁₂ ∨ B₁₁) ∧ (¬P₂₁ ∨ B₁₁) ✓

The Resolution Rule

    ℓ₁ ∨ ... ∨ p         ¬p ∨ m₁ ∨ ... ∨ mₙ
   ────────────────────────────────────────────
         ℓ₁ ∨ ... ∨ m₁ ∨ ... ∨ mₙ

The complementary literal pair p and ¬p are resolved away. The result is their resolvent.

Unit Resolution (Special Case)

    α ∨ β        ¬β
   ──────────────────
         α

Example: (¬B₁₁ ∨ P₁₂ ∨ P₂₁) and B₁₁ → resolvent (P₁₂ ∨ P₂₁).

Full Resolution Example

Prove KB ⊨ ¬P₁₂ where KB = {¬B₁₁, B₁₁ ↔︎ (P₁₂ ∨ P₂₁), ¬P₂₁}.

After CNF conversion and adding P₁₂ (negated goal): 1. ¬B₁₁ 2. ¬B₁₁ ∨ P₁₂ ∨ P₂₁ 3. ¬P₁₂ ∨ B₁₁ 4. ¬P₂₁ ∨ B₁₁ 5. P₁₂ (assumed) 6. ¬P₂₁

Steps: - Resolve 5 (P₁₂) with 3 (¬P₁₂ ∨ B₁₁) → B₁₁ - Resolve B₁₁ with 1 (¬B₁₁) → empty clause (⊥) ✓ Contradiction → KB ⊨ ¬P₁₂

PL-RESOLUTION Algorithm

function PL-RESOLUTION(KB, α) returns true or false
    clauses ← CNF(KB ∧ ¬α)
    new ← {}
    loop do
        for each pair of clauses Cᵢ, Cⱼ in clauses do
            resolvents ← PL-RESOLVE(Cᵢ, Cⱼ)
            if resolvents contains the empty clause then return true
            new ← new ∪ resolvents
        if new ⊆ clauses then return false   -- no progress
        clauses ← clauses ∪ new

Properties

Summary: The Proof Pipeline

KB ⊨ α?
    ↓
Add ¬α to KB
    ↓
Convert all to CNF → collect clauses
    ↓
Repeatedly apply resolution rule
    ↓
Empty clause derived?  →  Yes: KB ⊨ α  (refutation found)
                       →  No new clauses: KB ⊭ α

Resolution is the gold standard for propositional theorem proving: one rule, no special cases, provably complete for refutation.