{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:08:18Z","timestamp":1750219698557,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2023,10,1]],"date-time":"2023-10-01T00:00:00Z","timestamp":1696118400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2023,10]]},"abstract":"<jats:p>Superposition is a highly successful proof calculus for reasoning about first-order logic with equality. We present \u03bb-superposition, which extends superposition to higher-order logic. Its design goals include soundness, completeness, efficiency, and gracefulness with respect to standard first-order superposition. The calculus is implemented in two automatic theorem provers: E and Zipper position. These provers regularly win trophies at the CADE ATP System Competition, confirming the calculus's applicability. This paper is a summary of research that took place between 2017 and 2022.<\/jats:p>","DOI":"10.1145\/3636362.3636367","type":"journal-article","created":{"date-parts":[[2023,12,4]],"date-time":"2023-12-04T17:07:49Z","timestamp":1701709669000},"page":"25-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Complete and Efficient Higher-Order Reasoning via Lambda-Superposition"],"prefix":"10.1145","volume":"10","author":[{"given":"Alexander","family":"Bentkamp","sequence":"first","affiliation":[{"name":"Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jasmin","family":"Blanchette","sequence":"additional","affiliation":[{"name":"Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Visa","family":"Nummelin","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, the Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sophie","family":"Tourret","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, Inria, LORIA, Nancy, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[{"name":"Max-Planck-Institut f\u00fcr Informatik, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,12,4]]},"reference":[{"volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"Andrews Peter B.","key":"e_1_2_1_1_1","unstructured":"Peter B. Andrews . 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof ( second ed.). Applied Logic, Vol . 27. Springer . Peter B. Andrews. 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (second ed.). Applied Logic, Vol. 27. Springer."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00252180"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.3.217"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9233-2"},{"key":"e_1_2_1_5_1","volume-title":"Cesare Tinelli, and Clark W. Barrett.","author":"Barbosa Haniel","year":"2019","unstructured":"Haniel Barbosa , Andrew Reynolds , Daniel El Ouraoui , Cesare Tinelli, and Clark W. Barrett. 2019 . Extending SMT solvers to higher-order logic. In CADE-27 (LNCS), Pascal Fontaine (Ed.), Vol. 11716 . Springer , 35--54. Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark W. Barrett. 2019. Extending SMT solvers to higher-order logic. In CADE-27 (LNCS), Pascal Fontaine (Ed.), Vol. 11716. Springer, 35--54."},{"key":"e_1_2_1_6_1","volume-title":"Uwe Waldmann, and Daniel Wand.","author":"Becker Heiko","year":"2017","unstructured":"Heiko Becker , Jasmin Christian Blanchette , Uwe Waldmann, and Daniel Wand. 2017 . A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. In CADE-26 (LNCS), Leonardo de Moura (Ed.), Vol. 10395 . Springer , 432--453. Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. 2017. A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. In CADE-26 (LNCS), Leonardo de Moura (Ed.), Vol. 10395. Springer, 432--453."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3557998"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-022-09649-9"},{"volume-title":"CADE-15 (LNCS), Claude Kirchner and H\u00e9l\u00e8ne Kirchner (Eds.)","author":"Benzm\u00fcller Christoph","key":"e_1_2_1_9_1","unstructured":"Christoph Benzm\u00fcller and Michael Kohlhase . 1998. Extensional Higher-Order Resolution . In CADE-15 (LNCS), Claude Kirchner and H\u00e9l\u00e8ne Kirchner (Eds.) , Vol. 1421 . Springer , 56--71. Christoph Benzm\u00fcller and Michael Kohlhase. 1998. Extensional Higher-Order Resolution. In CADE-15 (LNCS), Claude Kirchner and H\u00e9l\u00e8ne Kirchner (Eds.), Vol. 1421. Springer, 56--71."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9348-y"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Ahmed Bhayat Michael Rawson and Johannes Schoisswohl. 2023. Superposition with Delayed Unification. (2023).  Ahmed Bhayat Michael Rawson and Johannes Schoisswohl. 2023. Superposition with Delayed Unification. (2023).","DOI":"10.1007\/978-3-031-38499-8_2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_16"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_16"},{"key":"e_1_2_1_14_1","volume-title":"Satallax: An Automatic Higher-Order Prover. In IJCAR 2012 (LNCS), Bernhard Gramlich, Dale Miller, and Uli Sattler (Eds.)","volume":"7364","author":"Brown Chad E.","year":"2012","unstructured":"Chad E. Brown . 2012 . Satallax: An Automatic Higher-Order Prover. In IJCAR 2012 (LNCS), Bernhard Gramlich, Dale Miller, and Uli Sattler (Eds.) , Vol. 7364 . Springer, 111--117. Chad E. Brown. 2012. Satallax: An Automatic Higher-Order Prover. In IJCAR 2012 (LNCS), Bernhard Gramlich, Dale Miller, and Uli Sattler (Eds.), Vol. 7364. Springer, 111--117."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"volume-title":"CADE-28 (LNCS), Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.)","author":"de Moura Leonardo","key":"e_1_2_1_16_1","unstructured":"Leonardo de Moura and Sebastian Ullrich . 2021. The Lean 4 Theorem Prover and Programming Language . In CADE-28 (LNCS), Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.) , Vol. 12699 . Springer , 625--635. Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In CADE-28 (LNCS), Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.), Vol. 12699. Springer, 625--635."},{"key":"e_1_2_1_17_1","volume-title":"ITP 2022 (LIPIcs), June Andronick and Leonardo de Moura (Eds.)","volume":"237","author":"Desharnais Martin","year":"2022","unstructured":"Martin Desharnais , Petar Vukmirovi\u0107 , Jasmin Blanchette , and Makarius Wenzel . 2022 . Seventeen provers under the hammer . In ITP 2022 (LIPIcs), June Andronick and Leonardo de Moura (Eds.) , Vol. 237 . Schloss Dagstuhl---Leibniz-Zentrum f\u00fcr Informatik, 8:1--8:18. Martin Desharnais, Petar Vukmirovi\u0107, Jasmin Blanchette, and Makarius Wenzel. 2022. Seventeen provers under the hammer. In ITP 2022 (LIPIcs), June Andronick and Leonardo de Moura (Eds.), Vol. 237. Schloss Dagstuhl---Leibniz-Zentrum f\u00fcr Informatik, 8:1--8:18."},{"key":"e_1_2_1_18_1","volume-title":"HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon M. J. C.","year":"1993","unstructured":"M. J. C. Gordon and T. F. Melham (Eds.). 1993 . Introduction to HOL: A Theorem Proving Environment for Higher Order Logic . Cambridge University Press . M. J. C. Gordon and T. F. Melham (Eds.). 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press."},{"volume-title":"TPHOLs 2009 (LNCS)","author":"Harrison John","key":"e_1_2_1_19_1","unstructured":"John Harrison . 2009. HOL Light: An Overview . In TPHOLs 2009 (LNCS) , Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674 . Springer , 60--66. John Harrison. 2009. HOL Light: An Overview. In TPHOLs 2009 (LNCS), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674. Springer, 60--66."},{"volume-title":"IJCAI-73, Nils J","author":"Huet G\u00e9rard P.","key":"e_1_2_1_20_1","unstructured":"G\u00e9rard P. Huet . 1973. A Mechanization of Type Theory . In IJCAI-73, Nils J . Nilsson (Ed.). William Kaufmann , 139--146. G\u00e9rard P. Huet. 1973. A Mechanization of Type Theory. In IJCAI-73, Nils J. Nilsson (Ed.). William Kaufmann, 139--146."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"volume-title":"Two generalizations of the recursive path ordering. Unpublished manuscript","author":"Kamin Samuel","key":"e_1_2_1_22_1","unstructured":"Samuel Kamin and Jean-Jacques L\u00e9vy . 1980. Two generalizations of the recursive path ordering. Unpublished manuscript . University of Illinois. Samuel Kamin and Jean-Jacques L\u00e9vy. 1980. Two generalizations of the recursive path ordering. Unpublished manuscript. University of Illinois."},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"D. E. Knuth and P. B. Bendix. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra J. Leech (Ed.). Pergamon Press 263--297.  D. E. Knuth and P. B. Bendix. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra J. Leech (Ed.). Pergamon Press 263--297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"e_1_2_1_24_1","volume-title":"Higher-Order Tableaux. In TABLEAUX '95 (LNCS), Peter Baumgartner, Reiner H\u00e4hnle, and Joachim Posegga (Eds.)","volume":"918","author":"Kohlhase Michael","year":"1995","unstructured":"Michael Kohlhase . 1995 . Higher-Order Tableaux. In TABLEAUX '95 (LNCS), Peter Baumgartner, Reiner H\u00e4hnle, and Joachim Posegga (Eds.) , Vol. 918 . Springer, 294--309. Michael Kohlhase. 1995. Higher-Order Tableaux. In TABLEAUX '95 (LNCS), Peter Baumgartner, Reiner H\u00e4hnle, and Joachim Posegga (Eds.), Vol. 918. Springer, 294--309."},{"key":"e_1_2_1_25_1","volume-title":"HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux. In TPHOLs '98 (LNCS), Jim Grundy and Malcolm C","author":"Konrad Karsten","year":"1998","unstructured":"Karsten Konrad . 1998 . HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux. In TPHOLs '98 (LNCS), Jim Grundy and Malcolm C . Newey (Eds.), Vol. 1479 . Springer , 245--261. Karsten Konrad. 1998. HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux. In TPHOLs '98 (LNCS), Jim Grundy and Malcolm C. Newey (Eds.), Vol. 1479. Springer, 245--261."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_5"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_2_1_28_1","volume-title":"LNCS","volume":"2283","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2002 . Isabelle\/HOL: A Proof Assistant for Higher-Order Logic . LNCS , Vol. 2283 . Springer. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, Vol. 2283. Springer."},{"volume-title":"Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.).","author":"Nonnengart Andreas","key":"e_1_2_1_29_1","unstructured":"Andreas Nonnengart and Christoph Weidenbach . 2001. Computing Small Clause Normal Forms . In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Vol. I . Elsevier , 335--367. Andreas Nonnengart and Christoph Weidenbach. 2001. Computing Small Clause Normal Forms. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Vol. I. Elsevier, 335--367."},{"key":"e_1_2_1_30_1","volume-title":"Paulson and Jasmin Christian Blanchette","author":"Lawrence","year":"2012","unstructured":"Lawrence C. Paulson and Jasmin Christian Blanchette . 2012 . Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In IWIL-2010 (EPiC), Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska (Eds.), Vol. 2 . EasyChair , 1--11. Lawrence C. Paulson and Jasmin Christian Blanchette. 2012. Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In IWIL-2010 (EPiC), Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska (Eds.), Vol. 2. EasyChair, 1--11."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"volume-title":"Mechanizing higher order logic","author":"Robinson J. A.","key":"e_1_2_1_32_1","unstructured":"J. A. Robinson . 1969. Mechanizing higher order logic . In Machine Intelligence, B. Meltzer and D. Michie (Eds.). Vol. 4 . Edinburgh University Press , 151--170. J. A. Robinson. 1969. Mechanizing higher order logic. In Machine Intelligence, B. Meltzer and D. Michie (Eds.). Vol. 4. Edinburgh University Press, 151--170."},{"volume-title":"TPHOLs 2008 (LNCS), Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.)","author":"Slind Konrad","key":"e_1_2_1_33_1","unstructured":"Konrad Slind and Michael Norrish . 2008. A Brief Overview of HOL4 . In TPHOLs 2008 (LNCS), Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.) , Vol. 5170 . Springer , 28--32. Konrad Slind and Michael Norrish. 2008. A Brief Overview of HOL4. In TPHOLs 2008 (LNCS), Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.), Vol. 5170. Springer, 28--32."},{"key":"e_1_2_1_34_1","volume-title":"The Higher-Order Prover Leo-III. In IJCAR 2018 (LNCS), Didier Galmiche, Stephan Schulz, and Roberto Sebastiani (Eds.)","volume":"10900","author":"Steen Alexander","year":"2018","unstructured":"Alexander Steen and Christoph Benzm\u00fcller . 2018 . The Higher-Order Prover Leo-III. In IJCAR 2018 (LNCS), Didier Galmiche, Stephan Schulz, and Roberto Sebastiani (Eds.) , Vol. 10900 . Springer, 108--116. Alexander Steen and Christoph Benzm\u00fcller. 2018. The Higher-Order Prover Leo-III. In IJCAR 2018 (LNCS), Didier Galmiche, Stephan Schulz, and Roberto Sebastiani (Eds.), Vol. 10900. Springer, 108--116."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09588-x"},{"volume-title":"The Design and Evolution of C++","author":"Stroustrup Bjarne","key":"e_1_2_1_36_1","unstructured":"Bjarne Stroustrup . 1995. The Design and Evolution of C++ . Addison-Wesley . Bjarne Stroustrup. 1995. The Design and Evolution of C++. Addison-Wesley."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9407-7"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273733"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09613-z"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_10"}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636362.3636367","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3636362.3636367","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:35:41Z","timestamp":1750178141000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636362.3636367"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,10]]}},"alternative-id":["10.1145\/3636362.3636367"],"URL":"https:\/\/doi.org\/10.1145\/3636362.3636367","relation":{},"ISSN":["2372-3491"],"issn-type":[{"type":"electronic","value":"2372-3491"}],"subject":[],"published":{"date-parts":[[2023,10]]},"assertion":[{"value":"2023-12-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}