How to generate Skolem function in practice

Question

Context: Skolemization is the process of removing the existential quantifiers in a first-order formula. The existential bounded variables are replaced with existential quantified function.

Questions: How, in practice, are these functions generated by an algorithm? Do we have another choice than a brute force strategy over all the possible functions? Is it of any practical use?

Example: Assume the formula $\forall{x}.\exists{y}.x \neq y$, then the Skolem form is $\exists{f}.\forall{x}.x \neq f(x)$ where $f$ is the function that explicits the dependency between $x$ and $y$. With resolution or any other method, how to, algorithmically, decide what is the result of $f(x)$? Is it all the values of the domain of discourse of $y$? If yes, does it mean that the role of the function is actually to "forbid" the value of $f(x)$ to change when a variable other than $x$ (if there was any) is instantiated?

Partial answer: As given below, we do not need to interpret the function $f$ to prove the validity. However, what about finding a model that satisfies the formula?

As I understood it...: Replying to myself to close this question. I guess there is no magic and we need to consider every function $f$ until we find a model. So if $f$ takes 2 arguments, it can maps to $|U| * |U|$ values ($|U|$ being the cardinality of the universe of discourse) and hence, the Skolem function is equivalent to the initial $\exists$ quantifier.

Answer 1

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}$.