{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T19:48:56Z","timestamp":1672516136123},"reference-count":43,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2014,8,13]],"date-time":"2014-08-13T00:00:00Z","timestamp":1407888000000},"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":[[2015,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Recently, there has been an increasing interest in the bottom-up evaluation of the semantics of logic programs with complex terms. The presence of function symbols in the program may render the ground instantiation infinite, and finiteness of models and termination of the evaluation procedure, in the general case, are not guaranteed anymore. Since the program termination problem is undecidable in the general case, several decidable criteria (called program termination criteria) have been recently proposed. However, current conditions are not able to identify even simple programs, whose bottom-up execution always terminates. The paper introduces new decidable criteria for checking termination of logic programs with function symbols under bottom-up evaluation, by deeply analyzing the program structure. First, we analyze the propagation of complex terms among arguments by means of the extended version of the argument graph called<jats:italic>propagation graph<\/jats:italic>. The resulting criterion, called<jats:italic>acyclicity<\/jats:italic>, generalizes most of the decidable criteria proposed so far. Next, we study how rules may activate each other and define a more powerful criterion, called<jats:italic>safety<\/jats:italic>. This criterion uses the so-called<jats:italic>safety function<\/jats:italic>able to analyze how rules may activate each other and how the presence of some arguments in a rule limits its activation. We also study the application of the proposed criteria to bound queries and show that the safety criterion is well-suited to identify relevant classes of programs and bound queries. Finally, we propose a hierarchy of classes of terminating programs, called<jats:italic>k-safety<\/jats:italic>, where the<jats:italic>k<\/jats:italic>-safe class strictly includes the (<jats:italic>k<\/jats:italic>-1)-safe class.<\/jats:p>","DOI":"10.1017\/s1471068414000623","type":"journal-article","created":{"date-parts":[[2014,8,13]],"date-time":"2014-08-13T21:08:39Z","timestamp":1407964119000},"page":"854-889","source":"Crossref","is-referenced-by-count":5,"title":["Checking termination of bottom-up evaluation of logic programs with function symbols"],"prefix":"10.1017","volume":"15","author":[{"given":"MARCO","family":"CALAUTTI","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"SERGIO","family":"GRECO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"FRANCESCA","family":"SPEZZANO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"IRINA","family":"TRUBITSYNA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,8,13]]},"reference":[{"key":"S1471068414000623_ref42","first-page":"133","volume-title":"Proc. of 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR)","author":"Voets","year":"2010"},{"key":"S1471068414000623_ref39","first-page":"184","volume-title":"Proc. of 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR)","author":"Str\u00f6der","year":"2010"},{"key":"S1471068414000623_ref34","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000165"},{"key":"S1471068414000623_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614433"},{"key":"S1471068414000623_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s002000100064"},{"key":"S1471068414000623_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-010-0122-4"},{"key":"S1471068414000623_ref28","unstructured":"Meier M. , Schmidt M. and Lausen G. 2009. On chase termination beyond stratification. CoRR abs\/0906.4228."},{"key":"S1471068414000623_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014328"},{"key":"S1471068414000623_ref25","first-page":"489","volume-title":"Proc. of 25th International Conference on Logic Programming (ICLP)","author":"Lierler","year":"2009"},{"key":"S1471068414000623_ref43","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":"S1471068414000623_ref21","first-page":"323","volume-title":"Proc. of International Conference on Logic Programming (Technical Communications)","author":"Greco","year":"2012"},{"key":"S1471068414000623_ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2003.1185840"},{"key":"S1471068414000623_ref15","first-page":"1070","volume-title":"Proc. of 5th International Conference and Symposium on Logic Programming (ICLP\/SLP)","author":"Gelfond","year":"1988"},{"key":"S1471068414000623_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72200-7_24"},{"key":"S1471068414000623_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72200-7_23"},{"key":"S1471068414000623_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90027-2"},{"key":"S1471068414000623_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/BF01191381"},{"key":"S1471068414000623_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.033"},{"key":"S1471068414000623_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9087-9"},{"key":"S1471068414000623_ref9","first-page":"326","volume-title":"Proc. of 21st International Conference on Logic Programming (ICLP)","author":"Codish","year":"2005"},{"key":"S1471068414000623_ref8","first-page":"407","volume-title":"Proc. of 24th International Conference on Logic Programming (ICLP)","author":"Calimeri","year":"2008"},{"key":"S1471068414000623_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.02.001"},{"key":"S1471068414000623_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(91)90038-Q"},{"key":"S1471068414000623_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S147106840900372X"},{"key":"S1471068414000623_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"S1471068414000623_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000244"},{"key":"S1471068414000623_ref29","first-page":"8","volume-title":"Proc. of 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR)","author":"Nguyen","year":"2007"},{"key":"S1471068414000623_ref36","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002248"},{"key":"S1471068414000623_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068413000446"},{"key":"S1471068414000623_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70590-1_23"},{"key":"S1471068414000623_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_13"},{"key":"S1471068414000623_ref20","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":"Proceedings of the VLDB Endowment (PVLDB)"},{"key":"S1471068414000623_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/BF02575754"},{"key":"S1471068414000623_ref27","first-page":"13","volume-title":"Proc. of 28th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS)","author":"Marnette","year":"2009"},{"key":"S1471068414000623_ref19","doi-asserted-by":"publisher","DOI":"10.14778\/1920841.1920858"},{"key":"S1471068414000623_ref22","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1996.0009"},{"key":"S1471068414000623_ref32","first-page":"37","volume-title":"Proc. of 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR)","author":"Schneider-Kamp","year":"2009"},{"key":"S1471068414000623_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45757-7_50"},{"key":"S1471068414000623_ref40","first-page":"267","volume-title":"Proc. of 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR)","author":"Syrj\u00e4nen","year":"2001"},{"key":"S1471068414000623_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"S1471068414000623_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002273"},{"key":"S1471068414000623_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037169"},{"key":"S1471068414000623_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00187-X"}],"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\/S1471068414000623","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T05:47:44Z","timestamp":1598161664000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068414000623\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,13]]},"references-count":43,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["S1471068414000623"],"URL":"https:\/\/doi.org\/10.1017\/s1471068414000623","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,13]]}}}