Uses of Skolemization
One of the uses of Skolemization is automated theorem proving. For example, in the method of analytic tableaux, whenever a formula whose leading quantifier is existential occurs, the formula obtained by removing that quantifier via Skolemization can be generated. For example, if occurs in a tableau, where are the free variables of, then can be added to the same branch of the tableau. This addition does not alter the satisfiability of the tableau: every model of the old formula can be extended, by adding a suitable evaluation of, to a model of the new formula.
This form of Skolemization is actually an improvement over "classical" Skolemization in that only variables that are free in the formula are placed in the Skolem term. This is an improvement because the semantics of tableau may implicitly place the formula in the scope of some universally quantified variables that are not in the formula itself; these variables are not in the Skolem term, while they would be there according to the original definition of Skolemization. Another improvement that can be used is using the same Skolem function symbol for formulae that are identical up to variable renaming.
Another use is in the resolution method for first order logic, where formulas are represented as sets of clauses understood to be universally quantified. (For an example see drinker paradox.)
Read more about this topic: Skolem Normal Form