Skip to main content
⚡ Calmops
🤖 AI 🏗️ Architecture 🌐 Web 🗃️ Database ⚙️ DevOps 🌍 Network 💻 Programming 🧮 Algorithms 📐 Software Eng. ☁️ Cloud 🔒 Security 📈 Finance More →

Resolution and Refutation: Proof by Contradiction

Created: December 20, 2025 7 min read

Introduction

Resolution is one of the most important inference rules in automated reasoning. Combined with refutation (proof by contradiction), it provides a complete and efficient method for proving theorems in first-order logic. The resolution principle, discovered by John Alan Robinson in 1965, revolutionized automated theorem proving by providing a single, uniform inference rule.

This article explores resolution, refutation, and practical applications in automated reasoning.

Historical Context

John Alan Robinson’s discovery of the resolution principle in 1965 was a breakthrough in automated reasoning. It provided a single, complete inference rule that could be used for both propositional and first-order logic. This led to the development of SLD resolution (used in Prolog) and many modern SAT and SMT solvers. Resolution remains the foundation of most automated reasoning systems.

Resolution Principle

Basic Resolution Rule

Definition: From clauses (P ∨ Q) and (¬P ∨ R), infer (Q ∨ R)

Notation:

P ∨ Q    ¬P ∨ R
─────────────────
    Q ∨ R

Intuition: If P is true, then R must be true (from second clause). If P is false, then Q must be true (from first clause). Either way, Q ∨ R is true.

Clausal Form

Clause: A disjunction of literals (L₁ ∨ L₂ ∨ … ∨ Lₙ)

Unit Clause: A clause with single literal

Empty Clause: A clause with no literals (represents contradiction, denoted □)

Conversion to CNF: Any formula can be converted to conjunctive normal form (CNF)—a conjunction of clauses

Example:

Original: (P → Q) ∧ (Q → R)
CNF: (¬P ∨ Q) ∧ (¬Q ∨ R)
Clauses: {¬P ∨ Q, ¬Q ∨ R}

Resolvent

Definition: The clause obtained by applying resolution to two clauses

Resolvent of (P ∨ Q) and (¬P ∨ R): (Q ∨ R)

Properties:

  • Resolvent is a logical consequence of the two parent clauses
  • If parent clauses are satisfiable, resolvent may or may not be satisfiable
  • If resolvent is empty clause, parent clauses are unsatisfiable

Refutation Proof

Proof by Contradiction

Strategy: To prove Γ ⊢ φ:

  1. Assume ¬φ
  2. Add ¬φ to Γ
  3. Derive contradiction (empty clause)
  4. Conclude φ must be true

Notation: Γ ⊢ φ iff Γ ∪ {¬φ} ⊢ □

Refutation Algorithm

Input: Set of clauses S (including negated goal) Output: Proof or failure

Algorithm: Resolution Refutation
1. Convert all formulas to CNF
2. Add negation of goal as clauses
3. While empty clause not derived:
   a. Select two clauses with complementary literals
   b. Compute resolvent
   c. Add resolvent to clause set
   d. If resolvent is empty clause, return PROOF
4. If no more resolvents can be generated, return FAILURE

Example: Simple Proof

Goal: Prove P from {P → Q, Q → R, P}

Refutation:

1. ¬P ∨ Q        (from P → Q)
2. ¬Q ∨ R        (from Q → R)
3. P              (given)
4. ¬P             (negation of goal)
5. Q              (resolve 1, 4)
6. R              (resolve 2, 5)
7. ¬R             (negation of goal)
8. □              (resolve 6, 7)

Wait, this example is incorrect. Let me provide a correct one:

Goal: Prove Q from {P → Q, P}

Refutation:

1. ¬P ∨ Q        (from P → Q)
2. P              (given)
3. ¬Q             (negation of goal)
4. Q              (resolve 1, 2)
5. □              (resolve 3, 4)

First-Order Resolution

Unification in Resolution

Problem: Clauses may contain variables

Solution: Use unification to match complementary literals

Example:

Clause 1: P(x) ∨ Q(x)
Clause 2: ¬P(f(a)) ∨ R(a)

Unify P(x) with P(f(a)): x ← f(a)
Resolvent: Q(f(a)) ∨ R(a)

Substitution and Renaming

Variable Renaming: Rename variables to avoid conflicts

Example:

Clause 1: P(x) ∨ Q(x)
Clause 2: ¬P(y) ∨ R(y)

Rename: Clause 2 becomes ¬P(z) ∨ R(z)
Unify P(x) with P(z): x ← z
Resolvent: Q(z) ∨ R(z)

First-Order Resolution Rule

Definition: From (P(t₁) ∨ Q) and (¬P(t₂) ∨ R), if σ is MGU of P(t₁) and P(t₂), infer (Q ∨ R)σ

Completeness: First-order resolution is complete (if formula is valid, resolution will find proof)

Resolution Strategies

Breadth-First Resolution

Strategy: Generate all possible resolvents at each level

Advantages: Complete, finds shortest proofs Disadvantage: Memory-intensive

Depth-First Resolution

Strategy: Follow one resolution path fully before backtracking

Advantages: Memory-efficient Disadvantage: May not find shortest proofs

Unit Resolution

Strategy: Prioritize resolution with unit clauses

Advantages: Often faster, reduces search space Disadvantage: May miss some proofs

Linear Resolution

Strategy: Each resolvent is used with a clause from original set

Advantages: Efficient, complete for Horn clauses Disadvantage: Less complete for general clauses

SLD Resolution

Strategy: Specific Linear Definite clause resolution (used in Prolog)

Advantages: Efficient for logic programming Disadvantage: Incomplete for general first-order logic

Optimization Techniques

Subsumption

Definition: Clause C₁ subsumes C₂ if C₁ ⊆ C₂ (after substitution)

Example: P(x) subsumes P(a) ∨ Q(b)

Optimization: Remove subsumed clauses

Tautology Elimination

Definition: Remove clauses containing both P and ¬P

Example: P ∨ ¬P ∨ Q is a tautology

Optimization: Never add tautologies to clause set

Redundancy Elimination

Strategies:

  • Remove duplicate clauses
  • Remove clauses subsumed by others
  • Remove tautologies

Clause Selection Heuristics

Strategies:

  • Shortest clause first: Prefer shorter clauses
  • Newest clause first: Prefer recently generated clauses
  • Most constrained first: Prefer clauses with specific instantiations

Practical Example: Proving a Theorem

Theorem: From {∀x(P(x) → Q(x)), ∃x P(x)}, prove ∃x Q(x)

Step 1: Convert to CNF

∀x(P(x) → Q(x)) becomes ¬P(x) ∨ Q(x)
∃x P(x) becomes P(a) for some constant a
Goal: ∃x Q(x)
Negation: ¬∃x Q(x) becomes ∀x ¬Q(x), which is ¬Q(x)

Step 2: Clause Set

1. ¬P(x) ∨ Q(x)
2. P(a)
3. ¬Q(x)

Step 3: Resolution

4. Q(a)           (resolve 1, 2 with x ← a)
5. □              (resolve 3, 4 with x ← a)

Conclusion: Proof found! ∃x Q(x) is provable.

Limitations and Extensions

Limitations

Undecidability: First-order logic is undecidable

  • Some valid formulas may require infinite proofs
  • Some invalid formulas cannot be shown invalid

Efficiency: Resolution can be inefficient

  • Combinatorial explosion in search space
  • May generate many irrelevant clauses

Extensions

Paramodulation: Handle equality reasoning

Superposition: Combine resolution with ordering

Hyper-resolution: Resolve multiple clauses simultaneously

Ordered resolution: Use term ordering to guide resolution

Glossary

Clause: A disjunction of literals

Complementary Literals: P and ¬P

Empty Clause: Clause with no literals (contradiction)

Literal: An atomic formula or its negation

MGU (Most General Unifier): Most general substitution making terms equal

Refutation: Proof by deriving contradiction

Resolvent: Clause obtained by resolution

Resolution: Inference rule combining two clauses

Subsumption: One clause subsumes another if it’s more general

Unification: Finding substitution making terms equal

Practice Problems

Problem 1: Apply resolution to prove Q from {P → Q, P}.

Solution:

1. ¬P ∨ Q        (from P → Q)
2. P              (given)
3. ¬Q             (negation of goal)
4. Q              (resolve 1, 2)
5. □              (resolve 3, 4)
Proof complete!

Problem 2: Convert (P ∧ Q) → R to CNF and apply resolution.

Solution:

(P ∧ Q) → R
¬(P ∧ Q) ∨ R
(¬P ∨ ¬Q) ∨ R
¬P ∨ ¬Q ∨ R
CNF: {¬P ∨ ¬Q ∨ R}

Problem 3: Prove ∀x(P(x) → Q(x)), P(a) ⊢ Q(a) using resolution.

Solution:

1. ¬P(x) ∨ Q(x)  (from ∀x(P(x) → Q(x)))
2. P(a)           (given)
3. ¬Q(a)          (negation of goal)
4. Q(a)           (resolve 1, 2 with x ← a)
5. □              (resolve 3, 4)
Proof complete!

Conclusion

Resolution and refutation provide a powerful, complete method for automated theorem proving. By converting formulas to clausal form and systematically applying the resolution rule, we can prove any valid theorem in first-order logic (though the search may not terminate for invalid formulas).

Understanding resolution is essential for anyone working in automated reasoning, logic programming, or formal verification. Modern SAT and SMT solvers build on resolution principles, making it a foundational technique in computational logic.

The elegance of resolution—a single, uniform inference rule that is both sound and complete—demonstrates the power of logical reasoning and its computational implementation.

Comments