{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:29:10Z","timestamp":1725488950083},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_31","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"377-391","source":"Crossref","is-referenced-by-count":5,"title":["The Reflection Theorem: A Study in Meta-theoretic Reasoning"],"prefix":"10.1007","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"31_CR1","unstructured":"Grzegorz Bancerek. The reflection theorem. Journal of Formalized Mathematics, 2, 1990. http:\/\/megrez.mizar.org\/mirror\/JFM\/Vol2\/zf_refle.html ."},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Johan G. F. Belinfante. Computer proofs in G\u00f6del\u2019s class theory with equational definitions for composite and cross. Journal of Automated Reasoning, 22(3):311\u2013339, March 1999.","DOI":"10.1023\/A:1006050629424"},{"key":"31_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs\u2019 99","year":"1999","unstructured":"Yves Bertot, Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin, and Laurent Th\u00e9ry, editors. Theorem Proving in Higher Order Logics: TPHOLs\u2019 99, LNCS 1690. Springer, 1999."},{"key":"31_CR4","unstructured":"Frank R. Drake. Set Theory: An Introduction to Large Cardinals. North-Holland, 1974."},{"key":"31_CR5","unstructured":"Kurt G\u00f6del. The consistency of the axiom of choice and of the generalized continuum hypothesis with the axioms of set theory. In S. Feferman et al., editors, Kurt G\u00f6del: Collected Works, volume II. Oxford University Press, 1990. First published in 1940."},{"key":"31_CR6","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"G. P. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"31_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs\u2019 99","author":"F. Kamm\u00fcller","year":"1999","unstructured":"Florian Kamm\u00fcller, Markus Wenzel, and Lawrence C. Paulson. Locales: A sectioning concept for Isabelle. In Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin, and Laurent Th\u00e9ry, editors. Theorem Proving in Higher Order Logics: TPHOLs\u2019 99, LNCS 1690. Springer, 1999 Bertot et al. [3], pages 149\u2013165."},{"key":"31_CR8","unstructured":"Kenneth Kunen. Set Theory: An Introduction to Independence Proofs. North-Holland, 1980."},{"key":"31_CR9","unstructured":"Andrzej Mostowski. Constructible Sets with Applications. North-Holland, 1969."},{"issue":"3","key":"31_CR10","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L. C. Paulson","year":"1993","unstructured":"Lawrence C. Paulson. Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning, 11(3):353\u2013389, 1993.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"31_CR11","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L. C. Paulson","year":"1995","unstructured":"Lawrence C. Paulson. Set theory for verification: II. Induction and recursion. Journal of Automated Reasoning, 15(2):167\u2013215, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson and Krzysztof Grcabczewski. Mechanizing set theory: Cardinal arithmetic and the axiom of choice. Journal of Automated Reasoning, 17(3):291\u2013323, December 1996.","DOI":"10.1007\/BF00283132"},{"key":"31_CR13","unstructured":"The QED manifesto. http:\/\/www-unix.mcs.anl.gov\/qed\/ , 1995."},{"issue":"1","key":"31_CR14","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A. Quaife","year":"1992","unstructured":"Art Quaife. Automated deduction in von Neumann-Bernays-G\u00f6del set theory. Journal of Automated Reasoning, 8(1):91\u2013147, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"31_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs\u2019 97","author":"M. Wenzel","year":"1997","unstructured":"Markus Wenzel. Type classes and overloading in higher-order logic. In Elsa L. Gunter and Amy Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs\u2019 97, LNCS 1275, pages 307\u2013322. Springer, 1997."},{"key":"31_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs\u2019 99","author":"M. Wenzel","year":"1999","unstructured":"Markus Wenzel. Isar: A generic interpretative approach to readable formal proof documents. In Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin, and Laurent Th\u00e9ry, editors. Theorem Proving in Higher Order Logics: TPHOLs\u2019 99, LNCS 1690. Springer, 1999 Bertot et al. [3], pages 167\u2013183."},{"issue":"3","key":"31_CR17","doi-asserted-by":"publisher","first-page":"443","DOI":"10.2307\/2118559","volume":"141","author":"A. J. Wiles","year":"1995","unstructured":"Andrew J. Wiles. Modular elliptic curves and Fermat\u2019s Last Theorem. Annals of Mathematics, 141(3):443\u2013551, 1995.","journal-title":"Annals of Mathematics"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:56:15Z","timestamp":1556740575000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_31","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}