{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:48:38Z","timestamp":1767926918177,"version":"3.49.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,6,7]],"date-time":"2022-06-07T00:00:00Z","timestamp":1654560000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,6,7]],"date-time":"2022-06-07T00:00:00Z","timestamp":1654560000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"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\/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":[[2022,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but the standard notion of redundancy is too weak: A clause <jats:italic>C<\/jats:italic> does not make an instance <jats:inline-formula><jats:alternatives><jats:tex-math>$$C\\sigma $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>C<\/mml:mi>\n                    <mml:mi>\u03c3<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> redundant. We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution and superposition. The framework modularly extends redundancy criteria derived via a familiar ground-to-nonground lifting. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures so that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus within, for instance, an Otter or DISCOUNT loop. Our framework is mechanized in Isabelle\/HOL.<\/jats:p>","DOI":"10.1007\/s10817-022-09621-7","type":"journal-article","created":{"date-parts":[[2022,6,7]],"date-time":"2022-06-07T10:03:19Z","timestamp":1654596199000},"page":"499-539","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Comprehensive Framework for Saturation Theorem Proving"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0676-7195","authenticated-orcid":false,"given":"Uwe","family":"Waldmann","sequence":"first","affiliation":[]},{"given":"Sophie","family":"Tourret","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Robillard","sequence":"additional","affiliation":[]},{"given":"Jasmin","family":"Blanchette","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,6,7]]},"reference":[{"key":"9621_CR1","doi-asserted-by":"crossref","unstructured":"Avenhaus, J., Denzinger, J., Fuchs, M.: DISCOUNT: a system for distributed equational deduction. In: Hsiang, J. (ed.) RTA-95. LNCS, pp. 397\u2013402. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-59200-8_72"},{"key":"9621_CR2","first-page":"1","volume-title":"Rewriting Techniques-Resolution of Equations in Algebraic Structures","author":"L Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: A\u00eft-Kaci, H., Nivat, M. (eds.) Rewriting Techniques-Resolution of Equations in Algebraic Structures, vol. 2, pp. 1\u201330. Academic Press, Boston (1989)"},{"key":"9621_CR3","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M.E. (ed.) CADE-10. LNCS, vol. 449, pp. 427\u2013441. Springer, Heidelberg (1990)","DOI":"10.1007\/3-540-52885-7_105"},{"key":"9621_CR4","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Associative-commutative superposition. In: Dershowitz, N., Lindenstrauss, N. (eds.) CTRS-94. LNCS, pp. 1\u201314. Springer, Heidelberg (1994)","DOI":"10.1007\/3-540-60381-6_1"},{"issue":"3","key":"9621_CR5","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":"9621_CR6","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, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 19\u201399. Elsevier and MIT Press, Cambridge (2001)"},{"key":"9621_CR7","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a desision procedure for the monadic class with equality. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC \u201993. LNCS, vol. 713, pp. 83\u201396. Springer, Heidelberg (1993)","DOI":"10.1007\/BFb0022557"},{"key":"9621_CR8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"issue":"2","key":"9621_CR9","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: A module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reason."},{"key":"9621_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-030-22102-7_2","volume-title":"Description Logic, Theory Combination, and All That-Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday","author":"P Baumgartner","year":"2019","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition revisited. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A., Wolter, F. (eds.) Description Logic, Theory Combination, and All That-Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday. LNCS, vol. 11560, pp. 15\u201356. Springer, Heidelberg (2019)"},{"key":"9621_CR11","series-title":"LNCS","first-page":"442","volume-title":"CADE-10","author":"D Benanav","year":"1990","unstructured":"Benanav, D.: Simultaneous paramodulation. In: Stickel, M.E. (ed.) CADE-10. LNCS, vol. 449, pp. 442\u2013455. Springer, Heidelberg (1990)"},{"key":"9621_CR12","unstructured":"Bentkamp, A., Blanchette, J., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. Log. Meth. Comput. Sci. 17(2) (2021)"},{"key":"9621_CR13","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P.: Superposition for full higher-order logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28. LNCS, pp. 396\u2013412. Springer, Heidelberg (2021)","DOI":"10.1007\/978-3-030-79876-5_23"},{"key":"9621_CR14","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P., Waldmann, U.: Superposition with lambdas. J. Autom. Reason. 65(7), 893\u2013940 (2021)","DOI":"10.1007\/s10817-021-09595-y"},{"key":"9621_CR15","unstructured":"Bhayat, A.: Automated theorem proving in higher-order logic. Ph.D. thesis, University of Manchester (2021)"},{"key":"9621_CR16","unstructured":"Blanchette, J., Tourret, S.: Extensions to the comprehensive framework for saturation theorem proving. Archive of Formal Proofs 2021 (2021). https:\/\/www.isa-afp.org\/entries\/Saturation_Framework_Extensions.html"},{"key":"9621_CR17","first-page":"1","volume-title":"CPP 2019","author":"JC Blanchette","year":"2019","unstructured":"Blanchette, J.C.: Formalizing the metatheory of logical calculi and automatic provers in Isabelle\/HOL (invited talk). In: Mahboubi, A., Myreen, M.O. (eds.) CPP 2019, pp. 1\u201313. ACM, New York (2019)"},{"key":"9621_CR18","series-title":"LNCS","first-page":"93","volume-title":"ITP 2014","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Heidelberg (2014)"},{"key":"9621_CR19","series-title":"LNCS","first-page":"370","volume-title":"IJCAR 2018","author":"JC Blanchette","year":"2018","unstructured":"Blanchette, J.C., Peltier, N., Robillard, S.: Superposition with datatypes and codatatypes. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS, vol. 10900, pp. 370\u2013387. Springer, Heidelberg (2018)"},{"key":"9621_CR20","doi-asserted-by":"crossref","unstructured":"Duarte, A., Korovin, K.: Implementing superposition in iProver (system description). In: IJCAR (2). LNCS, vol. 12167, pp. 388\u2013397. Springer, Heidelberg (2020)","DOI":"10.1007\/978-3-030-51054-1_24"},{"key":"9621_CR21","doi-asserted-by":"crossref","unstructured":"Ebner, G., Blanchette, J., Tourret, S.: A unifying splitting framework. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28. LNCS, vol. 12699, pp. 344\u2013360. Springer, Heidelberg (2021)","DOI":"10.1007\/978-3-030-79876-5_20"},{"issue":"1\u20132","key":"9621_CR22","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10472-009-9150-9","volume":"55","author":"A Fietzke","year":"2009","unstructured":"Fietzke, A., Weidenbach, C.: Labelled splitting. Ann. Math. Artif. Intell. 55(1\u20132), 3\u201334 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1\u20132","key":"9621_CR23","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. Information and Computation 199(1\u20132), 3\u201323 (2005)","journal-title":"Information and Computation"},{"key":"9621_CR24","series-title":"LNCS","first-page":"486","volume-title":"CADE-18","author":"T Hillenbrand","year":"2002","unstructured":"Hillenbrand, T., L\u00f6chner, B.: The next Waldmeister loop. In: Voronkov, A. (ed.) CADE-18. LNCS, vol. 2392, pp. 486\u2013500. Springer, Heidelberg (2002)"},{"key":"9621_CR25","unstructured":"Huet, G.P.: A mechanization of type theory. In: Nilsson, N.J. (ed.) IJCAI-73, pp. 139\u2013146. William Kaufmann, San Mateo (1973)"},{"key":"9621_CR26","series-title":"LNCS","first-page":"129","volume-title":"TACAS 2010","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"9621_CR27","series-title":"LNCS","first-page":"1","volume-title":"CAV 2013","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013)"},{"issue":"2","key":"9621_CR28","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"W McCune","year":"1997","unstructured":"McCune, W., Wos, L.: Otter\u2014the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211\u2013220 (1997)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9621_CR29","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering and equality constrained clauses. J. Symb. Comput. 19(4), 321\u2013351 (1995)","journal-title":"J. Symb. Comput."},{"key":"9621_CR30","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 371\u2013443. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"9621_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, Heidelberg (2014)"},{"key":"9621_CR32","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"9621_CR33","series-title":"LNCS","first-page":"378","volume-title":"CADE-28","author":"V Nummelin","year":"2021","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, vol. 12699, pp. 378\u2013395. Springer, Heidelberg (2021)"},{"key":"9621_CR34","unstructured":"Peltier, N.: A variant of the superposition calculus. Archive of Formal Proofs 2016, (2016). https:\/\/www.isa-afp.org\/entries\/SuperCalc.shtml"},{"issue":"1","key":"9621_CR35","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"7","key":"9621_CR36","doi-asserted-by":"publisher","first-page":"1169","DOI":"10.1007\/s10817-020-09561-0","volume":"64","author":"A Schlichtkrull","year":"2020","unstructured":"Schlichtkrull, A., Blanchette, J., Traytel, D., Waldmann, U.: Formalizing Bachmair and Ganzinger\u2019s ordered resolution prover. J. Autom. Reason. 64(7), 1169\u20131195 (2020)","journal-title":"J. Autom. Reason."},{"key":"9621_CR37","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1145\/3293880.3294100","volume-title":"CPP 2019","author":"A Schlichtkrull","year":"2019","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D.: A verified prover based on ordered resolution. In: Mahboubi, A., Myreen, M.O. (eds.) CPP 2019, pp. 152\u2013165. ACM, New York (2019)"},{"key":"9621_CR38","doi-asserted-by":"crossref","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalization of Bachmair and Ganzinger\u2019s ordered resolution prover. Archive of Formal Proofs, vol. 2018, (2018). https:\/\/www.isa-afp.org\/entries\/Ordered_Resolution_Prover.html","DOI":"10.29007\/pn71"},{"issue":"2\u20133","key":"9621_CR39","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E\u2014a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9621_CR40","unstructured":"Tourret, S.: A comprehensive framework for saturation theorem proving. Archive of Formal Proofs vol. 2020 (2020). https:\/\/www.isa-afp.org\/entries\/Saturation_Framework.shtml"},{"key":"9621_CR41","first-page":"224","volume-title":"CPP 2021","author":"S Tourret","year":"2021","unstructured":"Tourret, S., Blanchette, J.: A modular Isabelle framework for verifying saturation provers. In: Hri\u0163cu, C., Popescu, A. (eds.) CPP 2021, pp. 224\u2013237. ACM, New York (2021)"},{"key":"9621_CR42","series-title":"LNCS","first-page":"696","volume-title":"CAV 2014","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Heidelberg (2014)"},{"key":"9621_CR43","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, P., Blanchette, J., Heule, M.J.: SAT-inspired eliminations for superposition. In: FMCAD 2021, pp. 231\u2013240. IEEE (2021)","DOI":"10.1145\/3565366"},{"key":"9621_CR44","doi-asserted-by":"crossref","unstructured":"Waldmann, U.: Cancellative abelian monoids and related structures in refutational theorem proving (part I). J. Symb. Comput. 33(6), 777\u2013829 (2002)","DOI":"10.1006\/jsco.2002.0536"},{"key":"9621_CR45","series-title":"LNCS","first-page":"316","volume-title":"IJCAR 2020, Part I","author":"U Waldmann","year":"2020","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, Heidelberg (2020)"},{"key":"9621_CR46","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning","author":"C Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, pp. 1965\u20132013. Elsevier and MIT Press, Cambridge (2001)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09621-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09621-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09621-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,5]],"date-time":"2022-11-05T11:16:06Z","timestamp":1667646966000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09621-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,7]]},"references-count":46,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9621"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09621-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6,7]]},"assertion":[{"value":"28 May 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 March 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 June 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}