{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:04:42Z","timestamp":1750089882868},"publisher-location":"Cham","reference-count":34,"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_26","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"413-431","source":"Crossref","is-referenced-by-count":2,"title":["Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems"],"prefix":"10.1007","author":[{"given":"Christian","family":"Sternagel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Sternagel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-17796-5_12","volume-title":"Algebraic Methodology and Software Technology","author":"B Alarc\u00f3n","year":"2011","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201\u2013208. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-17796-5_12"},{"issue":"4","key":"26_CR2","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1721654.1721675","volume":"53","author":"S Antoy","year":"2010","unstructured":"Antoy, S., Hanus, M.: Functional logic programming. Commun. ACM 53(4), 74\u201385 (2010). doi: 10.1145\/1721654.1721675","journal-title":"Commun. ACM"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-319-21401-6_5","volume-title":"Automated Deduction \u2013 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 (LNAI), vol. 9195, pp. 101\u2013104. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_5"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/3-540-58216-9_40","volume-title":"Logic Programming and Automated Reasoning","author":"J Avenhaus","year":"1994","unstructured":"Avenhaus, J., Lor\u00eda-S\u00e1enz, C.: On conditional rewrite systems with extra variables and deterministic logic programs. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 215\u2013229. Springer, Heidelberg (1994). doi: 10.1007\/3-540-58216-9_40"},{"key":"26_CR5","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)"},{"key":"26_CR6","unstructured":"Blanchette, J., Paulson, L.: Hammering away - a user\u2019s guide to sledgehammer for Isabelle\/HOL (2010). https:\/\/isabelle.in.tum.de\/dist\/doc\/sledgehammer.pdf"},{"issue":"1","key":"26_CR7","doi-asserted-by":"publisher","first-page":"101","DOI":"10.6092\/issn.1972-5787\/4593","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101\u2013148 (2016). doi: 10.6092\/issn.1972-5787\/4593","journal-title":"J. Formalized Reasoning"},{"issue":"4","key":"26_CR8","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"21","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21(4), 827\u2013859 (2011). doi: 10.1017\/S0960129511000120","journal-title":"Math. Struct. Comput. Sci."},{"key":"26_CR9","doi-asserted-by":"publisher","unstructured":"Contejean, \u00c9., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with C $$i$$ ME 3 In: Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA). LIPIcs, vol. 10, pp. 21\u201330. Schloss Dagstuhl (2011), doi: 10.4230\/LIPIcs.RTA.2011.21","DOI":"10.4230\/LIPIcs.RTA.2011.21"},{"key":"26_CR10","unstructured":"Cops: The confluence problems database. http:\/\/cops.uibk.ac.at\/?q=ctrs"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 281\u2013286. Springer, Heidelberg (2006). doi: 10.1007\/11814771_24"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/11559306_12","volume-title":"Frontiers of Combining Systems","author":"J Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 216\u2013231. Springer, Heidelberg (2005). doi: 10.1007\/11559306_12"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-319-21401-6_6","volume-title":"Automated Deduction \u2013 CADE-25","author":"J Giesl","year":"2015","unstructured":"Giesl, J., Mesnard, F., Rubio, A., Thiemann, R., Waldmann, J.: Termination competition (termCOMP 2015). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 105\u2013108. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_6"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-08970-6_19","volume-title":"Interactive Theorem Proving","author":"N Hirokawa","year":"2014","unstructured":"Hirokawa, N., Middeldorp, A., Sternagel, C.: A new and formalized proof of abstract completion. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 292\u2013307. Springer, Cham (2014). doi: 10.1007\/978-3-319-08970-6_19"},{"issue":"4","key":"26_CR15","doi-asserted-by":"crossref","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":"26_CR16","doi-asserted-by":"crossref","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 (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"26_CR17","unstructured":"Kop, C.: Higher-order termination: automatable techniques for proving termination of higher-order term rewriting systems. Ph.D. thesis, VU University Amsterdam (2012). http:\/\/hdl.handle.net\/1871\/39346"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-02348-4_21","volume-title":"Rewriting Techniques and Applications","author":"M Korp","year":"2009","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295\u2013304. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02348-4_21"},{"issue":"4","key":"26_CR19","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1016\/j.ipl.2005.05.002","volume":"95","author":"S Lucas","year":"2005","unstructured":"Lucas, S., March\u00e9, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95(4), 446\u2013453 (2005). doi: 10.1016\/j.ipl.2005.05.002","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"26_CR20","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1016\/j.jlamp.2016.03.003","volume":"86","author":"S Lucas","year":"2017","unstructured":"Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Logical Algebraic Methods Program. 86(1), 236\u2013268 (2017). doi: 10.1016\/j.jlamp.2016.03.003","journal-title":"J. Logical Algebraic Methods Program."},{"key":"26_CR21","unstructured":"Marlow, S.: Haskell 2010 language report. https:\/\/www.haskell.org\/definition\/haskell2010.pdf"},{"issue":"2","key":"26_CR22","doi-asserted-by":"crossref","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."},{"issue":"2","key":"26_CR23","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0167-6423(89)90038-5","volume":"12","author":"T Nipkow","year":"1989","unstructured":"Nipkow, T.: Equational reasoning in Isabelle. Sci. Comput. Program. 12(2), 123\u2013149 (1989). doi: 10.1016\/0167-6423(89)90038-5","journal-title":"Sci. Comput. Program."},{"key":"26_CR24","doi-asserted-by":"crossref","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, New York (2002)"},{"key":"26_CR25","unstructured":"Sternagel, C., Sternagel, T.: Level-confluence of 3-CTRSs in Isabelle\/HOL. In: Proceedings of the 4th International Workshop on Confluence (IWC), arXiv:1602.07115 (2015)"},{"key":"26_CR26","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Sternagel, T.: Certifying confluence of almost orthogonal CTRSs via exact tree automata completion. In: Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD). LIPIcs, vol. 51, pp. 29:1\u201329:16 (2016). doi: 10.4230\/LIPIcs.FSCD.2016.29","DOI":"10.4230\/LIPIcs.FSCD.2016.29"},{"key":"26_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-319-08918-8_31","volume-title":"Rewriting and Typed Lambda Calculi","author":"T Sternagel","year":"2014","unstructured":"Sternagel, T., Middeldorp, A.: Conditional confluence (system description). In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 456\u2013465. Springer, Cham (2014). doi: 10.1007\/978-3-319-08918-8_31"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"Sternagel, T., Sternagel, C.: Formalized confluence of quasi-decreasing, strongly deterministic conditional TRSs. In: Proceedings of the 5th International Workshop on Confluence (IWC), arXiv:1609.03341 (2016)","DOI":"10.1007\/978-3-319-63046-5_26"},{"key":"26_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). doi: 10.1007\/978-3-319-08587-6_28"},{"key":"26_CR30","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":"26_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-540-25979-4_6","volume-title":"Rewriting Techniques and Applications","author":"J Waldmann","year":"2004","unstructured":"Waldmann, J.: Matchbox: a tool for match-bounded string rewriting. In: Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 85\u201394. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-25979-4_6"},{"key":"26_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-319-24246-0_15","volume-title":"Frontiers of Combining Systems","author":"S Winkler","year":"2015","unstructured":"Winkler, S., Thiemann, R.: Formalizing soundness and completeness of unravelings. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 239\u2013255. Springer, Cham (2015). doi: 10.1007\/978-3-319-24246-0_15"},{"key":"26_CR33","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). doi: 10.1007\/978-3-319-08918-8_32"},{"key":"26_CR34","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"}],"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_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,29]],"date-time":"2019-09-29T08:28:38Z","timestamp":1569745718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}