@MISC{Nonnengart-StrSkol97,
	AUTHOR = {Andreas Nonnengart},
	TITLE = {Strong Skolemization},
	HOWPUBLISHED = {Submitted},
	YEAR = {1997},
	ABSTRACT = {Skolemization is a means to eliminate existential quantifiers within
predicate logic sentences by replacing existentially quantified variables
with Skolem function applications.
The arguments of such Skolem functions are variables that are quantified outside
the sub-formula under consideration.
In this article a skolemization technique is introduced which abstracts from
some of the Skolem function arguments.
It turns out that the result obtained this way is
usually more general than what can be achieved from standard (classical)
Skolemization techniques.
From a theorem prover's point of view such generalizations often lead to a
reduction of both search space and proof length.},
}