Skolem Normal Form

Created on March 5, 2013, 10:04 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:31 p.m.

The Skolem Normal Form is about the removal of Existential Quantifiers. To remove Existential Quantifiers one has to consider their Positions as one can not simple change universals and existential Quantifiers that changes also the Meaning of the Formulas behind them.

If the existential quantifier is independent of any other as it is not precede by anything it can be replaced by a Constant. On the other hand if a Universal Quantifier is preceding it must be replaced by a Function of the Universal Quantifier because it depends on it. If there are more than one Universal Quantifiers all of the Variables of the Universal Quantifiers must be represented within this Function, the Skolem Function

  • remove existential quantifiers
    (∃X)(∀Y)(∃Z) (( penguin(X) ∧ ¬blackandwhite(X) )
    ∨ ( ¬oldTVshow(Y)  ∨ ¬blackandwhite(Y) ) )
    ∨ ( penguin(Z) ^ oldTVshow(Z) )

is transformed into

   (∀Y)( ( penguin(a) ∧ ¬blackandwhite(a) )
   ∧ ( ¬oldTVshow(Y) ∨ ¬blackandwhite(Y) ) )
   ∨ ( penguin( f(Y) ) ∧ oldTVshow( f(Y) ) )
  • where a ad f are new symbols (so called Skolem Constant or Skolem Function).

The Skolem Normal Formula Algorithm for Removal of all Existential Quantifiers starts from left to the right and works like the following.

  • How to:
  • remove Essential Quantifiers from left to right
  • If there is no Universal Quantifier left of the Existential Quantifier to be removed, then the according Variable is substituted by a new Constant Symbol.
  • If there are n Universal Quantifiers left of the Existential Quantifier to be removed, the according Variable is substituted with a new Function Symbol with arity n, whose arguments are exactly the Variables of the n Universal Quantifiers.

Tags: transformation, formula, equivalences
Parent: Canonical Form

Update entry (Admin) | See changes

Comment on This Data Unit