## Change - Prenex Normal Form

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

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 Norma
l form is to put all Quantifications in front of the Formula without losing its Connections to the Formula were the Quantifier is applied to. ¶

Clean up Formulas (Quantifiers are bound to different Variables) ¶

( (∃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) ) ¶

Then put all Quantifiers from Negation Normal Form in front ¶

(∃X)(∀Y)(∃Z)(( penguin(X) ∧ ¬blackandhite(X) ) ¶
∨ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) ) ¶
∨ ( penguin(Z) ∧ oldTVshow(Z) ) ¶

Comment: Updated entry