TutorialsArena

Resolution in First-Order Logic (FOL): A Theorem Proving Technique

Learn about Resolution, a fundamental theorem-proving technique in First-Order Logic (FOL). This method uses refutation to prove statements by demonstrating that their negation leads to a contradiction. Discover how Resolution resolves clauses containing complementary literals, utilizing unification to derive new clauses and ultimately demonstrate logical consequences. Understand the core concepts and application of this powerful technique in automated reasoning.

Resolution in First-Order Logic (FOL): A Theorem Proving Technique

Introduction to Resolution

Resolution is a powerful theorem-proving technique in first-order logic (FOL) that uses a method called refutation—proving a statement is true by showing its negation leads to a contradiction. Developed by John Alan Robinson in 1965, resolution works by resolving clauses (disjunctions of literals) that contain complementary literals.

Key Concepts in Resolution

  • Clause: A disjunction of literals (atomic sentences or their negations).
  • Conjunctive Normal Form (CNF): A logical sentence expressed as a conjunction of clauses.
  • Complementary Literals: Literals that are negations of each other (e.g., `Loves(x,y)` and `¬Loves(x,y)`).
  • Unification: The process of finding substitutions for variables that make two literals complementary.

The Resolution Inference Rule

The resolution rule states that if two clauses contain complementary literals (after applying unification to make them exactly complementary), a new clause (called the resolvent) can be inferred. This is a "lifted" version of the propositional resolution rule.

The rule is often called binary resolution because it operates on exactly two clauses at a time.

Steps in a Resolution Proof

  1. Convert facts to FOL: Express the given statements in first-order logic.
  2. Convert to Conjunctive Normal Form (CNF): Transform the FOL statements into CNF for easier resolution.
  3. Negate the conclusion: Add the negation of the statement you want to prove (proof by contradiction).
  4. Apply the Resolution Rule: Repeatedly apply the resolution rule, using unification to find complementary literals. If a contradiction is reached (an empty clause is derived), the original statement is proven.

Example: Proving "John Likes Peanuts"

(A detailed example demonstrating a resolution proof, converting statements to FOL, converting to CNF, negating the conclusion, and constructing a resolution graph with unifications, would be included here. This example, including the resolution graph, would be added to the HTML.)