{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:53:43Z","timestamp":1781927623592,"version":"3.54.5"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2023,6,30]],"date-time":"2023-06-30T00:00:00Z","timestamp":1688083200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,6,30]],"date-time":"2023-06-30T00:00:00Z","timestamp":1688083200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Max Planck Institute for Informatics"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose a new calculus SCL(EQ) for first-order logic with equality that only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal model assumption is used to guide inferences that are then guaranteed to be non-redundant. Redundancy is defined with respect to a dynamically changing ordering derived from the ground literal model assumption. We prove SCL(EQ) sound and complete and provide examples where our calculus improves on superposition.<\/jats:p>","DOI":"10.1007\/s10817-023-09673-3","type":"journal-article","created":{"date-parts":[[2023,6,30]],"date-time":"2023-06-30T16:02:10Z","timestamp":1688140930000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["SCL(EQ): SCL for First-Order Logic with Equality"],"prefix":"10.1007","volume":"67","author":[{"given":"Hendrik","family":"Leidinger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,6,30]]},"reference":[{"key":"9673_CR1","doi-asserted-by":"publisher","unstructured":"Alagi, G., Weidenbach, C.: NRCL - A model building approach to the Bernays-Sch\u00f6nfinkel fragment. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems\u201410th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21\u201324, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9322, pp. 69\u201384. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-24246-0_5 (2015)","DOI":"10.1007\/978-3-319-24246-0_5"},{"issue":"3","key":"9673_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). https:\/\/doi.org\/10.1093\/logcom\/4.3.217","journal-title":"J. Log. Comput."},{"key":"9673_CR3","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) Computational Logic and Proof Theory, Third Kurt G\u00f6del Colloquium. LNCS, vol. 713, pp. 83\u201396. Springer, Berlin. https:\/\/doi.org\/10.1007\/BFb0022557 (1993)","DOI":"10.1007\/BFb0022557"},{"key":"9673_CR4","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H., Voronkov, A.: Elimination of equality via transformation with ordering constraints. In: Kirchner, C., Kirchner, H. (eds.) International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 1421, pp. 175\u2013190. Springer, Berlin. https:\/\/doi.org\/10.1007\/BFb0054259 (1998)","DOI":"10.1007\/BFb0054259"},{"key":"9673_CR5","doi-asserted-by":"publisher","unstructured":"Baumgartner, P.: Hyper tableau\u2014the next generation. In: de Swart, H.C.M. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX \u201998, Oisterwijk, The Netherlands, May 5\u20138, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1397, pp. 60\u201376. Springer, Berlin. https:\/\/doi.org\/10.1007\/3-540-69778-0_14 (1998)","DOI":"10.1007\/3-540-69778-0_14"},{"key":"9673_CR6","doi-asserted-by":"publisher","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus with equality. In: Nieuwenhuis, R. (ed.) 20th International Conference on Automated Deduction. LNAI, vol. 3632, pp. 392\u2013408. Springer, Berlin. https:\/\/doi.org\/10.1007\/11532231_29 (2005)","DOI":"10.1007\/11532231_29"},{"key":"9673_CR7","doi-asserted-by":"publisher","unstructured":"Baumgartner, P., Waldmann, U.: Superposition and model evolution combined. In: Schmidt, R.A. (ed.) Automated Deduction\u2014CADE-22. LNAI, vol. 5663, pp. 17\u201334. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-642-02959-2_2 (2009)","DOI":"10.1007\/978-3-642-02959-2_2"},{"key":"9673_CR8","doi-asserted-by":"publisher","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma learning in the model evolution calculus. In: Hermann, M., Voronkov, A. (eds.) 13th International Conference, LPAR 2006. LNAI, vol. 4246, pp. 572\u2013586. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/11916277_39 (2006)","DOI":"10.1007\/11916277_39"},{"key":"9673_CR9","doi-asserted-by":"publisher","unstructured":"Baumgartner, P., Furbach, U., Pelzer, B.: Hyper tableaux with equality. In: Pfenning, F. (ed.) International Conference on Automated Deduction. LNAI, vol. 4603, pp. 492\u2013507. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-540-73595-3_36 (2007)","DOI":"10.1007\/978-3-540-73595-3_36"},{"issue":"9","key":"9673_CR10","doi-asserted-by":"publisher","first-page":"1011","DOI":"10.1016\/j.jsc.2011.12.031","volume":"47","author":"P Baumgartner","year":"2012","unstructured":"Baumgartner, P., Pelzer, B., Tinelli, C.: Model evolution with equality-revised and implemented. J. Symb. Comput. 47(9), 1011\u20131045 (2012). https:\/\/doi.org\/10.1016\/j.jsc.2011.12.031","journal-title":"J. Symb. Comput."},{"key":"9673_CR11","doi-asserted-by":"publisher","unstructured":"Bayardo, R.J., Schrag, R.: Using CSP look-back techniques to solve exceptionally hard SAT instances. In: Freuder, E.C. (ed.) Proceedings of the Second International Conference on Principles and Practice of Constraint Programming, Cambridge, Massachusetts, USA, August 19\u201322, 1996. LNCS, vol. 1118, pp. 46\u201360. Springer, Berlin. https:\/\/doi.org\/10.1007\/3-540-61551-2_65 (1996)","DOI":"10.1007\/3-540-61551-2_65"},{"key":"9673_CR12","volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"9673_CR13","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Schulz, S., Moura, L.D., Konev, B. (eds.) PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning. EPiC Series in Computing, vol. 31, pp. 25\u201338. EasyChair, Bramhall. https:\/\/doi.org\/10.29007\/m2vf (2015)","DOI":"10.29007\/m2vf"},{"key":"9673_CR14","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P., Furbach, U., Sofronie-Stokkermans, V.: In: Mart\u00ed-Oliet, N., \u00d6lveczky, P.C., Talcott, C. (eds.) On First-Order Model-Based Reasoning. LNAI, vol. 9200, pp. 181\u2013204. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-23165-5_8 (2015)","DOI":"10.1007\/978-3-319-23165-5_8"},{"key":"9673_CR15","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Fiori, A., Weidenbach, C.: Deciding the Bernays\u2013Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation\u201422nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17\u201319, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12597, pp. 511\u2013533. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-67067-2_23 (2021)","DOI":"10.1007\/978-3-030-67067-2_23"},{"key":"9673_CR16","unstructured":"Bromberger, M., Gehl, T., Leutgeb, L., Weidenbach, C.: A two-watched literal scheme for first-order logic. In: Boris\u00a0Konev, A.S. Claudia\u00a0Schon (ed.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC\/IJCAR 2022). CEUR Workshop Proceedings, vol. 3201. CEUR-WS.org, RWTH Aachen, Ahornstr. 55, 52056 Aachen (2022)"},{"key":"9673_CR17","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: SCL(FOL) Revisited. Preprint at http:\/\/arxiv.org\/2302.05954 (2023)"},{"issue":"3","key":"9673_CR18","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960). https:\/\/doi.org\/10.1145\/321033.321034","journal-title":"J. ACM"},{"issue":"7","key":"9673_CR19","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962). https:\/\/doi.org\/10.1145\/368273.368557","journal-title":"Commun. ACM"},{"key":"9673_CR20","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1016\/B978-044450813-3\/50011-4","volume-title":"Handbook of Automated Reasoning","author":"N Dershowitz","year":"2001","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 535\u2013610. Elsevier, Berlin (2001)"},{"key":"9673_CR21","doi-asserted-by":"publisher","unstructured":"Fiori, A., Weidenbach, C.: SCL clause learning from simple models. In: Fontaine, P. (ed.) 27th International Conference on Automated Deduction, CADE-27. LNAI, vol. 11716. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_14 (2019)","DOI":"10.1007\/978-3-030-29436-6_14"},{"issue":"1","key":"9673_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/138027.138032","volume":"40","author":"J Gallier","year":"1993","unstructured":"Gallier, J., Narendran, P., Plaisted, D., Raatz, S., Snyder, W.: An algorithm for finding canonical sets of ground rewrite rules in polynomial time. J. ACM 40(1), 1\u201316 (1993). https:\/\/doi.org\/10.1145\/138027.138032","journal-title":"J. ACM"},{"key":"9673_CR23","doi-asserted-by":"publisher","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: LICS, pp. 295\u2013304. https:\/\/doi.org\/10.1109\/LICS.1999.782624 (1999)","DOI":"10.1109\/LICS.1999.782624"},{"key":"9673_CR24","doi-asserted-by":"publisher","unstructured":"Gleiss, B., Kov\u00e1cs, L., Rath, J.: Subsumption demodulation in first-order theorem proving. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning\u201410th International Joint Conference, IJCAR 2020, Paris, France, July 1\u20134, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12166, pp. 297\u2013315. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-51074-9_17 (2020)","DOI":"10.1007\/978-3-030-51074-9_17"},{"key":"9673_CR25","doi-asserted-by":"publisher","unstructured":"Korovin, K.: In: Voronkov, A., Weidenbach, C. (eds.) Inst-Gen\u2014A Modular Approach to Instantiation-Based Automated Reasoning, pp. 239\u2013270. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-642-37651-1_10 (2013)","DOI":"10.1007\/978-3-642-37651-1_10"},{"key":"9673_CR26","doi-asserted-by":"publisher","unstructured":"Korovin, K., Sticksel, C.: iProver-Eq: An instantiation-based theorem prover with equality. In: Giesl, J., H\u00e4hnle, R. (eds.) 5th International Joint Conference, IJCAR 2010. LNAI, vol. 6173, pp. 196\u2013202. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-642-14203-1_17 (2010)","DOI":"10.1007\/978-3-642-14203-1_17"},{"key":"9673_CR27","doi-asserted-by":"publisher","unstructured":"Leidinger, H., and, C.W.: SCL(EQ): SCL for first-order logic with equality. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning\u201411th International Joint Conference, IJCAR 2022 Held as Part of the Federated Logic Conference, Haifa, Israel, August 8\u201310, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 228\u2013247. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-10769-6_14 (2022)","DOI":"10.1007\/978-3-031-10769-6_14"},{"key":"9673_CR28","doi-asserted-by":"publisher","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Design Automation Conference, 2001. Proceedings, pp. 530\u2013535. ACM, New York. https:\/\/doi.org\/10.1145\/378239.379017 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"9673_CR29","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980). https:\/\/doi.org\/10.1145\/322186.322198","journal-title":"J. ACM"},{"key":"9673_CR30","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving sat and sat modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to dpll(t). J. ACM 53, 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"3","key":"9673_CR31","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"DA Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered semantic hyper-linking. J. Autom. Reason. 25(3), 167\u2013217 (2000). https:\/\/doi.org\/10.1023\/A:1006376231563","journal-title":"J. Autom. Reason."},{"key":"9673_CR32","doi-asserted-by":"publisher","unstructured":"Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 4, pp. 135\u2013150. https:\/\/doi.org\/10.1007\/978-3-642-81955-1_19 (1969)","DOI":"10.1007\/978-3-642-81955-1_19"},{"key":"9673_CR33","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP\u2014a new search algorithm for satisfiability. In: International Conference on Computer Aided Design, ICCAD, pp. 220\u2013227. IEEE Computer Society Press, Boston. https:\/\/doi.org\/10.1007\/978-1-4615-0292-0_7 (1996)","DOI":"10.1007\/978-1-4615-0292-0_7"},{"issue":"4","key":"9673_CR34","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). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","journal-title":"J. Autom. Reason."},{"key":"9673_CR35","doi-asserted-by":"publisher","unstructured":"Teucke, A.: An approximation and refinement approach to first-order automated reasoning. Doctoral thesis, Saarland University. https:\/\/doi.org\/10.22028\/D291-27196 (2018)","DOI":"10.22028\/D291-27196"},{"key":"9673_CR36","doi-asserted-by":"publisher","unstructured":"Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning\u201410th International Joint Conference, IJCAR 2020, Paris, France, July 1\u20134, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12166, pp. 316\u2013334. Springer, Cham. https:\/\/doi.org\/10.1007\/s10817-022-09621-7 (2020)","DOI":"10.1007\/s10817-022-09621-7"},{"key":"9673_CR37","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. 2, pp. 1965\u20132012. Elsevier, Hoboken (2001)"},{"key":"9673_CR38","doi-asserted-by":"publisher","unstructured":"Wischnewski, P.: Efficient reasoning procedures for complex first-order theories. PhD thesis, Saarland University. https:\/\/doi.org\/10.22028\/D291-26406 (2012)","DOI":"10.22028\/D291-26406"},{"key":"9673_CR39","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Automated reasoning building blocks. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design\u2014Symposium in Honor of Ernst-R\u00fcdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8\u20139, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9360, pp. 172\u2013188. Springer, Cham (2015)","DOI":"10.1007\/978-3-319-23506-6_12"},{"key":"9673_CR40","unstructured":"Weidenbach, C., Wischnewski, P.: Contextual rewriting in SPASS. In: PAAR\/ESHOL. CEUR Workshop Proceedings, vol. 373, pp. 115\u2013124 (2008)"},{"issue":"2\u20133","key":"9673_CR41","doi-asserted-by":"publisher","first-page":"97","DOI":"10.3233\/AIC-2010-0459","volume":"23","author":"C Weidenbach","year":"2010","unstructured":"Weidenbach, C., Wischnewski, P.: Subterm contextual rewriting. AI Commun. 23(2\u20133), 97\u2013109 (2010). https:\/\/doi.org\/10.3233\/AIC-2010-0459","journal-title":"AI Commun."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09673-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09673-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09673-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,21]],"date-time":"2023-09-21T04:02:35Z","timestamp":1695268955000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09673-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,30]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9]]}},"alternative-id":["9673"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09673-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,30]]},"assertion":[{"value":"8 February 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 June 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 June 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"22"}}