---
title: "Conversion to conjunctive normal form"
subject: "Artificial Intelligence"
chapter: 4
key: "semester_6/artificial_intelligence:cnf-conversion-steps"
source: https://www.bctengineer.com/q/semester_6/artificial_intelligence/cnf-conversion-steps
site: BCT Engineering
---

# Conversion to conjunctive normal form

Artificial Intelligence · Chapter 4: Knowledge Representation, Inference & Reasoning

- Asked in: 2069 Poush, 10 marks; 2070 Bhadra, 8 marks; 2075 Baisakh, 2+6 marks (asked 3 times)
- Video: [13 First Order Logic to Conjunctive Normal Form Solved Example Artificial Intelligence Mahesh Huddar](https://www.youtube.com/watch?v=6P8zrHCmAPQ) — Mahesh Huddar
- Answer checked by Claude Opus 5.5 (high effort) on 2026-10-14
- Page: https://www.bctengineer.com/q/semester_6/artificial_intelligence/cnf-conversion-steps
- Whole chapter: https://www.bctengineer.com/md/semester_6/artificial_intelligence/chapter-4

## Question

Explain all the steps involved in the conversion of a (quantified) statement to conjunctive normal form (CNF) with a suitable example. Why is CNF required?

## Short answer

Resolution requires CNF, a conjunction of disjunctions of literals. Convert by eliminating → and ↔, moving ¬ inward, standardizing variables, prenex, Skolemizing existentials, dropping ∀, distributing ∨ over ∧, splitting conjunctions, and standardizing variables apart.

## Answer

**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) ]

```text
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)

## Check yourself

The answer's key points as multiple-choice questions, with the correct option and why.

1. What is conjunctive normal form?
   A. A disjunction of conjunctions
   B. A conjunction of clauses, each clause a disjunction of literals
   C. A single implication
   D. A set of quantified formulas
   Answer: B. CNF is an AND of clauses where each clause is an OR of literals. (Key point: What CNF is)

2. Why is CNF required for resolution?
   A. Resolution works on pairs of clauses with complementary literals, so all sentences must be clauses
   B. It makes statements longer
   C. It removes the need for a goal
   D. It makes the proof unsound
   Answer: A. CNF gives a uniform quantifier-free form on which the resolution rule can be applied mechanically. (Key point: Why CNF)

3. Which is the correct beginning of the conversion order?
   A. Skolemise, then eliminate implications
   B. Eliminate implications and biconditionals, then move negation inwards
   C. Distribute OR over AND, then remove implications
   D. Drop quantifiers, then standardise variables
   Answer: B. First P → Q is replaced by ¬P ∨ Q, then negation is pushed inward by De Morgan and quantifier laws. (Key point: Order of first steps)

4. How is an existential quantifier removed?
   A. Replace the variable by a Skolem constant, or by a Skolem function of the preceding universal variables
   B. Replace it by a universal quantifier
   C. Delete it together with its predicate
   D. Replace it by a negation
   Answer: A. ∃ is replaced by a Skolem constant when no ∀ precedes it, otherwise by a Skolem function of those universal variables. (Key point: Skolemisation)

## Related in Artificial Intelligence

- [Hopfield network and its steps](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Ahopfield-network-steps) — Artificial Intelligence, chapter 6
- [Self-organizing map (SOM) steps](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aself-organizing-map) — Artificial Intelligence, chapter 6
- [NLU and NLG; NLP steps](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Anlu-nlg-nlp-steps) — Artificial Intelligence, chapter 7

## Related in other subjects

- [CNF conversion (grammar with S→A|B)](https://www.bctengineer.com/question.md?key=semester_3%2Ftheory_of_computation%3Acnf-conversion-s-a-b) — Theory of Computation, chapter 3
- [Define CNF; convert S→MaN|bL|bM grammar](https://www.bctengineer.com/question.md?key=semester_3%2Ftheory_of_computation%3Acnf-define-convert-mln) — Theory of Computation, chapter 3
- [System implementation and conversion](https://www.bctengineer.com/question.md?key=semester_8%2Finformation_system%3Asystem-implementation-conversion) — Information System, chapter 6
- [PCM and analog-to-digital conversion](https://www.bctengineer.com/question.md?key=semester_5%2Fdata_communication%3Apcm-working) — Data Communication, chapter 5, asked 4×