Change - Conjunctive Normal Form

Created on March 5, 2013, 10:15 p.m. by Hevok & updated on March 28, 2013, 9:21 p.m. by Hevok

If there are only Universal Quantifiers, they can be safely be removed so that it results into a Formula without any Quantifiers. ¶

In order to get into the Conjunctive Normal Form, one can for example use the Formulas for Distributive Law, so that the Formula gets switched into a Conjunction of Disjunctions which would then be the Conjunctive Normal Form (Clausal Form). ¶

There are only Universal Quantifiers, therefore we can remove them ¶

( penguin(a) ∧ ¬blackandwhite(a) ) ¶
∨ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) ) ¶
∨ ( penguin(f(Y)) ∧ oldTVshow(f(Y)) ¶

With the help of logical equivalences the formula is now transformed into a Conjunction of Disjunctions. ¶

F ∨ (G ∧ H) ≡ (F v G) ∧ (F ∨ H) ¶
F ∧ (G ∨ H) ≡ (F ∧ G) ∨ (F ∧ H) ¶

* For Example: ¶

(penguin(a) ∨ ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ∨ penguin(f(Y)) ) ¶
∧ (penguin(a) ∨ ¬oldTVshow(Y) ∨ ¬blackendwhite(Y) ∨ oldTVshow(f(Y)) ) ¶
∧ (¬blachandwhite(a) ∨ ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ∨ penguin(f(Y)) ) ¶
∧ (¬blackandwhite(a) ∨ ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ∨ oldTVshow(f(Y)) ) ¶

is transformed into ¶

{ {penguin(a), ¬oldTVshow(Y), ¬blackandwhite(Y), penguin(f(Y))}, ¶
{penguin(a), ¬oldTVshow(Y), ¬blackandwhite(Y), oldTVshow(f(Y))}, ¶
{ ¬blackandwhite(a), ¬oldTVshow(Y), ¬blackandwhite(Y), penguin(f(Y))}, ¶
{ ¬blackandwhite(a), ¬oldTVshow(Y), ¬blackandwhite(Y), oldTVshow(f(Y))} } ¶

This results in Formulas that are bigger, but this is no Problem as Computers should do that.


Comment: Updated entry

Comment on This Data Unit