{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:18:24Z","timestamp":1753888704275,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03bb<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus\u2019s two predecessors, new challenges arise from the interplay between<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03bb<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_23","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"396-412","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Superposition for Full Higher-order Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7158-3595","authenticated-orcid":false,"given":"Alexander","family":"Bentkamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8367-0936","authenticated-orcid":false,"given":"Jasmin","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6070-796X","authenticated-orcid":false,"given":"Sophie","family":"Tourret","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7049-6847","authenticated-orcid":false,"given":"Petar","family":"Vukmirovi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Andrews, P.B.: On connections and higher-order logic. J. Autom. Reason. 5(3), 257\u2013291 (1989)","DOI":"10.1007\/BF00248320"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","DOI":"10.1093\/logcom\/4.3.217"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Benanav, D.: Simultaneous paramodulation. In: Stickel, M.E. (ed.) CADE-10. LNCS, vol.\u00a0449, pp. 442\u2013455. Springer (1990)","DOI":"10.1007\/3-540-52885-7_106"},{"key":"23_CR5","doi-asserted-by":"publisher","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P.: Superposition for full higher-order logic (supplementary material), https:\/\/doi.org\/10.5281\/zenodo.4534759","DOI":"10.5281\/zenodo.4534759"},{"key":"23_CR6","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P., Waldmann, U.: Superposition with lambdas, accepted in J. Autom. Reason. Preprint at https:\/\/arxiv.org\/abs\/2102.00453v1 (2021)"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS, vol. 10900, pp. 28\u201346. Springer (2018)","DOI":"10.1007\/978-3-319-94205-6_3"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J.C., Tourret, S., Vukmirovi\u0107, P.: Superposition for full higher-order logic (technical report). Technical report (2021), https:\/\/matryoshka-project.github.io\/pubs\/hosup_report.pdf","DOI":"10.1007\/978-3-030-79876-5_23"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II\u2014A cooperative automatic theorem prover for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol.\u00a05195, pp. 162\u2013170. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_14"},{"key":"23_CR10","unstructured":"Bhayat, A., Reger, G.: Set of support for higher-order reasoning. In: Konev, B., Urban, J., R\u00fcmmer, P. (eds.) PAAR-2018. CEUR Workshop Proceedings, vol.\u00a02162, pp. 2\u201316. CEUR-WS.org (2018)"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I. LNCS, vol. 12166, pp. 278\u2013296. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_16"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 107\u2013121. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Satallax: An automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 111\u2013117. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"23_CR14","unstructured":"Cruanes, S.: Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. Ph.D. thesis, \u00c9cole polytechnique (2015)"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Types, Tableaus, and G\u00f6del\u2019s God. Kluwer (2002)","DOI":"10.1007\/978-94-010-0411-4"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Information and Computation 199(1\u20132), 3\u201323 (2005)","DOI":"10.1016\/j.ic.2004.10.010"},{"key":"23_CR17","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press (1993)"},{"key":"23_CR18","unstructured":"Huet, G.P.: A mechanization of type theory. In: Nilsson, N.J. (ed.) IJCAI-73. pp. 139\u2013146. William Kaufmann (1973)"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Jensen, D.C., Pietrzykowski, T.: Mechanizing $$\\omega $$-order type theory through unification. Theor. Comput. Sci. 3(2), 123\u2013171 (1976)","DOI":"10.1016\/0304-3975(76)90021-9"},{"key":"23_CR20","unstructured":"Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: The TPTP typed higher-order form with rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR-2016. CEUR Workshop Proceedings, vol.\u00a01635, pp. 41\u201355. CEUR-WS.org (2016)"},{"key":"23_CR21","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Suda, M., Voronkov, A.: A clausal normal form translation for FOOL. In: Benzm\u00fcller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016. EPiC, vol.\u00a041, pp. 53\u201371. EasyChair (2016)"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) LPAR-14. LNCS, vol.\u00a04790, pp. 348\u2013362. Springer (2007)","DOI":"10.1007\/978-3-540-75560-9_26"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Nummelin, V., Bentkamp, A., Tourret, S., Vukmirovi\u0107, P.: Superposition with first-class Booleans and inprocessing clausification. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28. LNCS, Springer (2021)","DOI":"10.1007\/978-3-030-79876-5_22"},{"key":"23_CR24","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a\u00a0practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010. EPiC, vol.\u00a02, pp. 1\u201311. EasyChair (2012)"},{"key":"23_CR25","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2-3), 111\u2013126 (2002)"},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS, vol. 10900, pp. 108\u2013116. Springer (2018)","DOI":"10.1007\/978-3-319-94205-6_8"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure\u2014from CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28. LNCS, Springer (2021)","DOI":"10.1007\/978-3-030-79876-5_24"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Nummelin, V.: Efficient full higher-order unification. In: Ariola, Z.M. (ed.) FSCD 2020. LIPIcs, vol.\u00a0167, pp. 5:1\u20135:17. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik (2020)","DOI":"10.46298\/lmcs-17(4:18)2021"},{"key":"23_CR30","unstructured":"Vukmirovi\u0107, P., Nummelin, V.: Boolean reasoning in a higher-order superposition prover. In: PAAR-2020. CEUR Workshop Proceedings, vol.\u00a02752, pp. 148\u2013166. CEUR-WS.org (2020)"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I. LNCS, vol. 12166, pp. 316\u2013334. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_18"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:29:13Z","timestamp":1672723753000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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":"38% - 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","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":"5","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","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)"}}]}}