Prenex Normal Form

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.

• 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) )
  

Tags: transformation, formula, equivalences
Parent: Canonical Form

Update entry (Admin) | See changes

---

Back to top

---