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).

Every sentence in First-Order Logic (FOL) can be converted into an inferentially equivalent CNF sentence using a systematic six-step procedure.

---

The Six Steps of CNF Conversion

We will illustrate the conversion process 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 ($A \Rightarrow B$) and biconditionals ($A \Leftrightarrow B$) using their 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 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

Move negation symbols ($\neg$) inwards until they apply only to individual predicates. Use 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 \equiv \exists x \neg P$
• $\neg \exists x P \equiv \forall x \neg P$
• $\neg (\neg A) \equiv A$

Pushing the negation inwards: $\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 each quantifier binds a unique variable name to prevent naming conflicts:

• Rename the second variable $y$ in the existential quantifier 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 is the process of removing existential quantifiers ($\exists$) by replacing existential variables with constants or functions:

• Skolem Constants: If the existential quantifier is not inside the scope of a universal quantifier, replace the variable with a brand-new constant. (e.g., $\exists x \text{ Rich}(x) \rightarrow \text{Rich}(G_1)$).
• Skolem Functions: If the existential quantifier is within the scope of a universal quantifier, the existential variable depends on the universal variable. Replace it with a new function of that universal variable.

In our sentence:

• The existential variable $y$ is within the scope of universal quantifier $x$. Replace $y$ with Skolem function $F(x)$.
• The existential variable $z$ is within the scope of universal quantifier $x$. Replace $z$ with Skolem function $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 omit the universal quantifier symbols ($\forall$). The 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$

Rearrange the formula using the distributive law: $(A \land B) \lor C \equiv (A \lor C) \land (B \lor C)$. $\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 yields two distinct CNF clauses:

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

---

Resolution Proofs: "Curiosity Killed the Cat"

To prove a goal using the resolution rule, we use Proof by Contradiction:

1. Express all knowledge-base facts and rules in FOL.
2. Negate the goal statement.
3. Convert all statements into CNF.
4. Apply resolution steps, replacing complementary literals using Unification (substituting variables), until the empty clause ($\bot$) is derived.

Let's solve the famous logical 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 \text{Kills}(\text{Curiosity}, \text{Tuna})$

Step B: Convert All Sentences to CNF Clauses

• 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)$
• Clause B: $\neg \text{Loves}(y, x) \lor \neg \text{Animal}(z) \lor \neg \text{Kills}(x, z)$
• Clause C: $\neg \text{Animal}(w) \lor \text{Loves}(\text{Jack}, w)$ (Variable renamed to $w$)
• Clause D: $\text{Kills}(\text{Jack}, \text{Tuna}) \lor \text{Kills}(\text{Curiosity}, \text{Tuna})$
• Clause E: $\text{Cat}(\text{Tuna})$
• Clause F: $\neg \text{Cat}(u) \lor \text{Animal}(u)$ (Variable renamed to $u$)
• Clause G (Negated Goal): $\neg \text{Kills}(\text{Curiosity}, \text{Tuna})$

---

Step C: Resolution Derivation Trace

1. Resolve E and F using substitution $\{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 (resolves $\text{Kills}(\text{Curiosity}, \text{Tuna})$):
   • 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 using substitution $\{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 (resolves $\text{Animal}(\text{Tuna})$):
   • 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 using substitution $\{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 using substitution $\{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 using substitution $\{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

Since resolution leads directly to the empty clause ($\bot$), the negated goal is false, and it is proven that Curiosity killed the cat.