{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:00:37Z","timestamp":1759147237892,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030510534"},{"type":"electronic","value":"9783030510541"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-51054-1_13","type":"book-chapter","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T19:02:39Z","timestamp":1593457359000},"page":"221-235","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formalization of Forcing in Isabelle\/ZF"],"prefix":"10.1007","author":[{"given":"Emmanuel","family":"Gunther","sequence":"first","affiliation":[]},{"given":"Miguel","family":"Pagano","sequence":"additional","affiliation":[]},{"given":"Pedro","family":"S\u00e1nchez Terraf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,6,24]]},"reference":[{"unstructured":"Carneiro, M.: The type theory of Lean. Master\u2019s thesis, Carnegie Mellon University, April 2019. \nhttps:\/\/github.com\/digama0\/lean-type-theory\/releases\/tag\/v1.0","key":"13_CR1"},{"key":"13_CR2","series-title":"Annals of Mathematics Studies, no. 3","doi-asserted-by":"publisher","DOI":"10.1515\/9781400881635","volume-title":"The Consistency of the Continuum Hypothesis","author":"K G\u00f6del","year":"1940","unstructured":"G\u00f6del, K.: The Consistency of the Continuum Hypothesis. Annals of Mathematics Studies, no. 3. Princeton University Press, Princeton (1940)"},{"doi-asserted-by":"publisher","unstructured":"Gunther, E., Pagano, M., S\u00e1nchez Terraf, P.: First steps towards a formalization of forcing. In: Accattoli, B., Olarte, C. (eds.) Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2018, Fortaleza, Brazil, 26\u201328 September 2018. Electronic Notes in Theoretical Computer Science, vol. 344, pp. 119\u2013136. Elsevier (2018). \nhttps:\/\/doi.org\/10.1016\/j.entcs.2019.07.008","key":"13_CR3","DOI":"10.1016\/j.entcs.2019.07.008"},{"unstructured":"Gunther, E., Pagano, M., S\u00e1nchez Terraf, P.: Mechanization of separation in generic extensions. arXiv e-prints \narXiv:1901.03313\n\n, January 2019","key":"13_CR4"},{"doi-asserted-by":"publisher","unstructured":"Han, J.M., van Doorn, F.: A formalization of forcing and the unprovability of the continuum hypothesis. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 141, pp. 19:1\u201319:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2019). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.19","key":"13_CR5","DOI":"10.4230\/LIPIcs.ITP.2019.19"},{"doi-asserted-by":"publisher","unstructured":"Han, J.M., van Doorn, F.: A formal proof of the independence of the continuum hypothesis. In: Blanchette, J., Hritcu, C. (eds.) Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, 20\u201321 January 2020. ACM (2020). \nhttps:\/\/doi.org\/10.1145\/3372885","key":"13_CR6","DOI":"10.1145\/3372885"},{"key":"13_CR7","series-title":"Springer Monographs in Mathematics","volume-title":"Set Theory. The Millennium Edition","author":"T Jech","year":"2002","unstructured":"Jech, T.: Set Theory. The Millennium Edition. Springer Monographs in Mathematics, 3rd edn. Springer, Heidelberg (2002). Corrected fourth printing (2006)","edition":"3"},{"key":"13_CR8","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Set Theory: An Introduction to Independence Proofs","author":"K Kunen","year":"1980","unstructured":"Kunen, K.: Set Theory: An Introduction to Independence Proofs. Studies in Logic and the Foundations of Mathematics. Elsevier Science, Amsterdam (1980)"},{"key":"13_CR9","series-title":"Studies in Logic","volume-title":"Set Theory","author":"K Kunen","year":"2011","unstructured":"Kunen, K.: Set Theory. Studies in Logic, 2nd edn. College Publications, London (2011). Revised edition (2013)","edition":"2"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"unstructured":"Neeman, I.: Topics in set theory, forcing (2011). Course Lecture Notes \nhttps:\/\/bit.ly\/2ErcbmI","key":"13_CR11"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11921240_19","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"S Obua","year":"2006","unstructured":"Obua, S.: Partizan games in Isabelle\/HOLZF. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 272\u2013286. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11921240_19"},{"issue":"3","key":"13_CR13","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"LC Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363\u2013397 (1989). \nhttps:\/\/doi.org\/10.1007\/BF00248324","journal-title":"J. Autom. Reason."},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","year":"1994","unstructured":"Paulson, L.C. (ed.): Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994). \nhttps:\/\/doi.org\/10.1007\/BFb0030541"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1112\/S1461157000000449","volume":"6","author":"LC Paulson","year":"2003","unstructured":"Paulson, L.C.: The relative consistency of the axiom of choice mechanized using Isabelle\/ZF. LMS J. Comput. Math. 6, 198\u2013248 (2003). \nhttps:\/\/doi.org\/10.1112\/S1461157000000449","journal-title":"LMS J. Comput. Math."},{"unstructured":"Paulson, L.C.: Zermelo Fraenkel set theory in higher-order logic. Archive of Formal Proofs, October 2019. \nhttp:\/\/isa-afp.org\/entries\/ZFC_in_HOL.html\n\n. Formal proof development","key":"13_CR16"},{"issue":"3","key":"13_CR17","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/BF00283132","volume":"17","author":"LC Paulson","year":"1996","unstructured":"Paulson, L.C., Grabczewski, K.: Mechanizing set theory. J. Autom. Reason. 17(3), 291\u2013323 (1996). \nhttps:\/\/doi.org\/10.1007\/BF00283132","journal-title":"J. Autom. Reason."},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71067-7_7","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"2008","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33\u201338. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_7"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/BFb0014566","volume-title":"Theoretical Aspects of Computer Software","author":"B Werner","year":"1997","unstructured":"Werner, B.: Sets in types, types in sets. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 530\u2013546. Springer, Heidelberg (1997). \nhttps:\/\/doi.org\/10.1007\/BFb0014566"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51054-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T21:11:40Z","timestamp":1593465100000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-51054-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030510534","9783030510541"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51054-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"24 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ijcar2020.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"150","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.03","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7.38","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11 system descriptions are also included. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}