{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:14:58Z","timestamp":1753888498046,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030294359"},{"type":"electronic","value":"9783030294366"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29436-6_19","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"319-336","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Confluence by Critical Pair Analysis Revisited"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8499-0501","authenticated-orcid":false,"given":"Nao","family":"Hirokawa","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4727-4637","authenticated-orcid":false,"given":"Julian","family":"Nagele","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4818-7383","authenticated-orcid":false,"given":"Vincent","family":"van Oostrom","sequence":"additional","affiliation":[]},{"given":"Michio","family":"Oyamaguchi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"key":"19_CR1","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)"},{"key":"19_CR2","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland (1985)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-62950-5_74","volume-title":"Rewriting Techniques and Applications","author":"D Bechet","year":"1997","unstructured":"Bechet, D., de Groote, P., Retor\u00e9, C.: A complete axiomatisation for the inclusion of series-parallel partial orders. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 230\u2013240. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-62950-5_74"},{"key":"19_CR4","unstructured":"Boudol, G.: Computational semantics of term rewriting systems. In: Nivat, M., Reynolds, J. (eds.) Algebraic Methods in Semantics, pp. 169\u2013236. Cambridge University Press (1985)"},{"key":"19_CR5","doi-asserted-by":"publisher","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: meta-level guidance for mathematical reasoning. In: Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2005). https:\/\/doi.org\/10.1017\/CBO9780511543326","DOI":"10.1017\/CBO9780511543326"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1090\/S0002-9947-1936-1501858-0","volume":"39","author":"A Church","year":"1936","unstructured":"Church, A., Rosser, J.: Some properties of conversion. Transact. Am. Math. Soc. 39, 472\u2013482 (1936)","journal-title":"Transact. Am. Math. Soc."},{"key":"19_CR7","unstructured":"Comon, H., et al.: Tree Automata Techniques and Applications (2007). http:\/\/www.grappa.univ-lille3.fr\/tata"},{"key":"19_CR8","volume-title":"Introduction to Lattices and Order","author":"B Davey","year":"1990","unstructured":"Davey, B., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, Formal Models and Semantics, pp. 243\u2013320. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"Endrullis, J., Klop, J., Overbeek, R.: Decreasing diagrams with two labels are complete for confluence of countable systems. In: Proceedings of 3rd FSCD. LIPIcs, vol. 108, pp. 14:1\u201314:15 (2018). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.14","DOI":"10.4230\/LIPIcs.FSCD.2018.14"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2710017","volume":"16","author":"B Felgenhauer","year":"2015","unstructured":"Felgenhauer, B., Middeldorp, A., Zankl, H., van Oostrom, V.: Layer systems for proving confluence. ACM Transact. Computat. Logic 16, 1\u201332 (2015)","journal-title":"ACM Transact. Computat. Logic"},{"key":"19_CR13","unstructured":"Felgenhauer, B.: Labeling multi-steps for confluence of left-linear term rewrite systems. In: Tiwari, A., Aoto, T. (eds.) Proceedings of 4th IWC, pp. 33\u201337 (2015)"},{"key":"19_CR14","unstructured":"Hirokawa, H., Klein, D.: Saigawa: A confluence tool. In: Proceedings of 1st IWC, p. 49 (2012). http:\/\/www.jaist.ac.jp\/project\/saigawa\/"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-319-94205-6_23","volume-title":"Automated Reasoning","author":"N Hirokawa","year":"2018","unstructured":"Hirokawa, N., Nagele, J., Middeldorp, A.: Cops and CoCoWeb: infrastructure for confluence tools. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 346\u2013353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_23"},{"issue":"4","key":"19_CR16","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. Reasoning 47(4), 481\u2013501 (2011)","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"19_CR17","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":"19_CR18","unstructured":"Huet, G., L\u00e9vy, J.J.: Computations in orthogonal rewriting systems, I. In: Lassez, J.L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, chap. 11. The MIT Press (1991)"},{"key":"19_CR19","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, Proceedings of a Conference held at Oxford under the Auspices of the Science Research Council Atlas Computer Laboratory, 29 August\u20132 September 1967. pp. 263\u2013297 (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"19_CR20","unstructured":"Liu, J.L.: Propri\u00e9t\u00e9s de Confluence des R\u00e8gles de R\u00e9\u00e9criture par des Diagrammes D\u00e9croissants. Ph.D. thesis, Tsinghua University and l\u2019Universit\u00e9 Paris-Saclay pr\u00e9par\u00e9e \u00e0 l\u2019\u00c9cole Polytechnique (2016)"},{"issue":"1","key":"19_CR21","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoret. Comput. Sci. 192(1), 3\u201329 (1998). https:\/\/doi.org\/10.1016\/S0304-3975(97)00143-6","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR22","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96, 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"19_CR23","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0020-0190(83)90009-1","volume":"16","author":"Y M\u00e9tivier","year":"1983","unstructured":"M\u00e9tivier, Y.: About the rewriting systems produced by the Knuth\u2013Bendix completion algorithm. Inf. Process. Lett. 16(1), 31\u201334 (1983)","journal-title":"Inf. Process. Lett."},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-319-43144-4_18","volume-title":"Interactive Theorem Proving","author":"J Nagele","year":"2016","unstructured":"Nagele, J., Middeldorp, A.: Certification of classical confluence results for left-linear term rewrite systems. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 290\u2013306. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_18"},{"issue":"2","key":"19_CR25","doi-asserted-by":"publisher","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M Newman","year":"1942","unstructured":"Newman, M.: On theories with a combinatorial definition of equivalence. Ann. Math. 43(2), 223\u2013243 (1942)","journal-title":"Ann. Math."},{"key":"19_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, Heidelberg (2002). https:\/\/doi.org\/10.1007\/978-1-4757-3661-8"},{"key":"19_CR27","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). https:\/\/doi.org\/10.1007\/BFb0052357"},{"key":"19_CR28","unstructured":"van Oostrom, V.: Confluence for Abstract and Higher-Order Rewriting. Ph.D. thesis, Vrije Universiteit, Amsterdam, March 1994"},{"issue":"1","key":"19_CR29","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":"19_CR30","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). https:\/\/doi.org\/10.1007\/978-3-540-70590-1_21"},{"key":"19_CR31","doi-asserted-by":"publisher","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, 160\u2013187 (1973)","journal-title":"J. ACM"},{"key":"19_CR32","unstructured":"Terese: Term Rewriting Systems. Cambridge University Press (2003)"},{"issue":"1","key":"19_CR33","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"},{"key":"19_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-319-08918-8_32","volume-title":"Rewriting and Typed Lambda Calculi","author":"A Yamada","year":"2014","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Nagoya termination tool. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 466\u2013475. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_32"},{"issue":"2","key":"19_CR35","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/s10817-014-9316-y","volume":"54","author":"H Zankl","year":"2015","unstructured":"Zankl, H., Felgenhauer, B., Middeldorp, A.: Labelings for decreasing diagrams. J. Autom. Reasoning 54(2), 101\u2013133 (2015)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 27"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:55:24Z","timestamp":1657576524000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Natal","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.mat.ufrn.br\/CADE-27\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}