Hilbert's Epsilon terms in Automated Theorem Proving
----------------------------------------------------

Martin Giese, Wolfgang Ahrendt

epsilon-terms, introduced by David Hilbert, have the form
`epsilon x. phi', where x is a variable and phi is a formula. Their
syntactical structure is thus similar to that of a quantified
formulae, but they are terms, denoting `an element for which phi
holds, if there is any'.

The topic of this paper is an investigation into the possibilities and
limits of using epsilon-terms for automated theorem proving.  We
discuss the relationship between epsilon-terms and Skolem terms (which
both can be used alternatively for the purpose of existential
quantifier elimination), in particular with respect to efficiency and
intuition.  We also discuss the consequences of allowing epsilon-terms
in theorems (and cuts). This leads to a distinction between
(essentially two) semantics and corresponding calculi, one enabling
efficient automated proof search, and the other one requiring human
guidance but enabling a very intuitive (i.e. semantic) treatment of
epsilon-terms.  We give a theoretical foundation of the usage of both
variants in a single framework. Finally, we argue that these two
approaches to epsilon are just the extremes of a range of
epsilon-treatments, corresponding to a range of different possible
Skolemization variants.