Instruments for getting Skolem normal form I have a problem to solve: 
$\forall x[\neg P(x) \land \forall y \neg Q(x,y) \rightarrow \forall x \forall y R(x,y,z)]$ 
I see that two quantifiers are influencing on the exact same variable.That's why I'm to make a change of variables: x change to t and y to k
Then this is what I have :
$\forall x[ P(x) \lor \exists y Q(x,y) \lor \forall t \forall k R(t,k,z)]$ 
Then I am making a preformed normal form
$\forall x \exists y \forall t \forall k [P(x) \lor  Q(x,y) \lor  R(t,k,z)]$ 
And finally making skolemization
y=f(x)
$\forall x  \forall t \forall k [P(x) \lor  Q(x,f(x)) \lor  R(t,k,z)]$ 
Is it a right answer? Because I still don't know what to make with free variable z.
How can I automatically check the answer of such  problems? I mean can MATLAB or Mathematica solve the skolemization problems like this?
 A: There are different procedures for forming the skolemization, but if you want to treat open formulas (= formulas with free variables), you'd normally start by forming the universal closure of the formula, that is, for each free variable, introduce a universal quantifier to the beginning of the formula:  
$0.\ ∀x[¬P(x)∧∀y¬Q(x,y)→∀x∀yR(x,y,z)]$ (original formula)
$1.\ ∀z∀x[¬P(x)∧∀y¬Q(x,y)→∀x∀yR(x,y,z)]$ (universal closure)
$2.\ ∀z∀x[P(x)∨∃yQ(x,y)∨∀t∀kR(t,k,z)]$ (resolve variable conflicts)  
...
This is sound because semantically, free variables are implicitly universally quantified: By the definition of validity, a formula is valid if it is true under all valuations; but if a formula with free variables fulfills that requirement, that amounts to just the same as universally quantifying over all the free variables. So just putting a $\forall$ in front of every free variable leaves you with essentially the same formula that is now closed. (After all, with skolemization we do just the same vice versa in the end, where we remove all the $\forall$ quantifiers in the prefix to yield an quantifier-less, open formula.)
A different procedure that allows to treat open formulas without requiring to form the universal closure at the very beginning eliminates universal quantifiers on the fly rather than at the very end, but the above mentioned procedure should be fine with the way you layed out the skolemization in your post.
What's missing in your skolemization is the final, most crucial step, namely the elimination of the quantifiers:
...
$4.\ ∀z∀x∀t∀k[P(x)∨Q(x,f(z,x))∨R(t,k,z)]$ (note that with the additional $\forall z$ in front of the $\exists y$, we now also need $z$ in $f(z,x)$)
$5.\ P(x)∨Q(x,f(z,x))∨R(t,k,z)$ (eliminate universal quantifiers -- this is your fully skolemized formula)
