{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,24]],"date-time":"2026-09-24T09:35:47Z","timestamp":1790242547057,"version":"4.1.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_8","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"127-136","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems"],"prefix":"10.1007","author":[{"given":"Kiraku","family":"Shintani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nao","family":"Hirokawa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"8_CR1","unstructured":"Hindley, J.R.: The Church-Rosser Property and a Result in Combinatory Logic. Ph.D. thesis, University of Newcastle-upon-Tyne (1964)"},{"key":"8_CR2","doi-asserted-by":"crossref","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":"4","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"JP Jouannaud","year":"1986","unstructured":"Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"issue":"2","key":"8_CR4","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1006\/inco.2002.3158","volume":"178","author":"A Rubio","year":"2002","unstructured":"Rubio, A.: A fully syntactic AC-RPO. Inf. Comput. 178(2), 515\u2013533 (2002)","journal-title":"Inf. Comput."},{"key":"8_CR5","first-page":"73","volume":"7","author":"G Plotkin","year":"1972","unstructured":"Plotkin, G.: Building in equational theories. Mach. Intell. 7, 73\u201390 (1972)","journal-title":"Mach. Intell."},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/3-540-56730-5_36","volume-title":"Word Equations and Related Topics","author":"K Schulz","year":"1993","unstructured":"Schulz, K.: Word unification and transformation of generalized equations. In: Abdulrab, H., Pecuchet, J.-P. (eds.) IWWERT 1991. LNCS, vol. 677, pp. 150\u2013176. Springer, Heidelberg (1993)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/BFb0052364","volume-title":"Rewriting Techniques and Applications","author":"RA Schmidt","year":"1998","unstructured":"Schmidt, R.A.: $$E$$-Unification for subsystems of $$S4$$. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 106\u2013120. Springer, Heidelberg (1998)"},{"issue":"2","key":"8_CR8","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G Peterson","year":"1981","unstructured":"Peterson, G., Stickel, M.: Complete sets of reductions for some equational theories. J. ACM 28(2), 233\u2013264 (1981)","journal-title":"J. ACM"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-02348-4_7","volume-title":"Rewriting Techniques and Applications","author":"T Aoto","year":"2009","unstructured":"Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 93\u2013102. Springer, Heidelberg (2009)"},{"issue":"4","key":"8_CR10","doi-asserted-by":"publisher","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":"8_CR11","first-page":"393","volume-title":"Programming of Future Generation Computers II","author":"Y Toyama","year":"1988","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, Amsterdam (1988)"},{"issue":"1","key":"8_CR12","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. Theoret. Comput. Sci. 175(1), 159\u2013181 (1997)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-70590-1_21","volume-title":"Rewriting Techniques and Applications","author":"V van Oostrom","year":"2008","unstructured":"van Oostrom, V.: Confluence by decreasing diagrams. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 306\u2013320. Springer, Heidelberg (2008)"},{"key":"8_CR14","unstructured":"Aoto, T.: Automated confluence proof by decreasing diagrams based on rule-labelling. In: Lynch, C. (ed.) RTA 2010, LIPIcs, vol. 6, pp. 7\u201316 (2010)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-53904-2_94","volume-title":"Rewriting Techniques and Applications","author":"L Pottier","year":"1991","unstructured":"Pottier, L.: Minimal solutions of linear diophantine systems: bounds and algorithms. In: Book, R.V. (ed.) Rewriting Techniques and Applications. LNCS, vol. 488, pp. 162\u2013173. Springer, Heidelberg (1991)"},{"key":"8_CR16","unstructured":"Ohlebusch, E.: Modular Properties of Composable Term Rewriting Systems. Ph.D. thesis, Universit\u00e4t Bielefeld (1994)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-642-22438-6_38","volume-title":"Automated Deduction \u2013 CADE-23","author":"H Zankl","year":"2011","unstructured":"Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI \u2013 a confluence tool. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE-23. LNCS, vol. 6803, pp. 499\u2013505. Springer, Heidelberg (2011)"},{"issue":"4","key":"8_CR18","doi-asserted-by":"publisher","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."},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-16310-4_6","volume-title":"Rewriting Logic and Its Applications","author":"F Dur\u00e1n","year":"2010","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational maude specifications. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 69\u201385. Springer, Heidelberg (2010)"},{"issue":"1","key":"8_CR20","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. LMCS 8(1), 1\u201329 (2012)","journal-title":"LMCS"},{"issue":"1","key":"8_CR21","doi-asserted-by":"publisher","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"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T09:46:02Z","timestamp":1676972762000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}