Created on March 5, 2013, 10:15 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:31 p.m.
If there are only Universal Quantifiers, they can 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 on This Data Unit