Skip to main content

Hilbert’s ε-terms in automated theorem proving

Citations of this article
Mendeley users who have this article in their library.
Get full text


ε-terms, introduced by David Hilbert [8], have the form εx.φ, where x is a variable and φ is a formula. Their syntactical structure is thus similar to that of a quantified formulae, but they are terms, denoting ‘an element for which φ holds, if there is any’. The topic of this paper is an investigation into the possibilities and limits of using ε-terms for automated theorem proving. We discuss the relationship between ε-terms and Skolem terms (which both can be used alternatively for the purpose of ∃-quantifier elimination), in particular with respect to efficiency and intuition. We also discuss the consequences of allowing ε-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 ε-terms. We give a theoretical foundation of the usage of both variants in a single framework. Finally, we argue that these two approaches to ε are just the extremes of a range of ε-treatments, corresponding to a range of different possible Skolemization variants.




Giese, M., & Ahrendt, W. (1999). Hilbert’s ε-terms in automated theorem proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 171–185). Springer Verlag.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free