Hilbert's $ε$-Terms in Automated Theorem Proving TeX Export

@incollection{citeulike:1743022, abstract = {\$ε\$-terms, introduced by David Hilbert [2], 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.}, author = {Giese, Martin and Ahrendt, Wolfgang}, citeulike-article-id = {1743022}, citeulike-linkout-0 = {http://www.springerlink.com/content/rpcl7fn93dm3vr07}, journal = {Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX´99, Saratoga Springs, NY, USA, June 1999. Proceedings}, keywords = {epsilon, proof\_theory, tableaux}, pages = {662}, posted-at = {2007-10-08 19:35:15}, priority = {0}, title = {Hilbert's \$\varepsilon\$-Terms in Automated Theorem Proving}, url = {http://www.springerlink.com/content/rpcl7fn93dm3vr07}, year = {1999} }

TY - CHAP ID - citeulike:1743022 L3 - citeulike-article-id:1743022 N2 - $ε$-terms, introduced by David Hilbert [2], 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. JF - Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX´99, Saratoga Springs, NY, USA, June 1999. Proceedings EP - 662 TI - Hilbert's $\varepsilon$-Terms in Automated Theorem Proving SP - 662 KW - epsilon KW - proof_theory KW - tableaux AU - Giese, Martin AU - Ahrendt, Wolfgang PY - 1999/// UR - http://www.springerlink.com/content/rpcl7fn93dm3vr07 ER -