{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:24:40Z","timestamp":1753889080483,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"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 present a complete superposition calculus for first-order logic with an interpreted Boolean type. Our motivation is to lay the foundation for refutationally complete calculi in more expressive logics with Booleans, such as higher-order logic, and to make superposition work efficiently on problems that would be obfuscated when using clausification as preprocessing. Working directly on formulas, our calculus avoids the costly axiomatic encoding of the theory of Booleans into first-order logic and offers various ways to interleave clausification with other derivation steps. We evaluate our calculus using the Zipperposition theorem prover, and observe that, with no tuning of parameters, our approach is on a par with the state-of-the-art approach.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_22","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"378-395","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Superposition with First-class Booleans and Inprocessing Clausification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0078-790X","authenticated-orcid":false,"given":"Visa","family":"Nummelin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7158-3595","authenticated-orcid":false,"given":"Alexander","family":"Bentkamp","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":"22_CR1","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Harald Ganzinger. Non-clausal resolution and superposition with selection and redundancy criteria. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning (LPAR\u201992), volume 624 of LNCS, pages 273\u2013284. Springer, 1992.","DOI":"10.1007\/BFb0013068"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Harald Ganzinger. 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":"22_CR3","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In John\u00a0Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume\u00a0I, pages 19\u201399. Elsevier and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Leo Bachmair, Harald Ganzinger, David\u00a0A. McAllester, and Christopher Lynch. Resolution theorem proving. In Handbook of Automated Reasoning, pages 19\u201399. Elsevier and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"22_CR5","unstructured":"Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org."},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Peter Baumgartner and Uwe Waldmann. Hierarchic superposition with weak abstraction. In Maria\u00a0Paola Bonacina, editor, CADE-24, volume 7898 of LNCS, pages 39\u201357. Springer, 2013.","DOI":"10.1007\/978-3-642-38574-2_3"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Dan Benanav. Simultaneous paramodulation. In Mark\u00a0E. Stickel, editor, CADE-10, volume 449 of LNCS, pages 442\u2013455. Springer, 1990.","DOI":"10.1007\/3-540-52885-7_106"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirovi\u0107. Superposition for full higher-order logic. In Andr\u00e9 Platzer and Geoff Sutcliffe, editors, CADE-28, LNCS. Springer, 2021.","DOI":"10.1007\/978-3-319-94205-6_3"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Christoph Benzm\u00fcller. Extensional higher-order paramodulation and RUE-resolution. In Harald Ganzinger, editor, CADE-16, volume 1632 of LNCS, pages 399\u2013413. Springer, 1999.","DOI":"10.1007\/3-540-48660-7_39"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Jasmin\u00a0Christian Blanchette, Nicolas Peltier, and Simon Robillard. Superposition with datatypes and codatatypes. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, IJCAR 2018, volume 10900 of LNCS, pages 370\u2013387. Springer, 2018.","DOI":"10.1007\/978-3-319-94205-6_25"},{"key":"22_CR11","unstructured":"Simon Cruanes. Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. Ph.D. thesis, \u00c9cole polytechnique, 2015."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. Why3\u2014where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, European Symposium on Programming (ESOP 2013), volume 7792 of LNCS, pages 125\u2013128. Springer, 2013.","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Harald Ganzinger and J\u00fcrgen Stuber. Superposition with equivalence reasoning and delayed clause normal form transformation. Inf. Comput., 199(1-2):3\u201323, 2005.","DOI":"10.1016\/j.ic.2004.10.010"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Thomas Hillenbrand and Christoph Weidenbach. Superposition for bounded domains. In Maria\u00a0Paola Bonacina and Mark\u00a0E. Stickel, editors, Automated Reasoning and Mathematics, volume 7788 of LNCS, pages 68\u2013100. Springer, 2013.","DOI":"10.1007\/978-3-642-36675-8_4"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"D.\u00a0E. Knuth and P.\u00a0B. Bendix. Simple word problems in universal algebras. In J.\u00a0Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"22_CR16","unstructured":"Evgenii Kotelnikov, Laura Kov\u00e1cs, Martin Suda, and Andrei Voronkov. A clausal normal form translation for FOOL. In Christoph Benzm\u00fcller, Geoff Sutcliffe, and Ra\u00fal Rojas, editors, Global Conference on Artificial Intelligence (GCAI 2016), volume\u00a041 of EPiC, pages 53\u201371. EasyChair, 2016."},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Evgenii Kotelnikov, Laura Kov\u00e1cs, and Andrei Voronkov. A first class Boolean sort in first-order theorem proving and TPTP. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics (CICM 2015), volume 9150 of LNCS, pages 71\u201386. Springer, 2015.","DOI":"10.1007\/978-3-319-20615-8_5"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Laura Kov\u00e1cs and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification (CAV 2013), volume 8044 of LNCS, pages 1\u201335. Springer, 2013.","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Michel Ludwig and Uwe Waldmann. An extension of the Knuth-Bendix ordering with LPO-like properties. In Nachum Dershowitz and Andrei Voronkov, editors, Logic Programming and Automated Reasoning (LPAR 2007), volume 4790 of LNCS, pages 348\u2013362. Springer, 2007.","DOI":"10.1007\/978-3-540-75560-9_26"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Zohar Manna and Richard\u00a0J. Waldinger. A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst., 2(1):90\u2013121, 1980.","DOI":"10.1145\/357084.357090"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Neil\u00a0V. Murray. Completely non-clausal theorem proving. Artif. Intell., 18(1):67\u201385, 1982.","DOI":"10.1016\/0004-3702(82)90011-X"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM, 53(6):937\u2013977, 2006.","DOI":"10.1145\/1217856.1217859"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Robert Nieuwenhuis and Albert Rubio. Basic superposition is complete. In Bernd Krieg-Br\u00fcckner, editor, European Symposium on Programming (ESOP \u201992), volume 582 of LNCS, pages 371\u2013389. Springer, 1992.","DOI":"10.1007\/3-540-55253-7_22"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Andreas Nonnengart and Christoph Weidenbach. Computing small clause normal forms. In Handbook of Automated Reasoning, pages 335\u2013367. Elsevier and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Visa Nummelin, Alexander Bentkamp, Sophie Tourret, and Petar Vukmirovi\u0107. Superposition with first-class Booleans and inprocessing clausification (technical report). Technical report, 2021. https:\/\/matryoshka-project.github.io\/pubs\/boolsup_report.pdf.","DOI":"10.1007\/978-3-030-79876-5_22"},{"key":"22_CR26","unstructured":"Martina Seidl, Florian Lonsing, and Armin Biere. qbf2epr: A tool for generating EPR formulas from QBF. In Pascal Fontaine, Renate\u00a0A. Schmidt, and Stephan Schulz, editors, Practical Aspects of Automated Reasoning (PAAR-2012), volume\u00a021 of EPiC Series in Computing, pages 139\u2013148. EasyChair, 2012."},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Alexander Steen. Extensional Paramodulation for Higher-order Logic and Its Effective Implementation Leo-III. Dissertationen zur k\u00fcnstlichen Intelligenz. Akademische Verlagsgesellschaft AKA GmbH, 2018.","DOI":"10.1007\/s13218-019-00628-8"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"Aaron Stump, Geoff Sutcliffe, and Cesare Tinelli. Starexec: A cross-community infrastructure for logic solving. In IJCAR 2014, volume 8562 of LNCS, pages 367\u2013373. Springer, 2014.","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Geoff Sutcliffe. 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":"22_CR30","unstructured":"Geoff Sutcliffe and Evgenii Kotelnikov. TFX: the TPTP extended typed first-order form. In Boris Konev, Josef Urban, and Philipp R\u00fcmmer, editors, Practical Aspects of Automated Reasoning (PAAR-2018), volume 2162 of CEUR Workshop Proceedings, pages 72\u201387. CEUR-WS.org, 2018."},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Grigori Tseitin. On the complexity of derivation in propositional calculus. In Automation of reasoning: Classical Papers on Computational Logic, volume\u00a02, pages 466\u2013483. Springer, 1983.","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Andrei Voronkov. AVATAR: the architecture for first-order theorem provers. In CAV 2014, volume 8559 of LNCS, pages 696\u2013710. Springer, 2014.","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"22_CR33","unstructured":"Petar Vukmirovi\u0107 and Visa Nummelin. Boolean reasoning in a higher-order superposition prover. In Pascal Fontaine, Konstantin Korovin, Ilias\u00a0S. Kotsireas, Philipp R\u00fcmmer, and Sophie Tourret, editors, Practical Aspects of Automated Reasoning (PAAR-2020), volume 2752 of CEUR Workshop Proceedings, pages 148\u2013166. CEUR-WS.org, 2020."},{"key":"22_CR34","unstructured":"Petar Vukmirovi\u0107, Jasmin Blanchette, Simon Cruanes, and Stephan Schulz. Extending a brainiac prover to lambda-free higher-order logic. Accepted in International Journal on Software Tools for Technology Transfer."},{"key":"22_CR35","doi-asserted-by":"crossref","unstructured":"Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. A comprehensive framework for saturation theorem proving. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, IJCAR 2020, LNCS. 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_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:29:05Z","timestamp":1672723745000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_22","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)"}}]}}