{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:39:40Z","timestamp":1725514780462},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540694052"},{"type":"electronic","value":"9783540694076"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69407-6_52","type":"book-chapter","created":{"date-parts":[[2008,6,10]],"date-time":"2008-06-10T09:39:35Z","timestamp":1213090775000},"page":"486-490","source":"Crossref","is-referenced-by-count":2,"title":["The Relative Consistency of the Axiom of Choice \u2014 Mechanized Using Isabelle\/ZF"],"prefix":"10.1007","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"3-4","key":"52_CR1","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1021966832558","volume":"29","author":"G. Bancerek","year":"2002","unstructured":"Bancerek, G., Rudnicki, P.: A compendium of continuous lattices in mizar. Journal of Automated Reasoning\u00a029(3-4), 189\u2013224 (2002)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"52_CR2","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(3), 341\u2013378 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"52_CR3","first-page":"33","volume-title":"Kurt G\u00f6del: Collected Works","author":"K. G\u00f6del.","year":"1990","unstructured":"G\u00f6del, K.: The consistency of the axiom of choice and of the generalized continuum hypothesis with the axioms of set theory. In: Feferman, S., et al. (eds.) Kurt G\u00f6del: Collected Works, vol.\u00a0II, pp. 33\u2013101. Oxford University Press, Oxford (1990); First published in 1940 by Princeton University Press"},{"key":"52_CR4","volume-title":"Set Theory: An Introduction to Independence Proofs","author":"K. Kunen","year":"1980","unstructured":"Kunen, K.: Set Theory: An Introduction to Independence Proofs. North-Holland, Amsterdam (1980)"},{"issue":"3","key":"52_CR5","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L.C. Paulson","year":"1993","unstructured":"Paulson, L.C.: Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning\u00a011(3), 353\u2013389 (1993)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"52_CR6","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. Journal of Automated Reasoning\u00a015(2), 167\u2013215 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"52_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/3-540-45620-1_31","volume-title":"Automated Deduction - CADE-18","author":"L.C. Paulson","year":"2002","unstructured":"Paulson, L.C.: The reflection theorem: A study in meta-theoretic reasoning. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 377\u2013391. Springer, Heidelberg (2002)"},{"key":"52_CR8","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1112\/S1461157000000449","volume":"6","author":"L.C. Paulson","year":"2003","unstructured":"Paulson, L.C.: The relative consistency of the axiom of choice \u2014 mechanized using Isabelle\/ZF. LMS Journal of Computation and Mathematics\u00a06, 198\u2013248 (2003), \n                  \n                    http:\/\/www.lms.ac.uk\/jcm\/6\/lms2003-001\/","journal-title":"LMS Journal of Computation and Mathematics"},{"issue":"1","key":"52_CR9","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(1), 91\u2013147 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"52_CR10","unstructured":"Urban, J.: Basic facts about inaccessible and measurable cardinals. Journal of Formalized Mathematics\u00a012 (2000), \n                  \n                    http:\/\/mizar.uwb.edu.pl\/JFM\/Vol12\/card_fil.html"}],"container-title":["Lecture Notes in Computer Science","Logic and Theory of Algorithms"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69407-6_52.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:38:40Z","timestamp":1620002320000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69407-6_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540694052","9783540694076"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69407-6_52","relation":{},"subject":[]}}