Lecture 09.2: CNF Conversion and Resolution

To perform automated theorem proving, AI systems convert logical sentences into a standardized format called Conjunctive Normal Form (CNF). A sentence in CNF is a conjunction ($\land$) of clauses, where each clause is a disjunction ($\lor$) of literals (a literal is a predicate or its negation).

---

Why Use Normal Forms?

Converting complex logical sentences into normal forms (like CNF or DNF) provides several major advantages for AI reasoning systems:

1. Common Language: Acts as a unified standard for logic-based AI systems, enabling consistent knowledge representation and exchange.
2. Simplifies Reasoning: Standardized structural formats allow inference algorithms to operate systematically without needing custom logic for arbitrary sentence structures.
3. Automated Theorem Proving: Advanced reasoning algorithms—most notably Resolution—require statements to be in CNF to function correctly and efficiently.
4. Knowledge Base Management: Facts and rules in a Knowledge Base (KB) are easier to store, query, index, and update when maintained in a consistent normal form.
5. Algorithm Compatibility & SAT Solvers: Specialized solvers (such as modern SAT and SMT solvers) operate directly on CNF clauses to perform satisfiability checking and inference efficiently.
6. Universality: Every sentence in First-Order Logic can be converted into an inferentially equivalent CNF formula without losing logical meaning.

---

The Six Steps of CNF Conversion

Every First-Order Logic (FOL) sentence can be converted to CNF using a systematic six-step procedure.

We illustrate the procedure using the sentence: "Everyone who loves all animals is loved by someone."

$\forall x \left[ \forall y (\text{Animal}(y) \Rightarrow \text{Loves}(x, y)) \Rightarrow \exists y \text{Loves}(y, x) \right]$

Step 1: Eliminate Biconditionals and Implications

Replace all implications ($\Rightarrow$) and biconditionals ($\Leftrightarrow$) using equivalent disjunctions:

• $A \Rightarrow B \equiv \neg A \lor B$
• $A \Leftrightarrow B \equiv (\neg A \lor B) \land (\neg B \lor A)$

Applying this to our example sentence: $\forall x \left[ \neg \forall y (\neg \text{Animal}(y) \lor \text{Loves}(x, y)) \lor \exists y \text{Loves}(y, x) \right]$

---

Step 2: Move Negations Inward

Push negation symbols ($\neg$) inward until they apply only to individual predicates, using De Morgan's laws and quantifier negation rules:

• $\neg (A \lor B) \equiv \neg A \land \neg B$
• $\neg (A \land B) \equiv \neg A \lor \neg B$
• $\neg \forall x P(x) \equiv \exists x \neg P(x)$
• $\neg \exists x P(x) \equiv \forall x \neg P(x)$
• $\neg (\neg A) \equiv A$

Pushing $\neg$ inward: $\forall x \left[ \exists y \neg(\neg \text{Animal}(y) \lor \text{Loves}(x, y)) \lor \exists y \text{Loves}(y, x) \right]$ $\forall x \left[ \exists y (\text{Animal}(y) \land \neg \text{Loves}(x, y)) \lor \exists y \text{Loves}(y, x) \right]$

---

Step 3: Standardize Variables

Ensure every quantifier uses a unique variable name to prevent scope overlaps: $\forall x \left[ \exists y (\text{Animal}(y) \land \neg \text{Loves}(x, y)) \lor (\exists z \text{Q}(z)) \right]$

Renaming the second $y$ to $z$: $\forall x \left[ \exists y (\text{Animal}(y) \land \neg \text{Loves}(x, y)) \lor \exists z \text{Loves}(z, x) \right]$

---

Step 4: Skolemize Existential Quantifiers

Skolemization eliminates existential quantifiers ($\exists$) by replacing existential variables with Skolem constants or Skolem functions:

• Skolem Constant: Used when an existential quantifier is not enclosed within any universal quantifier scope. Replace the existential variable with a new constant symbol (e.g., $\exists x \text{Rich}(x) \to \text{Rich}(G_1)$).
• Skolem Function: Used when an existential quantifier lies within the scope of a universal quantifier. The existential variable depends on the universally quantified variable, so it is replaced with a new function of that variable.

Skolemization Examples

1. Example 1 (Skolem Function): "For every person $x$, there exists a person $y$ that $x$ loves" ($\forall x \exists y \text{Loves}(x, y)$).
   • Replacing $y$ with Skolem function $c$ or $f(x)$ yields: $\forall x \text{Loves}(x, f(x))$. (The person loved depends on $x$).
2. Example 2 (Mother function): $\forall x \exists y (\text{Mother}(x, y) \land \text{Loves}(y, x))$.
   • Replacing $y$ with Skolem function $\text{mother\_of}(x)$ yields: $\forall x (\text{Mother}(x, \text{mother\_of}(x)) \land \text{Loves}(\text{mother\_of}(x), x))$.
3. Example 3 ("Everyone has a heart"): $\forall x (\text{Person}(x) \Rightarrow \exists y (\text{Heart}(y) \land \text{Has}(x, y)))$.
   • Skolemizing $y \to H(x)$ yields: $\forall x (\text{Person}(x) \Rightarrow \text{Heart}(H(x)) \land \text{Has}(x, H(x)))$.

In our sentence:

• Existential variable $y$ is inside universal quantifier $x \implies$ replace $y$ with $F(x)$.
• Existential variable $z$ is inside universal quantifier $x \implies$ replace $z$ with $G(x)$.

$\forall x \left[ (\text{Animal}(F(x)) \land \neg \text{Loves}(x, F(x))) \lor \text{Loves}(G(x), x) \right]$

---

Step 5: Drop Universal Quantifiers

Since all remaining variables are universally quantified, we drop the explicit $\forall$ symbols. All variables are implicitly assumed to be universally quantified: $\left( \text{Animal}(F(x)) \land \neg \text{Loves}(x, F(x)) \right) \lor \text{Loves}(G(x), x)$

---

Step 6: Distribute $\lor$ over $\land$

Use the distributive law $(A \land B) \lor C \equiv (A \lor C) \land (B \lor C)$ to yield conjunctions of disjunctions: $\left( \text{Animal}(F(x)) \lor \text{Loves}(G(x), x) \right) \land \left( \neg \text{Loves}(x, F(x)) \lor \text{Loves}(G(x), x) \right)$

This gives two final CNF clauses:

• Clause 1a: $\text{Animal}(F(x)) \lor \text{Loves}(G(x), x)$
• Clause 1b: $\neg \text{Loves}(x, F(x)) \lor \text{Loves}(G(x), x)$

---

Resolution and Resolution Rules

Resolution is a powerful inference rule for automated theorem proving in CNF formulas.

The Resolution Rule

Given two clauses containing complementary literals (e.g., $A$ and $\neg A$), resolution eliminates the complementary literals and combines the remaining literals into a new clause called the resolvent:

$\frac{\text{Clause 1: } A \lor B \quad \quad \text{Clause 2: } \neg A \lor C}{\text{Resolvent: } B \lor C}$

Proof by Contradiction (Refutation Procedure)

To prove a query $G$ from a Knowledge Base $KB$:

1. Negate the Goal: Assume $\neg G$.
2. Convert to FOPL: Translate all facts, rules, and $\neg G$ into First-Order Logic.
3. Convert to CNF: Standardize all sentences into CNF clauses.
4. Derive Contradiction: Repeatedly apply the resolution rule to derive the empty clause ($\bot$). Deriving $\bot$ proves that $KB \land \neg G$ is unsatisfiable, thus proving $G$ is true.

---

Resolution Graphs

A Resolution Graph is a Directed Acyclic Graph (DAG) that visualizes the step-by-step resolution process:

• Nodes: Represent individual clauses (either initial input clauses or derived resolvents).
• Edges: Point from parent clauses to their derived resolvent clause.
• Leaf Nodes: The original input clauses from the KB and negated goal.
• Root Node: The empty clause ($\bot$), indicating contradiction and completing the proof.

Simple Resolution Graph Example

Given the CNF clauses:

1. $A \lor B$
2. $\neg A$
3. $\neg B$

• Step 1: Resolve Clause (1) $A \lor B$ and Clause (2) $\neg A$ by eliminating $A$ and $\neg A \implies$ Resolvent: $B$.
• Step 2: Resolve $B$ with Clause (3) $\neg B \implies$ Resolvent: $\bot$ (Contradiction).

---

Resolution Example 1: Jack and Nature

Let's solve a complete resolution problem step by step:

Domain Facts:

1. Everyone who loves all animals is a lover of nature.
2. Jack loves all animals.
3. Cats are animals.
4. Jack does not love nature.

Step 1: Formalize in FOL and Convert to CNF

1. Statement 1: $\forall x \left[ (\forall y (\text{Animal}(y) \Rightarrow \text{Loves}(x, y))) \Rightarrow \text{LovesNature}(x) \right]$

   • Implication removal: $\forall x \left[ \neg (\forall y (\neg \text{Animal}(y) \lor \text{Loves}(x, y))) \lor \text{LovesNature}(x) \right]$
   • Push negation inward: $\forall x \left[ (\exists y (\text{Animal}(y) \land \neg \text{Loves}(x, y))) \lor \text{LovesNature}(x) \right]$
   • Skolemize ($y \to f(x)$): $\forall x \left[ (\text{Animal}(f(x)) \land \neg \text{Loves}(x, f(x))) \lor \text{LovesNature}(x) \right]$
   • Distribute $\lor$ over $\land$:
     • Clause 1a (C1a): $\text{Animal}(f(x)) \lor \text{LovesNature}(x)$
     • Clause 1b (C1b): $\neg \text{Loves}(x, f(x)) \lor \text{LovesNature}(x)$

2. Statement 2: $\forall y (\text{Animal}(y) \Rightarrow \text{Loves}(\text{Jack}, y))$

   • Clause 2 (C2): $\neg \text{Animal}(y) \lor \text{Loves}(\text{Jack}, y)$

3. Statement 3: Cats are animals.

   • Clause 3 (C3): $\text{Animal}(\text{Cat})$

4. Statement 4: Jack does not love nature.

   • Clause 4 (C4): $\neg \text{LovesNature}(\text{Jack})$

---

Step 2: Resolution Derivations

1. Resolve C2 and C3 with substitution $\{y / \text{Cat}\}$:
   • Parent 1: $\neg \text{Animal}(y) \lor \text{Loves}(\text{Jack}, y)$
   • Parent 2: $\text{Animal}(\text{Cat})$
   • Clause 5 (C5): $\text{Loves}(\text{Jack}, \text{Cat})$
2. Resolve C1b and C5 with substitution $\{x / \text{Jack}, f(\text{Jack}) = \text{Cat}\}$:
   • Parent 1: $\neg \text{Loves}(x, f(x)) \lor \text{LovesNature}(x)$
   • Parent 2: $\text{Loves}(\text{Jack}, \text{Cat})$
   • Clause 6 (C6): $\text{LovesNature}(\text{Jack})$
3. Resolve C6 and C4:
   • Parent 1: $\text{LovesNature}(\text{Jack})$
   • Parent 2: $\neg \text{LovesNature}(\text{Jack})$
   • Clause 7 (C7): $\bot$ (Contradiction!)

---

Step 3: Resolution Graph (Jack and Nature)

---

Resolution Example 2: "Curiosity Killed the Cat"

Let's work through the classic theorem-proving puzzle:

Facts:

1. Everyone who loves all animals is loved by someone.
2. Anyone who kills an animal is loved by no one.
3. Jack loves all animals.
4. Either Jack or Curiosity killed the cat, who is named Tuna.
5. Tuna is a cat.
6. Cats are animals.

Goal: Prove that Curiosity killed the cat ($\text{Kills}(\text{Curiosity}, \text{Tuna})$).

Step A: Negated Goal

$\neg G: \quad \neg \text{Kills}(\text{Curiosity}, \text{Tuna})$

Step B: Sentences in FOL and CNF Clauses

• Statement A: $\forall x \left[ (\forall y \text{Animal}(y) \Rightarrow \text{Loves}(x, y)) \Rightarrow \exists y \text{Loves}(y, x) \right]$
  • Clause A1: $\text{Animal}(F(x)) \lor \text{Loves}(G(x), x)$
  • Clause A2: $\neg \text{Loves}(x, F(x)) \lor \text{Loves}(G(x), x)$
• Statement B: $\forall x \left[ (\exists z \text{Animal}(z) \land \text{Kills}(x, z)) \Rightarrow (\forall y \neg \text{Loves}(y, x)) \right]$
  • Clause B: $\neg \text{Loves}(y, x) \lor \neg \text{Animal}(z) \lor \neg \text{Kills}(x, z)$
• Statement C: $\forall x (\text{Animal}(x) \Rightarrow \text{Loves}(\text{Jack}, x))$
  • Clause C: $\neg \text{Animal}(w) \lor \text{Loves}(\text{Jack}, w)$
• Statement D: $\text{Kills}(\text{Jack}, \text{Tuna}) \lor \text{Kills}(\text{Curiosity}, \text{Tuna})$
  • Clause D: $\text{Kills}(\text{Jack}, \text{Tuna}) \lor \text{Kills}(\text{Curiosity}, \text{Tuna})$
• Statement E: $\text{Cat}(\text{Tuna})$
  • Clause E: $\text{Cat}(\text{Tuna})$
• Statement F: $\forall x (\text{Cat}(x) \Rightarrow \text{Animal}(x))$
  • Clause F: $\neg \text{Cat}(u) \lor \text{Animal}(u)$
• Statement $\neg G$ (Negated Goal):
  • Clause G: $\neg \text{Kills}(\text{Curiosity}, \text{Tuna})$

---

Step C: Step-by-Step Resolution Trace

1. Resolve E and F ($\{u / \text{Tuna}\}$):
   • Parent 1: $\text{Cat}(\text{Tuna})$
   • Parent 2: $\neg \text{Cat}(u) \lor \text{Animal}(u)$
   • Resolvent R1: $\text{Animal}(\text{Tuna})$
2. Resolve D and G:
   • Parent 1: $\text{Kills}(\text{Jack}, \text{Tuna}) \lor \text{Kills}(\text{Curiosity}, \text{Tuna})$
   • Parent 2: $\neg \text{Kills}(\text{Curiosity}, \text{Tuna})$
   • Resolvent R2: $\text{Kills}(\text{Jack}, \text{Tuna})$
3. Resolve B and R2 ($\{x / \text{Jack}, z / \text{Tuna}\}$):
   • Parent 1: $\neg \text{Loves}(y, x) \lor \neg \text{Animal}(z) \lor \neg \text{Kills}(x, z)$
   • Parent 2: $\text{Kills}(\text{Jack}, \text{Tuna})$
   • Resolvent R3: $\neg \text{Loves}(y, \text{Jack}) \lor \neg \text{Animal}(\text{Tuna})$
4. Resolve R3 and R1:
   • Parent 1: $\neg \text{Loves}(y, \text{Jack}) \lor \neg \text{Animal}(\text{Tuna})$
   • Parent 2: $\text{Animal}(\text{Tuna})$
   • Resolvent R4: $\neg \text{Loves}(y, \text{Jack})$
5. Resolve A2 and C ($\{x / \text{Jack}, w / F(\text{Jack})\}$):
   • Parent 1: $\neg \text{Loves}(x, F(x)) \lor \text{Loves}(G(x), x)$
   • Parent 2: $\neg \text{Animal}(w) \lor \text{Loves}(\text{Jack}, w)$
   • Resolvent R5: $\neg \text{Animal}(F(\text{Jack})) \lor \text{Loves}(G(\text{Jack}), \text{Jack})$
6. Resolve R5 and A1 ($\{x / \text{Jack}\}$):
   • Parent 1: $\neg \text{Animal}(F(\text{Jack})) \lor \text{Loves}(G(\text{Jack}), \text{Jack})$
   • Parent 2: $\text{Animal}(F(x)) \lor \text{Loves}(G(x), x)$
   • Resolvent R6: $\text{Loves}(G(\text{Jack}), \text{Jack})$
7. Resolve R6 and R4 ($\{y / G(\text{Jack})\}$):
   • Parent 1: $\text{Loves}(G(\text{Jack}), \text{Jack})$
   • Parent 2: $\neg \text{Loves}(y, \text{Jack})$
   • Resolvent R7: $\bot$ (Contradiction!)

---

Step D: The Resolution Graph (Curiosity Killed the Cat)

Deriving the empty clause ($\bot$) confirms that the negated goal is false, proving conclusively that Curiosity killed the cat.