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 -
is satisfiable in some model, then there must be some point in the model for every -
which makes -
true, and there will be some function -
which makes the formula -
hold in this model. The function f is called a Skolem function.
|
|
