{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:53:59Z","timestamp":1781927639061,"version":"3.54.5"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,4,30]],"date-time":"2016-04-30T00:00:00Z","timestamp":1461974400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["Y757"],"award-info":[{"award-number":["Y757"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"publisher","award":["TIN2013-44742-C4-1-R"],"award-info":[{"award-number":["TIN2013-44742-C4-1-R"]}],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003359","name":"Generalitat Valenciana","doi-asserted-by":"publisher","award":["PROMETEOII2015\/013"],"award-info":[{"award-number":["PROMETEOII2015\/013"]}],"id":[{"id":"10.13039\/501100003359","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s10817-016-9373-5","type":"journal-article","created":{"date-parts":[[2016,4,30]],"date-time":"2016-04-30T07:10:50Z","timestamp":1462000250000},"page":"391-411","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Relative Termination via Dependency Pairs"],"prefix":"10.1007","volume":"58","author":[{"given":"Jos\u00e9","family":"Iborra","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Naoki","family":"Nishida","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Germ\u00e1n","family":"Vidal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8872-2240","authenticated-orcid":false,"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,4,30]]},"reference":[{"key":"9373_CR1","unstructured":"Alarc\u00f3n, B., Lucas, S., Meseguer, J.: A dependency pair framework for A $$\\vee $$ \u2228 C-termination. In: WRLA 2010, LNCS, vol. 6381, pp. 36\u201352. Springer (2010)"},{"issue":"1\u20132","key":"9373_CR2","doi-asserted-by":"crossref","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":"9373_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":"9373_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)"},{"key":"9373_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L Bachmair","year":"1988","unstructured":"Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. J. Symb. Comput. 6, 1\u201318 (1988)","journal-title":"J. Symb. Comput."},{"key":"9373_CR6","doi-asserted-by":"crossref","unstructured":"Bonacina, M., Hsiang, J.: On fairness of completion-based theorem proving strategies. In: RTA 1991, LNCS, vol. 488, pp. 348\u2013360. Springer (1991)","DOI":"10.1007\/3-540-53904-2_109"},{"issue":"1&2","key":"9373_CR7","doi-asserted-by":"crossref","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":"9373_CR8","doi-asserted-by":"crossref","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. Reason. 40(2\u20133), 195\u2013220 (2008)","journal-title":"J. Autom. Reason."},{"key":"9373_CR9","volume-title":"Relative Termination. Dissertation, Fakult\u00e4t f\u00fcr Mathematik und Informatik","author":"A Geser","year":"1990","unstructured":"Geser, A.: Relative Termination. Dissertation, Fakult\u00e4t f\u00fcr Mathematik und Informatik. Universit\u00e4t Passau, Germany (1990)"},{"key":"9373_CR10","doi-asserted-by":"crossref","unstructured":"Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: RTA 2001, LNCS, vol. 2051, pp. 93\u2013107. Springer (2001)","DOI":"10.1007\/3-540-45127-7_9"},{"key":"9373_CR11","doi-asserted-by":"crossref","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: IJCAR 2006, LNCS, vol. 4130, pp. 281\u2013286. Springer (2006)","DOI":"10.1007\/11814771_24"},{"issue":"3","key":"9373_CR12","doi-asserted-by":"crossref","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. Reason. 37(3), 155\u2013203 (2006)","journal-title":"J. Autom. Reason."},{"key":"9373_CR13","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: RTA 2004, LNCS, vol. 3091, pp. 249\u2013268. Springer (2004)","DOI":"10.1007\/978-3-540-25979-4_18"},{"key":"9373_CR14","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: AISC 2004, LNAI, vol. 3249, pp. 185\u2013198. Springer (2004)","DOI":"10.1007\/978-3-540-30210-0_16"},{"issue":"4","key":"9373_CR15","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1016\/j.ic.2006.08.010","volume":"205","author":"N Hirokawa","year":"2007","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: techniques and features. Inf. Comput. 205(4), 474\u2013511 (2007)","journal-title":"Inf. Comput."},{"issue":"4","key":"9373_CR16","doi-asserted-by":"crossref","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. Reason. 47(4), 481\u2013501 (2011)","journal-title":"J. Autom. Reason."},{"key":"9373_CR17","doi-asserted-by":"crossref","unstructured":"Hullot, J.M.: Canonical forms and unification. In: CADE 1980, LNCS, vol.\u00a087, pp. 318\u2013334. Springer (1980)","DOI":"10.1007\/3-540-10009-1_25"},{"key":"9373_CR18","doi-asserted-by":"crossref","unstructured":"Iborra, J., Nishida, N., Vidal, G.: Goal-directed and relative dependency pairs for proving the termination of narrowing. In: LOPSTR 2009, LNCS, vol. 6037, pp. 52\u201366. Springer (2010)","DOI":"10.1007\/978-3-642-12592-8_5"},{"key":"9373_CR19","doi-asserted-by":"crossref","unstructured":"Iborra, J., Nishida, N., Vidal, G., Yamada, A.: Reducing relative termination to dependency pair problems. In: CADE-25, LNAI, vol. 9195, pp. 163\u2013178. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_11"},{"key":"9373_CR20","unstructured":"Kamin, S., L\u00e9vy, J.J.: Two generalizations of the recursive path ordering (1980). Unpublished note"},{"key":"9373_CR21","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":"9373_CR22","doi-asserted-by":"crossref","unstructured":"Koprowski, A.: TPA: termination proved automatically. In: RTA 2006, LNCS, vol. 4098, pp. 257\u2013266. Springer (2006)","DOI":"10.1007\/11805618_19"},{"key":"9373_CR23","doi-asserted-by":"crossref","unstructured":"Koprowski, A., Zantema, H.: Proving liveness with fairness using rewriting. In: FroCoS 2005, LNCS, vol. 3717, pp. 232\u2013247. Springer (2005)","DOI":"10.1007\/11559306_13"},{"key":"9373_CR24","doi-asserted-by":"crossref","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: RTA 2009, LNCS, vol. 5595, pp. 295\u2013304. Springer (2009)","DOI":"10.1007\/978-3-642-02348-4_21"},{"issue":"5","key":"9373_CR25","first-page":"439","volume":"E84\u2013D","author":"K Kusakari","year":"2001","unstructured":"Kusakari, K., Toyama, Y.: On proving AC-termination by AC-dependency pairs. IEICE Trans. Inf. Syst. E84\u2013D(5), 439\u2013447 (2001)","journal-title":"IEICE Trans. Inf. Syst."},{"key":"9373_CR26","unstructured":"Lankford, D.: Canonical algebraic simplification in computational logic. Technical report ATP-25, University of Texas (1975)"},{"issue":"1","key":"9373_CR27","doi-asserted-by":"crossref","first-page":"873","DOI":"10.1016\/j.jsc.2004.02.003","volume":"38","author":"C March\u00e9","year":"2004","unstructured":"March\u00e9, C., Urbain, X.: Modular and incremental proofs of AC-termination. J. Symb. Comput. 38(1), 873\u2013897 (2004)","journal-title":"J. Symb. Comput."},{"issue":"3","key":"9373_CR28","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":"9373_CR29","doi-asserted-by":"crossref","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":"9373_CR30","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, London (2002)"},{"issue":"4","key":"9373_CR31","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J Slagle","year":"1974","unstructured":"Slagle, J.: Automated theorem-proving for theories with simplifiers commutativity and associativity. J. ACM 21(4), 622\u2013642 (1974)","journal-title":"J. ACM"},{"key":"9373_CR32","unstructured":"Thiemann, R., Allais, G., Nagele, J.: On the formalization of termination techniques based on multiset orderings. In: RTA 2012, LIPIcs, vol.\u00a015, pp. 339\u2013354. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"9373_CR33","doi-asserted-by":"crossref","unstructured":"Vidal, G.: Termination of narrowing in left-linear constructor systems. In: FLOPS 2008, LNCS, vol. 4989, pp. 113\u2013129. Springer (2008)","DOI":"10.1007\/978-3-540-78969-7_10"},{"key":"9373_CR34","doi-asserted-by":"crossref","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Nagoya termination tool. In: RTA-TLCA 2014, LNCS, pp. 466\u2013475. Springer (2014)","DOI":"10.1007\/978-3-319-08918-8_32"},{"key":"9373_CR35","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/j.scico.2014.07.009","volume":"111","author":"A Yamada","year":"2015","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Sci. Comput. Program. 111, 110\u2013134 (2015)","journal-title":"Sci. Comput. Program."},{"issue":"1\/2","key":"9373_CR36","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. Fundam. Inf. 24(1\/2), 89\u2013105 (1995)","journal-title":"Fundam. Inf."},{"key":"9373_CR37","unstructured":"Zantema, H.: Termination. In: Bezem, M., Klop, J. W., de Vrijer, R. (eds.) Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, chap. 6, vol. 55, pp. 181\u2013259. Cambridge University Press, Cambridge (2003)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9373-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9373-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9373-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9373-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,19]],"date-time":"2020-09-19T08:19:55Z","timestamp":1600503595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9373-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,30]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["9373"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9373-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,30]]}}}