Conversion to conjunctive normal form

Conjunctive Normal Form (CNF) is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals: (A ∨ ¬B) ∧ (C ∨ D ∨ ¬E). Resolution theorem proving needs all statements in this clause form.

Why CNF is required

• The resolution rule works on a pair of clauses containing complementary literals, so every sentence must be written as clauses.
• It gives a uniform, simple form (no quantifiers, no → or ↔) that can be processed mechanically by a computer.
• Any FOPL sentence can be converted to CNF (an equisatisfiable one, after Skolemisation), and resolution on clauses is sound and refutation-complete.

Steps of conversion

1. Eliminate implications and biconditionals: replace P → Q by ¬P ∨ Q, and P ↔ Q by (¬P ∨ Q) ∧ (¬Q ∨ P).
2. Move negation inwards (De Morgan and quantifier laws): ¬(P ∧ Q) = ¬P ∨ ¬Q; ¬(P ∨ Q) = ¬P ∧ ¬Q; ¬∀x P = ∃x ¬P; ¬∃x P = ∀x ¬P; ¬¬P = P.
3. Standardise variables: rename so each quantifier uses a different variable name.
4. Move quantifiers to the left (prenex form), keeping their order.
5. Skolemise: remove each existential quantifier by replacing its variable with a Skolem constant (if no ∀ precedes it) or a Skolem function of the preceding universally quantified variables.
6. Drop the universal quantifiers (all remaining variables are universal).
7. Distribute ∨ over ∧ to get a conjunction of disjunctions: (A ∧ B) ∨ C = (A ∨ C) ∧ (B ∨ C).
8. Split the conjunctions into separate clauses.
9. Standardise variables apart: rename variables so no two clauses share a variable.

Example

Statement: "Everyone who loves all animals is loved by someone."

∀x [ ∀y (Animal(y) → Loves(x,y)) → ∃y Loves(y,x) ]

1. Remove →:
   ∀x [ ¬∀y (¬Animal(y) ∨ Loves(x,y)) ∨ ∃y Loves(y,x) ]
2. Move ¬ inward:
   ∀x [ ∃y (Animal(y) ∧ ¬Loves(x,y)) ∨ ∃y Loves(y,x) ]
3. Standardise (rename 2nd y to z):
   ∀x [ ∃y (Animal(y) ∧ ¬Loves(x,y)) ∨ ∃z Loves(z,x) ]
4. Skolemise (y -> F(x), z -> G(x)):
   ∀x [ (Animal(F(x)) ∧ ¬Loves(x,F(x))) ∨ Loves(G(x),x) ]
5. Drop ∀:
   (Animal(F(x)) ∧ ¬Loves(x,F(x))) ∨ Loves(G(x),x)
6. Distribute ∨ over ∧:
   (Animal(F(x)) ∨ Loves(G(x),x)) ∧
   (¬Loves(x,F(x)) ∨ Loves(G(x),x))

Clauses obtained:

• C1: Animal(F(x)) ∨ Loves(G(x), x)
• C2: ¬Loves(x, F(x)) ∨ Loves(G(x), x)