Computer Proofs in Gödel’s Class Theory with Equational Definitions for Composite and Cross
Tóm tắt
Some basic theorems about composition and other key constructs of set theory were proved using McCune’s computer program OTTER, building on Quaife’s modification of Gödel’s class theory. Our proofs use equational definitions in terms of Gödel’s flip and rotate functors. A new way to prove the composition of homomorphisms theorem is also presented.
Tài liệu tham khảo
Belinfante, J.: On a modification of Gödel's algorithm for class formation, Association for Automated Reasoning Newsletter 34 (1996), 10–15.
Boyer, R., Lusk, E., McCune, W., OverÒeek, R., Stickel, M., and Wos, L.: Set theory in first order logic: Clauses for Gödel's axioms, J. Automated Reasoning 2 (1986), 287–327.
Gödel, K.: The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis, Princeton University Press, Princeton, NJ, 1940.
McCune, W. W.: Otter 3.0 reference manual and guide, Argonne National LaÒoratory Report ANL–94/6, Argonne National LaÒoratory, Argonne, IL, January 1994.
Quaife, A.: Automated Development of Fundamental Mathematical Theories, Ph.D. Thesis, University of California at Berkeley, Kluwer Academic PuÒlishers, Dordrecht, the Netherlands, 1992.
Tarski, A. and Givant, S.: A Formalization of Set Theory without VariaÒles, Amer.Math. Soc., Colloquium PuÒlications, Vol. 41, Providence, 1987. Reviewed Òy Lisl Gaal in The Amer.Math. Monthly, March 1990.
Wolfram, S.: Mathematica TM , A System for Doing Mathematics Òy Computer, 2nd edn, Addison–Wesley, New York, 1991.
Wos, L.: Automated Reasoning: 33 Basic Research ProÒlems, Prentice-Hall, Englewood Cliffs, NJ, 1988.