{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:33:29Z","timestamp":1753886009792,"version":"3.41.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_24","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"385-397","source":"Crossref","is-referenced-by-count":17,"title":["CSI: New Evidence \u2013 A Progress Report"],"prefix":"10.1007","author":[{"given":"Julian","family":"Nagele","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertram","family":"Felgenhauer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-319-21401-6_5","volume-title":"Automated Deduction - CADE-25","author":"T Aoto","year":"2015","unstructured":"Aoto, T., Hirokawa, N., Nagele, J., Nishida, N., Zankl, H.: Confluence competition 2015. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 101\u2013104. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_5"},{"issue":"1: 31","key":"24_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(1:31)2012","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: 31), 1\u201329 (2012). doi: 10.2168\/LMCS-8(1:31)2012","journal-title":"LMCS"},{"key":"24_CR3","doi-asserted-by":"publisher","unstructured":"Aoto, T., Toyama, Y.: Ground confluence prover based on rewriting induction. In: Proceedings of 1st FSCD. LIPIcs, vol. 52, pp. 33: 1\u201333: 12 (2016). doi: 10.4230\/LIPIcs.FSCD.2016.33","DOI":"10.4230\/LIPIcs.FSCD.2016.33"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-319-08918-8_4","volume-title":"Rewriting and Typed Lambda Calculi","author":"T Aoto","year":"2014","unstructured":"Aoto, T., Toyama, Y., Uchida, K.: Proving confluence of term rewriting systems via persistency and decreasing diagrams. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 46\u201360. Springer, Cham (2014). doi: 10.1007\/978-3-319-08918-8_4"},{"key":"24_CR5","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). doi: 10.1007\/978-3-642-02348-4_7"},{"key":"24_CR6","doi-asserted-by":"publisher","unstructured":"Appel, C., van Oostrom, V., Simonsen, J.G.: Higher-order (non-)modularity. In: Proceedings of 21st RTA. LIPIcs, vol. 6, pp. 17\u201332 (2010). doi: 10.4230\/LIPIcs.RTA.2010.17","DOI":"10.4230\/LIPIcs.RTA.20"},{"key":"24_CR7","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, New York (1998)"},{"key":"24_CR8","doi-asserted-by":"publisher","unstructured":"Felgenhauer, B.: Deciding confluence of ground term rewrite systems in cubic time. In: Proceedings of 23rd RTA. LIPIcs, vol. 15, pp. 165\u2013175 (2012). doi: 10.4230\/LIPIcs.RTA.2012.165","DOI":"10.4230\/LIPIcs.RTA.2012.165"},{"key":"24_CR9","unstructured":"Felgenhauer, B.: Efficiently deciding uniqueness of normal forms and unique normalization for ground TRSs. In: Proceedings of 5th IWC, pp. 16\u201320 (2016)"},{"issue":"2: 14","key":"24_CR10","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., Oostrom, V.O.: Layer systems for proving confluence. ACM TOCL 16(2: 14), 1\u201332 (2015). doi: 10.1145\/2710017","journal-title":"ACM TOCL"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-319-04921-2_28","volume-title":"Language and Automata Theory and Applications","author":"B Felgenhauer","year":"2014","unstructured":"Felgenhauer, B., Thiemann, R.: Reachability analysis with state-compatible automata. In: Dediu, A.-H., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 347\u2013359. Springer, Cham (2014). doi: 10.1007\/978-3-319-04921-2_28"},{"issue":"4","key":"24_CR12","doi-asserted-by":"publisher","first-page":"797","DOI":"10.23638\/LMCS-13(2:4)2017","volume":"27","author":"G Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. JACM 27(4), 797\u2013821 (1980). doi: 10.23638\/LMCS-13(2:4)2017","journal-title":"JACM"},{"issue":"4","key":"24_CR13","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). doi: 10.1137\/0215084","journal-title":"SIAM J. Comput."},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"Kahrs, S., Smith, C.: Non- $$\\omega $$ -overlapping TRSs are UN. In: Proceedings of 1st FSCD. LIPIcs, vol. 52, pp. 22: 1\u201322: 17 (2016). doi: 10.4230\/LIPIcs.FSCD.2016.22","DOI":"10.4230\/LIPIcs.FSCD.2016.22"},{"key":"24_CR15","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 2012. LNCS, vol. 7180, pp. 258\u2013273. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28717-6_21"},{"key":"24_CR16","unstructured":"Klop, J.: Combinatory reduction systems. Ph.D. thesis, Utrecht University (1980)"},{"key":"24_CR17","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D Knuth","year":"1970","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, Oxford (1970)"},{"key":"24_CR18","unstructured":"Kop, C.: Higher order termination. Ph.D. thesis, Vrije Universiteit, Amsterdam (2012)"},{"issue":"10","key":"24_CR19","first-page":"2007","volume":"92\u2013D","author":"K Kusakari","year":"2009","unstructured":"Kusakari, K., Isogai, Y., Sakai, M., Blanqui, F.: Static dependency pair method based on strong computability for higher-order rewrite systems. IEICE TIS 92\u2013D(10), 2007\u20132015 (2009)","journal-title":"IEICE TIS"},{"issue":"1","key":"24_CR20","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. TCS 192(1), 3\u201329 (1998). doi: 10.1016\/S0304-3975(97)00143-6","journal-title":"TCS"},{"issue":"4","key":"24_CR21","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. JLP 1(4), 497\u2013536 (1991). doi: 10.1093\/logcom\/1.4.497","journal-title":"JLP"},{"key":"24_CR22","doi-asserted-by":"publisher","unstructured":"Nagele, J., Felgenhauer, B., Middeldorp, A.: Improving automatic confluence analysis of rewrite systems by redundant rules. In: Proceedings of 26th RTA. LIPIcs, vol. 36, pp. 257\u2013268 (2015). doi: 10.4230\/LIPIcs.RTA.2015.257","DOI":"10.4230\/LIPIcs.RTA.2015.257"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Nagele, J., Felgenhauer, B., Zankl, H.: Certifying confluence proofs via relative termination and rule labeling. LMCS (to appear) (2017)","DOI":"10.23638\/LMCS-13(2:4)2017"},{"key":"24_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). doi: 10.1007\/978-3-319-43144-4_18"},{"key":"24_CR25","unstructured":"Nagele, J., Thiemann, R.: Certification of confluence proofs using CeTA. In: Proceedings of 3rd IWC, pp. 19\u201323 (2014)"},{"issue":"2","key":"24_CR26","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.: Fast decision procedures based on congruence closure. JACM 27(2), 356\u2013364 (1980). doi: 10.1145\/322186.322198","journal-title":"JACM"},{"key":"24_CR27","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proceedings of 6th LICS, pp. 342\u2013349 (1991). doi: 10.1109\/LICS.1991.151658","DOI":"10.1109\/LICS.1991.151658"},{"key":"24_CR28","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Functional unification of higher-order patterns. In: Proceedings of 8th LICS, pp. 64\u201374 (1993). doi: 10.1109\/LICS.1993.287599","DOI":"10.1109\/LICS.1993.287599"},{"issue":"1","key":"24_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. TCS 175(1), 159\u2013181 (1997). doi: 10.1016\/S0304-3975(96)00173-9","journal-title":"TCS"},{"key":"24_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/3-540-58140-5_35","volume-title":"Logical Foundations of Computer Science","author":"V van Oostrom","year":"1994","unstructured":"van Oostrom, V., Raamsdonk, F.: Weak orthogonality implies confluence: the higher-order case. In: Nerode, A., Matiyasevich, Y.V. (eds.) LFCS 1994. LNCS, vol. 813, pp. 379\u2013392. Springer, Heidelberg (1994). doi: 10.1007\/3-540-58140-5_35"},{"key":"24_CR31","unstructured":"Oyamaguchi, M., Hirokawa, N.: Confluence and critical-pair-closing systems. In: Proceedings of 3rd IWC, pp. 29\u201333 (2014)"},{"issue":"2","key":"24_CR32","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"GE Peterson","year":"1981","unstructured":"Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. JACM 28(2), 233\u2013264 (1981). doi: 10.1145\/322248.322251","journal-title":"JACM"},{"key":"24_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-45127-7_20","volume-title":"Rewriting Techniques and Applications","author":"F van Raamsdonk","year":"2001","unstructured":"van Raamsdonk, F.: On termination of higher-order rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 261\u2013275. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45127-7_20"},{"issue":"2","key":"24_CR34","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0304-3975(94)90012-4","volume":"126","author":"L Regnier","year":"1994","unstructured":"Regnier, L.: Une \u00e9quivalence sur les lambda-termes. TCS 126(2), 281\u2013292 (1994). doi: 10.1016\/0304-3975(94)90012-4","journal-title":"TCS"},{"issue":"1","key":"24_CR35","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. JACM 20(1), 160\u2013187 (1973). doi: 10.1145\/321738.321750","journal-title":"JACM"},{"issue":"2","key":"24_CR36","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. I&C 178(2), 515\u2013533 (2002). doi: 10.1006\/inco.2002.3158","journal-title":"I&C"},{"key":"24_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-21401-6_7","volume-title":"Automated Deduction - CADE-25","author":"M Sakai","year":"2015","unstructured":"Sakai, M., Oyamaguchi, M., Ogawa, M.: Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 111\u2013126. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_7"},{"key":"24_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-21401-6_8","volume-title":"Automated Deduction - CADE-25","author":"K Shintani","year":"2015","unstructured":"Shintani, K., Hirokawa, N.: CoLL: A confluence tool for left-linear term rewrite systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 127\u2013136. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_8"},{"key":"24_CR39","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: Proceedings of 24th RTA. LIPIcs, vol. 21, pp. 287\u2013302 (2013).doi: 10.4230\/LIPIcs.RTA.2013.287","DOI":"10.4230\/LIPIcs.RTA.2013.287"},{"key":"24_CR40","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: Proceedings of 11th UITP. EPTCS, vol. 167, pp. 61\u201372 (2014). doi: 10.4204\/EPTCS.167.8","DOI":"10.4204\/EPTCS.167.8"},{"key":"24_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452\u2013468. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03359-9_31"},{"key":"24_CR42","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 Publishing, North Holland (1988)"},{"key":"24_CR43","doi-asserted-by":"publisher","unstructured":"Toyama, Y., Oyamaguchi, M.: Church-Rosser property and unique normal form property of non-duplicating term rewriting systems. In: Proceedings of the 4th CTRS withDershowitz N., Lindenstrauss N. (eds.) CTRS 1994. LNCS, vol. 968 (1995). doi: 10.1007\/3-540-60381-6_19","DOI":"10.1007\/3-540-60381-6_19"},{"key":"24_CR44","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 2011. LNCS, vol. 6803, pp. 499\u2013505. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_38"},{"issue":"2","key":"24_CR45","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. JAR 54(2), 101\u2013133 (2015). doi: 10.1007\/s10817-014-9316-y","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:24:59Z","timestamp":1750533899000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}