{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,4]],"date-time":"2024-03-04T02:40:02Z","timestamp":1709520002354},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,12,3]],"date-time":"2008-12-03T00:00:00Z","timestamp":1228262400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2009,2]]},"DOI":"10.1007\/s00236-008-0085-0","type":"journal-article","created":{"date-parts":[[2008,12,2]],"date-time":"2008-12-02T08:25:40Z","timestamp":1228206340000},"page":"57-72","source":"Crossref","is-referenced-by-count":5,"title":["A complexity tradeoff in ranking-function termination proofs"],"prefix":"10.1007","volume":"46","author":[{"given":"Amir M.","family":"Ben-Amram","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,12,3]]},"reference":[{"key":"85_CR1","volume-title":"Functional and Logic Programming: Eighth International Symposium, FLOPS 2006, Lecture Notes in Computer Science, vol. 3945","author":"J. Avery","year":"2006","unstructured":"Avery J.: Size-change termination and bound analysis. In: Hagiya, M., Wadler, P. (eds) Functional and Logic Programming: Eighth International Symposium, FLOPS 2006, Lecture Notes in Computer Science, vol. 3945., Springer, Heidelberg (2006)"},{"key":"85_CR2","first-page":"46","volume-title":"14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 5028","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) 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 5028, pp. 46\u201355. Springer, Heidelberg (2008)"},{"key":"85_CR3","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Lee, C.S.: Size-change analysis in polynomial time. ACM Trans. Program. Lang. Syst. 29(1), 5:1\u20135:37 (2007)","DOI":"10.1145\/1180475.1180480"},{"key":"85_CR4","first-page":"326","volume-title":"Logic Programming, 21st International Conference, ICLP 2005, Lecture Notes in Computer Science, vol. 3668","author":"M. Codish","year":"2005","unstructured":"Codish M., Lagoon V., Stuckey P.J.: Testing for termination with monotonicity constraints. In: Gabbrielli, M., Gupta, G. (eds) Logic Programming, 21st International Conference, ICLP 2005, Lecture Notes in Computer Science, vol. 3668, pp. 326\u2013340. Springer, Heidelberg (2005)"},{"key":"85_CR5","doi-asserted-by":"crossref","unstructured":"Codish, M., Taboch, C.: A semantic basis for termination analysis of logic programs. J. Logic Programming 41(1), 103\u2013123, (1999) preliminary (conference) version in Lecture Notes in Computer Science 1298 (1997)","DOI":"10.1016\/S0743-1066(99)00006-0"},{"key":"85_CR6","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach, M.I., Ball, T. (eds.) Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (PLDI), Ottawa, Canada, June 2006, pp. 415\u2013426. ACM, New York (2006)","DOI":"10.1145\/1133981.1134029"},{"issue":"1\u20132","key":"85_CR7","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/s002000100065","volume":"12","author":"N. Dershowitz","year":"2001","unstructured":"Dershowitz N., Lindenstrauss N., Sagiv Y., Serebrenik A.: A general framework for automatic termination analysis of logic programs. Appl. Algebra Eng. Commun. Comput. 12(1\u20132), 117\u2013156 (2001)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"issue":"8","key":"85_CR8","doi-asserted-by":"crossref","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. Commun. ACM 22(8), 465\u2013476 (1979)","journal-title":"Commun. ACM"},{"key":"85_CR9","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Bohr, N.: Termination analysis of the untyped lambda calculus. In: Proceedings of the 15th International Conference on Rewriting Techniques and Applications, RTA\u201904, Lecture Notes in Computer Science, vol. 3091, pp. 1\u201323. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-25979-4_1"},{"key":"85_CR10","volume-title":"Termination Analysis and Specialization-Point Insertion in Off-Line Partial Evaluation. Technical Report D-498, DIKU","author":"N.D. Jones","year":"2004","unstructured":"Jones N.D., Glenstrup A.: Termination Analysis and Specialization-Point Insertion in Off-Line Partial Evaluation. Technical Report D-498, DIKU. University of Copenhagen, Denmark (2004)"},{"key":"85_CR11","doi-asserted-by":"crossref","unstructured":"Lee, C.S.: Ranking functions for size-change termination. ACM Trans. Program. Lang. Syst. (to appear) (2008)","DOI":"10.1145\/1498926.1498928"},{"key":"85_CR12","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of the Twenty-Eigth ACM Symposium on Principles of Programming Languages, January 2001, vol. 28, pp. 81\u201392. ACM Press, New York (2001)","DOI":"10.1145\/360204.360210"},{"key":"85_CR13","doi-asserted-by":"crossref","unstructured":"Lindenstrauss, N., Sagiv, Y.: Automatic termination analysis of prolog programs. In: Naish, L. (ed.) Proceedings of the Fourteenth International Conference on Logic Programming, pp. 64\u201377. MIT Press, Leuven (1997)","DOI":"10.7551\/mitpress\/4299.003.0011"},{"key":"85_CR14","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou C.H.: Computational Complexity. Addison-Wesley, New York (1994)"},{"key":"85_CR15","volume-title":"Combinatorial Optimization: Algorithms and Complexity","author":"C.H. Papadimitriou","year":"1982","unstructured":"Papadimitriou C.H., Steiglitz K.: Combinatorial Optimization: Algorithms and Complexity. Prentice-Hall, Englewood Cliffs (1982)"},{"key":"85_CR16","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Ganzinger, H. (ed.) LICS\u201904: Logic in Computer Science, pp. 32\u201341. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"85_CR17","first-page":"518","volume-title":"Logic Programming, Proceedings of the 1991 International Symposium, San Diego, California, USA","author":"Y. Sagiv","year":"1991","unstructured":"Sagiv Y.: A termination test for logic programs. In: Saraswat, V., Ueda, K. (eds) Logic Programming, Proceedings of the 1991 International Symposium, San Diego, California, USA, pp. 518\u2013532. MIT Press, Cambridge (1991)"},{"issue":"4","key":"85_CR18","doi-asserted-by":"crossref","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. Appl. Algebra Eng. Commun. Comput. 16(4), 229\u2013270 (2005)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"85_CR19","unstructured":"Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67\u201369, (1948). Reprinted in The Early British Computer Conferences. Charles Babbage Institute Reprint Series For The History Of Computing, vol. 14. MIT Press, Cambridge (1989)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-008-0085-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-008-0085-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-008-0085-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,4]],"date-time":"2024-03-04T02:09:11Z","timestamp":1709518151000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-008-0085-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12,3]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["85"],"URL":"https:\/\/doi.org\/10.1007\/s00236-008-0085-0","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12,3]]}}}