{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:17:47Z","timestamp":1759033067620,"version":"3.37.3"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,7,25]],"date-time":"2022-07-25T00:00:00Z","timestamp":1658707200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,7,25]],"date-time":"2022-07-25T00:00:00Z","timestamp":1658707200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["ERATO HASUO Project"],"award-info":[{"award-number":["ERATO HASUO Project"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["Y757","P27502"],"award-info":[{"award-number":["Y757","P27502"]}],"id":[{"id":"10.13039\/501100002428","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":[[2022,11]]},"DOI":"10.1007\/s10817-022-09640-4","type":"journal-article","created":{"date-parts":[[2022,7,25]],"date-time":"2022-07-25T17:04:05Z","timestamp":1658768645000},"page":"667-688","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Tuple Interpretations for Termination of Term Rewriting"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8872-2240","authenticated-orcid":false,"given":"Akihisa","family":"Yamada","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,25]]},"reference":[{"issue":"1\u20132","key":"9640_CR1","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). https:\/\/doi.org\/10.1016\/S0304-3975(99)00207-8","journal-title":"Theor. Comput. Sci."},{"key":"9640_CR2","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)"},{"key":"9640_CR3","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"9640_CR4","doi-asserted-by":"publisher","unstructured":"Ben-Amram, A.M., Codish, M.: A SAT-based approach to size change termination with global ranking functions. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 218\u2013232. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_16","DOI":"10.1007\/978-3-540-78800-3_16"},{"issue":"4","key":"9640_CR5","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). https:\/\/doi.org\/10.1017\/S0960129511000120","journal-title":"Math. Struct. Comput. Sci."},{"key":"9640_CR6","doi-asserted-by":"publisher","unstructured":"Contejean, \u00c9., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Schmidt-Schau\u00df, M. (ed.) RTA 2011. LIPIcs, vol.\u00a010, pp. 21\u201330. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl (2011). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2011.21","DOI":"10.4230\/LIPIcs.RTA.2011.21"},{"key":"9640_CR7","doi-asserted-by":"publisher","unstructured":"Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretation. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorn\u00fd, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol.\u00a05901, pp. 283\u2013295. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11266-9_24","DOI":"10.1007\/978-3-642-11266-9_24"},{"key":"9640_CR8","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9640_CR9","doi-asserted-by":"publisher","unstructured":"Dershowitz, N.: 33 examples of termination. In: Comon, H., Jounnaud, J.P. (eds.) Term Rewriting. pp. 16\u201326. Springer, Cham (1995). https:\/\/doi.org\/10.1007\/3-540-59340-3_2","DOI":"10.1007\/3-540-59340-3_2"},{"issue":"2\u20133","key":"9640_CR10","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. Reason. 40(2\u20133), 195\u2013220 (2008). https:\/\/doi.org\/10.1007\/s10817-007-9087-9","journal-title":"J. Autom. Reason."},{"key":"9640_CR11","doi-asserted-by":"publisher","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol.\u00a05117, pp. 110\u2013125. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70590-1_8","DOI":"10.1007\/978-3-540-70590-1_8"},{"key":"9640_CR12","doi-asserted-by":"publisher","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_21","DOI":"10.1007\/978-3-540-32275-7_21"},{"issue":"3","key":"9640_CR13","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. Reason. 37(3), 155\u2013203 (2006). https:\/\/doi.org\/10.1007\/s10817-006-9057-7","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9640_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58(1), 3\u201331 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9388-y","journal-title":"J. Autom. Reason."},{"key":"9640_CR15","doi-asserted-by":"publisher","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019 (3). LNCS, vol. 11429, pp. 156\u2013166. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"9640_CR16","doi-asserted-by":"publisher","unstructured":"Guti\u00e9rrez, R., Lucas, S.: mu-term: Verify termination properties automatically (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020 (2). LNCS, vol. 12167, pp. 436\u2013447. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_28","DOI":"10.1007\/978-3-030-51054-1_28"},{"key":"9640_CR17","doi-asserted-by":"publisher","unstructured":"Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 249\u2013268. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-25979-4_18","DOI":"10.1007\/978-3-540-25979-4_18"},{"key":"9640_CR18","doi-asserted-by":"publisher","unstructured":"Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNAI, vol.\u00a03249, pp. 185\u2013198. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30210-0_16","DOI":"10.1007\/978-3-540-30210-0_16"},{"key":"9640_CR19","doi-asserted-by":"publisher","unstructured":"Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 328\u2013342. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11805618_25","DOI":"10.1007\/11805618_25"},{"key":"9640_CR20","doi-asserted-by":"publisher","unstructured":"Jouannaud, J., Rubio, A.: The higher-order recursive path ordering. In: LICS 1999, pp. 402\u2013411. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782635","DOI":"10.1109\/LICS.1999.782635"},{"key":"9640_CR21","doi-asserted-by":"publisher","unstructured":"Kop, C., Vale, D.: Tuple interpretations for higher-order complexity. In: Kobayashi, N. (ed.) FSCD 2021. LIPIcs, vol.\u00a0195, pp. 31:1\u201331:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Wadern (2021). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2021.31","DOI":"10.4230\/LIPIcs.FSCD.2021.31"},{"key":"9640_CR22","doi-asserted-by":"publisher","unstructured":"Kop, C., van Raamsdonk, F.: Dynamic dependency pairs for algebraic functional systems. Log. Methods Comput. Sci. (2012). https:\/\/doi.org\/10.2168\/LMCS-8(2:10)2012","DOI":"10.2168\/LMCS-8(2:10)2012"},{"issue":"2","key":"9640_CR23","first-page":"357","volume":"19","author":"A Koprowski","year":"2009","unstructured":"Koprowski, A., Waldmann, J.: Max\/plus tree automata for termination of term rewriting. Acta Cybern. 19(2), 357\u2013392 (2009)","journal-title":"Acta Cybern."},{"key":"9640_CR24","doi-asserted-by":"publisher","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool\u00a02. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 295\u2013304. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_21","DOI":"10.1007\/978-3-642-02348-4_21"},{"key":"9640_CR25","doi-asserted-by":"publisher","unstructured":"Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol.\u00a01702, pp. 47\u201361. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/10704567_3","DOI":"10.1007\/10704567_3"},{"key":"9640_CR26","unstructured":"Lankford, D.: Canonical algebraic simplification in computational logic. Tech. Rep. ATP-25, University of Texas (1975)"},{"issue":"4","key":"9640_CR27","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s10817-017-9419-3","volume":"60","author":"S Lucas","year":"2018","unstructured":"Lucas, S., Guti\u00e9rrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465\u2013501 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9419-3","journal-title":"J. Autom. Reason."},{"key":"9640_CR28","unstructured":"Manna, Z., Ness, S.: On the termination of Markov algorithms. In: The 3rd Hawaii International Conference on System Science, pp. 789\u2013792 (1970)"},{"key":"9640_CR29","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: Benzm\u00fcller, C., Paleo, B.W. (eds.) UITP 2014. EPTCS, vol.\u00a0167, pp. 61\u201372 (2014). https:\/\/doi.org\/10.4204\/EPTCS.167.8","DOI":"10.4204\/EPTCS.167.8"},{"key":"9640_CR30","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: Formalizing monotone algebras for certification of termination and complexity proofs. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol.\u00a08560, pp. 441\u2013455. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_30","DOI":"10.1007\/978-3-319-08918-8_30"},{"key":"9640_CR31","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR. LNCS, vol.\u00a08562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"9640_CR32","doi-asserted-by":"publisher","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.\u00a05674, pp. 452\u2013468. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_31","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"9640_CR33","doi-asserted-by":"publisher","unstructured":"Thiemann, R., Sch\u00f6pf, J., Sternagel, C., Yamada, A.: Certifying the Weighted Path Order (Invited Talk). In: Ariola, Z.M. (ed.) FSCD 2020. LIPIcs, vol.\u00a0167, pp. 4:1\u20134:20. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.4","DOI":"10.4230\/LIPIcs.FSCD.2020.4"},{"key":"9640_CR34","unstructured":"TPDB: The termination problem data base. http:\/\/termination-portal.org\/wiki\/TPDB"},{"key":"9640_CR35","unstructured":"Watson, T., Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness, and implementation of abstract data types. In: Current Trends in Programming Methodology. Prentice Hall, Englewood Cliffs (1976)"},{"key":"9640_CR36","doi-asserted-by":"publisher","unstructured":"Yamada, A.: Multi-dimensional interpretations for termination of term rewriting. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28. LNCS, vol. 12699, pp. 273\u2013290. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_16","DOI":"10.1007\/978-3-030-79876-5_16"},{"key":"9640_CR37","doi-asserted-by":"publisher","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Nagoya Termination Tool. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol.\u00a08560, pp. 466\u2013475. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_32","DOI":"10.1007\/978-3-319-08918-8_32"},{"key":"9640_CR38","doi-asserted-by":"publisher","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 order for termination proving. Sci. Comput. Program. 111, 110\u2013134 (2015). https:\/\/doi.org\/10.1016\/j.scico.2014.07.009","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"9640_CR39","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H Zantema","year":"1994","unstructured":"Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17(1), 23\u201350 (1994). https:\/\/doi.org\/10.1006\/jsco.1994.1003","journal-title":"J. Symb. Comput."},{"issue":"1\/2","key":"9640_CR40","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s002000100061","volume":"12","author":"H Zantema","year":"2001","unstructured":"Zantema, H.: The termination hierarchy for term rewriting. Appl. Algebr. Eng. Commun. Comput. 12(1\/2), 3\u201319 (2001). https:\/\/doi.org\/10.1007\/s002000100061","journal-title":"Appl. Algebr. Eng. Commun. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09640-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09640-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09640-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,5]],"date-time":"2022-11-05T11:19:38Z","timestamp":1667647178000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09640-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,25]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9640"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09640-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2022,7,25]]},"assertion":[{"value":"4 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 June 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 July 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}