Maths / Logic and Modelling – CNF

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:

1. 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
     
2. 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
     
3. 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
     
4. Finally we use the expansion rule next:
   • (p /\ ¬q) \/ r    =    (p \/ r) /\ (¬q \/ r)

And there we go :D , 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)