Change: Prenex Normal Form

created on March 5, 2013, 9:50 p.m. by Hevok & updated on March 5, 2013, 9:50 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 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) )
    
prenex.jpg

Categories:
Parent: Canonical Form

Comment: Corrected formulas.

See entry | Admin

Comment on This Data Unit