{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:21Z","timestamp":1776333381814,"version":"3.51.2"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,1,21]],"date-time":"2023-01-21T00:00:00Z","timestamp":1674259200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,21]],"date-time":"2023-01-21T00:00:00Z","timestamp":1674259200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["016.Vidi.189.037"],"award-info":[{"award-number":["016.Vidi.189.037"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,3]]},"DOI":"10.1007\/s10817-022-09649-9","type":"journal-article","created":{"date-parts":[[2023,1,21]],"date-time":"2023-01-21T05:02:56Z","timestamp":1674277376000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Superposition for Higher-Order Logic"],"prefix":"10.1007","volume":"67","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":[[2023,1,21]]},"reference":[{"issue":"3","key":"9649_CR1","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF00248320","volume":"5","author":"PB Andrews","year":"1989","unstructured":"Andrews, P.B.: On connections and higher-order logic. J. Autom. Reason. 5(3), 257\u2013291 (1989)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9649_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"key":"9649_CR3","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 19\u201399. MIT Press, Cambridge (2001)"},{"key":"9649_CR4","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: D.\u00a0Kapur (ed.) CADE-11, LNCS, vol. 607, pp. 462\u2013476. Springer (1992)","DOI":"10.1007\/3-540-55602-8_185"},{"key":"9649_CR5","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. 6806, pp. 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9649_CR6","doi-asserted-by":"crossref","unstructured":"Benanav, D.: Simultaneous paramodulation. In: M.E. Stickel (ed.) CADE-10, LNCS, vol. 449, pp. 442\u2013455. Springer (1990)","DOI":"10.1007\/3-540-52885-7_106"},{"key":"9649_CR7","doi-asserted-by":"crossref","unstructured":"Bentkamp, A.: Superposition for higher-order logic. Ph.D. thesis, Vrije Universiteit Amsterdam (2021)","DOI":"10.1007\/978-3-030-79876-5_23"},{"issue":"2","key":"9649_CR8","first-page":"1:1","volume":"17","author":"A Bentkamp","year":"2021","unstructured":"Bentkamp, A., Blanchette, J., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. Log. Meth. Comput. Sci. 17(2), 1:1-1:38 (2021)","journal-title":"Log. Meth. Comput. Sci."},{"key":"9649_CR9","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovic, P.: Superposition for full higher-order logic. In: A.\u00a0Platzer, G.\u00a0Sutcliffe (eds.) CADE-28, LNCS, vol. 12699, pp. 396\u2013412. Springer (2021)","DOI":"10.1007\/978-3-030-79876-5_23"},{"key":"9649_CR10","doi-asserted-by":"publisher","first-page":"893","DOI":"10.1007\/s10817-021-09595-y","volume":"65","author":"A Bentkamp","year":"2021","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P., Waldmann, U.: Superposition with lambdas. J. Autom. Reason. 65, 893\u2013940 (2021)","journal-title":"J. Autom. Reason."},{"key":"9649_CR11","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: A.\u00a0Armando, P.\u00a0Baumgartner, G.\u00a0Dowek (eds.) IJCAR 2008, LNCS, vol. 5195, pp. 162\u2013170. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_14"},{"key":"9649_CR12","unstructured":"Bhayat, A., Reger, G.: Set of support for higher-order reasoning. In: B.\u00a0Konev, J.\u00a0Urban, P.\u00a0R\u00fcmmer (eds.) PAAR-2018, CEUR Workshop Proceedings, vol. 2162, pp. 2\u201316. CEUR-WS.org (2018)"},{"key":"9649_CR13","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: N.\u00a0Peltier, V.\u00a0Sofronie-Stokkermans (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 278\u2013296. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_16"},{"issue":"4","key":"9649_CR14","doi-asserted-by":"publisher","first-page":"15","DOI":"10.2168\/LMCS-11(4:3)2015","volume":"11","author":"F Blanqui","year":"2015","unstructured":"Blanqui, F., Jouannaud, J.P., Rubio, A.: The computability path ordering. Log. Meth. Comput. Sci. 11(4), 15 (2015)","journal-title":"Log. Meth. Comput. Sci."},{"key":"9649_CR15","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: J.\u00a0Giesl, R.\u00a0H\u00e4hnle (eds.) IJCAR 2010, LNCS, vol. 6173, pp. 107\u2013121. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"9649_CR16","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Satallax: An automatic higher-order prover. In: B.\u00a0Gramlich, D.\u00a0Miller, U.\u00a0Sattler (eds.) IJCAR 2012, LNCS, vol. 7364, pp. 111\u2013117. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_11"},{"issue":"5","key":"9649_CR17","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1093\/logcom\/13.5.639","volume":"13","author":"I Cervesato","year":"2003","unstructured":"Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639\u2013688 (2003)","journal-title":"J. Log. Comput."},{"key":"9649_CR18","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Types, Tableaus, and G\u00f6del\u2019s God. Kluwer (2002)","DOI":"10.1007\/978-94-010-0411-4"},{"issue":"1\u20132","key":"9649_CR19","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.ic.2004.10.010","volume":"199","author":"H Ganzinger","year":"2005","unstructured":"Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Inform. Comput. 199(1\u20132), 3\u201323 (2005)","journal-title":"Inform. Comput."},{"key":"9649_CR20","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":"9649_CR21","unstructured":"Huet, G.P.: A mechanization of type theory. In: N.J. Nilsson (ed.) IJCAI-73, pp. 139\u2013146. William Kaufmann (1973)"},{"issue":"1","key":"9649_CR22","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"GP Huet","year":"1975","unstructured":"Huet, G.P.: A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1(1), 27\u201357 (1975)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"9649_CR23","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","volume":"3","author":"DC Jensen","year":"1976","unstructured":"Jensen, D.C., Pietrzykowski, T.: Mechanizing $$\\omega $$-order type theory through unification. Theor. Comput. Sci. 3(2), 123\u2013171 (1976)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"9649_CR24","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/S0304-3975(98)00078-4","volume":"208","author":"JP Jouannaud","year":"1998","unstructured":"Jouannaud, J.P., Rubio, A.: Rewrite orderings for higher-order terms in eta-long beta-normal form and recursive path ordering. Theor. Comput. Sci. 208(1\u20132), 33\u201358 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"9649_CR25","unstructured":"Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: The TPTP typed higher-order form with rank-1 polymorphism. In: P.\u00a0Fontaine, S.\u00a0Schulz, J.\u00a0Urban (eds.) PAAR-2016, CEUR Workshop Proceedings, vol. 1635, pp. 41\u201355. CEUR-WS.org (2016)"},{"issue":"3:2\u20133","key":"9649_CR26","first-page":"121","volume":"3499\/2009","author":"D K\u0151nig","year":"1927","unstructured":"K\u0151nig, D.: \u00dcber eine Schlussweise aus dem Endlichen ins Unendliche. Acta Sci. Math. (Szeged) 3499\/2009(3:2\u20133), 121\u2013130 (1927)","journal-title":"Acta Sci. Math. (Szeged)"},{"key":"9649_CR27","doi-asserted-by":"crossref","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Suda, M., Voronkov, A.: A clausal normal form translation for FOOL. In: C.\u00a0Benzm\u00fcller, G.\u00a0Sutcliffe, R.\u00a0Rojas (eds.) GCAI 2016, EPiC, vol.\u00a041, pp. 53\u201371. EasyChair (2016)","DOI":"10.29007\/ltkk"},{"key":"9649_CR28","doi-asserted-by":"crossref","unstructured":"Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: N.\u00a0Dershowitz, A.\u00a0Voronkov (eds.) LPAR-14, LNCS, vol. 4790, pp. 348\u2013362. Springer (2007)","DOI":"10.1007\/978-3-540-75560-9_26"},{"issue":"1","key":"9649_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theor. Comput. Sci. 192(1), 3\u201329 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"9649_CR30","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, pp. 335\u2013367. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"9649_CR31","unstructured":"Nummelin, V., Bentkamp, A., Tourret, S., Vukmirovi\u0107, P.: Superposition with first-class Booleans and inprocessing clausification (technical report). https:\/\/matryoshka-project.github.io\/pubs\/boolsup_report.pdf"},{"key":"9649_CR32","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a\u00a0practical link between automatic and interactive theorem provers. In: G.\u00a0Sutcliffe, S.\u00a0Schulz, E.\u00a0Ternovska (eds.) IWIL-2010, EPiC, vol.\u00a02, pp. 1\u201311. EasyChair (2012)","DOI":"10.29007\/36dt"},{"issue":"2\u20133","key":"9649_CR33","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E-a Brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9649_CR34","doi-asserted-by":"crossref","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: D.\u00a0Galmiche, S.\u00a0Schulz, R.\u00a0Sebastiani (eds.) IJCAR 2018, LNCS, vol. 10900, pp. 108\u2013116. Springer (2018)","DOI":"10.1007\/978-3-319-94205-6_8"},{"issue":"4","key":"9649_CR35","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","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)","journal-title":"Autom. Reason."},{"key":"9649_CR36","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Automation of reasoning: Classical Papers on Computational Logic, vol.\u00a02, pp. 466\u2013483. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"9649_CR37","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: A.\u00a0Platzer, G.\u00a0Sutcliffe (eds.) CADE-28, LNCS. Springer (2021)","DOI":"10.1007\/978-3-030-79876-5_24"},{"key":"9649_CR38","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Nummelin, V.: Efficient full higher-order unification. In: Z.M. Ariola (ed.) FSCD 2020, LIPIcs, vol. 167, pp. 5:1\u20135:17. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik (2020)","DOI":"10.46298\/lmcs-17(4:18)2021"},{"key":"9649_CR39","unstructured":"Vukmirovi\u0107, P., Nummelin, V.: Boolean reasoning in a higher-order superposition prover. In: PAAR-2020, CEUR Workshop Proceedings, vol. 2752, pp. 148\u2013166. CEUR-WS.org (2020)"},{"key":"9649_CR40","doi-asserted-by":"crossref","unstructured":"Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. In: N.\u00a0Peltier, V.\u00a0Sofronie-Stokkermans (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 316\u2013334. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_18"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09649-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09649-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09649-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T18:26:30Z","timestamp":1728757590000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09649-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,21]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["9649"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09649-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,21]]},"assertion":[{"value":"1 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 August 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 January 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"10"}}