{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:57:05Z","timestamp":1781884625395,"version":"3.54.5"},"publisher-location":"Cham","reference-count":32,"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>Congruence closure on ground equations is a well-established and efficient algorithm for deciding ground equalities. It constructs an explicit representation of ground equivalence classes based on a given set of input equations, allowing ground equalities to be decided by membership. In many applications, these ground equations originate from grounding non-ground equations.<\/jats:p>\n                  <jats:p>We propose an algorithm that directly computes a non-ground representation of ground congruence classes for non-ground equations. Our approach is sound and complete with respect to the corresponding ground congruence classes. Experimental results demonstrate that computing non-ground congruence classes often outperforms the classical ground congruence closure algorithm in efficiency.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_31","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:59Z","timestamp":1753789679000},"page":"594-613","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Computing Ground Congruence Classes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2634-4154","authenticated-orcid":false,"given":"Hendrik","family":"Leidinger","sequence":"first","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":"31_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"31_CR2","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, 2\u20137 April 2022, Proceedings, Part I. LNCS, vol. 13243, pp. 415\u2013442. Springer (2022)"},{"key":"31_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Fontaine, P., Reynolds, A.: Congruence closure with free variables. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 214\u2013230. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_13","DOI":"10.1007\/978-3-662-54580-5_13"},{"key":"31_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"31_CR5","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Bouton, T., Caminha B.\u00a0de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: International Conference on Automated Deduction, pp. 151\u2013156. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"31_CR7","doi-asserted-by":"publisher","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Bromberger, M., Fleury, M., Schwarz, S., Weidenbach, C.: SPASS-SATT - A CDCL(LA) solver (2019)","DOI":"10.1007\/978-3-030-29436-6_7"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, 16\u201324 March 2013. Proceedings. vol.\u00a07795, pp. 93\u2013107. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting, Chap.\u00a09. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, pp. 535\u2013610. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"issue":"4","key":"31_CR11","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"PJ Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758\u2013771 (1980)","journal-title":"J. ACM"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer-Aided Verification (CAV\u20192014). LNCS, vol.\u00a08559, pp. 737\u2013744. Springer, July 2014","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"31_CR13","unstructured":"Fontaine, P.: Techniques for verification of concurrent systems with invariants. Ph.D. thesis, Institut Montefiore, Universit\u00e9 de Liege, Belgium (2004)"},{"key":"31_CR14","doi-asserted-by":"publisher","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_14","DOI":"10.1007\/978-3-540-27813-9_14"},{"issue":"1","key":"31_CR15","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1093\/jigpal\/9.1.53","volume":"9","author":"J Hurd","year":"2001","unstructured":"Hurd, J.: Congruence classes with logic variables. Log. J. IGPL 9(1), 53\u201369 (2001)","journal-title":"Log. J. IGPL"},{"key":"31_CR16","doi-asserted-by":"crossref","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, 19\u201322 August 1996. LNCS, vol.\u00a01118, pp. 46\u201360. Springer (1996)","DOI":"10.1007\/3-540-61551-2_65"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, I. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"issue":"3","key":"31_CR18","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/s10817-023-09673-3","volume":"67","author":"H Leidinger","year":"2023","unstructured":"Leidinger, H., Weidenbach, C.: SCL(EQ): SCL for first-order logic with equality. J. Autom. Reason. 67(3), 22 (2023)","journal-title":"J. Autom. Reason."},{"key":"31_CR19","unstructured":"Leidinger, H., Weidenbach, C.: Non-ground congruence closure. CoRR abs\/2412.10066 (2024)"},{"issue":"2","key":"31_CR20","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. J. Autom. Reason. 9(2), 147\u2013167 (1992)","journal-title":"J. Autom. Reason."},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: 2001 Proceedings of the Design Automation Conference, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"31_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","year":"2008","unstructured":"Ramakrishnan, C.R., Rehof, J. (eds.): TACAS 2008. LNCS, vol. 4963. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3"},{"issue":"2","key":"31_CR23","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)","journal-title":"J. ACM"},{"key":"31_CR24","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001, LNCS, vol. 2083, pp. 257\u2013271. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_19","DOI":"10.1007\/3-540-45744-5_19"},{"issue":"4","key":"31_CR25","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007)","journal-title":"Inf. Comput."},{"key":"31_CR26","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-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53, 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"31_CR27","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, 14\u201320 April 2018, Proceedings, Part II. LNCS, vol. 10806, pp. 112\u2013131. Springer, Heidelberg (2018)","DOI":"10.1007\/978-3-319-89963-3_7"},{"key":"31_CR28","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., de\u00a0Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: 2014 Formal Methods in Computer-Aided Design (FMCAD), pp. 195\u2013202 (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987613","DOI":"10.1109\/FMCAD.2014.6987613"},{"issue":"1","key":"31_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"RE Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1\u201312 (1984)","journal-title":"J. ACM"},{"key":"31_CR30","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: International Conference on Computer Aided Design, ICCAD, pp. 220\u2013227. IEEE Computer Society Press (1996)"},{"key":"31_CR31","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure - from CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"31_CR32","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Automated reasoning building blocks. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design - Symposium in Honor of Ernst-R\u00fcdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, 8\u20139 September 2015. Proceedings. LNCS, vol.\u00a09360, pp. 172\u2013188. Springer, Heidelberg (2015)","DOI":"10.1007\/978-3-319-23506-6_12"}],"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_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:28:21Z","timestamp":1781882901000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_31","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 paper.","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"}}]}}