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 on This Data Unit