{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:56:26Z","timestamp":1781884586704,"version":"3.54.5"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Recently, it has been demonstrated that SCL(FOL) can simulate ground ordered resolution\u00a0[6]. We revisit this result and provide a new formal proof in Isabelle\/HOL. The existing pen-and-paper proof is monolithic and challenging to comprehend. In order to improve clarity, we develop an alternative proof structured as eleven (bi)simulation steps between the two calculi, transitioning from ordered resolution to SCL(FOL). A key simulation lemma ensures that, under certain conditions, one simulation direction can be automatically lifted to the other. Consequently, for each of the eleven steps, it suffices to establish only one direction of simulation. The complete proof is included in the \n\n\"Image missing\"\n                    \n                    .\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_17","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:40Z","timestamp":1753789660000},"page":"302-322","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-2190","authenticated-orcid":false,"given":"Martin","family":"Bromberger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1830-7532","authenticated-orcid":false,"given":"Martin","family":"Desharnais","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6002-0458","authenticated-orcid":false,"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994). ISSN: 0955-792X. https:\/\/doi.org\/10.1093\/logcom\/4.3.217","DOI":"10.1093\/logcom\/4.3.217"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-61551-2_65","volume-title":"Principles and Practice of Constraint Programming \u2014 CP96","author":"RJ Bayardo","year":"1996","unstructured":"Bayardo, R.J., Schrag, R.: Using CSP look-back techniques to solve exceptionally hard SAT instances. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 46\u201360. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61551-2_65"},{"key":"17_CR3","doi-asserted-by":"publisher","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.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2019, Cascais, Portugal, 14 January 2019\u201315 January 2019, pp. 1\u201313. Association for Computing Machinery, 14 January 2019. ISBN: 978-1-4503-6222-1. https:\/\/doi.org\/10.1145\/3293880.3294087. The IsaFoL (Isabelle Formalization of Logic) repository is hosted at https:\/\/github.com\/IsaFoL\/IsaFoL","DOI":"10.1145\/3293880.3294087"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Desharnais, M., Weidenbach, C.: An Isabelle\/HOL formalization of the SCL(FOL) calculus. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction \u2013 CADE 29. Proceedings of the 29th International Conference on Automated Deduction, CADE 2023. LNCS, Rome, Italy, 1 July 2023\u20134 July 2023, vol. 14132, pp. 116\u2013 133. Springer, Cham, 2 September 2023. ISBN: 978-3-031-38498-1. https:\/\/doi.org\/10.1007\/978-3-031-38499-8_7","DOI":"10.1007\/978-3-031-38499-8_7"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-030-67067-2_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Bromberger","year":"2021","unstructured":"Bromberger, M., Fiori, A., Weidenbach, C.: Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 511\u2013533. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_23"},{"key":"17_CR6","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Jain, C., Weidenbach, C.: SCL(FOL) can simulate non-redundant superposition clause learning. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction \u2013 CADE 29. Proceedings of the 29th International Conference on Automated Deduction. CADE 2023. LNCS, Rome, Italy, 1 July 2023\u20134 July 2023, vol. 14132, pp. 134\u2013152. Springer, Cham, 3 September 2023. ISBN: 978-3-031-38498-1. https:\/\/doi.org\/10.1007\/978-3-031-38499-8_8","DOI":"10.1007\/978-3-031-38499-8_8"},{"key":"17_CR7","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: Exploring partial models with SCL. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-Located with the 11th International Joint Conference on Automated Reasoning (FLoC\/IJCAR 2022), Haifa, Israel, 11\u201312 August 2022, vol. 3201. CEUR Workshop Proceedings. CEURWS.org (2022). http:\/\/ceur-ws.org\/Vol-3201\/paper5.pdf"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: SCL(FOL) Revisited (2023). https:\/\/doi.org\/10.48550\/arXiv.2302.05954. arXiv: 2302.05954 [cs.LO]","DOI":"10.48550\/arXiv.2302.05954"},{"key":"17_CR9","unstructured":"Desharnais, M.: A generic framework for verified compilers. Arch. Formal Proofs (2020). https:\/\/isa-afp.org\/entries\/VeriComp html. Formal proof development. ISSN: 2150-914x"},{"key":"17_CR10","unstructured":"Desharnais, M.: A formalization of the SCL(FOL) calculus: simple clause learning for first-order logic. Arch. Formal Proofs (2023). https:\/\/isa-afp.org\/entries\/Simple_Clause_Learning.html. Formal proof development. ISSN: 2150-914x"},{"key":"17_CR11","unstructured":"Desharnais, M.: SCL simulates nonredundant ground resolution. Arch. Formal Proofs (2024). https:\/\/isa-afp.org\/entries\/SCL_Simulates_Ground_Resolution.html. Formal proof development. ISSN: 2150-914x"},{"key":"17_CR12","unstructured":"Desharnais, M., Brunthaler, S.: A generic framework for verified compilers using Isabelle\/HOL\u2019s locales. In: Nipkow, T., Paulson, L., Wenzel, M. (eds.) Isabelle Workshop (2020). https:\/\/sketis.net\/isabelle\/isabelle-workshop-2020"},{"key":"17_CR13","unstructured":"Desharnais, M., Toth, B.: A modular formalization of superposition. Arch. Formal Proofs (2024). https:\/\/isaafp.org\/entries\/Superposition_Calculus.html. Formal proof development. ISSN: 2150-914x"},{"key":"17_CR14","doi-asserted-by":"publisher","unstructured":"Desharnais, M., Toth, B., Waldmann, U., Blanchette, J., Tourret, S.: A modular formalization of superposition in Isabelle\/HOL. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving. ITP 2024, Tbilisi, Georgia, 9 September 2024\u201314 September 2024. Leibniz International Proceedings in Informatics (LIPIcs), vol. 309, pp. 12:1\u201312:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 2 September 2024. ISBN: 978-3-95977-337-9. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.12","DOI":"10.4230\/LIPIcs.ITP.2024.12"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-030-29436-6_14","volume-title":"Automated Deduction \u2013 CADE 27","author":"A Fiori","year":"2019","unstructured":"Fiori, A., Weidenbach, C.: SCL clause learning from simple models. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 233\u2013249. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_14"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"Leidinger, H., Weidenbach, C.: SCL(EQ): SCL for first- order logic with equality. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022. LNCS, Haifa, Israel, 8\u201310 August 2022, Proceedings, vol. 13385, pp. 228\u2013247. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_14","DOI":"10.1007\/978-3-031-10769-6_14"},{"key":"17_CR18","doi-asserted-by":"publisher","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009). ISSN: 0168- 7433. https:\/\/doi.org\/10.1007\/s10817-009-9155-4","DOI":"10.1007\/s10817-009-9155-4"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Marques Silva, J.P., Sakallah, K.A.: GRASP-a new search algorithm for satisfiability. In: Proceedings of International Conference on Computer Aided Design, pp. 220\u2013227 (1996). https:\/\/doi.org\/10.1109\/ICCAD.996.569607","DOI":"10.1109\/ICCAD.996.569607"},{"key":"17_CR20","unstructured":"Peltier, N.: A variant of the superposition calculus. Arch. Formal Proofs (2016). https:\/\/www.isa-afp.org\/entries\/SuperCalc.html"},{"issue":"7","key":"17_CR21","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). https:\/\/doi.org\/10.1007\/s10817-020-09561-0","journal-title":"J. Autom. Reason."},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalization of Bachmair and Ganzinger\u2019s ordered resolution prover. Arch. Formal Proofs (2018). https:\/\/isa-afp.org\/entries\/Ordered_Resolution_Prover.html. Formal proof development. ISSN: 2150-914x","DOI":"10.29007\/pn71"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:27:08Z","timestamp":1781882828000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}