{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:00Z","timestamp":1725490860081},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_33","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"443-459","source":"Crossref","is-referenced-by-count":11,"title":["Proving Termination by Bounded Increase"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Giesl","sequence":"first","affiliation":[]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Swiderski","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_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":"33_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"33_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/BFb0054264","volume-title":"Automated Deduction - CADE-15","author":"J. Brauburger","year":"1998","unstructured":"Brauburger, J., Giesl, J.: Termination analysis by inductive evaluation. In: Kirchner, C., Kirchner, H. (eds.) Automated Deduction - CADE-15. LNCS (LNAI), vol.\u00a01421, pp. 254\u2013269. Springer, Heidelberg (1998)"},{"issue":"4","key":"33_CR4","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10817-005-9022-x","volume":"34","author":"E. Contejean","year":"2005","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Aut. Reason.\u00a034(4), 325\u2013363 (2005)","journal-title":"J. Aut. Reason."},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 415\u2013418. Springer, Heidelberg (2006)"},{"issue":"3","key":"33_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.ipl.2004.10.005","volume":"93","author":"M.-L. Fern\u00e1ndez","year":"2005","unstructured":"Fern\u00e1ndez, M.-L.: Relaxing monotonicity for innermost termination. Information Processing Letters\u00a093(3), 117\u2013123 (2005)","journal-title":"Information Processing Letters"},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"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, Springer, Heidelberg (2007)"},{"key":"33_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","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":"33_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: AProVE 1.2: Automatic termination proofs in the DP framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"issue":"3","key":"33_CR10","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. Journal of Automated Reasoning\u00a037(3), 155\u2013203 (2006)","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR11","unstructured":"Giesl, J., Thiemann, R., Swiderski, S., Schneider-Kamp, P.: Proving termination by bounded increase. Technical Report AIB-2007-03, RWTH Aachen (2007), Available from \n                    \n                      http:\/\/aib.informatik.rwth-aachen.de"},{"issue":"1,2","key":"33_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"},{"issue":"4","key":"33_CR13","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":"33_CR14","unstructured":"Lankford, D.: On proving term rewriting systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/11817963_36","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"2006","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 401\u2013414. Springer, Heidelberg (2006)"},{"key":"33_CR16","unstructured":"March\u00e9, C., Zantema, H.: The termination competition. In: Proc. RTA\u00a0 2007 (to appear, 2007)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:08Z","timestamp":1619517188000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}