{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T19:48:53Z","timestamp":1672516133897},"reference-count":54,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2016,3,31]],"date-time":"2016-03-31T00:00:00Z","timestamp":1459382400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2016,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>It is widely acknowledged that function symbols are an important feature in answer set programming, as they make modelling easier, increase the expressive power, and allow us to deal with infinite domains. The main issue with their introduction is that the evaluation of a program might not terminate and checking whether it terminates or not is undecidable. To cope with this problem, several classes of logic programs have been proposed where the use of function symbols is restricted but the program evaluation termination is guaranteed. Despite the significant body of work in this area, current approaches do not include many simple practical programs whose evaluation terminates. In this paper, we present the novel classes of<jats:italic>rule-bounded<\/jats:italic>and<jats:italic>cycle-bounded programs<\/jats:italic>, which overcome different limitations of current approaches by performing a more global analysis of how terms are propagated from the body to the head of rules. Results on the correctness, the complexity, and the expressivity of the proposed approach are provided.<\/jats:p>","DOI":"10.1017\/s1471068416000077","type":"journal-article","created":{"date-parts":[[2016,3,31]],"date-time":"2016-03-31T09:48:18Z","timestamp":1459417698000},"page":"353-377","source":"Crossref","is-referenced-by-count":2,"title":["Using linear constraints for logic program termination analysis"],"prefix":"10.1017","volume":"16","author":[{"given":"MARCO","family":"CALAUTTI","sequence":"first","affiliation":[]},{"given":"SERGIO","family":"GRECO","sequence":"additional","affiliation":[]},{"given":"CRISTIAN","family":"MOLINARO","sequence":"additional","affiliation":[]},{"given":"IRINA","family":"TRUBITSYNA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,3,31]]},"reference":[{"key":"S1471068416000077_ref49","doi-asserted-by":"crossref","unstructured":"Syrjanen T. 2001. Omega-restricted logic programs. In Proc. of the 6th International Conference on Logic Programming and Non-Monotonic Reasoning. Lecture Notes in Computer Science, Vol. 2173. Springer, 267\u2013279.","DOI":"10.1007\/3-540-45402-0_20"},{"key":"S1471068416000077_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/BF02575754"},{"key":"S1471068416000077_ref39","first-page":"1","volume-title":"Data Exchange, Integration, and Streams","author":"Onet","year":"2013"},{"key":"S1471068416000077_ref15","unstructured":"Eiter T. , Fink M. , Krennwallner T. and Redl C. 2013. Liberal safety for answer set programs with external sources. In Proc. of the 27th AAAI Conference on Artificial Intelligence, AAAI Press, 267\u2013275."},{"key":"S1471068416000077_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068414000623"},{"key":"S1471068416000077_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90027-2"},{"key":"S1471068416000077_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"S1471068416000077_ref34","first-page":"13","volume-title":"Proc. of the 28th Symposium on Principles of Database Systems","author":"Marnette","year":"2009"},{"key":"S1471068416000077_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83952-8"},{"key":"S1471068416000077_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037169"},{"key":"S1471068416000077_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068409990251"},{"key":"S1471068416000077_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S147106840900372X"},{"key":"S1471068416000077_ref22","doi-asserted-by":"publisher","DOI":"10.1109\/69.761663"},{"key":"S1471068416000077_ref19","doi-asserted-by":"crossref","unstructured":"Gebser M. , Schaub T. and Thiele S. 2007. Gringo: A new grounder for answer set programming. In Proc. of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning. Lecture Notes in Computer Science, Vol. 4483. Springer, 266\u2013271.","DOI":"10.1007\/978-3-540-72200-7_24"},{"key":"S1471068416000077_ref46","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002248"},{"key":"S1471068416000077_ref36","first-page":"8","volume-title":"Proc. of the 17th International Symposium on Logic-based Program Synthesis and Transformation","author":"Nguyen","year":"2007"},{"key":"S1471068416000077_ref48","doi-asserted-by":"crossref","unstructured":"Sternagel C. and Middeldorp A. 2008. Root-labeling. In Proc. of the 19th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science, Vol. 5117. Springer, 336\u2013350.","DOI":"10.1007\/978-3-540-70590-1_23"},{"key":"S1471068416000077_ref13","doi-asserted-by":"crossref","unstructured":"Codish M. , Lagoon V. and Stuckey P. J. 2005. Testing for termination with monotonicity constraints. In Proc. of the 21st International Conference on Logic Programming. Lecture Notes in Computer Science, Vol. 3668. Springer, 326\u2013340.","DOI":"10.1007\/11562931_25"},{"key":"S1471068416000077_ref20","unstructured":"Gelfond M. and Lifschitz V. 1988. The stable model semantics for logic programming. In Proc. of the 5th International Conference and Symposium on Logic Programming, MIT Press, 1070\u20131080."},{"key":"S1471068416000077_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.01.005"},{"key":"S1471068416000077_ref6","first-page":"97","volume-title":"Proc. of the 8th International Web Rule Symposium","author":"Calautti","year":"2014"},{"key":"S1471068416000077_ref10","unstructured":"Calimeri F. , Cozza S. , Ianni G. and Leone N. 2008. Computable functions in ASP: Theory and implementation. In Proc. of the 24th International Conference on Logic Programming. Lecture Notes in Computer Science, Vol. 5366. Springer, 407\u2013424."},{"key":"S1471068416000077_ref9","first-page":"228","volume-title":"Proc. of the 25th Symposium on Logic in Computer Science","author":"Cal\u00ec","year":"2010"},{"key":"S1471068416000077_ref30","first-page":"105","volume-title":"Proc. of the 11th Symposium on Principles of Database Systems","author":"Greco","year":"1992"},{"key":"S1471068416000077_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/s002000100064"},{"key":"S1471068416000077_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90013-6"},{"key":"S1471068416000077_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614433"},{"key":"S1471068416000077_ref24","unstructured":"Greco S. , Molinaro C. and Trubitsyna I. 2013a. Bounded programs: A new decidable class of logic programs with function symbols. In Proc. of the 23rd International Joint Conference on Artificial Intelligence, IJCAI\/AAAI, 926\u2013932."},{"key":"S1471068416000077_ref54","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","article-title":"Termination of term rewriting by semantic labelling","volume":"24","author":"Zantema","year":"1995","journal-title":"Fundamenta Informaticae"},{"key":"S1471068416000077_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2629337"},{"key":"S1471068416000077_ref29","unstructured":"Greco S. , Spezzano F. and Trubitsyna I. 2012. On the termination of logic programs with function symbols. In Technical Communications of the 28th International Conference on Logic Programming. LIPIcs, Vol. 17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 323\u2013333."},{"key":"S1471068416000077_ref52","first-page":"51","volume-title":"Proc. of the 2007 Workshop on Partial Evaluation and Semantics-based Program Manipulation","author":"Vidal","year":"2007"},{"key":"S1471068416000077_ref18","volume-title":"Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning","author":"Gebser","year":"2012"},{"key":"S1471068416000077_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9087-9"},{"key":"S1471068416000077_ref47","first-page":"216","volume-title":"Proc. of the 10th Symposium on Principles of Database Systems","author":"Sohn","year":"1991"},{"key":"S1471068416000077_ref8","first-page":"239","volume-title":"Proc. of the 15th International Symposium on Principles and Practice of Declarative Programming","author":"Calautti","year":"2013"},{"key":"S1471068416000077_ref32","doi-asserted-by":"crossref","unstructured":"Lierler Y. and Lifschitz V. 2009. One more decidable class of finitely ground programs. In Proc. of the 25th International Conference on Logic Programming. Lecture Notes in Computer Science, Vol. 5649. Springer, 489\u2013493.","DOI":"10.1007\/978-3-642-02846-5_40"},{"key":"S1471068416000077_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15918-3_23"},{"key":"S1471068416000077_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/322276.322287"},{"key":"S1471068416000077_ref23","doi-asserted-by":"crossref","DOI":"10.2200\/S00435ED1V01Y201207DTM029","volume-title":"Incomplete Data and Data Dependencies in Relational Databases","author":"Greco","year":"2012"},{"key":"S1471068416000077_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371357"},{"key":"S1471068416000077_ref25","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841300046X"},{"key":"S1471068416000077_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000244"},{"key":"S1471068416000077_ref27","doi-asserted-by":"publisher","DOI":"10.14778\/1920841.1920858"},{"key":"S1471068416000077_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.02.001"},{"key":"S1471068416000077_ref28","doi-asserted-by":"crossref","first-page":"1158","DOI":"10.14778\/3402707.3402750","article-title":"Stratification criteria and rewriting techniques for checking chase termination","volume":"4","author":"Greco","year":"2011","journal-title":"Proc. of the VLDB Endowment"},{"key":"S1471068416000077_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000664"},{"key":"S1471068416000077_ref45","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000165"},{"key":"S1471068416000077_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF01191381"},{"key":"S1471068416000077_ref33","doi-asserted-by":"crossref","unstructured":"Marchiori M. 1996. Proving existential termination of normal logic programs. In Proc. of the 5th International Conference on Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, Vol. 1101. Springer, 375\u2013390.","DOI":"10.1007\/BFb0014328"},{"key":"S1471068416000077_ref53","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000159"},{"key":"S1471068416000077_ref12","article-title":"Object-oriented knowledge bases in logic programming","volume":"13","author":"Chaudhri","year":"2013","journal-title":"Theory and Practice of Logic Programming"},{"key":"S1471068416000077_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"S1471068416000077_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-010-0122-4"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068416000077","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,18]],"date-time":"2020-09-18T00:48:30Z","timestamp":1600390110000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068416000077\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,31]]},"references-count":54,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,5]]}},"alternative-id":["S1471068416000077"],"URL":"https:\/\/doi.org\/10.1017\/s1471068416000077","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,31]]}}}