Skolemization of a Formula

Question

I have the following formula:

 forall x(p(x) <- exists y q(y,x))

What is the Skolemization of the above formula?

Answer 1

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).