{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T06:52:20Z","timestamp":1743144740512,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_18","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"228-242","source":"Crossref","is-referenced-by-count":3,"title":["Reasoning about Iteration in G\u00f6del\u2019s Class Theory"],"prefix":"10.1007","author":[{"given":"Johan Gijsbertus Frederik","family":"Belinfante","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P.B. Andrews","year":"1996","unstructured":"Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfennig, F., Xi, H.: TPS: A theorem-proving system for classical type theory. Journal of Automated Reasoning\u00a016, 321\u2013353 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR2","unstructured":"Andrews, P.B.: Proving theorems automatically and interactively with TPS, Special Session SS S3. In: Automated Reasoning in Mathematics and Logic. American Mathematical Society Meeting No. 975 in Atlanta, GA., March 9 (2002), Abstract 975-03-86"},{"key":"18_CR3","first-page":"10","volume":"34","author":"J.G.F. Belinfante","year":"1996","unstructured":"Belinfante, J.G.F.: On a modification of G\u00f6del\u2019s algorithm for class formation. Association for Automated Reasoning News Letter\u00a0(34), 10\u201315 (1996)","journal-title":"Association for Automated Reasoning News Letter"},{"key":"18_CR4","first-page":"5","volume":"37","author":"J.G.F. Belinfante","year":"1997","unstructured":"Belinfante, J.G.F.: On Quaife\u2019s development of class theory. Association for Automated Reasoning Newsletter\u00a0(37), 5\u20139 (1997)","journal-title":"Association for Automated Reasoning Newsletter"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1023\/A:1006050629424","volume":"22","author":"J.G.F. Belinfante","year":"1999","unstructured":"Belinfante, J.G.F.: Computer proofs in G\u00f6del\u2019s class theory with equational definitions for composite and cross. Journal of Automated Reasoning\u00a022, 311\u2013339 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1023\/A:1006010913494","volume":"22","author":"J.G.F. Belinfante","year":"1999","unstructured":"Belinfante, J.G.F.: On computer-assisted proofs in ordinal number theory. Journal of Automated Reasoning\u00a022, 341\u2013378 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/10721959_9","volume-title":"Automated Deduction - CADE-17","author":"J.G.F. Belinfante","year":"2000","unstructured":"Belinfante, J.G.F.: G\u00f6del\u2019s Algorithm for Class Formation. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 132\u2013147. Springer, Heidelberg (2000)"},{"key":"18_CR8","unstructured":"Belinfante, J.G.F.: The Unifying Concept of Subvariance. In: Baumgartner, P., Zhang, H. (eds.) FTP 2000, Third International Workshop on First-Order Theorem Proving, St. Andrews, Scotland. Fachberichte Informatik, Universit \u201dat Koblenz-Landau, pp. 56\u201367 (2000)"},{"key":"18_CR9","unstructured":"Belinfante, J.G.F.: Computer Proofs about Transitive Closure. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) International Joint Conference on Automated Reasoning, IJCAR-2001 Short Papers, Technical Report DII 11\/01, Siena, Italy, June 19\u201323, pp. 11\u201320 (2001)"},{"key":"18_CR10","unstructured":"Belinfante, J.G.F.: Discovering Theorems using GOEDEL: A Case Study. In: Linton, S., Sebastiani, R. (eds.) Calculemus-2001, 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Siena, Italy, June 21\u201322 (2001)"},{"key":"18_CR11","unstructured":"Belinfante, J.G.F.: Automated reasoning about the Zermelo-von Neumann cumulative hierarchy. In: Special Session SS S3. Automated Reasoning in Mathematics and Logic, American Mathematical Society Meeting No. 975, Atlanta, GA., March 9 (2002) (abstract 975-03-83)"},{"key":"18_CR12","volume-title":"Axiomatic Set Theory","author":"P. Bernays","year":"1958","unstructured":"Bernays, P.: Axiomatic Set Theory, 1st edn. North Holland Publishing Co., Amsterdam (1958); 2nd edn. (1968); Republished in 1991 by Dover Publications, New York","edition":"1"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"R. Boyer","year":"1986","unstructured":"Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.: Set theory in first orderlogic: clauses for G\u00f6del\u2019s axioms. Journal of Automated Reasoning\u00a02, 287\u2013327 (1986)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR14","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Strother Moore, J.: A Computational Logic Handbook. Academic Press, London (1988)"},{"key":"18_CR15","volume-title":"The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory","author":"K. G\u00f6del","year":"1940","unstructured":"G\u00f6del, 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)"},{"key":"18_CR16","unstructured":"McCune, W.W.: Otter 3.0 Reference Manual and Guide, Argonne National Laboratory Report ANL\u201394\/6, Argonne National Laboratory, Argonne, IL (January 1994)"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning\u00a019, 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR18","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L.C. Paulson","year":"1995","unstructured":"Paulson, L.C.: Set Theory for Verification. II. Induction and Recursion. Induction and Recursion, Journal of Automated Reasoning\u00a015, 167\u2013215 (1995)","journal-title":"Induction and Recursion, Journal of Automated Reasoning"},{"key":"18_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A. Quaife","year":"1992","unstructured":"Quaife, A.: Automated Deduction in von Neumann-Bernays-G\u00f6del Set Theory. Journal of Automated Reasoning\u00a08, 91\u2013147 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR20","unstructured":"Quaife, A.: Automated Development of Fundamental Mathematical Theories, Ph.D. thesis, Univ. of California at Berkeley. Kluwer Acad. Publishers, Dordrecht (1992)"},{"key":"18_CR21","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1023\/A:1006135322108","volume":"23","author":"T. Recio","year":"1999","unstructured":"Recio, T., V\u00e9lez, M.P.: Automatic Discovery of Theorems in Elementary Geometry. Journal of Automated Reasoning\u00a023, 63\u201382 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR22","unstructured":"Rubin, J.E.: Set Theory for the Mathematician. Holden-Day, San Francisco (1967)"},{"key":"18_CR23","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1145\/44483.44484","volume":"35","author":"N. Shankar","year":"1988","unstructured":"Shankar, N.: A mechanical proof of the Church-Rosser theorem. Journal of the Association for Computing Machinery\u00a035, 475\u2013522 (1988)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"18_CR24","unstructured":"Wiedijk, F., \n                      http:\/\/www.cs.kun.nl\/~freek\/notes\/"},{"key":"18_CR25","doi-asserted-by":"publisher","DOI":"10.1142\/9789812817952","volume-title":"A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning","author":"L. Wos","year":"1999","unstructured":"Wos, L., Pieper, G.W.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning. World Scientific, Singapore (1999)"},{"key":"18_CR26","unstructured":"Wolfram, S.: The Mathematica\n                    TM\n                   Book, Wolfram Media Inc., Champaign, Illinois (1996)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T21:22:20Z","timestamp":1676668940000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}