Abstract
A computer implementation of Gödel’s algorithm for class formation in MathematicaTM is useful for automated reasoning in set theory. The original intent was to forge a convenient preprocessing tool to help prepare input files for McCune’s automated reasoning program Otter. The program is also valuable for discovering new theorems. Some applications are described, especially to the definition of functions. A brief extract from the program is included in an appendix.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Belinfante, J.G.F.: On a Modification of Gódel’s Algorithm for Class Formation. Association for Automated Reasoning News Letter, No. 34, 10–15 (1996)
Belinfante, J.G.F.: On Quaife’s Development of Class Theory. Association for Automated Reasoning Newsletter, No. 37, 5–9 (1997)
Belinfante, J.G.F.: Computer Proofs in Gödel’s Class Theory with Equational Definitions for Composite and Cross. Journal of Automated Reasoning 22, 311–339 (1999)
Belinfante, J.G.F.: On Computer-Assisted Proofs in Ordinal Number Theory. Journal of Automated Reasoning 22, 341–378 (1999)
Bernays, P.: Axiomatic Set Theory, 1st edn. North Holland Publishing Co., Amsterdam (1958); Second edition: 1968. Republished in 1991 by Dover Publications, New York
Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.: Set Theory in First Order Logic: Clauses for Gödel’s Axioms. Journal of Automated Reasoning 2, 287–327 (1986)
Formisano, A., Omodeo, E.G.: An Equational Re-Engineering of Set Theories presented at the FTP 1998. International Workshop on First Order Theorem Proving, November 23-25 (1998)
Gödel, K.: The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory. Princeton University Press, Princeton (1940)
Isbell, J.R.: A Definition of Ordinal Numbers. The American Mathematical Monthly 67, 51–52 (1960)
McCune, W.W.: Otter 3.0 Reference Manual and Guide, Argonne National Laboratory Report ANL–94/6, Argonne National Laboratory, Argonne, IL (January 1994)
Megill, N.D.: Metamath: A Computer Language for Pure Mathematics 1997
Noël, P.A.J.: Experimenting with Isabelle in ZF set theory. Journal of Automated Reasoning 10, 15–58 (1993)
Paulson, L.C., Grąbczewski, K.: Mechanizing Set Theory. Journal of Automated Reasoning 17, 291–323 (1996)
Quaife, A.: Automated Deduction in von Neumann-Bernays-Gödel Set Theory. Journal of Automated Reasoning 8, 91–147 (1992)
Quaife, A.: Automated Development of Fundamental Mathematical Theories, Ph.D. thesis. Univ. of California at Berkeley. Kluwer Acad. Publishers, Dordrecht (1992)
Tarski, A., Givant, S.: A Formalization of Set Theory without Variables, vol. 41. American Mathematical Society Colloquium Publications, Providence, Rhode Island (1987)
Wos, L.: Automated Reasoning: 33 Basic Research Problems. Prentice Hall, Englewood Cliffs (1988)
Wos, L.: The problem of finding an inference rule for set theory. Journal of Automated Reasoning 5, 93–95 (1989)
Wos, L., Overbeek, R., Lusk, E., Boyle, J.: Automated Reasoning: Introduction and Applications, 2nd edn. McGraw Hill, New York (1992)
Wolfram, S.: The Mathematica TM Book. Wolfram Media Inc., Champaign, Illinois (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Belinfante, J.G.F. (2000). Gödel’s Algorithm for Class Formation. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_9
Download citation
DOI: https://doi.org/10.1007/10721959_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive