{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:10:22Z","timestamp":1759846222630,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:00:00Z","timestamp":1759881600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:00:00Z","timestamp":1759881600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-07021-0_1","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:40:24Z","timestamp":1759844424000},"page":"3-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Hammering Higher Order Set Theory"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-6059","authenticated-orcid":false,"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1384-1613","authenticated-orcid":false,"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,8]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Haniel Barbosa, Clark\u00a0W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 415\u2013442. Springer, 2022. https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24 .","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann. Superposition for lambda-free higher-order logic. Log. Methods Comput. Sci., 17(2), 2021. URL: https:\/\/lmcs.episciences.org\/7349.","DOI":"10.23638\/LMCS-17(2:1)2021"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Christoph Benzm\u00fcller, Florian Rabe, and Geoff Sutcliffe. THF0 - the core of the TPTP language for higher-order logic. In IJCAR 2008, volume 5195 of LNCS, pages 491\u2013506. Springer, 2008.","DOI":"10.1007\/978-3-540-71070-7_41"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Ahmed Bhayat and Martin Suda. A higher-order vampire (short paper). In Christoph Benzm\u00fcller, Marijn J.\u00a0H. Heule, and Renate\u00a0A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 75\u201385. Springer, 2024. https:\/\/doi.org\/10.1007\/978-3-031-63498-7_5 .","DOI":"10.1007\/978-3-031-63498-7_5"},{"key":"1_CR5","unstructured":"Jasmin\u00a0Christian Blanchette. Automatic Proofs and Refutations for Higher-Order Logic. PhD thesis, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 2012."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Jasmin\u00a0Christian Blanchette, Sascha B\u00f6hme, and Lawrence\u00a0C. Paulson.Extending Sledgehammer with SMT solvers. In Nikolaj Bj\u00f8rner and Viorica Sofronie-Stokkermans, editors, CADE, volume 6803 of LNCS, pages 116\u2013130. Springer, 2011.","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Jasmin\u00a0Christian Blanchette, Sascha B\u00f6hme, Andrei Popescu, and Nicholas Smallbone. Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci., 12(4), 2016. https:\/\/doi.org\/10.2168\/LMCS-12(4:13) 2016 .","DOI":"10.2168\/LMCS-12(4:13)2016"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Jasmin\u00a0Christian Blanchette, Sascha B\u00f6hme, Andrei Popescu, and Nicholas Smallbone. Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci., 12(4), 2016. https:\/\/doi.org\/10.2168\/LMCS-12(4:13)2016 .","DOI":"10.2168\/LMCS-12(4:13)2016"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Jasmin\u00a0Christian Blanchette, Cezary Kaliszyk, Lawrence\u00a0C. Paulson, and Josef Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101\u2013148, 2016. URL: http:\/\/dx.doi.org\/10.6092\/issn.1972-5787\/4593, https:\/\/doi.org\/10.6092\/issn.1972-5787\/4593.","DOI":"10.6092\/issn.1972-5787\/4593"},{"issue":"3","key":"1_CR10","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s10817-015-9340-6","volume":"55","author":"CE Brown","year":"2015","unstructured":"Chad\u00a0E. Brown. Reconsidering Pairs and Functions as Sets. Journal of Automated Reasoning, 55(3):199\u2013210, Oct 2015.","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Chad\u00a0E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, and Josef Urban. GRUNGE: A grand unified ATP challenge. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, volume 11716 of Lecture Notes in Computer Science, pages 123\u2013141. Springer, 2019. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_8 .","DOI":"10.1007\/978-3-030-29436-6_8"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Chad\u00a0E. Brown and Cezary Kaliszyk. Lash 1.0 (system description). In Jasmin Blanchette, Laura Kov\u00e1cs, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 350\u2013358. Springer, 2022. https:\/\/doi.org\/10.1007\/978-3-031-10769-6_21.","DOI":"10.1007\/978-3-031-10769-6_21"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Chad\u00a0E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban. Proofgold: Blockchain for formal methods. In Zaynah Dargaye and Clara Schneidewind, editors, 4th International Workshop on Formal Methods for Blockchains, FMBC@CAV 2022, August 11, 2022, Haifa, Israel, volume 105 of OASIcs, pages 4:1\u20134:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2022. URL: https:\/\/doi.org\/10.4230\/OASIcs.FMBC.2022.4, https:\/\/doi.org\/10.4230\/OASICS.FMBC.2022.4 .","DOI":"10.4230\/OASICS.FMBC.2022.4"},{"key":"1_CR14","unstructured":"Chad\u00a0E. Brown, Cezary Kaliszyk, and Josef Urban. Payment channels with proofs. Available online., 2025. URL: http:\/\/grid01.ciirc.cvut.cz\/~mptp\/FMBC_2025_paper_6.pdf."},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Chad\u00a0E. Brown and Karol P\u0105k. A tale of two set theories. In Cezary Kaliszyk, Edwin\u00a0C. Brady, Andrea Kohlhase, and Claudio\u00a0Sacerdoti Coen, editors, Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings, volume 11617 of Lecture Notes in Computer Science, pages 44\u201360. Springer, 2019.","DOI":"10.1007\/978-3-030-23250-4_4"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Chad\u00a0E. Brown and Josef Urban. Extracting higher-order goals from the mizar mathematical library. In Michael Kohlhase, Moa Johansson, Bruce\u00a0R. Miller, Leonardo de\u00a0Moura, and Frank\u00a0Wm. Tompa, editors, Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings, volume 9791 of Lecture Notes in Computer Science, pages 99\u2013114. Springer, 2016. https:\/\/doi.org\/10.1007\/978-3-319-42547-4_8 .","DOI":"10.1007\/978-3-319-42547-4_8"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Mario Carneiro, Chad\u00a0E. Brown, and Josef Urban. Automated theorem proving for Metamath. In Adam Naumowicz and Ren\u00e9 Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bia\u0142ystok, Poland, volume 268 of LIPIcs, pages 9:1\u20139:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2023. URL: https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.9, https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.9.","DOI":"10.4230\/LIPICS.ITP.2023.9"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"John\u00a0H. Conway. On numbers and games, Second Edition. A K Peters, 2001.","DOI":"10.1201\/9781439864159"},{"key":"1_CR19","unstructured":"Marcos Cramer. The Naproche system: Proof-checking mathematical texts in controlled natural language.In Hermann C\u00f6lfen, Ulrich Schmitz, and Bernhard Schr\u00f6der, editors,Sprache und Datenverarbeitung, volume\u00a038, pages 9\u201333. Universit\u00e4tsverlag Rhein-Ruhr, Duisburg, 2014."},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Lukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for dependent type theory. J. Autom. Reasoning, 61(1-4):423\u2013453, 2018. https:\/\/doi.org\/10.1007\/s10817-018-9458-4.","DOI":"10.1007\/s10817-018-9458-4"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Ingo Dahn. Interpretation of a Mizar-like logic in first-order logic. In Ricardo Caferra and Gernot Salzer, editors, FTP (LNCS Selection), volume 1761 of LNCS, pages 137\u2013151. Springer, 1998.","DOI":"10.1007\/3-540-46508-1_9"},{"key":"1_CR22","unstructured":"The Dedukti logical framework. https:\/\/deducteam.github.io."},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, and Makarius Wenzel. Seventeen provers under the hammer. In June Andronick and Leonardo de\u00a0Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 8:1\u20138:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2022. URL: https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.8, https:\/\/doi.org\/10.4230\/LIPICS.ITP.2022.8.","DOI":"10.4230\/LIPICS.ITP.2022.8"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Certified Programs and Proofs (CPP\u201915), LNCS. Springer, 2015. http:\/\/dx.doi.org\/10.1145\/2676724.2693173. URL: http:\/\/dx.doi.org\/10.1145\/2676724.2693173, https:\/\/doi.org\/10.1145\/2676724.2693173.","DOI":"10.1145\/2676724.2693173"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Michael Gordon. Set theory, higher order logic or both? In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics, TPHOLs\u201996, volume 1125 of LNCS, pages 191\u2013201. Springer, 1996. https:\/\/doi.org\/10.1007\/BFb0105405","DOI":"10.1007\/BFb0105405"},{"key":"1_CR26","unstructured":"Joe Hurd. Integrating Gandalf and HOL. In Yves Bertot, Gilles Dowek, Andr\u00e9 Hirschowitz, C.\u00a0Paulin, and Laurent Th\u00e9ry, editors, TPHOLs, volume 1690 of LNCS, pages 311\u2013322. Springer, 1999."},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Joe Hurd. An LCF-style interface between HOL and first-order logic. In Andrei Voronkov, editor, CADE, volume 2392 of LNCS, pages 134\u2013138. Springer, 2002.","DOI":"10.1007\/3-540-45620-1_10"},{"key":"1_CR28","unstructured":"Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Myla Archer, Ben\u00a0Di Vito, and C\u00e9sar Mu\u00f1oz, editors, Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA 2003), number NASA\/CP-2003-212448 in NASA Technical Reports, pages 56\u201368, September 2003. URL: http:\/\/techreports.larc.nasa.gov\/ltrs\/PDF\/2003\/cp\/NASA-2003-cp212448.pdf."},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173\u2013213, 2014. https:\/\/doi.org\/10.1007\/s10817-014-9303-3 .","DOI":"10.1007\/s10817-014-9303-3"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173\u2013213, 2014. URL: http:\/\/dx.doi.org\/10.1007\/s10817-014-9303-3, https:\/\/doi.org\/10.1007\/s10817-014-9303-3.","DOI":"10.1007\/s10817-014-9303-3"},{"key":"1_CR31","unstructured":"Anja\u00a0Petkovi\u0107 Komel, Michael Rawson, and Martin Suda. Case study: Verified vampire proofs in the lambdapi-calculus modulo, 2025. URL: https:\/\/arxiv.org\/abs\/2503.15541, https:\/\/arxiv.org\/abs\/2503.15541."},{"key":"1_CR32","unstructured":"W.\u00a0McCune. Prover9 and mace4. http:\/\/www.cs.unm.edu\/~mccune\/prover9\/, 2005\u20132010."},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Jia Meng and Lawrence\u00a0C. Paulson. Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic, 7(1):41\u201357, 2009. Special Issue: Empirically Successful Computerized Reasoning. URL: https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1570868307000626, https:\/\/doi.org\/10.1016\/j.jal.2007.07.004.","DOI":"10.1016\/j.jal.2007.07.004"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"N. D. Goodman and J. Myhill. Choice Implies Excluded Middle. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 24:461, 1978.","DOI":"10.1002\/malq.19780242514"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"Karol Pak and Cezary Kaliszyk. Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia, volume 309 of LIPIcs, pages 29:1\u201329:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2024. URL: https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.29, https:\/\/doi.org\/10.4230\/LIPICS.ITP.2024.29.","DOI":"10.4230\/LIPICS.ITP.2024.29"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Lawrence\u00a0C. Paulson. Set theory for verification: I. from foundations to functions. Journal of Automated Reasoning, 11:353\u2013389, 1993.","DOI":"10.1007\/BF00881873"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Lawrence\u00a0C. Paulson. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Renate\u00a0A. Schmidt, Stephan Schulz, and Boris Konev, editors, Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, volume\u00a09 of EPiC, pages 1\u201310. EasyChair, 2010. URL: https:\/\/doi.org\/10.29007\/tnfd, https:\/\/doi.org\/10.29007\/TNFD.","DOI":"10.29007\/TNFD"},{"key":"1_CR38","unstructured":"Dag Prawitz. Natural deduction: a proof-theoretical study. Dover, 2006."},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"R. Diaconescu. Axiom of choice and complementation.Proceedings of the American Mathematical Society, 51:176\u2013178, 1975.","DOI":"10.1090\/S0002-9939-1975-0373893-X"},{"key":"1_CR40","unstructured":"Bertrand Russell. The Principles of Mathematics. Cambridge University Press, 1903."},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"J.\u00a0Urban. Translating Mizar for First Order Theorem Provers. In A.\u00a0Asperti, B.\u00a0Buchberger, and J.H. Davenport, editors, Proceedings of the 2nd International Conference on Mathematical Knowledge Management, number 2594 in LNCS, pages 203\u2013215. Springer, 2003.","DOI":"10.1007\/3-540-36469-2_16"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Josef Urban. MPTP \u2013 Motivation, Implementation, First Experiments. J. Autom. Reasoning, 33(3-4):319\u2013339, 2004. https:\/\/doi.org\/10.1007\/s10817-004-6245-1.","DOI":"10.1007\/s10817-004-6245-1"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"Petar Vukmirovi\u0107, Jasmin Blanchette, and Stephan Schulz. Extending a high-performance prover to higher-order logic. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, volume 13994 of Lecture Notes in Computer Science, pages 111\u2013129. Springer, 2023. https:\/\/doi.org\/10.1007\/978-3-031-30820-8_10 .","DOI":"10.1007\/978-3-031-30820-8_10"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07021-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:40:31Z","timestamp":1759844431000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,8]]},"ISBN":["9783032070203","9783032070210"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,8]]},"assertion":[{"value":"8 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brasilia","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2025\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}