Science Fair Project Encyclopedia

Science Fair Project Encyclopedia Contents Page

Skolem normal form

A formula of first-order logic is in Skolem normal form if its prenex normal form has only universal quantifiers. A formula can be Skolemized, that is have its existential quantifiers eliminated to produce an equisatisfiable formula to the original.

The essence of skolemization is the observation that if a formula in the form

$\forall x_1 \dots \forall x_n \exists y M(x_1,\dots,x_n,y)$

is satisfiable in some model, then there must be some point in the model for every

$x_1,\dots,x_n$

which makes

$M(x_1,\dots,x_n,y)$

true, and there will be some function

$y = f(x_1,\dots,x_n)$

which makes the formula

$\forall x_1 \dots \forall x_n M(x_1,\dots,x_n,f(x_1,\dots,x_n))$

hold in this model.

The function f is called a Skolem function.

Categories: Model theory

Science Fair Project Encyclopedia Contents Page

10-26-2009 08:16:03
The contents of this article is licensed from www.wikipedia.org under the GNU Free Documentation License. Click here to see the transparent copy and copyright details

All Science Fair Projects

Science Fair Project Encyclopedia for Schools!

Science Fair Project Encyclopedia

Skolem normal form