Created on March 5, 2013, 9:50 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:31 p.m.
The Prenex Normal Form is about to clean up Formulas so that Quantifiers are all bound to the same Variables
need to be bound in in each single part to another Variable.
By doing this one has a unique Identification that a quantifier denotes a defined Variable and each Formula relates to a Quantifier.
The reason for doing the Prenex Normal form is to put all Quantifications in front of the Formula without losing its Connections to the Formula were the Quantifier is applied to.
( (∃X)( penguin(X) ∧ ¬blackandwhite(X) )
∨ (∀X)(¬oldTVshow(X) ∨ ¬blackanwhite(X) )
) ∨ (∃X)( penguin(X) ∧ oldTVshow(X) )
is transformed into
( (∃X)( penguin(X) ∧ ¬blackandwhite(X) )
∨ (∀Y)( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) )
) ∨ (∃Y)( penguin(Z) ∧ oldTVsow(Z) )
(∃X)(∀Y)(∃Z)(( penguin(X) ∧ ¬blackandhite(X) )
∨ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) )
∨ ( penguin(Z) ∧ oldTVshow(Z) )
Comment on This Data Unit