{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:37:29Z","timestamp":1742978249731,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"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_7","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"111-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent"],"prefix":"10.1007","author":[{"given":"Masahiko","family":"Sakai","sequence":"first","affiliation":[]},{"given":"Michio","family":"Oyamaguchi","sequence":"additional","affiliation":[]},{"given":"Mizuhito","family":"Ogawa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"7_CR1","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, 154\u2013191 (1994)","journal-title":"Inf. Comput."},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/11538363_37","volume-title":"Computer Science Logic","author":"G Godoy","year":"2005","unstructured":"Godoy, G., Tiwari, A.: Confluence of shallow right-linear rewrite systems. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 541\u2013556. Springer, Heidelberg (2005)"},{"issue":"4","key":"7_CR3","first-page":"992","volume":"39","author":"H Gomi","year":"1998","unstructured":"Gomi, H., Oyamaguchi, M., Ohta, Y.: On the church-rosser property of root-E-overlapping and strongly depth-preserving term rewriting systems. IPS J 39(4), 992\u20131005 (1998)","journal-title":"IPS J"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-61064-2_39","volume-title":"Trees in Algebra and Programming","author":"B Gramlich","year":"1996","unstructured":"Gramlich, B.: Confluence without termination via parallel critical pairs. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 211\u2013225. Springer, Heidelberg (1996)"},{"issue":"4","key":"7_CR5","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":"7_CR6","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, 797\u2013821 (1980)","journal-title":"J. ACM"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-28717-6_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Klein","year":"2012","unstructured":"Klein, D., Hirokawa, N.: Confluence of non-left-linear TRSs via relative termination. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 258\u2013273. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297 (1970)","key":"7_CR8","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"7_CR9","volume-title":"Term Rewriting Systems, in Handbook of Logic in Computer Science","author":"JW Klop","year":"1993","unstructured":"Klop, J.W.: Term Rewriting Systems, in Handbook of Logic in Computer Science, vol. 2. Oxford University Press, New York (1993)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/978-3-319-08918-8_20","volume-title":"Rewriting and Typed Lambda Calculi","author":"J Liu","year":"2014","unstructured":"Liu, J., Dershowitz, N., Jouannaud, J.-P.: Confluence by critical pair analysis. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 287\u2013302. Springer, Heidelberg (2014)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/11856290_8","volume-title":"Artificial Intelligence and Symbolic Computation","author":"I Mitsuhashi","year":"2006","unstructured":"Mitsuhashi, I., Oyamaguch, M., Jacquemard, F.: The confluence problem for flat TRSs. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol. 4120, pp. 68\u201381. Springer, Heidelberg (2006)"},{"issue":"10","key":"7_CR12","first-page":"2313","volume":"53","author":"I Mitsuhashi","year":"2012","unstructured":"Mitsuhashi, I., Oyamaguchi, M., Matsuura, K.: On the $$E$$-overlapping property of Wweak monadic TRSs. IPS J. 53(10), 2313\u20132327 (2012). (in Japanese)","journal-title":"IPS J."},{"unstructured":"Ogawa, M., Ono, S.: On the uniquely converging property of nonlinear term rewriting systems. Technical report of IEICE, COMP89\u20137, pp. 61\u201370 (1989)","key":"7_CR13"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/BFb0052357","volume-title":"Rewriting Techniques and Applications","author":"S Okui","year":"1998","unstructured":"Okui, S.: Simultaneous critical pairs and church-rosser property. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 2\u201316. Springer, Heidelberg (1998)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-61254-8_26","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"V van Oostrom","year":"1996","unstructured":"van Oostrom, V.: Development closed critical pairs. In: Dowek, G., Heering, J., Meinke, K., M\u00f6ller, B. (eds.) HOA 1995. LNCS, vol. 1074, pp. 185\u2013200. Springer, Heidelberg (1996)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-62950-5_70","volume-title":"Rewriting Techniques and Applications","author":"M Oyamaguchi","year":"1997","unstructured":"Oyamaguchi, M., Ohta, Y.: A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 187\u2013201. Springer, Heidelberg (1997)"},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"BK Rosen","year":"1973","unstructured":"Rosen, B.K.: Tree-manipulating systems and Church-Rosser theorems. J. ACM 20, 160\u2013187 (1973)","journal-title":"J. ACM"},{"key":"7_CR18","first-page":"53","volume":"204","author":"M Sakai","year":"2008","unstructured":"Sakai, M., Wang, Y.: Undecidable properties on length-two string rewriting systems. ENTCS 204, 53\u201369 (2008)","journal-title":"ENTCS"},{"key":"7_CR19","doi-asserted-by":"publisher","first-page":"810","DOI":"10.1016\/j.ipl.2010.06.015","volume":"110","author":"M Sakai","year":"2010","unstructured":"Sakai, M., Ogawa, M.: Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent. Inf. Process. Lett. 110, 810\u2013814 (2010)","journal-title":"Inf. Process. Lett."},{"key":"7_CR20","first-page":"2014","volume":"34\u201338","author":"M Sakai","year":"2014","unstructured":"Sakai, M., Oyamaguchi, M., Ogawa, M.: Non-E-overlapping and weakly shallow TRSs are confluent (extended abstract). IWC 34\u201338, 2014 (2014)","journal-title":"IWC"},{"unstructured":"Toyama, Y.: Commutativity of term rewriting systems. In: Programming of Future Generation Computer II, pp. 393\u2013407 (1988)","key":"7_CR21"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/3-540-60381-6_19","volume-title":"Conditional and Typed Rewriting Systems","author":"Y Toyama","year":"1995","unstructured":"Toyama, Y., Oyamaguchi, M.: Church-Rosser property and unique normal form property of non-duplicating term rewriting systems. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 316\u2013331. Springer, Heidelberg (1995)"}],"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_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T10:41:49Z","timestamp":1676025709000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}