Consider a formula in prenex normal form,
 |
If 
is the existential quantifier (
) and 
, ..., 
are all the universal
quantifier variables such that 
, 
, then introduce the new function symbol 
and term 
. (If 
, then 
is a constant.) This function is called Skolem function (or
Herbrand function).
Now replace all occurrences of 
by this term and remove 
. When all existential
quantifiers are removed, convert 
into conjunctive normal
form. This process, which usually termed skolemization, results in a formula
in Skolemized form. The resulting formula is unsatisfiable iff the source formula is unsatisfiable.
Note that if the source formula is satisfiable, it is not necessarily equivalent
to the resulting formula.
