WOLFRAM|DEMONSTRATIONS PROJECT

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.