Skolemization

Skolemization step

2

4

6

8

10

arithmetical level

Σ : existential

Π : universal

alternations

1

2

3

repeating quantifiers

1

2

free variable

yes

no

initial formula:

∃

x1

∀

x2

∃

x3

P(x1,x2,x3)x3

The process of removing all the existential quantifiers from a formula is known as Skolemization. The result is a formula in Skolem normal form that is equivalent in computational complexity to the original. This Demonstration shows the rewriting process of a Skolemization step by step for all general cases up to three quantifier alternations and seven variables or constants.

External Links

Skolem Normal Form (Wolfram MathWorld)

Permanent Citation

Hector Zenil

"Skolemization"
http://demonstrations.wolfram.com/Skolemization/
Wolfram Demonstrations Project
Published: September 28, 2007