# Maths / Logic and Modelling – CNF

January 10, 2010 Leave a comment

This is going to be the first post I’m going to write that is valid for BOTH year 1 and year 2. Just in case you get confused as to who should be reading it 😉

CNF is short for Conjunctive Normal Form. A formula is in CNF if it is True (T) or False ( _|_ ) or a conjunction of disjunctions:

Such as:

- T or _|_
- (q \/ p) /\ p
- (q \/ p) /\ (r \/ q)

# Rewrite Rules

In order to convert a formula to CNF, one much rewrite the formulas sub-formulas. For example, using these rewrite rules:

- A <-> B = (¬A \/ B) /\ (¬B \/ A)
- A –> B = ¬A \/ B
- ¬(A \/ B) = ¬A /\ ¬B
- ¬(A /\ B) = ¬A \/ ¬B
- ¬¬A = A
- (A /\ B) \/ C = (A \/ C) /\ (B \/ C)

Now, have you noticed? None of the rewrites contain either “<->” or “->”, this is because a CNF formula must contain NO “<->” or “->” 😉

# Example

Lets now consider a quick example. Consider the following formula:

- ((p –> q) –> r)

Now lets go through the steps to transform it:

- Using the priorities, the first part to rewrite is “p –> q” so we get:
- p –> q = ¬p \/ q
Now we have the formula (¬p \/ q) –> r

- p –> q = ¬p \/ q
- Next we have to rewrite the whole of the formula using the implication rewrite rule so we get:
- (¬p \/ q) –> r = ¬(¬p \/ q) \/ r
now we have to simplify this:

- ¬(¬p \/ q) \/ r = (¬¬p /\ ¬q) \/ r

- (¬p \/ q) –> r = ¬(¬p \/ q) \/ r
- As you can now see we have a double negation on ‘¬¬p’, so we use the rule above so that we have:
- (¬¬p /\ ¬q) \/ r = (p /\ ¬q) \/ r

- Finally we use the expansion rule next:
- (p /\ ¬q) \/ r = (p \/ r) /\ (¬q \/ r)

And there we go 😀 , the CNF form of the formula ((p –> q) –> r) is *(p \/ r) /\ (¬q \/ r)*

# Clauses – Year 2 Only

As a quick note – and this is only for second years… When using the DPLL algorithm we a CNF’ed formula we need to use the clauses to check satisfiability. The clauses from the CNF formula above are:

- (p \/ r)
- (¬q \/ r)