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
(∃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) ) )
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.
Comment on This Data Unit