Skolemization of a Formula I have the following formula:
 forall x(p(x) <- exists y q(y,x))

What is the Skolemization of the above formula?
 A: I managed to see the skolemization in a theorem prover:
============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 7.
% Level of proof is 3.
% Maximum clause weight is 0.
% Given clauses 0.

1 (all x (p(x) <- (exists y q(y,x)))) # label(non_clause).  [assumption].
2 p(2) # label(non_clause) # label(goal).  [goal].
3 -p(2).  [deny(2)].
4 p(x) | -q(y,x).  [clausify(1)].
5 -q(x,2).  [resolve(3,a,4,a)].
6 q(1,2).  [assumption].
7 $F.  [resolve(5,a,6,a)].

============================== end of proof ==========================

The Skolemization and Clausal Form is seen in step 4. It reads 
as follows:
p(x) v ~q(y,x)

It basically results from first replacing A <- B by A v ~B. And  moving the quantifier out so that a prenex form results. In the present case, when moving the quantifier out the existential quantifier turns into a forall quantifier. So that in the end no skolem function is needed.
Bye
P.S.: The theorem prover can be downloaded from here. It has a GUI and is available for Mac,  Windows and Linux:
http://www.cs.unm.edu/~mccune/prover9/gui/v05.html
But it doesn't work as a general method to obtain a Skolemization, since it will not show Skolemizations of formulas just like that. It will only show for those that are used in a proof. In the present case, to force a proof I have added the fact p(1,2) and the goal p(2).
A: Maybe the following will help with Skolemization in general...
Reading Change and Lee's Symbolic Logic and Mechanical Theorem Proving it seems to me that roughly speaking a Skolemization can get described as replacing the variable that an existential quantifier quantifies with a function f(a, ..., n) [sic, the function here is f(a, ..., z)... the functor is "f")] of arity n such that n is equal to the number of universally quantified variables that precede the existential quantifier.  The variables of the function also get inherited from the universal quantifiers or quantifier.  So, for example if we Skolemitize 
exists x x

then since no universal quantifiers preceding "exists x", we replace x by a nullary function obtaining 
a

If we had 
all x all y exists z all u exists v P(x, y, z, u, v)

The first exists has two universal quantifiers preceding it, so if we just "Skolemtize" the first existential quantifier out we obtain
all x all y all u exists v P[x, y, f(x, y), u, v]

And now Skolemtizing "exists v" we obtain
all x all y all u P[x, y, f(x, y), u, g(x, y, u)]

