{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:54:33Z","timestamp":1781927673742,"version":"3.54.5"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,12,17]],"date-time":"2014-12-17T00:00:00Z","timestamp":1418774400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10817-014-9316-y","type":"journal-article","created":{"date-parts":[[2014,12,16]],"date-time":"2014-12-16T17:57:19Z","timestamp":1418752639000},"page":"101-133","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Labelings for Decreasing Diagrams"],"prefix":"10.1007","volume":"54","author":[{"given":"Harald","family":"Zankl","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bertram","family":"Felgenhauer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2014,12,17]]},"reference":[{"key":"9316_CR1","first-page":"7","volume":"6","author":"T Aoto","year":"2010","unstructured":"Aoto, T.: Automated confluence proof by decreasing diagrams based on rule-labelling. In: Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics 6, 7\u201316 (2010)","journal-title":"Leibniz International Proceedings in Informatics"},{"issue":"1:31","key":"9316_CR2","first-page":"1","volume":"8","author":"T Aoto","year":"2012","unstructured":"Aoto, T., Toyama, Y.: A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. Logical Methods in Computer Science 8(1:31), 1\u201329 (2012)","journal-title":"Logical Methods in Computer Science"},{"issue":"11","key":"9316_CR3","first-page":"1134","volume":"3","author":"T Aoto","year":"1997","unstructured":"Aoto, T., Toyama, Y.: Persistency of confluence. Journal of Universal Computer Science 3(11), 1134\u20131147 (1997)","journal-title":"Journal of Universal Computer Science"},{"key":"9316_CR4","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-642-02348-4_7","volume":"5595","author":"T Aoto","year":"2009","unstructured":"Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Proceedings of the 20th International Conference on Rewriting Techniques and Applications. Lect. Notes Comput. Sci. 5595, 93\u2013102 (2009)","journal-title":"Lect. Notes Comput. Sci."},{"key":"9316_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"9316_CR6","unstructured":"Felgenhauer, B.: Rule labeling for confluence of left-linear term rewrite systems. In: Proceedings of the 2nd International Workshop on Confluence, pp. 23\u201327 (2013)"},{"key":"9316_CR7","first-page":"288","volume":"13","author":"B Felgenhauer","year":"2011","unstructured":"Felgenhauer, B., Zankl, H., Middeldorp, A.: Proving confluence with layer systems. In: Proceedings of the 31st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics 13, 288\u2013299 (2011)","journal-title":"Leibniz International Proceedings in Informatics"},{"key":"9316_CR8","unstructured":"Geser, A. Relative termination. Ph.D. thesis, Universit\u00e4t Passau (1990). Available as technical report 91-03"},{"key":"9316_CR9","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/3-540-61064-2_39","volume":"1059","author":"B Gramlich","year":"1996","unstructured":"Gramlich, B.: Confluence without termination via parallel critical pairs. In: Proceedings of the 21st International Colloquium on Trees in Algebra and Programming. Lect. Notes Comput. Sci. 1059, 211\u2013225 (1996)","journal-title":"Lect. Notes Comput. Sci."},{"key":"9316_CR10","unstructured":"Hirokawa, N., Middeldorp, A.: Commutation via relative termination. In: Proceedings of the 2nd International Workshop on Confluence, pp. 29\u201333 (2013)"},{"issue":"4","key":"9316_CR11","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/s10817-011-9238-x","volume":"47","author":"N Hirokawa","year":"2011","unstructured":"Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. J. Autom. Reason. 47(4), 481\u2013501 (2011)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9316_CR12","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797\u2013821 (1980)","journal-title":"J. ACM"},{"key":"9316_CR13","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-642-28717-6_21","volume":"7180","author":"D Klein","year":"2012","unstructured":"Klein, D., Hirokawa, N.: Confluence of non-left-linear TRSs via relative termination. In: Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Lect. Notes Comput. Sci. 7180, 258\u2013273 (2012). (Advanced Research in Computing and Software Science)","journal-title":"Lect. Notes Comput. Sci."},{"key":"9316_CR14","doi-asserted-by":"crossref","unstructured":"Knuth, D., Bendix, P.: 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":"9316_CR15","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/BFb0052357","volume":"1379","author":"S Okui","year":"1998","unstructured":"Okui, S.: Simultaneous critical pairs and Church-Rosser property. In: Proceedings of the 9th International Conference on Techniques, Rewriting, Applications. Lect. Notes Comput. Sci. 1379, 2\u201316 (1998)","journal-title":"Lect. Notes Comput. Sci."},{"issue":"2","key":"9316_CR16","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1016\/0304-3975(92)00023-K","volume":"126","author":"V van Oostrom","year":"1994","unstructured":"van Oostrom, V.: Confluence by decreasing diagrams. Theor. Comput. Sci. 126(2), 259\u2013280 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"9316_CR17","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/978-3-540-70590-1_21","volume":"5117","author":"V van Oostrom","year":"2008","unstructured":"van Oostrom, V.: Confluence by decreasing diagrams \u2013 converted. In: Proceedings of the 19th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science 5117, 306\u2013320 (2008)","journal-title":"Lecture Notes in Computer Science"},{"key":"9316_CR18","unstructured":"van Oostrom, V.: Confluence via critical valleys. In: Proceedings 6th International Workshop on Higher-Order Rewriting, pp. 9\u201311 (2012)"},{"issue":"1","key":"9316_CR19","doi-asserted-by":"crossref","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."},{"key":"9316_CR20","doi-asserted-by":"crossref","unstructured":"Oyamaguchi, M., Ohta, Y.: A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In: Proceedings of the 8th International Conference on Rewriting Techniques and Applications. Lect. Notes Comput. Sci. 1232 (1997), 187\u2013201","DOI":"10.1007\/3-540-62950-5_70"},{"issue":"1","key":"9316_CR21","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"B Rosen","year":"1973","unstructured":"Rosen, B.: Tree-manipulating systems and Church-Rosser theorems. J. ACM 20(1), 160\u2013187 (1973)","journal-title":"J. ACM"},{"issue":"1:4","key":"9316_CR22","first-page":"1","volume":"9","author":"A Stump","year":"2012","unstructured":"Stump, A., Zantema, H., Kimmell, G., Omar, R.: A rewriting view of simple typing. Logical Methods in Computer Science 9(1:4), 1\u201329 (2012)","journal-title":"Logical Methods in Computer Science"},{"key":"9316_CR23","unstructured":"Terese: Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)"},{"key":"9316_CR24","unstructured":"Toyama, Y.: Commutativity of term rewriting systems. In: Fuchi, K., Kott, L. (eds.) Programming of Future Generation Computers II, pp. 393\u2013407. North-Holland (1988)"},{"issue":"1","key":"9316_CR25","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/7531.7534","volume":"34","author":"Y Toyama","year":"1987","unstructured":"Toyama, Y.: On the Church-Rosser property for the direct sum of term rewriting systems. J. ACM 34(1), 128\u2013143 (1987)","journal-title":"J. ACM"},{"key":"9316_CR26","unstructured":"Toyama, Y.: On the Church-Rosser property of term rewriting systems. Tech. Rep. 17672 (1981). NTT ECL"},{"issue":"1","key":"9316_CR27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(92)90322-7","volume":"94","author":"U Waldmann","year":"1992","unstructured":"Waldmann, U.: Semantics of order-sorted specifications. Theor. Comput. Sci. 94(1), 1\u201335 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"9316_CR28","first-page":"352","volume":"21","author":"H Zankl","year":"2013","unstructured":"Zankl, H.: Confluence by decreasing diagrams \u2013 formalized. In: Proceedings of the 24th International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics 21, 352\u2013367 (2013)","journal-title":"Leibniz International Proceedings in Informatics"},{"key":"9316_CR29","unstructured":"Zankl, H. Decreasing diagrams. Archive of Formal Proofs (2013). Formal proof development, http:\/\/afp.sf.net\/entries\/Decreasing-Diagrams.shtml"},{"key":"9316_CR30","first-page":"499","volume":"6803","author":"H Zankl","year":"2011","unstructured":"Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI \u2013 A confluence tool. In: Proceedings of the 23rd International Conference on Deduction, Automated. Lecture Notes in Artificial Intelligence 6803, 499\u2013505 (2011)","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"9316_CR31","first-page":"377","volume":"10","author":"H Zankl","year":"2011","unstructured":"Zankl, H., Felgenhauer, B., Middeldorp, A.: Labelings for decreasing diagrams. In: Proceedings of the 22nd International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics 10, 377\u2013392 (2011)","journal-title":"Leibniz International Proceedings in Informatics"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9316-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-014-9316-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9316-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T14:01:03Z","timestamp":1566136863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-014-9316-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,17]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["9316"],"URL":"https:\/\/doi.org\/10.1007\/s10817-014-9316-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,17]]}}}