{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:22:41Z","timestamp":1743139361140,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Interpretation methods constitute a foundation of termination analysis for term rewriting. From time to time remarkable instances of interpretation methods appeared, such as polynomial interpretations, matrix interpretations, arctic interpretations, and their variants. In this paper we introduce a general framework, the multi-dimensional interpretation method, that subsumes these variants as well as many previously unknown interpretation methods as instances. Employing the notion of derivers, we prove the soundness of the proposed method in an elegant way. We implement the proposed method in the termination prover  and verify its significance through experiments.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_16","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"273-290","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Multi-Dimensional Interpretations for Termination of Term Rewriting"],"prefix":"10.1007","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":[[2021,7,5]]},"reference":[{"issue":"1\u20132","key":"16_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. Compt. Sci. 236(1\u20132), 133\u2013178 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00207-8","journal-title":"Theor. Compt. Sci."},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"16_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 (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"issue":"4","key":"16_CR4","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":"16_CR5","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. 10, pp. 21\u201330. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2011). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2011.21","DOI":"10.4230\/LIPIcs.RTA.2011.21"},{"key":"16_CR6","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. 5901, pp. 283\u2013295. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-11266-9_24","DOI":"10.1007\/978-3-642-11266-9_24"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Dershowitz, N.: 33 examples of termination. In: Comon, H., Jounnaud, J.P. (eds.) Term Rewriting. pp. 16\u201326. Springer (1995). https:\/\/doi.org\/10.1007\/3-540-59340-3_2","DOI":"10.1007\/3-540-59340-3_2"},{"issue":"2\u20133","key":"16_CR8","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":"16_CR9","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. 5117, pp. 110\u2013125. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-70590-1_8","DOI":"10.1007\/978-3-540-70590-1_8"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 184\u2013191. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_13","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"16_CR11","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 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"16_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. 3452, pp. 301\u2013331. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_21","DOI":"10.1007\/978-3-540-32275-7_21"},{"issue":"3","key":"16_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."},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249\u2013268. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-25979-4_18","DOI":"10.1007\/978-3-540-25979-4_18"},{"key":"16_CR15","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. 3249, pp. 185\u2013198. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30210-0_16","DOI":"10.1007\/978-3-540-30210-0_16"},{"key":"16_CR16","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 (2006). https:\/\/doi.org\/10.1007\/11805618_25","DOI":"10.1007\/11805618_25"},{"key":"16_CR17","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":"16_CR18","doi-asserted-by":"publisher","unstructured":"Kop, C., van Raamsdonk, F.: Dynamic dependency pairs for algebraic functional systems. Log. Methods Comput. Sci. 8(2) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(2:10)2012","DOI":"10.2168\/LMCS-8(2:10)2012"},{"issue":"2","key":"16_CR19","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":"16_CR20","doi-asserted-by":"publisher","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 (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_21","DOI":"10.1007\/978-3-642-02348-4_21"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 47\u201361. Springer (1999). https:\/\/doi.org\/10.1007\/10704567_3","DOI":"10.1007\/10704567_3"},{"key":"16_CR22","unstructured":"Lankford, D.: Canonical algebraic simplification in computational logic. Tech. Rep. ATP-25, University of Texas (1975)"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Lucas, S.: MU-TERM: A tool for proving termination of context-sensitive rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 200\u2013209. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-25979-4_14","DOI":"10.1007\/978-3-540-25979-4_14"},{"issue":"4","key":"16_CR24","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":"16_CR25","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":"16_CR26","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"16_CR27","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. 167, pp. 61\u201372 (2014). https:\/\/doi.org\/10.4204\/EPTCS.167.8","DOI":"10.4204\/EPTCS.167.8"},{"key":"16_CR28","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. 8560, pp. 441\u2013455. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_30","DOI":"10.1007\/978-3-319-08918-8_30"},{"key":"16_CR29","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. 8562, pp. 367\u2013373. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"16_CR30","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. 167, pp. 4:1\u20134:20. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.4","DOI":"10.4230\/LIPIcs.FSCD.2020.4"},{"key":"16_CR31","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. 5674, pp. 452\u2013468. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_31","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"16_CR32","unstructured":"The termination problem data base, http:\/\/termination-portal.org\/wiki\/TPDB"},{"key":"16_CR33","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 (1976)"},{"key":"16_CR34","doi-asserted-by":"publisher","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Nagoya Termination Tool. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 466\u2013475. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_32","DOI":"10.1007\/978-3-319-08918-8_32"},{"key":"16_CR35","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":"16_CR36","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":"16_CR37","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. Comm. Compt. 12(1\/2), 3\u201319 (2001). https:\/\/doi.org\/10.1007\/s002000100061","journal-title":"Appl. Algebr. Eng. Comm. Compt."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:28:43Z","timestamp":1625650123000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}