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.