{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:20:04Z","timestamp":1725567604819},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_16","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T12:51:59Z","timestamp":1286196719000},"page":"217-232","source":"Crossref","is-referenced-by-count":6,"title":["Lazy Abstraction for Size-Change Termination"],"prefix":"10.1007","author":[{"given":"Michael","family":"Codish","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"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. Theoretical Computer Science\u00a0236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/11737414_14","volume-title":"Functional and Logic Programming","author":"J. Avery","year":"2006","unstructured":"Avery, J.: Size-change termination and bound analysis. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol.\u00a03945, pp. 192\u2013207. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That, Cambridge (1998)","key":"16_CR3","DOI":"10.1017\/CBO9781139172752"},{"doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Lee, C.S.: Size-change termination in polynomial time. ACM Transactions on Programming Languages and Systems\u00a029(1) (2007)","key":"16_CR4","DOI":"10.1145\/1180475.1180480"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-78800-3_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.M. Ben-Amram","year":"2008","unstructured":"Ben-Amram, A.M., Codish, M.: A SAT-based approach to size change termination with global ranking functions. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 218\u2013232. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Codish, M., Fuhs, C., Giesl, J., Schneider-Kamp, P.: Lazy abstraction for size-change termination. Technical Report AIB-2010-14, RWTH Aachen University (2010), http:\/\/aib.informatik.rwth-aachen.de","key":"16_CR6","DOI":"10.1007\/978-3-642-16242-8_16"},{"issue":"1","key":"16_CR7","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0743-1066(99)00006-0","volume":"41","author":"M. Codish","year":"1999","unstructured":"Codish, M., Taboch, C.: A semantic basis for termination analysis of logic programs. Journal of Logic Programming\u00a041(1), 103\u2013123 (1999)","journal-title":"Journal of Logic Programming"},{"key":"16_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/11916277_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Codish","year":"2006","unstructured":"Codish, M., Schneider-Kamp, P., Lagoon, V., Thiemann, R., Giesl, J.: SAT solving for argument filterings. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 30\u201344. Springer, Heidelberg (2006)"},{"key":"16_CR9","doi-asserted-by":"crossref","first-page":"193","DOI":"10.3233\/SAT190056","volume":"5","author":"M. Codish","year":"2008","unstructured":"Codish, M., Lagoon, V., Stuckey, P.: Solving partial order constraints for LPO termination. J. Satisfiability, Boolean Modeling and Computation\u00a05, 193\u2013215 (2008)","journal-title":"J. Satisfiability, Boolean Modeling and Computation"},{"issue":"8","key":"16_CR10","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM\u00a022(8), 465\u2013476 (1979)","journal-title":"Communications of the ACM"},{"unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSAT, http:\/\/minisat.se","key":"16_CR11"},{"issue":"2-3","key":"16_CR12","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. Automated Reasoning\u00a040(2-3), 195\u2013220 (2008)","journal-title":"J. Automated Reasoning"},{"key":"16_CR13","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., Thiemann, R., Schneider-Kamp, P., 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":"16_CR14","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":"16_CR15","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., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2 automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"issue":"3","key":"16_CR16","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"},{"doi-asserted-by":"crossref","unstructured":"Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems (to appear, 2010); Preliminary version appeared in Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 297\u2013312. Springer, Heidelberg (2006)","key":"16_CR17","DOI":"10.1145\/1890028.1890030"},{"issue":"1,2","key":"16_CR18","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":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-25979-4_1","volume-title":"Rewriting Techniques and Applications","author":"N.D. Jones","year":"2004","unstructured":"Jones, N.D., Bohr, N.: Termination analysis of the untyped lambda calculus. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 1\u201323. Springer, Heidelberg (2004)"},{"unstructured":"Le Berre, D., Parrain, A.: SAT4J, http:\/\/www.sat4j.org","key":"16_CR20"},{"doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. POPL\u00a02001, pp. 81\u201392 (2001)","key":"16_CR21","DOI":"10.1145\/360204.360210"},{"issue":"3","key":"16_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1498926.1498928","volume":"31","author":"C.S. Lee","year":"2009","unstructured":"Lee, C.S.: Ranking functions for size-change termination. ACM Transactions on Programming Languages and Systems\u00a031(3), 1\u201342 (2009)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"unstructured":"Nguyen, M.T., De Schreye, D., Giesl, J., Schneider-Kamp, P.: Polytool: Polynomial interpretations as a basis for termination analysis of logic programs. In: Theory and Practice of Logic Programming (to appear, 2010)","key":"16_CR23"},{"doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proc. RTA\u00a02010. LIPIcs, vol.\u00a06, pp. 259\u2013276 (2010)","key":"16_CR24","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"16_CR25","first-page":"32","volume-title":"Proc. 19th LICS","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: Transition Invariants. In: Proc. 19th LICS, pp. 32\u201341. IEEE, Los Alamitos (2004)"},{"key":"16_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-540-74621-8_18","volume-title":"Frontiers of Combining Systems","author":"P. Schneider-Kamp","year":"2007","unstructured":"Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving termination using recursive path orders and SAT solving. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 267\u2013282. Springer, Heidelberg (2007)"},{"issue":"1","key":"16_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1614431.1614433","volume":"11","author":"P. Schneider-Kamp","year":"2009","unstructured":"Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination proofs for logic programs by term rewriting. ACM Transactions on Computational Logic\u00a011(1), 1\u201352 (2009)","journal-title":"ACM Transactions on Computational Logic"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11575467_19","volume-title":"Programming Languages and Systems","author":"D. Sereni","year":"2005","unstructured":"Sereni, D., Jones, N.D.: Termination analysis of higher-order functional programs. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 281\u2013297. Springer, Heidelberg (2005)"},{"issue":"4","key":"16_CR29","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. Applicable Algebra in Engineering, Communication and Computing\u00a016(4), 229\u2013270 (2005)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"issue":"2","key":"16_CR30","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. Journal of Automated Reasoning\u00a043(2), 173\u2013201 (2009)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,11]],"date-time":"2021-11-11T01:39:50Z","timestamp":1636594790000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}