Abstract
∈-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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Baaz and C.G. Fermüller. Non-elementary speedups between different versions of tableaux. In 4th International Workshop, TABLEAUX’95, LNCS 918, 1995.
Bernhard Beckert. Integrating and Unifying Methods of Tableau-based Theorem Proving. PhD thesis, Universität Karlsruhe, Fakultät für Informatik, 1998.
Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt. The even more liberalized δ-rule in free variable semantic tableaux. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Proceedings, 3rd Kurt Gödel Colloquium (KGC), Brno, Czech Republic, LNCS 713, pages 108–119. Springer, 1993.
Domenico Cantone and Marianna Nicolosi Asmundo. A further and effective liberalization of the δ-rule in free variable semantic tableaux. In Ricardo Caferra and Gernot Salzer, editors, Int. Workshop on First-Order Theorem Proving (FTP’98), Technical Report E1852-GS-981, pages 86–96. Technische Universität Wien, Austria, 1998. Electronically available from http://www.logic.at/ftp98.
Melvin C. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1990.
Martin Giese. Integriertes automatisches und interaktives Beweisen: Die Kalkülebene. Diploma Thesis, Fakultät für Informatik, Universität Karlsruhe, June 1998.
Reiner Hähnle and Peter H. Schmitt. The liberalized δ-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13(2):211–222, 1994.
D. Hilbert and P. Bernays. Grundlagen der Mathematik, volume 2. Springer Verlag, 1968.
A.C. Leisenring. Mathematical Logic and Hilbert’s ∈-Symbol. MacDonald, London, 1969.
W.P.M. Meyer Viol. Instantial Logic. An Investigation into Reasoning with Instances. Number DS-1995-11 in ILLC Dissertation Series. Universiteit van Amsterdam, 1995.
Raymond M. Smullyan. First-Order Logic, volume 43 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, New York, 1968.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giese, M., Ahrendt, W. (1999). Hilbert’s ∈-Terms in Automated Theorem Proving. In: Murray, N.V. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. Lecture Notes in Computer Science(), vol 1617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48754-9_17
Download citation
DOI: https://doi.org/10.1007/3-540-48754-9_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66086-6
Online ISBN: 978-3-540-48754-8
eBook Packages: Springer Book Archive