{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T00:09:15Z","timestamp":1768262955660,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371878","type":"print"},{"value":"9783540371885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_24","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T11:44:21Z","timestamp":1160048661000},"page":"281-286","source":"Crossref","is-referenced-by-count":136,"title":["AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Giesl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_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. Theoretical Computer Science\u00a0236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"24_CR2","unstructured":"Borralleras, C.: Ordering-based methods for proving termination automatically. PhD thesis, Universitat Polit\u00e8cnica de Catalunya (2003)"},{"key":"24_CR3","unstructured":"E.\u00a0Contejean, C.\u00a0March\u00e9, B.\u00a0Monate, and X.\u00a0Urbain. CiME. http:\/\/cime.lri.fr"},{"issue":"3,4","key":"24_CR4","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s00200-004-0162-8","volume":"15","author":"A. Geser","year":"2004","unstructured":"Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. Applicable Algebra in Eng., Comm. and Computing\u00a015(3,4), 149\u2013171 (2004)","journal-title":"Applicable Algebra in Eng., Comm. and Computing"},{"issue":"1","key":"24_CR5","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":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-540-39813-4_11","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Giesl","year":"2003","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Improving dependency pairs. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, pp. 165\u2013179. Springer, Heidelberg (2003)"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"24_CR8","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 DP framework: Combining techn. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"key":"24_CR9","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)"},{"key":"24_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":"24_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.A. (eds.) AISC 2004. LNCS (LNAI), vol.\u00a03249, pp. 185\u2013198. Springer, Heidelberg (2004)"},{"issue":"1,2","key":"24_CR12","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/j.ic.2004.10.004","volume":"199","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation\u00a0199(1,2), 172\u2013199 (2005)","journal-title":"Information and Computation"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-32033-3_14","volume-title":"Term Rewriting and Applications","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 175\u2013184. Springer, Heidelberg (2005)"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2006)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. 28th POPL, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"issue":"4","key":"24_CR16","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s00200-005-0179-7","volume":"16","author":"R. Thiemann","year":"2005","unstructured":"Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination of term rewriting. AAECC\u00a016(4), 229\u2013270 (2005)","journal-title":"AAECC"},{"key":"24_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-540-25984-8_4","volume-title":"Automated Reasoning","author":"R. Thiemann","year":"2004","unstructured":"Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 75\u201390. Springer, Heidelberg (2004)"},{"key":"24_CR18","unstructured":"van de Wulp, J.: Teparla, http:\/\/www.win.tue.nl\/~hzantema\/torpa.html"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 85\u201394. Springer, Heidelberg (2004)"},{"key":"24_CR20","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. Fundamenta Informaticae\u00a024, 89\u2013105 (1995)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:14:33Z","timestamp":1605626073000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11814771_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}