{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:30:58Z","timestamp":1784845858275,"version":"3.55.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319089171","type":"print"},{"value":"9783319089188","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08918-8_32","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T01:44:22Z","timestamp":1404265462000},"page":"466-475","source":"Crossref","is-referenced-by-count":24,"title":["Nagoya Termination Tool"],"prefix":"10.1007","author":[{"given":"Akihisa","family":"Yamada","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Keiichirou","family":"Kusakari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Toshiki","family":"Sakabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1-2","key":"32_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. TCS\u00a0236(1-2), 133\u2013178 (2000)","journal-title":"TCS"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-642-02959-2_23","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Borralleras","year":"2009","unstructured":"Borralleras, C., Lucas, S., Navarro-Marset, R., Rodr\u00edguez-Carbonell, E., Rubio, A.: Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 294\u2013305. Springer, Heidelberg (2009)"},{"issue":"3","key":"32_CR3","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. TCS\u00a017(3), 279\u2013301 (1982)","journal-title":"TCS"},{"issue":"2-3","key":"32_CR4","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. JAR\u00a040(2-3), 195\u2013220 (2008)","journal-title":"JAR"},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"key":"32_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-540-70590-1_8","volume-title":"Rewriting Techniques and Applications","author":"C. Fuhs","year":"2008","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)"},{"key":"32_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-540-32275-7_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Giesl","year":"2005","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 (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"key":"32_CR8","series-title":"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.\u00a03717, pp. 216\u2013231. Springer, Heidelberg (2005)"},{"issue":"3","key":"32_CR9","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. JAR\u00a037(3), 155\u2013203 (2006)","journal-title":"JAR"},{"key":"32_CR10","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.\u00a03091, pp. 249\u2013268. Springer, Heidelberg (2004)"},{"key":"32_CR11","series-title":"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.\u00a03249, pp. 185\u2013198. Springer, Heidelberg (2004)"},{"issue":"3","key":"32_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10817-012-9248-3","volume":"50","author":"N. Hirokawa","year":"2013","unstructured":"Hirokawa, N., Middeldorp, A., Zankl, H.: Uncurrying for termination and complexity. JAR\u00a050(3), 279\u2013315 (2013)","journal-title":"JAR"},{"key":"32_CR13","unstructured":"Kamin, S., L\u00e9vy, J.J.: Two generalizations of the recursive path ordering (1980) (unpublished note)"},{"key":"32_CR14","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/B978-0-08-012975-4.50028-X","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, New York (1970)"},{"key":"32_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 427\u2013443. Springer, Heidelberg (2012)"},{"key":"32_CR16","unstructured":"Lankford, D.: On proving term rewrite systems are Noetherian. Tech. Rep. MTP-3, Louisiana Technical University (1979)"},{"key":"32_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-75560-9_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Ludwig","year":"2007","unstructured":"Ludwig, M., Waldmann, U.: An extension of the knuth-bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 348\u2013362. Springer, Heidelberg (2007)"},{"issue":"1","key":"32_CR18","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/S0304-3975(96)00172-7","volume":"175","author":"A. Middeldorp","year":"1997","unstructured":"Middeldorp, A., Zantema, H.: Simple termination of rewrite systems. TCS\u00a0175(1), 127\u2013158 (1997)","journal-title":"TCS"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"Steinbach, J.: Extensions and comparison of simplification orders. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 434\u2013448. Springer, Heidelberg (1989)","DOI":"10.1007\/3-540-51081-8_124"},{"key":"32_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-24364-6_17","volume-title":"Frontiers of Combining Systems","author":"C. Sternagel","year":"2011","unstructured":"Sternagel, C., Thiemann, R.: Generalized and formalized uncurrying. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol.\u00a06989, pp. 243\u2013258. Springer, Heidelberg (2011)"},{"key":"32_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-642-28717-6_33","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Winkler","year":"2012","unstructured":"Winkler, S., Zankl, H., Middeldorp, A.: Ordinals and knuth-bendix orders. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 420\u2013434. Springer, Heidelberg (2012)"},{"key":"32_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BFb0052376","volume-title":"Rewriting Techniques and Applications","author":"H. Xi","year":"1998","unstructured":"Xi, H.: Towards automated termination proofs through freezing. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol.\u00a01379, pp. 271\u2013285. Springer, Heidelberg (1998)"},{"key":"32_CR23","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Partial status for KBO. In: Proceedings WST 2013, pp. 74\u201378 (2013)"},{"key":"32_CR24","doi-asserted-by":"crossref","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Unifying the Knuth-Bendix, recursive path and polynomial orders. In: Proceedings PPDP[15], pp. 181\u2013192 (2013)","DOI":"10.1145\/2505879.2505885"},{"key":"32_CR25","doi-asserted-by":"crossref","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Nagoya Termination Tool. CoRR abs\/1404.6626 (2014)","DOI":"10.1007\/978-3-319-08918-8_32"},{"key":"32_CR26","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: A unified order for termination proving. CoRR abs\/1404.6245 (2014) (submitted to SCP)"},{"issue":"2","key":"32_CR27","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-009-9131-z","volume":"43","author":"H. Zankl","year":"2009","unstructured":"Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. JAR\u00a043(2), 173\u2013201 (2009)","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Rewriting and Typed Lambda Calculi"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08918-8_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T01:45:59Z","timestamp":1558921559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08918-8_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089171","9783319089188"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08918-8_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}