{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,12]],"date-time":"2024-01-12T05:02:26Z","timestamp":1705035746399},"reference-count":34,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"vor","delay-in-days":5802,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1999]]},"DOI":"10.1016\/s1571-0661(04)00113-6","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T10:14:39Z","timestamp":1075371279000},"page":"39-58","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Termination Analysis of Programs Containing Arithmetic Predicates"],"prefix":"10.1016","volume":"30","author":[{"given":"Nachum","family":"Dershowitz","sequence":"first","affiliation":[]},{"given":"Naomi","family":"Lindenstrauss","sequence":"additional","affiliation":[]},{"given":"Yehoshua","family":"Sagiv","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Serebrenik","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB1","unstructured":"J. H. Andrews. Termination Semantics of Logic Programs with Cut and Related Features. Available at http:\/\/www.inferenzsysteme.informatik.tu-darmstadt.de\/~giesl\/WST99\/submissions\/andrews.ps, May 1999."},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB2","first-page":"493","article-title":"Logic programming","author":"Apt","year":"1990"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB3","unstructured":"K. R. Apt. From Logic Programming to Prolog. Prentice-Hall International Series in Computer Science. Prentice Hall, 1997."},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB4","doi-asserted-by":"crossref","unstructured":"F. Benoy and A. King. Inferring argument size relationships with CLP(R). In J. Gallagher, editor, Logic Program Synthesis and Transformation Proceedings, pages 204\u2013223. Springer Verlag, 1996. Lecture Notes in Computer Science, volume 1207.","DOI":"10.1007\/3-540-62718-9_12"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB5","series-title":"Algebraic and Logic Programming","first-page":"269","article-title":"Preserving universal termination through unfold\/fold","author":"Bossi","year":"1994"},{"issue":"2","key":"10.1016\/S1571-0661(04)00113-6_NEWBIB6","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(92)00019-N","article-title":"Norms on terms and their use in proving universal termination of a logic program","volume":"124","author":"Bossi","year":"1994","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"10.1016\/S1571-0661(04)00113-6_NEWBIB7","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/S0743-1066(96)00144-6","article-title":"Directional types and the annotation method","volume":"33","author":"Boye","year":"1997","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB8","doi-asserted-by":"crossref","unstructured":"A. Brodsky and Y. Sagiv. Inference of monotonicity constraints in datalog programs. In Proceedings of the Eighth ACM SIGACT-SIGART-SIGMOD Symposium on Principles of Database Systems, pages 190\u2013199, 1989.","DOI":"10.1145\/73721.73741"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB9","doi-asserted-by":"crossref","unstructured":"A. Brodsky and Y. Sagiv. Inference of inequality constraints in logic programs. In Proceedings of the Tenth ACM SIGACT-SIGART-SIGMOD Symposium on Principles of Database Systems, pages 227\u2013240, 1991.","DOI":"10.1145\/113413.113434"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB10","unstructured":"F. Bueno, M. J. Garc\u00eda de la Banda, and M. V. Hermenegildo. Effectiveness of global analysis in strict independence-based automatic parallelization. In M. Bruynooghe, editor, Logic Programming, Proceedings of the 1994 International Symposium, pages 320\u2013336. MIT Press, 1994."},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB11","unstructured":"M. Codish and V. Lagoon. Type dependencies for logic programs using ACI-unification. In Proceedingsof the 1996 Israeli Symposium on Theory of Computing and Systems, pages 136\u2013145. IEEE Press, June 1996."},{"issue":"1","key":"10.1016\/S1571-0661(04)00113-6_NEWBIB12","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/S0743-1066(99)00006-0","article-title":"A semantic basis for termination analysis of logic programs","volume":"41","author":"Codish","year":"1999","journal-title":"The Journal of Logic Programming"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB13","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","article-title":"Abstract interpretation and application to logic programs","volume":"13","author":"Cousot","year":"1992","journal-title":"The Journal of Logic Programming"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB14","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0743-1066(94)90027-2","article-title":"Termination of logic programs: The never-ending story","volume":"19\/20","author":"De Schreye","year":"1994","journal-title":"The Journal of Logic Programming"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB15","doi-asserted-by":"crossref","unstructured":"S. Decorte and D. De Schreye. Demand-driven and constraint-based automatic left termination analysis for logic programs. In L. Naish, editor, Proceedings of the Fourteenth International Conference on Logic Programming, pages 78\u201392. MIT Press, July 1997.","DOI":"10.7551\/mitpress\/4299.003.0012"},{"issue":"3","key":"10.1016\/S1571-0661(04)00113-6_NEWBIB16","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term-rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005797629953","article-title":"Termination of nested and mutually recursive algorithms","volume":"19","author":"Giesl","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB18","unstructured":"C. Holzbaur. OFAI CLP(Q,R) Manual. Technical Report TR-95\u201309, Austrian Research Insititute for Artificial Intelligence, Vienna, 1995."},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB19","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","article-title":"Constraint logic programming: a survey","volume":"19\/20","author":"Jaffar","year":"1994","journal-title":"The Journal of Logic Programming"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB20","series-title":"Artificial Intelligence and Mathematical Theory of Computation. Papers in Honor of John McCarthy","first-page":"207","article-title":"Textbook examples of recursion","author":"Knuth","year":"1991"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB21","doi-asserted-by":"crossref","unstructured":"N. Lindenstrauss and Y. Sagiv. Automatic termination analysis of logic programs. In L. Naish, editor, Proceedings of the Fourteenth International Conference on Logic Programming, pages 63\u201377. MIT Press, July 1997.","DOI":"10.7551\/mitpress\/4299.003.0011"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB22","doi-asserted-by":"crossref","unstructured":"N. Lindenstrauss, Y. Sagiv, and A. Serebrenik; TermiLog: A system for checking termination of queries to logic programs. In O. Grumberg, editor, Computer Aided Verification, 9th International Conference, pages 63\u201377. Springer Verlag, June 1997. Lecture Notes in Computer Science, volume 1254.","DOI":"10.1007\/3-540-63166-6_44"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB23","doi-asserted-by":"crossref","unstructured":"N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. Unfolding mystery of the mergesort. In N. Fuchs, Proceedings of the Seventh Internatinal Workshop on Logic Program Synthesis and Transformation, Springer Verlag, 1998. Lecture Notes in Computer Science, volume 1463.","DOI":"10.1007\/3-540-49674-2_11"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB24","first-page":"27","article-title":"Properties of Programs and partial function logic","volume":"5","author":"Manna","year":"1970","journal-title":"Machine Intelligence"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB25","doi-asserted-by":"crossref","unstructured":"F. Mesnard and J. Ganascia. CLP(Q) for proving interargument relations. In A. Petrossi, editor, Proceedings META'92, pages 309\u2013320. Springer Verlag, 1992.","DOI":"10.1007\/3-540-56282-6_21"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB26","doi-asserted-by":"crossref","unstructured":"L. Pl\u00fcmer. Termination Proofs for Logic Programs. Lecture Notes in Artificial Intelligence, volume 446, Springer Verlag, 1990.","DOI":"10.1007\/3-540-52837-7"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB27","doi-asserted-by":"crossref","unstructured":"L. Pl\u00fcmer. Termination proofs for logic programs based on predicate inequalities. In Proceedings of ICLP'90, pages 634\u2013648. MIT Press, 1990.","DOI":"10.1007\/3-540-52837-7"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB28","doi-asserted-by":"crossref","unstructured":"L. Pl\u00fcmer. Automatic termination proofs for prolog programs operating on nonground terms. In International Logic Programming Symposium. MIT Press, 1991.","DOI":"10.1007\/3-540-52837-7"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB29","unstructured":"K. F. Sagonas, T. Swift, and D. S. Warren. The XSB Programmer's Manual. Version 1.3 (\u03b2). Department of Computer Science, SUNY @ Stony Brook. U.S.A., September 1993."},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB30","unstructured":"SICS. User Manual. Version 3.7.1. Swedish Institute of Computer Science, 1998."},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB31","unstructured":"H. Tamaki and T. Sato. Unfold\/Fold transformation of logic programs. In S.-\u00c5.T\u00e4rnlund, editor, Proceedings of the Second International Logic Programming Conference, pages 127\u2013138. Upsala University, 1984."},{"issue":"2","key":"10.1016\/S1571-0661(04)00113-6_NEWBIB32","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1145\/42282.42285","article-title":"Efficient tests for top-down termination of logical rules","volume":"35","author":"Ullman","year":"1988","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB33","unstructured":"K. Verschaetse and D. De Schreye. Deriving termination proofs for logic programs, using abstract procedures. In K. Furukawa, editor, Logic Programming, Proceedings of the Eigth International Conference, pages 301\u2013315. MIT Press, 1991."},{"key":"10.1016\/S1571-0661(04)00113-6_NEWBIB34","doi-asserted-by":"crossref","unstructured":"K. Verschaetse and D. De Schreye. Deriving of Linear size relations by abstract interpretation. In M. Bryunooghe and M. Wirsing, editors, Programming Language Implementation and Logic Programming, 4th International Symposium, pages 296\u2013310. Springer Verlag, 1992. Lecture Notes in Computer Science, volume 631.","DOI":"10.1007\/3-540-55844-6_143"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001136?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001136?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,1,12]],"date-time":"2024-01-12T02:11:27Z","timestamp":1705025487000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104001136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999]]}},"alternative-id":["S1571066104001136"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00113-6","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}