{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:13:08Z","timestamp":1762459988016},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,5,28]],"date-time":"2021-05-28T00:00:00Z","timestamp":1622160000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,5,28]],"date-time":"2021-05-28T00:00:00Z","timestamp":1622160000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"University of Innsbruck and Medical University of Innsbruck"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We report on the 2019 edition of the Confluence Competition, a competition of software tools that aim to prove or disprove confluence and related (undecidable) properties of rewrite systems automatically.<\/jats:p>","DOI":"10.1007\/s10009-021-00620-4","type":"journal-article","created":{"date-parts":[[2021,5,28]],"date-time":"2021-05-28T08:05:51Z","timestamp":1622189151000},"page":"905-916","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["CoCo 2019: report on the eighth confluence competition"],"prefix":"10.1007","volume":"23","author":[{"given":"Aart","family":"Middeldorp","sequence":"first","affiliation":[]},{"given":"Julian","family":"Nagele","sequence":"additional","affiliation":[]},{"given":"Kiraku","family":"Shintani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,5,28]]},"reference":[{"key":"620_CR1","doi-asserted-by":"publisher","unstructured":"Aoto, T.: Automated confluence proof by decreasing diagrams based on rule-labelling. In: Proceedings of 21st International Conference on Rewriting Techniques and Applications, LIPIcs, vol.\u00a06, pp. 7\u201316 (2010). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2010.7","DOI":"10.4230\/LIPIcs.RTA.2010.7"},{"key":"620_CR2","doi-asserted-by":"publisher","unstructured":"Aoto, T., Toyama, Y.: Ground confluence prover based on rewriting induction. In: Proceedings of 1st International Conference on Formal Structures for Computation and Deduction, LIPIcs, vol.\u00a052, pp. 33:1\u201333:12 (2016). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.33","DOI":"10.4230\/LIPIcs.FSCD.2016.33"},{"key":"620_CR3","doi-asserted-by":"publisher","unstructured":"Aoto, T., Toyama, Y.: Automated proofs of unique normal forms with respect to conversion for term rewriting systems. In: Proceedings of 12th International Symposium on Frontiers of Combining Systems, LNCS, vol. 11715 (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_19","DOI":"10.1007\/978-3-030-29007-8_19"},{"key":"620_CR4","doi-asserted-by":"publisher","unstructured":"Aoto, T., Toyama, Y., Kimura, Y.: Improving rewriting induction approach for proving ground confluence. In: Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction, LIPIcs, vol.\u00a084, pp. 7:1\u20137:18 (2017). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2017.7","DOI":"10.4230\/LIPIcs.FSCD.2017.7"},{"key":"620_CR5","doi-asserted-by":"publisher","unstructured":"Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Proceedings of 20th International Conference on Rewriting Techniques and Applications, LNCS, vol. 5595, pp. 93\u2013102 (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_7","DOI":"10.1007\/978-3-642-02348-4_7"},{"key":"620_CR6","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236, 133\u2013178 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00207-8","journal-title":"Theor. Comput. Sci."},{"key":"620_CR7","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). https:\/\/doi.org\/10.1017\/CBO9781139172752"},{"issue":"3","key":"620_CR8","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.B.: Some properties of conversion. Trans. Am. Math. Soc. 39(3), 472\u2013482 (1936). https:\/\/doi.org\/10.1090\/S0002-9947-1936-1501858-0","journal-title":"Trans. Am. Math. Soc."},{"key":"620_CR9","doi-asserted-by":"publisher","unstructured":"Claessen, K., Smallbone, N.: Efficient encodings of first-order horn formulas in equational logic. In: Proceedings of 9th International Joint Conference on Automated Reasoning, LNAI, vol. 10900, pp. 388\u2013404 (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_2","DOI":"10.1007\/978-3-319-94205-6_2"},{"key":"620_CR10","doi-asserted-by":"publisher","unstructured":"Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: Proceedings of 5th IEEE Symposium on Logic in Computer Science, pp. 242\u2013248 (1990). https:\/\/doi.org\/10.1109\/LICS.1990.113750","DOI":"10.1109\/LICS.1990.113750"},{"key":"620_CR11","doi-asserted-by":"publisher","unstructured":"Dershowitz, N., Plaisted, D.A.: Chapter 9 \u2013 rewriting. In: Handbook of Automated Reasoning, pp. 535\u2013610. North-Holland (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50011-4","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"620_CR12","unstructured":"Felgenhauer, B., Waldmann, J.: Proving non-joinability using weakly monotone algebras. In: Joint Proceedings of the 10th Workshop on Higher-Order Rewriting and the 8th International Workshop on Confluence, pp. 28\u201332 (2019). Available from http:\/\/cl-informatik.uibk.ac.at\/iwc\/hor-iwc2019.pdf"},{"key":"620_CR13","doi-asserted-by":"publisher","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Proceedings of the 5th International Workshop on Frontiers of Combining Systems, LNAI, vol. 3717, pp. 216\u2013231 (2005). https:\/\/doi.org\/10.1007\/11559306_12","DOI":"10.1007\/11559306_12"},{"key":"620_CR14","doi-asserted-by":"publisher","unstructured":"Guti\u00e9rrez, R., Lucas, S.: Automatic generation of logical models with AGES. In: Proceedings of the 27th International Conference on Automated Deduction, LNAI, vol. 11716, pp. 287\u2013299 (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_17","DOI":"10.1007\/978-3-030-29436-6_17"},{"key":"620_CR15","unstructured":"Hirokawa, N., Klein, D.: Saigawa: A confluence tool. In: Proceedings of the 1st International Workshop on Confluence, p.\u00a049 (2012). Available from http:\/\/cl-informatik.uibk.ac.at\/iwc\/iwc2012.pdf"},{"key":"620_CR16","doi-asserted-by":"publisher","unstructured":"Hirokawa, N., Nagele, J., Middeldorp, A.: Cops and CoCoWeb \u2013 Infrastructure for confluence tools. In: Proceedings of the 9th International Joint Conference on Automated Reasoning, LNAI, vol. 10900, pp. 346\u2013353 (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_23","DOI":"10.1007\/978-3-319-94205-6_23"},{"issue":"4","key":"620_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). https:\/\/doi.org\/10.1145\/322217.322230","journal-title":"J. ACM"},{"key":"620_CR18","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. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"620_CR19","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.ipl.2018.04.002","volume":"136","author":"S Lucas","year":"2018","unstructured":"Lucas, S., Guti\u00e9rrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90\u201395 (2018). https:\/\/doi.org\/10.1016\/j.ipl.2018.04.002","journal-title":"Inf. Process. Lett."},{"key":"620_CR20","doi-asserted-by":"publisher","unstructured":"Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Proceedings of the 10th International Conference on Automated Deduction, LNCS, vol. 449, pp. 366\u2013380 (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_100","DOI":"10.1007\/3-540-52885-7_100"},{"issue":"1","key":"620_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. Theor. Comput. Sci. 192(1), 3\u201329 (1998). https:\/\/doi.org\/10.1016\/S0304-3975(97)00143-6","journal-title":"Theor. Comput. Sci."},{"key":"620_CR22","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"620_CR23","doi-asserted-by":"publisher","unstructured":"Me\u00dfner, F., Sternagel, C.: nonreach \u2013 A tool for nonreachability analysis. In: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Part I), LNCS, vol. 11427, pp. 337\u2013343 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_19","DOI":"10.1007\/978-3-030-17462-0_19"},{"key":"620_CR24","doi-asserted-by":"publisher","unstructured":"Middeldorp, A.: Approximating dependency graphs using tree automata techniques. In: Proceedings of the 1st International Joint Conference on Automated Reasoning, LNAI, vol. 2083, pp. 593\u2013610 (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_49","DOI":"10.1007\/3-540-45744-5_49"},{"key":"620_CR25","unstructured":"Nagele, J.: Mechanizing confluence: Automated and certified analysis of first- and higher-order rewrite systems. Ph.D. Thesis, University of Innsbruck (2017). http:\/\/resolver.obvsg.at\/urn:nbn:at:at-ubi:1-13305"},{"key":"620_CR26","doi-asserted-by":"publisher","unstructured":"Nagele, J., Felgenhauer, B., Middeldorp, A.: Improving automatic confluence analysis of rewrite systems by redundant rules. In: Proceedings of the 26th International Conference on Rewriting Techniques and Applications, LIPIcs, vol.\u00a036, pp. 257\u2013268 (2015). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2015.257","DOI":"10.4230\/LIPIcs.RTA.2015.257"},{"key":"620_CR27","doi-asserted-by":"publisher","unstructured":"Nagele, J., Felgenhauer, B., Middeldorp, A.: CSI: New evidence \u2013 a progress report. In: Proceedings of the 26th International Conference on Automated Deduction, LNAI, vol. 10395, pp. 385\u2013397 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_24","DOI":"10.1007\/978-3-319-63046-5_24"},{"key":"620_CR28","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"620_CR29","unstructured":"Nishida, N., Kuroda, T., Yanagisawa, M., Gmeiner, K.: CO3: A COnverter for proving COnfluence of COnditional TRSs. In: Proceedings of the 4th International Workshop on Confluence, p.\u00a042 (2015). Available from http:\/\/cl-informatik.uibk.ac.at\/iwc\/iwc2015.pdf"},{"key":"620_CR30","doi-asserted-by":"publisher","unstructured":"Nishida, N., Maeda, Y.: Narrowing trees for syntactically deterministic conditional term rewriting systems. In: Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, LIPIcs, vol. 108, pp. 26:1\u201326:20 (2018). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.26","DOI":"10.4230\/LIPIcs.FSCD.2018.26"},{"key":"620_CR31","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, Berlin (2002). https:\/\/doi.org\/10.1007\/978-1-4757-3661-8"},{"issue":"1","key":"620_CR32","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). https:\/\/doi.org\/10.1016\/S0304-3975(96)00173-9","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"620_CR33","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.tcs.2007.02.060","volume":"380","author":"D Pous","year":"2007","unstructured":"Pous, D.: New up-to techniques for weak bisimulation. Theor. Comput. Sci. 380(1), 164\u2013180 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2007.02.060","journal-title":"Theor. Comput. Sci."},{"key":"620_CR34","doi-asserted-by":"publisher","unstructured":"Rapp, F., Middeldorp, A.: Automating the first-order theory of rewriting for left-linear right-ground rewrite systems. In: Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, LIPIcs, vol.\u00a052, pp. 36:1\u201336:12 (2016). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.36","DOI":"10.4230\/LIPIcs.FSCD.2016.36"},{"key":"620_CR35","doi-asserted-by":"publisher","unstructured":"Rapp, F., Middeldorp, A.: FORT 2.0. In: Proceedings of the 9th International Joint Conference on Automated Reasoning, LNAI, vol. 10900, pp. 81\u201388 (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_6","DOI":"10.1007\/978-3-319-94205-6_6"},{"key":"620_CR36","doi-asserted-by":"publisher","unstructured":"Shintani, K., Hirokawa, N.: CoLL: A confluence tool for left-linear term rewrite systems. In: Proceedings of the 25th International Conference on Automated Deduction, LNCS, vol. 9195, pp. 127\u2013136 (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_8","DOI":"10.1007\/978-3-319-21401-6_8"},{"key":"620_CR37","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: Proceedings of the 11th Workshop on User Interfaces for Theorem Provers, Electronic Proceedings in Theoretical Computer Science, vol. 167, pp. 61\u201372 (2014). https:\/\/doi.org\/10.4204\/EPTCS.167.8","DOI":"10.4204\/EPTCS.167.8"},{"key":"620_CR38","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Winkler, S.: Certified equational reasoning via ordered completion. In: Proceedings of the 27th International Conference on Automated Deduction, LNAI, vol. 11716, pp. 508\u2013525 (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_30","DOI":"10.1007\/978-3-030-29436-6_30"},{"key":"620_CR39","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Yamada, A.: Reachability analysis for termination and confluence of rewriting. In: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Part I), LNCS, vol. 11427, pp. 262\u2013278 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_15","DOI":"10.1007\/978-3-030-17462-0_15"},{"key":"620_CR40","unstructured":"Sternagel, T.: Reliable confluence analysis of conditional term rewrite systems. Ph.D. Thesis, University of Innsbruck (2017). urn:nbn:at:at-ubi:1-9288"},{"key":"620_CR41","doi-asserted-by":"publisher","unstructured":"Sternagel, T., Middeldorp, A.: Conditional confluence (system description). In: Proceedings of the 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, LNCS (ARCoSS), vol. 8560, pp. 456\u2013465 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_31","DOI":"10.1007\/978-3-319-08918-8_31"},{"key":"620_CR42","unstructured":"Sternagel, T., Middeldorp, A.: Infeasible conditional critical pairs. In: Proceedings of the 4th International Workshop on Confluence, pp. 13\u201317 (2015)"},{"key":"620_CR43","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A cross-community infrastructure for logic solving. In: Proceedings of the 7th International Joint Conference on Automated Reasoning, LNAI, vol. 8562, pp. 367\u2013373 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"620_CR44","unstructured":"Terese: Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press (2003)"},{"key":"620_CR45","doi-asserted-by":"publisher","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, LNCS, vol. 5674, pp. 452\u2013468 (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_31","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"620_CR46","doi-asserted-by":"publisher","unstructured":"Winkler, S., Moser, G.: MaedMax: A maximal ordered completion tool. In: Proceedings of the 9th International Joint Conference on Automated Reasoning, LNAI, vol. 10900, pp. 472\u2013480 (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_31","DOI":"10.1007\/978-3-319-94205-6_31"},{"key":"620_CR47","doi-asserted-by":"publisher","unstructured":"Yamaguchi, M., Aoto, T.: A fast decision procedure for uniqueness of normal forms w.r.t. conversion of shallow term rewriting systems. In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, LIPIcs, vol. 167, pp. 11:1\u201311:23 (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.11","DOI":"10.4230\/LIPIcs.FSCD.2020.11"},{"key":"620_CR48","doi-asserted-by":"publisher","unstructured":"Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI \u2013 A confluence tool. In: Proceedings of the 23th International Conference on Automated Deduction, LNAI, vol. 6803, pp. 499\u2013505 (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_38","DOI":"10.1007\/978-3-642-22438-6_38"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00620-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00620-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00620-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,26]],"date-time":"2021-12-26T12:02:48Z","timestamp":1640520168000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00620-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,28]]},"references-count":48,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["620"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00620-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,5,28]]},"assertion":[{"value":"6 May 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 May 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}