{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,26]],"date-time":"2025-08-26T07:12:42Z","timestamp":1756192362686,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,5,7]],"date-time":"2022-05-07T00:00:00Z","timestamp":1651881600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,5,7]],"date-time":"2022-05-07T00:00:00Z","timestamp":1651881600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002957","name":"Technische Universit\u00e4t Dresden","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002957","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The word problem for a finite set of ground identities is known to be decidable in polynomial time using congruence closure, and this is also the case if some of the function symbols are assumed to be commutative or defined by certain shallow identities, called strongly shallow. We show that decidability in P is preserved if we add the assumption that certain function symbols<jats:italic>f<\/jats:italic>are<jats:italic>extensional<\/jats:italic>in the sense that<jats:inline-formula><jats:alternatives><jats:tex-math>$$f(s_1,\\ldots ,s_n) \\mathrel {\\approx }f(t_1,\\ldots ,t_n)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>f<\/mml:mi><mml:mrow><mml:mo>(<\/mml:mo><mml:msub><mml:mi>s<\/mml:mi><mml:mn>1<\/mml:mn><\/mml:msub><mml:mo>,<\/mml:mo><mml:mo>\u2026<\/mml:mo><mml:mo>,<\/mml:mo><mml:msub><mml:mi>s<\/mml:mi><mml:mi>n<\/mml:mi><\/mml:msub><mml:mo>)<\/mml:mo><\/mml:mrow><mml:mo>\u2248<\/mml:mo><mml:mi>f<\/mml:mi><mml:mrow><mml:mo>(<\/mml:mo><mml:msub><mml:mi>t<\/mml:mi><mml:mn>1<\/mml:mn><\/mml:msub><mml:mo>,<\/mml:mo><mml:mo>\u2026<\/mml:mo><mml:mo>,<\/mml:mo><mml:msub><mml:mi>t<\/mml:mi><mml:mi>n<\/mml:mi><\/mml:msub><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>implies<jats:inline-formula><jats:alternatives><jats:tex-math>$$s_1 \\mathrel {\\approx }t_1,\\ldots ,s_n \\mathrel {\\approx }t_n$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msub><mml:mi>s<\/mml:mi><mml:mn>1<\/mml:mn><\/mml:msub><mml:mo>\u2248<\/mml:mo><mml:msub><mml:mi>t<\/mml:mi><mml:mn>1<\/mml:mn><\/mml:msub><mml:mo>,<\/mml:mo><mml:mo>\u2026<\/mml:mo><mml:mo>,<\/mml:mo><mml:msub><mml:mi>s<\/mml:mi><mml:mi>n<\/mml:mi><\/mml:msub><mml:mo>\u2248<\/mml:mo><mml:msub><mml:mi>t<\/mml:mi><mml:mi>n<\/mml:mi><\/mml:msub><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP.<\/jats:p>","DOI":"10.1007\/s10817-022-09624-4","type":"journal-article","created":{"date-parts":[[2022,5,7]],"date-time":"2022-05-07T07:03:40Z","timestamp":1651907020000},"page":"301-329","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Deciding the Word Problem for Ground and Strongly Shallow\u00a0Identities w.r.t. Extensional Symbols"],"prefix":"10.1007","volume":"66","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,7]]},"reference":[{"key":"9624_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/9781139025355","volume-title":"An introduction to description logic","author":"F Baader","year":"2017","unstructured":"Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An introduction to description logic. Cambridge University Press, Cambridge (2017)"},{"key":"9624_CR2","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Complexity of finitely presented algebras. In: Proceedings of the 9th ACM symposium on theory of computing, pp. 164\u2013177. ACM (1977)","DOI":"10.1145\/800105.803406"},{"issue":"4","key":"9624_CR3","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"},{"issue":"2","key":"9624_CR4","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"9624_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term rewriting and all that","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, Cambridge (1998)"},{"issue":"7","key":"9624_CR6","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"RE Shostak","year":"1978","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7), 583\u2013585 (1978)","journal-title":"Commun. ACM"},{"key":"9624_CR7","first-page":"23","volume-title":"Proceedings of the 8th international conference on rewriting techniques and applications (RTA 1997), lecture notes in computer science","author":"D Kapur","year":"1997","unstructured":"Kapur, D.: Shostak\u2019s congruence closure as completion. In: Proceedings of the 8th international conference on rewriting techniques and applications (RTA 1997), lecture notes in computer science, vol. 1232, pp. 23\u201337. Springer, Berlin (1997)"},{"issue":"1","key":"9624_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/138027.138032","volume":"40","author":"JH Gallier","year":"1993","unstructured":"Gallier, J.H., Narendran, P., Plaisted, D.A., Raatz, S., Snyder, W.: An algorithm for finding canonical sets of ground rewrite rules in polynomial time. J. ACM 40(1), 1\u201316 (1993)","journal-title":"J. ACM"},{"issue":"4","key":"9624_CR9","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1006\/jsco.1993.1029","volume":"15","author":"W Snyder","year":"1993","unstructured":"Snyder, W.: A fast algorithm for generating reduced ground rewriting systems from a set of ground equations. J. Symb. Comput. 15(4), 415\u2013450 (1993)","journal-title":"J. Symb. Comput."},{"key":"9624_CR10","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: Proceedings of 16th annual IEEE symposium on logic in computer science (LICS 2001), pp. 29\u201337. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932480"},{"issue":"4","key":"9624_CR11","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."},{"issue":"1","key":"9624_CR12","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s11424-019-8377-8","volume":"32","author":"D Kapur","year":"2019","unstructured":"Kapur, D.: Conditional congruence closure over uninterpreted and interpreted symbols. J. Syst. Sci. Complex. 32(1), 317\u2013355 (2019)","journal-title":"J. Syst. Sci. Complex."},{"key":"9624_CR13","first-page":"163","volume-title":"Proceedings of the 10th international joint conference on automated reasoning IJCAR 2020. Part I, lecture notes in computer science","author":"F Baader","year":"2020","unstructured":"Baader, F., Kapur, D.: Deciding the word problem for ground identities with commutative and extensional symbols. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proceedings of the 10th international joint conference on automated reasoning IJCAR 2020. Part I, lecture notes in computer science, vol. 12166, pp. 163\u2013180. Springer, Cham (2020)"},{"issue":"1","key":"9624_CR14","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/BF00247671","volume":"17","author":"P Narendran","year":"1996","unstructured":"Narendran, P., Rusinowitch, M.: Any ground associative-commutative theory has a finite canonical system. J. Autom. Reason. 17(1), 131\u2013143 (1996)","journal-title":"J. Autom. Reason."},{"key":"9624_CR15","first-page":"245","volume-title":"Proceedings of the third international workshop on frontiers of combining systems (FroCoS 2000), lecture notes in computer science","author":"L Bachmair","year":"2000","unstructured":"Bachmair, L., Ramakrishnan, I.V., Tiwari, A., Vigneron, L.: Congruence closure modulo associativity and commutativity. In: Kirchner, H., Ringeissen, C. (eds.) Proceedings of the third international workshop on frontiers of combining systems (FroCoS 2000), lecture notes in computer science, vol. 1794, pp. 245\u2013259. Springer, Berlin (2000)"},{"issue":"1","key":"9624_CR16","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1006\/inco.1994.1043","volume":"111","author":"H Comon","year":"1994","unstructured":"Comon, H., Haberstrau, M., Jouannaud, J.-P.: Syntacticness, cycle-syntacticness, and shallow theories. Inf. Comput. 111(1), 154\u2013191 (1994)","journal-title":"Inf. Comput."},{"key":"9624_CR17","doi-asserted-by":"crossref","unstructured":"Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: M.E. Stickel (ed.) Proceedings of the 10th international conference on automated deduction (CADE 1990), lecture notes in computer science, vol. 449, pp. 366\u2013380. Springer (1990)","DOI":"10.1007\/3-540-52885-7_100"},{"issue":"2","key":"9624_CR18","first-page":"555","volume":"8","author":"Y Matijasevich","year":"1967","unstructured":"Matijasevich, Y.: Simple examples of undecidable associative calculi. Sov. Math. (Doklady) 8(2), 555\u2013557 (1967)","journal-title":"Sov. Math. (Doklady)"},{"key":"9624_CR19","volume-title":"Universal algebra for computer scientists, EATCS monographs on theoretical computer science","author":"W Wechler","year":"1992","unstructured":"Wechler, W.: Universal algebra for computer scientists, EATCS monographs on theoretical computer science, vol. 25. Springer, New York (1992)"},{"key":"9624_CR20","unstructured":"Siekmann, J.H.: Unification of commutative terms. In: Proceedings of the international symposium on symbolic and algebraic manipulation, EUROSAM\u201979, lecture notes in computer science, vol.\u00a072, pp. 531\u2013545. Springer, Marseille, France (1979)"},{"issue":"3","key":"9624_CR21","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","volume":"46","author":"EW Mayr","year":"1982","unstructured":"Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Adv. Math. 46(3), 305\u2013329 (1982)","journal-title":"Adv. Math."},{"key":"9624_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical equational proofs","author":"L Bachmair","year":"1991","unstructured":"Bachmair, L.: Canonical equational proofs. Birkh\u00e4user, Boston (1991)"},{"key":"9624_CR23","doi-asserted-by":"crossref","unstructured":"Lynch, C., Morawska, B.: Automatic decidability. In: Proceddings of the 17th IEEE symposium on logic in computer science (LICS 2002), pp. 7\u201316. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029813"},{"issue":"7","key":"9624_CR24","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1016\/j.ic.2011.03.005","volume":"209","author":"C Lynch","year":"2011","unstructured":"Lynch, C., Ranise, S., Ringeissen, C., Tran, D.: Automatic decidability and combinability. Inf. Comput. 209(7), 1026\u20131047 (2011)","journal-title":"Inf. Comput."},{"key":"9624_CR25","first-page":"19","volume-title":"Proceedings of the 14th international conference on automated deduction (CADE 1997), lecture notes in computer science","author":"F Baader","year":"1997","unstructured":"Baader, F., Tinelli, C.: A new approach for combining decision procedure for the word problem, and its connection to the Nelson-Oppen combination method. In: McCune, W. (ed.) Proceedings of the 14th international conference on automated deduction (CADE 1997), lecture notes in computer science, vol. 1249, pp. 19\u201333. Springer, Berlin (1997)"},{"key":"9624_CR26","unstructured":"Baader, F., Tinelli, C.: A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method. LTCS-report LTCS-96-01, LuFg theoretical computer science, RWTH Aachen (1996). https:\/\/tu-dresden.de\/ing\/informatik\/thi\/lat\/forschung\/technische-berichte"},{"key":"9624_CR27","first-page":"345","volume-title":"Proceedings of the first international conference on rewriting techniques and applications (RTA 1985), lecture notes in computer science","author":"A Kandri-Rody","year":"1985","unstructured":"Kandri-Rody, A., Kapur, D., Narendran, P.: An ideal-theoretic approach to work problems and unification problems over finitely presented commutative algebras. In: Jouannaud, J. (ed.) Proceedings of the first international conference on rewriting techniques and applications (RTA 1985), lecture notes in computer science, vol. 202, pp. 345\u2013364. Springer, Berlin (1985)"},{"key":"9624_CR28","first-page":"15:1","volume-title":"6th international conference on formal structures for computation and deduction (FSCD 2021), LIPIcs","author":"D Kapur","year":"2021","unstructured":"Kapur, D.: A modular associative commutative (AC) congruence closure algorithm. In: Kobayashi, N. (ed.) 6th international conference on formal structures for computation and deduction (FSCD 2021), LIPIcs, vol. 195, p. 15:1-15:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Wadern (2021)"},{"key":"9624_CR29","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1007\/3-540-52885-7_128","volume-title":"Proceedings of the 10th international conference on automated deduction (CADE\u201990), lecture notes in computer science","author":"T K\u00e4ufl","year":"1990","unstructured":"K\u00e4ufl, T., Zabel, N.: The theorem prover of the program verifier Tatzelwurm. In: Stickel, M.E. (ed.) Proceedings of the 10th international conference on automated deduction (CADE\u201990), lecture notes in computer science, vol. 449, pp. 657\u2013658. Springer, Berlin (1990)"},{"key":"9624_CR30","doi-asserted-by":"crossref","unstructured":"Schmidt, R.A., Waldmann, U.: Modal tableau systems with blocking and congruence closure. In: H.\u00a0de\u00a0Nivelle (ed.) Proceedings of the 24th international conference on automated reasoning with analytic tableaux and related methods (TABLEAUX 2015), lecture notes in computer science, vol. 9323, pp. 38\u201353. Springer (2015)","DOI":"10.1007\/978-3-319-24312-2_4"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09624-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09624-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09624-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,24]],"date-time":"2024-09-24T01:12:17Z","timestamp":1727140337000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09624-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,7]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["9624"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09624-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2022,5,7]]},"assertion":[{"value":"15 April 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 January 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 May 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}