{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:56:05Z","timestamp":1781884565494,"version":"3.54.5"},"publisher-location":"Cham","reference-count":36,"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                    <jats:italic>Generalized Term Rewriting Systems<\/jats:italic>\n                    (GTRSs) extend Conditional Term Rewriting Systems by (i) selecting the arguments of function symbols on which rewritings are allowed and (ii) allowing for more general conditions in rules, namely, atoms defined by a set of Horn clauses. They are useful to model and analyze properties of computations with sophisticated languages like . Toyama proved that left-linear and\n                    <jats:italic>almost<\/jats:italic>\n                    <jats:italic>parallel-closed<\/jats:italic>\n                    Term Rewriting Systems (TRSs) are confluent. In this paper, we generalize and extend his result to GTRSs\n                    <jats:italic>without requiring left-linearity<\/jats:italic>\n                    . This improves Toyama\u2019s result, as we show with some examples. Also, Toyama\u2019s result entails confluence of weakly orthogonal TRSs, thus providing a syntactic criterion for proving confluence\n                    <jats:italic>without requiring termination<\/jats:italic>\n                    . We similarly introduce\n                    <jats:italic>weakly V-orthogonal<\/jats:italic>\n                    GTRSs, which are confluent. Weak V-orthogonality checking is implemented in the confluence tool , to improve its ability to deal with context-sensitive and conditional term rewriting systems.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_11","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:57Z","timestamp":1753789677000},"page":"187-206","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Confluence of\u00a0Almost Parallel-Closed Generalized Term Rewriting Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9923-2108","authenticated-orcid":false,"given":"Salvador","family":"Lucas","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/3-540-58216-9_40","volume-title":"Logic Programming and Automated Reasoning","author":"J Avenhaus","year":"1994","unstructured":"Avenhaus, J., Lor\u00eda-S\u00e1enz, C.: On conditional rewrite systems with extra variables and deterministic logic programs. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 215\u2013229. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58216-9_40"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, Cham (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Dershowitz, N., Okada, M., Sivakumar, G.: Confluence of conditional rewrite systems. In: Kaplan, S., Jouannaud, J.-P. editors, Conditional Term Rewriting Systems, 1st International Workshop, Proceedings, volume 308 of Lecture Notes in Computer Science, pp. 31\u201344. Springer, Berlin, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-19242-5_3","DOI":"10.1007\/3-540-19242-5_3"},{"key":"11_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, New York, NY (1996). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3"},{"key":"11_CR6","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-61064-2_39","volume-title":"Trees in Algebra and Programming \u2014 CAAP \u201996","author":"B Gramlich","year":"1996","unstructured":"Gramlich, B.: Confluence without termination via parallel critical pairs. In: Kirchner, H. (ed.) Trees in Algebra and Programming \u2014 CAAP \u201996, pp. 211\u2013225. Springer, Berlin, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61064-2_39"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-030-29436-6_17","volume-title":"Automated Deduction \u2013 CADE 27","author":"R Guti\u00e9rrez","year":"2019","unstructured":"Guti\u00e9rrez, R., Lucas, S.: Automatic generation of logical models with AGES. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 287\u2013299. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_17"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/978-3-030-51054-1_27","volume-title":"Automated Reasoning","author":"R Guti\u00e9rrez","year":"2020","unstructured":"Guti\u00e9rrez, R., Lucas, S.: Automatically proving and disproving feasibility conditions. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 416\u2013435. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_27"},{"issue":"2","key":"11_CR9","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/FI-242192","volume":"192","author":"R Guti\u00e9rrez","year":"2024","unstructured":"Guti\u00e9rrez, R., Lucas, S., V\u00edtores, M.: Proving Confluence in the Confluence Framework with CONFident. Fundam. Informaticae 192(2), 167\u2013217 (2024)","journal-title":"Fundam. Informaticae"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Kim, D., Shintani, K., Thiemann, R.: Certification of confluence- and commutation-proofs via parallel critical pairs. In: Timany, A., Traytel, D., Pientka, B., Blazy, S., editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pp. 147\u2013161. ACM (2024)","DOI":"10.1145\/3636501.3636949"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-030-29436-6_19","volume-title":"Automated Deduction \u2013 CADE 27","author":"N Hirokawa","year":"2019","unstructured":"Hirokawa, N., Nagele, J., van Oostrom, V., Oyamaguchi, M.: Confluence by critical pair analysis revisited. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 319\u2013336. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_19"},{"issue":"4","key":"11_CR12","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"GP Huet","year":"1980","unstructured":"Huet, G.P.: Confluent Reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797\u2013821 (1980)","journal-title":"J. ACM"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/0304-3975(84)90087-2","volume":"33","author":"S Kaplan","year":"1984","unstructured":"Kaplan, S.: Conditional rewrite rules. Theor. Comput. Sci. 33, 175\u2013193 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Klop, J.W.: Chapter 1: Term rewriting systems. In: Abramsky, S., Gabbay, D., Maibaurn, T., (eds), Handbook of Logic in Computer Science, pp. 1\u2013116. Oxford University Press (1992)","DOI":"10.1093\/oso\/9780198537618.003.0001"},{"key":"11_CR15","unstructured":"Klop, J.W.: A counterexample to the Church-Rosser property for Lambda calculus with surjective pairing. Technical report, Department of Mathematics, Utrecht University. Preprint No. 102 (1979)"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.E.: Simple word problems in universal algebra. 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":"11_CR17","unstructured":"Liu, J., Jouannaud, J.-P., Ogawa, M.: Confluence of layered rewrite systems. In: Kreutzer, S., (ed), 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, vol.\u00a041 of LIPIcs, pp. 423\u2013440. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Lucas, S.: Context-sensitive rewriting. ACM Comput. Surv. 53(4), 78:1\u201378:36 (2020)","DOI":"10.1145\/3397677"},{"key":"11_CR19","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100680","volume":"121","author":"S Lucas","year":"2021","unstructured":"Lucas, S.: Applications and extensions of context-sensitive rewriting. J. Logical Algebraic Methods Program. 121, 100680 (2021)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"11_CR20","unstructured":"Lucas, S.: A roadmap to orthogonality of conditional term rewriting systems. In: Nishida, N., Chenavier, C., (eds), 13th International Workshop on Confluence, IWC 2024, pp. 28\u201334 (2024)"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Lucas, S.:. Local confluence of conditional and generalized term rewriting systems. J. Logical Algebraic Methods Program. 136, 100926, 1\u201323 (2024)","DOI":"10.1016\/j.jlamp.2023.100926"},{"key":"11_CR22","unstructured":"Lucas, S.: Termination of generalized term rewriting systems. In: Rehof, J. (ed), 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), volume 299 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 29:1\u201329:18, Dagstuhl, Germany. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"key":"11_CR23","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100749","volume":"126","author":"S Lucas","year":"2022","unstructured":"Lucas, S., V\u00edtores, M., Guti\u00e9rrez, R.: Proving and disproving confluence of context-sensitive rewriting. J. Logical and Algebraic Methods Program. 126, 100749 (2022)","journal-title":"J. Logical and Algebraic Methods Program."},{"key":"11_CR24","unstructured":"Mendelson, E.: Introduction to mathematical logic (4. ed.). Chapman and Hall (1997)"},{"key":"11_CR25","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF01190830","volume":"5","author":"A Middeldorp","year":"1994","unstructured":"Middeldorp, A., Hamoen, E.: Completeness results for basic narrowing. Appl. Algebra Eng. Commun. Comput. 5, 213\u2013253 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"11_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3661-8","volume-title":"Advanced Topics in Term Rewriting","author":"E Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York, NY (2002). https:\/\/doi.org\/10.1007\/978-1-4757-3661-8"},{"issue":"1","key":"11_CR27","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). https:\/\/doi.org\/10.1145\/321250.321253","journal-title":"J. ACM"},{"key":"11_CR28","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-031-63501-4_16","volume-title":"Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3\u20136, 2024, Proceedings, Part II","author":"J Sch\u00f6pf","year":"2024","unstructured":"Sch\u00f6pf, J., Mitterwallner, F., Middeldorp, A.: Confluence of\u00a0logically constrained rewrite systems revisited. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3\u20136, 2024, Proceedings, Part II, pp. 298\u2013316. Springer Nature Switzerland, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63501-4_16"},{"key":"11_CR29","unstructured":"Shintani, K., Hirokawa, N.: Compositional confluence criteria. In: Felty, A.P., ed, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 28:1\u201328:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"11_CR30","unstructured":"Sternagel, C., Sternagel, T.: Certifying confluence of almost orthogonal CTRSs via exact tree automata completion. In: Kesner, D., Pientka, B., (eds), 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 Proceedings in Informatics (LIPIcs), pp. 29:1\u201329:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"11_CR31","unstructured":"Stevanovic, F., Mitterwallner, F.: CoCo 2023 Participant: ConfCSR. In: 12th International Workshop on Confluence, IWC 2023, p.\u00a063 (2023)"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-59200-8_56","volume-title":"Rewriting Techniques and Applications","author":"T Suzuki","year":"1995","unstructured":"Suzuki, T., Middeldorp, A., Ida, T.: Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 179\u2013193. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59200-8_56"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Suzuki, T., Middeldorp, A., Ida, T.: Level-Confluence of conditional rewrite systems with extra variables in right-hand sides (1995). revised version of [32], http:\/\/cl-informatik.uibk.ac.at\/users\/ami\/research\/publications\/proceedings\/95rta.pdf","DOI":"10.1007\/3-540-59200-8_56"},{"key":"11_CR34","unstructured":"Terese. Term rewriting systems, volume\u00a055 of Cambridge tracts in theoretical computer science. Cambridge University Press (2003)"},{"key":"11_CR35","unstructured":"Toyama, Y.: Commutativity of term rewriting systems. In: Fuchi, K., Kott, L., (eds), Programming of Future Generation Computer, II. Proceedings of the Second Franco-Japanese Symposium on Programming of Future Generation Computers, Cannes, France, 9-11, November, 1987, pp. 393\u2013407. North-Holland (1988)"},{"issue":"1","key":"11_CR36","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/S0304-3975(96)00173-9","volume":"175","author":"V van Oostrom","year":"1997","unstructured":"van Oostrom, V.: Developing developments. Theor. Comput. Sci. 175(1), 159\u2013181 (1997)","journal-title":"Theor. Comput. Sci."}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:25:23Z","timestamp":1781882723000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_11","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 author has 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"}}]}}