{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:22:26Z","timestamp":1753885346501},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705888"},{"type":"electronic","value":"9783540705901"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70590-1_14","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"202-216","source":"Crossref","is-referenced-by-count":15,"title":["Arctic Termination ...Below Zero"],"prefix":"10.1007","author":[{"given":"Adam","family":"Koprowski","sequence":"first","affiliation":[]},{"given":"Johannes","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"14_CR1","first-page":"29","volume":"65","author":"R.M. Amadio","year":"2005","unstructured":"Amadio, R.M.: Synthesis of max-plus quasi-interpretations. Fundamenta Informaticae\u00a065(1-2), 29\u201360 (2005)","journal-title":"Fundamenta Informaticae"},{"issue":"1-2","key":"14_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. TCS\u00a0236(1-2), 133\u2013178 (2000)","journal-title":"TCS"},{"key":"14_CR3","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":"14_CR4","unstructured":"Blanqui, F., Delobel, W., Coupet-Grimal, S., Hinderer, S., Koprowski, A.: CoLoR, a Coq library on rewriting and termination. In: WST (2006), http:\/\/color.loria.fr"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"14_CR6","unstructured":"Endrullis, J.: Jambox, http:\/\/joerg.endrullis.de"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning (to appear, 2007)","DOI":"10.1007\/11814771_47"},{"key":"14_CR8","volume-title":"Partially Ordered Algebraic Systems","author":"L. Fuchs","year":"1962","unstructured":"Fuchs, L.: Partially Ordered Algebraic Systems. Addison-Wesley, Reading (1962)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BFb0023465","volume-title":"STACS 97","author":"S. Gaubert","year":"1997","unstructured":"Gaubert, S., Plus, M.: Methods and applications of (max, +) linear algebra. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol.\u00a01200, pp. 261\u2013282. Springer, Heidelberg (1997)"},{"issue":"1","key":"14_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1006\/jsco.2002.0541","volume":"34","author":"J. Giesl","year":"2002","unstructured":"Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. Journal of Symbolic Computation\u00a034(1), 21\u201358 (2002)","journal-title":"Journal of Symbolic Computation"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 210\u2013220. Springer, Heidelberg (2004)"},{"key":"14_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-73595-3_33","volume-title":"Automated Deduction \u2013 CADE-21","author":"J. Giesl","year":"2007","unstructured":"Giesl, J., Thiemann, R., Swiderski, S., Schneider-Kamp, P.: Proving termination by bounded increase. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 443\u2013459. Springer, Heidelberg (2007)"},{"key":"14_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9333-5","volume-title":"Semirings and their Applications","author":"J.S. Golan","year":"1999","unstructured":"Golan, J.S.: Semirings and their Applications. Kluwer, Dordrecht (1999)"},{"key":"14_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","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.A. (eds.) AISC 2004. LNCS (LNAI), vol.\u00a03249, pp. 185\u2013198. Springer, Heidelberg (2004)"},{"issue":"4","key":"14_CR15","doi-asserted-by":"publisher","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. Information and Computation\u00a0205(4), 474\u2013511 (2007)","journal-title":"Information and Computation"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-51081-8_107","volume-title":"Rewriting Techniques and Applications","author":"D. Hofbauer","year":"1989","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 167\u2013177. Springer, Heidelberg (1989)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/11805618_25","volume-title":"Term Rewriting and Applications","author":"D. Hofbauer","year":"2006","unstructured":"Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 328\u2013342. Springer, Heidelberg (2006)"},{"key":"14_CR18","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.\u00a04098, pp. 257\u2013266. Springer, Heidelberg (2006), http:\/\/www.win.tue.nl\/tpa"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Koprowski, A., Zantema, H.: Certification of proving termination of term rewriting by matrix interpretations. In: SOFSEM. LNCS, vol.\u00a04910, pp. 328\u2013339 (2008)","DOI":"10.1007\/978-3-540-77566-9_28"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/3-540-55719-9_67","volume-title":"Automata, Languages and Programming","author":"D. Krob","year":"1992","unstructured":"Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 101\u2013112. Springer, Heidelberg (1992)"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-540-25979-4_6","volume-title":"Rewriting Techniques and Applications","author":"J. Waldmann","year":"2004","unstructured":"Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 85\u201394. Springer, Heidelberg (2004), http:\/\/dfa.imn.htwk-leipzig.de\/matchbox"},{"key":"14_CR22","unstructured":"Waldmann, J.: Arctic termination. In: WST (2007)"},{"key":"14_CR23","unstructured":"Waldmann, J.: Weighted automata for proving termination of string rewriting. Journal of Automata, Languages and Combinatorics (to appear, 2007)"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-540-73449-9_30","volume-title":"Term Rewriting and Applications","author":"H. Zantema","year":"2007","unstructured":"Zantema, H., Waldmann, J.: Termination by quasi-periodic interpretations. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 404\u2013418. Springer, Heidelberg (2007)"},{"key":"14_CR25","unstructured":"The Coq proof assistant, http:\/\/coq.inria.fr"},{"key":"14_CR26","unstructured":"Termination competition, http:\/\/www.lri.fr\/~marche\/termination-competition"},{"key":"14_CR27","unstructured":"Termination problems data base, http:\/\/www.lri.fr\/~marche\/tpdb"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70590-1_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:08:19Z","timestamp":1605762499000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70590-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705888","9783540705901"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70590-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}