How to generate Skolem function in practice
First of all there are two Skolem transformations, one replaces universal quantifiers and preserves validity, the other one replaces existential quantifiers and preserves satisfiability of the formula. Your question is about the second kind, so I will present it this way, but the other version is dual (and at least for me easier to understand).

Lemma: let $F$ be a formula and $sk(F)$ a Skolem transformation of $F$. Then if there exists a model $\mathcal{M}$ s.t. $\mathcal{M} \models F$ there exists a model $\mathcal{N}$ s.t. $\mathcal{N} \models sk(F)$.

If we can show that $sk(F)$ is unsatisfiable, it has no model. But then also $F$ can not have a model.

Now, Resolution is a quite efficient method to show that a formula (in conjunctive normal form) is unsatisfiable. This leads to the following approach to proving the validity of some formula $F$:


Negate $F$
Skolemize, transform the formula into conjunctive normal form
Find a refutation for the CNF formula (a so called clause set)
Because $\neg F$ does not have a model, all interpretations of $F$ must be a model - in other words: $F$ is valid.


Nowhere in this procedure do you need the actual interpretation of a Skolem function, you just rely on the fact that one must exist as part of the model $\mathcal{N}$.