{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:27:59Z","timestamp":1742956079424,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"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_11","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"163-178","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Reducing Relative Termination to Dependency Pair Problems"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Iborra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Nishida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Germ\u00e1n","family":"Vidal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-16310-4_4","volume-title":"Rewriting Logic and Its Applications","author":"B Alarc\u00f3n","year":"2010","unstructured":"Alarc\u00f3n, B., Lucas, S., Meseguer, J.: A dependency pair framework for A\n\t\t\t\t\t$$\\vee $$\n\t\t\t\t\tC-termination. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 35\u201351. Springer, Heidelberg (2010)"},{"issue":"1\u20132","key":"11_CR2","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(1\u20132), 133\u2013178 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR3","unstructured":"Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical report AIB-2001-09, RWTH Aachen (2001)"},{"key":"11_CR4","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)"},{"issue":"1&2","key":"11_CR5","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3(1&2), 69\u2013115 (1987)","journal-title":"J. Symb. Comput."},{"issue":"2\u20133","key":"11_CR6","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J Endrullis","year":"2008","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reasoning 40(2\u20133), 195\u2013220 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"11_CR7","unstructured":"Geser, A.: Relative termination. Dissertation, Fakult\u00e4t f\u00fcr Mathematik und Informatik, Universit\u00e4t Passau, Germany (1990)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-45127-7_9","volume-title":"Rewriting Techniques and Applications","author":"J Giesl","year":"2001","unstructured":"Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 93\u2013107. Springer, Heidelberg (2001)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 4130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"issue":"3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reasoning 37(3), 155\u2013203 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-540-30210-0_16","volume-title":"Artificial Intelligence and Symbolic Computation","author":"N Hirokawa","year":"2004","unstructured":"Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: Buchberger, B., Campbell, J. (eds.) AISC 2004. LNCS (LNAI), vol. 3249, pp. 185\u2013198. Springer, Heidelberg (2004)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-25979-4_18","volume-title":"Rewriting Techniques and Applications","author":"N Hirokawa","year":"2004","unstructured":"Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249\u2013268. Springer, Heidelberg (2004)"},{"issue":"4","key":"11_CR13","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"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction Les Arcs,","author":"JM Hullot","year":"1980","unstructured":"Hullot, J.M.: Canonical forms and unification. CADE-5. LNCS, vol. 87, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-12592-8_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J Iborra","year":"2010","unstructured":"Iborra, J., Nishida, N., Vidal, G.: Goal-directed and relative dependency pairs for proving the termination of narrowing. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 52\u201366. Springer, Heidelberg (2010)"},{"key":"11_CR16","unstructured":"Kamin, S., L\u00e9vy, J.J.: Two generalizations of the recursive path ordering (1980, unpublished note)"},{"key":"11_CR17","first-page":"143","volume":"32","author":"JW Klop","year":"1987","unstructured":"Klop, J.W.: Term rewriting systems: a tutorial. Bull. Eur. Assoc. Theor. Comput. Sci. 32, 143\u2013183 (1987)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci."},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/11559306_13","volume-title":"Frontiers of Combining Systems","author":"A Koprowski","year":"2005","unstructured":"Koprowski, A., Zantema, H.: Proving liveness with fairness using rewriting. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 232\u2013247. Springer, Heidelberg (2005)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11805618_19","volume-title":"Term Rewriting and Applications","author":"A Koprowski","year":"2006","unstructured":"Koprowski, A.: TPA: termination proved automatically. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 257\u2013266. Springer, Heidelberg (2006)"},{"key":"11_CR20","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)"},{"key":"11_CR21","unstructured":"Lankford, D.: Canonical algebraic simplification in computational logic. Technical report ATP-25, University of Texas (1975)"},{"key":"11_CR22","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)"},{"issue":"3","key":"11_CR23","first-page":"52","volume":"86","author":"N Nishida","year":"2003","unstructured":"Nishida, N., Sakai, M., Sakabe, T.: Narrowing-based simulation of term rewriting systems with extra variables. ENTCS 86(3), 52\u201369 (2003)","journal-title":"ENTCS"},{"issue":"3","key":"11_CR24","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s00200-010-0122-4","volume":"21","author":"N Nishida","year":"2010","unstructured":"Nishida, N., Vidal, G.: Termination of narrowing via termination of rewriting. Appl. Algebra Eng. Commun. Comput. 21(3), 177\u2013225 (2010)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"11_CR25","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-Verlag, London (2002)"},{"key":"11_CR26","unstructured":"Thiemann, R., Allais, G., Nagele, J.: On the formalization of termination techniques based on multiset orderings. In: RTA 2012. LIPIcs, vol. 15, pp. 339\u2013354. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-78969-7_10","volume-title":"Functional and Logic Programming","author":"G Vidal","year":"2008","unstructured":"Vidal, G.: Termination of narrowing in left-linear constructor systems. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 113\u2013129. Springer, Heidelberg (2008)"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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-TLCA 2014. LNCS, vol. 8560, pp. 466\u2013475. Springer, Heidelberg (2014)"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Sci. Comput. Program. (2014). doi:10.1016\/j.scico.2014.07.009","DOI":"10.1016\/j.scico.2014.07.009"},{"issue":"1\/2","key":"11_CR30","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","volume":"24","author":"H Zantema","year":"1995","unstructured":"Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24(1\/2), 89\u2013105 (1995)","journal-title":"Fundamenta Informaticae"},{"key":"11_CR31","series-title":"Cambridge Tracts in Theoretical Computer Science","first-page":"181","volume-title":"Term Rewriting Systems","author":"H Zantema","year":"2003","unstructured":"Zantema, H.: Termination. In: Bezem, M., Klop, J.W., de Vrijer, R. (eds.) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 181\u2013259. Cambridge University Press, Cambridge (2003)"}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T09:46:26Z","timestamp":1676972786000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_11","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"}}]}}