First-Order Resolution and Resolution Refutation: A Practical Guide

Introduction

Automated theorem proving represents one of the foundational achievements of computer science and mathematical logic. At its core lies First-Order Resolution, a single, elegant inference rule that enables computers to prove mathematical theorems automatically. This method forms the backbone of logic programming languages like Prolog and powers modern SMT (Satisfiability Modulo Theories) solvers.

In this post, we’ll explore First-Order Resolution from both theoretical and practical perspectives. You’ll learn:

The formal definition of the resolution rule and how unification extends propositional resolution to first-order logic
How resolution refutation works as a proof technique by demonstrating contradictions
Systematic methods for determining whether a resolution refutation exists for any given set of clauses

By the end, you’ll be equipped to apply these techniques to real problems and understand the theoretical guarantees that make resolution a complete and sound method for automated reasoning.

Prerequisites

Before diving into First-Order Resolution, ensure you’re comfortable with:

Propositional logic: Connectives (¬, ∧, ∨, →, ↔), truth tables, tautologies
First-order logic: Predicates, quantifiers (∀, ∃), variables, domains
Normal forms: Conjunctive Normal Form (CNF), Prenex Normal Form
Substitutions: Basic concept of replacing variables with terms

If you need a refresher on any of these topics, I recommend reviewing introductory logic texts before continuing.

First-Order Resolution: The Inference Rule

From Propositional to First-Order

In propositional logic, resolution works on clauses composed of propositional variables. Given two clauses containing complementary literals, we can resolve them:

C1 ∨ p    C2 ∨ ¬p
----------------
    C1 ∨ C2

First-Order Resolution extends this idea to handle predicates with variables and terms. The key insight is that we need a mechanism to match literals that aren’t identical but can become identical through appropriate variable bindings.

Unification: The Heart of First-Order Resolution

Unification is the algorithmic process of finding a substitution that makes two expressions identical. A substitution is a set of bindings like {x/t1, y/t2}, where variables are replaced by terms.

The unifier of two expressions is a substitution that, when applied, makes them syntactically equal. A most general unifier (MGU) is a unifier that is more general than any other unifier.

Unification Algorithm Example

Let’s find the MGU of P(x, f(y)) and P(a, f(z)):

Compare first arguments: x and a. Bind x/a.
Apply substitution {x/a}: First expression becomes P(a, f(y)).
Compare second arguments: f(y) and f(z). Bind y/z.
Apply substitution {y/z}: First expression becomes P(a, f(z)).
Both expressions are now identical.

The MGU is {x/a, y/z}.

The Resolution Rule

Given two clauses containing complementary literals that can be unified, First-Order Resolution produces a new clause:

C1 ∨ L1    C2 ∨ L2
------------------  where σ = MGU(L1, ¬L2)
      σ(C1 ∨ C2)

Here, L1 and L2 are literals that can be unified (one positive, one negative), and σ denotes the application of substitution σ.

Example 1: Basic Resolution

Consider these two clauses:

C1: P(x) ∨ Q(x)
C2: ¬P(a) ∨ R(x)

We can resolve on P(x) and ¬P(a):

Find MGU of P(x) and P(a): {x/a}
Apply substitution to remaining literals: Q(a) and R(a)
Resolvent: Q(a) ∨ R(a)

P(x) ∨ Q(x)    ¬P(a) ∨ R(x)
---------------------------  σ = {x/a}
        Q(a) ∨ R(a)

Resolution Refutation: Proving by Contradiction

The Methodology

Resolution refutation is a proof technique that demonstrates a formula φ by showing that its negation ¬φ leads to a contradiction. The process follows these steps:

Negate the goal: Start with the negation of what you want to prove
Convert to CNF: Transform all formulas (premises and negated goal) into Clause Normal Form
Apply resolution: Repeatedly apply the resolution rule to derive new clauses
Derive the empty clause: If you can derive □ (the empty clause), the original goal is proven

The empty clause □ represents a contradiction—it’s false under all interpretations. Deriving □ means our set of clauses is unsatisfiable, which implies that the negation of our goal cannot be true, so the goal itself must be true.

Why This Works: Soundness and Completeness

Resolution is sound: If resolution derives a clause from a set of clauses, that clause is a logical consequence of the original set.

Resolution is complete: If a set of clauses is unsatisfiable, resolution will eventually derive the empty clause.

Together, these properties mean that resolution refutation is a decision procedure for first-order logic: a formula is provable if and only if a resolution refutation of its negation exists.

Step-by-Step Resolution Refutation Process

Let’s walk through the complete process:

Start with premises and goal: We have premises P1, P2, …, Pn and want to prove goal G
Negate the goal: Add ¬G to our set of clauses
Convert to CNF: Transform all formulas to CNF, resulting in a set of clauses S
Apply resolution systematically: Generate new clauses until either:
- The empty clause □ is derived (proof complete)
- No new clauses can be generated (proof fails, goal not provable)

Example 2: Syllogism via Resolution Refutation

Let’s prove a classic syllogism:

Premises:

All humans are mortal: ∀x (Human(x) → Mortal(x))
Socrates is human: Human(Socrates)

Goal: Socrates is mortal: Mortal(Socrates)

Step 1: Negate the Goal

Negate the conclusion: ¬Mortal(Socrates)

Step 2: Convert to CNF

Convert premises to CNF:

∀x (Human(x) → Mortal(x)) becomes ∀x (¬Human(x) ∨ Mortal(x))
- Clause: {¬Human(x), Mortal(x)}
Human(Socrates) is already in CNF
- Clause: {Human(Socrates)}
Negated goal: ¬Mortal(Socrates)
- Clause: {¬Mortal(Socrates)}

Our clause set S = {¬Human(x) ∨ Mortal(x), Human(Socrates), ¬Mortal(Socrates)}

Step 3: Apply Resolution

Let’s derive the empty clause:

Step 1: Resolve {¬Human(x) ∨ Mortal(x)} and {Human(Socrates)}
        MGU: {x/Socrates}
        Result: {Mortal(Socrates)}

Step 2: Resolve {Mortal(Socrates)} and {¬Mortal(Socrates)}
        No substitution needed (identical literals)
        Result: □ (empty clause)

  ¬Human(x) ∨ Mortal(x)      Human(Socrates)
  --------------------------------------------  σ={x/Socrates}
          Mortal(Socrates)
          
  Mortal(Socrates)    ¬Mortal(Socrates)
  -------------------------------------  
              □

Since we derived the empty clause, the original goal Mortal(Socrates) is proven.

Example 3: Quantifier Scoping and Resolution

Let’s prove a more complex example involving quantifier interaction:

Premises:

Everyone has a parent: ∀x ∃y Parent(y, x)
If someone has a parent, they are not orphaned: ∀x (∃y Parent(y, x) → ¬Orphaned(x))

Goal: No one is both orphaned and has a parent as themselves: ¬∃x Parent(x, x) ∧ Orphaned(x)

This is complex, so let’s simplify to a more tractable example:

Premises:

∀x (Brother(x, y) → Sibling(x, y)) (Brothers are siblings)
∀x ∀y (Sibling(x, y) → Sibling(y, x)) (Sibling is symmetric)
Brother(John, Bob)

Goal: Sibling(Bob, John)

Step 1: Negate the Goal

¬Sibling(Bob, John)

Step 2: Convert to CNF

∀x ∀y (¬Brother(x, y) ∨ Sibling(x, y))
- Clause: {¬Brother(x, y), Sibling(x, y)}
∀x ∀y (¬Sibling(x, y) ∨ Sibling(y, x))
- Clause: {¬Sibling(x, y), Sibling(y, x)}
Brother(John, Bob)
- Clause: {Brother(John, Bob)}
Negated goal: ¬Sibling(Bob, John)
- Clause: {¬Sibling(Bob, John)}

Step 3: Resolution Derivation

Step 1: Resolve {¬Brother(x, y), Sibling(x, y)} with {Brother(John, Bob)}
        MGU: {x/John, y/Bob}
        Result: {Sibling(John, Bob)}

Step 2: Resolve {¬Sibling(x, y), Sibling(y, x)} with {Sibling(John, Bob)}
        MGU: {x/John, y/Bob}
        Result: {Sibling(Bob, John)}

Step 3: Resolve {Sibling(Bob, John)} with {¬Sibling(Bob, John)}
        Result: □

  ¬Brother(x, y) ∨ Sibling(x, y)     Brother(John, Bob)
  ----------------------------------------------------  σ={x/John, y/Bob}
            Sibling(John, Bob)
            
  ¬Sibling(x, y) ∨ Sibling(y, x)     Sibling(John, Bob)
  ----------------------------------------------------  σ={x/John, y/Bob}
            Sibling(Bob, John)
            
  Sibling(Bob, John)     ¬Sibling(Bob, John)
  ------------------------------------------  
              □

The derivation of □ proves that Sibling(Bob, John) follows from the premises.

Determining Whether a Resolution Refutation Exists

The Decision Problem

Given a set of clauses S, how do we determine whether a resolution refutation exists? In first-order logic, this is semi-decidable: if a refutation exists, we can find it; if not, we may never know.

Systematic Search Strategies

Since the search space can be infinite, we need systematic strategies:

1. Set of Support Strategy

Restrict resolution to always involve at least one clause from a designated “set of support” (typically the negated goal plus clauses derived from it). This prevents wasting resolution steps on premises that are known to be satisfiable.

2. Unit Preference

Prioritize resolution steps involving unit clauses (clauses with a single literal). Unit clauses are more likely to produce useful resolvents.

3. Input Resolution

Only resolve clauses that were in the original input set (or derived from them via unit resolution). This restricts the search space but may not be complete.

4. Linear Resolution

Form a linear chain of resolutions where each step resolves the result of the previous step with another clause. This is more general than input resolution but still restricts the search.

5. Subsumption

Eliminate subsumed clauses. Clause C subsumes clause D if there’s a substitution σ such that σ(C) is a subset of D. Subsumed clauses can be safely removed.

Satisfiability Checking

A resolution refutation exists if and only if the clause set is unsatisfiable. Several techniques help determine this:

1. Model Checking

For finite domains, enumerate all possible interpretations. If no model satisfies the clauses, they’re unsatisfiable.

2. Herbrand’s Theorem

A set of first-order clauses is unsatisfiable if and only if a finite subset of its ground instances is unsatisfiable. This reduces first-order to propositional logic, though the ground instances may be enormous.

3. Resolution Derivation

Attempt to derive the empty clause using a systematic strategy. If successful, the set is unsatisfiable. If no new clauses can be generated and □ hasn’t been derived, the set may be satisfiable (but we can’t be certain without exploring all possibilities).

Termination Considerations

Resolution for first-order logic doesn’t always terminate. However, it terminates for:

Propositional clauses: Finite clause set means finite search space
Clauses over a finite domain with no functions: Finite Herbrand universe
Clauses in decidable fragments: E.g., monadic predicate logic, the Bernays-Schönfinkel class

Example 4: A Set with No Resolution Refutation

Consider a clause set that is satisfiable—no resolution refutation exists:

C1: Parent(John, Bob)
C2: ¬Parent(x, y) ∨ Person(x)
C3: ¬Parent(x, y) ∨ Person(y)

This represents: “John is Bob’s parent, and parents and children are people.”

Can we derive the empty clause? Let’s try:

Resolve C1 with C2: {Person(John)}
Resolve C1 with C3: {Person(Bob)}

We now have {Person(John), Person(Bob)}, but no clause contains negated Person literals. No further resolution is possible, and we cannot derive □.

This makes sense: the original clauses are satisfiable (take the domain {John, Bob} with the given parent relationship). Since the clause set is satisfiable, no resolution refutation can exist.

Example 5: Equality and Unification

Let’s prove a simple arithmetic property using resolution:

Premises:

∀x (x = x) (Reflexivity of equality)
∀x ∀y (x = y → y = x) (Symmetry)
a = b

Goal: b = a

Step 1: Negate the Goal

¬(b = a)

Step 2: Convert to CNF

{a = a} (from reflexivity, ground instance)
{¬(x = y), y = x} (symmetry in CNF)
{a = b} (premise)
{¬(b = a)} (negated goal)

Step 3: Resolution

Step 1: Resolve {¬(x = y), y = x} with {a = b}
        MGU: {x/a, y/b}
        Result: {b = a}

Step 2: Resolve {b = a} with {¬(b = a)}
        Result: □

  ¬(x = y) ∨ (y = x)     a = b
  ----------------------------  σ={x/a, y/b}
           b = a
   
  b = a     ¬(b = a)
  -----------------  
        □

The derivation of □ proves b = a.

Note: Equality requires special handling in resolution. Many implementations use paramodulation (a generalization of resolution for equality) rather than treating equality as a regular predicate.

Implementation Considerations

Data Structures

Efficient resolution implementations use:

Term trees: Represent terms as trees for efficient unification
Indexing structures: Substitution trees or discrimination trees to quickly find resolvable clauses
Clause sets with literals: Store clauses as sets of literals for efficient set operations

Heuristics

Modern provers use heuristics to guide search:

Weight-based ordering: Prefer resolving clauses with fewer literals or simpler terms
Literal selection: In positive resolution, only resolve on positive literals
Literal ordering: Order literals within clauses to improve search efficiency

Modern Resolution Provers

Vampire: High-performance prover for first-order logic
E Prover: Complete theorem prover for first-order logic with equality
Z3: SMT solver that uses resolution-like techniques
Prolog interpreters: Use SLD resolution (a restricted form of resolution)

Practical Applications

First-Order Resolution and resolution refutation have numerous real-world applications:

Logic Programming

Prolog and similar languages use SLD resolution (Selective Linear Definite clause resolution) as their execution model. When you query a Prolog program, the interpreter performs resolution refutation to find answers.

Automated Theorem Proving

Modern theorem provers like Vampire, E, and SPASS use sophisticated resolution strategies to prove mathematical theorems automatically. These tools are used in:

Software verification
Hardware verification
Mathematical research
Formal methods

SMT Solvers

Satisfiability Modulo Theories (SMT) solvers extend resolution with theory-specific reasoning. They’re used in:

Program analysis
Symbolic execution
Constraint solving
Optimization problems

Knowledge Representation

Resolution-based systems can reason about knowledge bases expressed in first-order logic, enabling:

Expert systems
Question answering
Semantic web reasoning
Database query optimization

Summary

First-Order Resolution provides an elegant and powerful framework for automated theorem proving. Its single inference rule, combined with unification, enables computers to prove mathematical theorems automatically.

Key takeaways:

Unification extends propositional resolution to first-order logic by finding substitutions that make literals match
Resolution refutation proves formulas by showing their negation leads to contradiction (the empty clause)
Soundness and completeness guarantee that resolution finds proofs when they exist
Systematic search strategies (set of support, unit preference, subsumption) make resolution practical
Semi-decidability means resolution will find proofs that exist but may not terminate on unprovable formulas

While determining whether a resolution refutation exists is only semi-decidable in first-order logic, systematic search strategies and modern prover implementations make resolution practical for many real-world problems.

Exercises

Test your understanding with these exercises:

Basic Resolution: Prove that if all students are smart and John is a student, then John is smart.
- Premises: ∀x (Student(x) → Smart(x)), Student(John)
- Goal: Smart(John)
Quantifier Interaction: Prove that if there exists someone who likes everyone, and everyone likes themselves, then there exists someone who likes themselves.
- Premises: ∃x ∀y Likes(x, y), ∀x Likes(x, x)
- Goal: ∃x Likes(x, x)
Satisfiability: Show that the clause set {P(x), P(f(x)), ¬P(a)} is satisfiable by constructing a model.
Equality Reasoning: Prove that if f is injective (∀x ∀y (f(x) = f(y) → x = y)) and f(a) = f(b), then a = b.
Transitive Closure: Given that “ancestor” is the transitive closure of “parent”, prove that if Parent(a, b) and Parent(b, c), then Ancestor(a, c).

Conclusion

First-Order Resolution stands as one of the most elegant and powerful ideas in computer science. From its theoretical foundations in mathematical logic to its practical applications in programming languages and verification tools, resolution demonstrates how a single, simple inference rule can enable sophisticated automated reasoning.

By mastering resolution refutation, you’ve gained insight into how computers can prove theorems, how logic programming languages work, and how modern verification tools ensure software correctness. These techniques continue to evolve, powering the next generation of AI systems, formal methods, and automated reasoning tools.

Whether you’re building a logic-based system, verifying software, or simply appreciating the beauty of automated reasoning, First-Order Resolution provides a solid foundation for understanding how machines can think logically.

Introduction

Prerequisites

First-Order Resolution: The Inference Rule

From Propositional to First-Order

Unification: The Heart of First-Order Resolution

Unification Algorithm Example

The Resolution Rule

Example 1: Basic Resolution

Resolution Refutation: Proving by Contradiction

The Methodology

Why This Works: Soundness and Completeness

Step-by-Step Resolution Refutation Process

Example 2: Syllogism via Resolution Refutation

Step 1: Negate the Goal

Step 2: Convert to CNF

Step 3: Apply Resolution

Example 3: Quantifier Scoping and Resolution

Step 1: Negate the Goal

Step 2: Convert to CNF

Step 3: Resolution Derivation

Determining Whether a Resolution Refutation Exists

The Decision Problem

Systematic Search Strategies

1. Set of Support Strategy

2. Unit Preference

3. Input Resolution

4. Linear Resolution

5. Subsumption

Satisfiability Checking

1. Model Checking

2. Herbrand’s Theorem

3. Resolution Derivation

Termination Considerations

Example 4: A Set with No Resolution Refutation

Example 5: Equality and Unification

Step 1: Negate the Goal

Step 2: Convert to CNF

Step 3: Resolution

Implementation Considerations

Data Structures

Heuristics

Modern Resolution Provers

Practical Applications

Logic Programming

Automated Theorem Proving

SMT Solvers

Knowledge Representation

Summary

Exercises

Further Reading

Books

Papers

Online Resources

Tools to Explore

Conclusion

Comments