{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T00:07:43Z","timestamp":1715645263193},"reference-count":40,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T00:00:00Z","timestamp":1380067200000},"content-version":"unspecified","delay-in-days":86,"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":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Recent years have witnessed an increasing interest in enhancing answer set solvers by allowing function symbols. Since the introduction of function symbols makes common inference tasks undecidable, research has focused on identifying classes of programs allowing only a restricted use of function symbols while ensuring decidability of common inference tasks. <jats:italic>Finitely-ground programs<\/jats:italic>, introduced in Calimeri <jats:italic>et al<\/jats:italic>. (2008), are guaranteed to admit a finite number of stable models with each of them of finite size. Stable models of such programs can be computed and thus common inference tasks become decidable. Unfortunately, checking whether a program is finitely-ground is semi-decidable. This has led to several decidable criteria, called <jats:italic>termination criteria<\/jats:italic>, providing sufficient conditions for a program to be finitely-ground. This paper presents a new technique that, used in conjunction with current termination criteria, allows us to detect more programs as finitely-ground. Specifically, the proposed technique takes a logic program <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S147106841300046X_inline1\"\/><jats:tex-math>${\\cal P}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> and transforms it into an adorned program <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S147106841300046X_inline1\"\/><jats:tex-math>${{\\cal P}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sup>\u03bc<\/jats:sup> with the aim of applying termination criteria to <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S147106841300046X_inline1\"\/><jats:tex-math>${{\\cal P}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sup>\u03bc<\/jats:sup> rather than <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S147106841300046X_inline1\"\/><jats:tex-math>${\\cal P}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. The transformation is sound in that if the adorned program satisfies a certain termination criterion, then the original program is finitely-ground. Importantly, applying termination criteria to adorned programs rather than the original ones strictly enlarges the class of programs recognized as finitely-ground.<\/jats:p>","DOI":"10.1017\/s147106841300046x","type":"journal-article","created":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T16:24:58Z","timestamp":1380126298000},"page":"737-752","source":"Crossref","is-referenced-by-count":7,"title":["Logic programming with function symbols: Checking termination of bottom-up evaluation through program adornments"],"prefix":"10.1017","volume":"13","author":[{"given":"SERGIO","family":"GRECO","sequence":"first","affiliation":[]},{"given":"CRISTIAN","family":"MOLINARO","sequence":"additional","affiliation":[]},{"given":"IRINA","family":"TRUBITSYNA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2013,9,25]]},"reference":[{"key":"S147106841300046X_ref37","unstructured":"Syrj\u00e4nen T. 2001. Omega-restricted logic programs. In International Conference on Logic Programming and Nonmonotonic Reasoning, 267\u2013279."},{"key":"S147106841300046X_ref36","unstructured":"Sternagel C. and Middeldorp A. 2008. Root-labeling. In Rewriting Techniques and Applications, 336\u2013350."},{"key":"S147106841300046X_ref35","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002248"},{"key":"S147106841300046X_ref34","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000165"},{"key":"S147106841300046X_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614433"},{"key":"S147106841300046X_ref32","unstructured":"Schneider-Kamp P. , Giesl J. and Nguyen M. T. 2009a. The dependency triple framework for termination of logic programs. In International Symposium on Logic-based Program Synthesis and Transformation, 37\u201351."},{"key":"S147106841300046X_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s002000100064"},{"key":"S147106841300046X_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-010-0122-4"},{"key":"S147106841300046X_ref29","unstructured":"Nguyen M. T. , Giesl J. , Schneider-Kamp P. and De Schreye D. 2007. Termination analysis of logic programs based on dependency graphs. In International Symposium on Logic-based Program Synthesis and Transformation, 8\u201322."},{"key":"S147106841300046X_ref28","first-page":"970","article-title":"On chase termination beyond stratification.","volume":"2","author":"Meier","year":"2009","journal-title":"Proceeding of the Very Large Data Base Conference"},{"key":"S147106841300046X_ref26","unstructured":"Marchiori M. 1996. Proving existential termination of normal logic programs. In Algebraic Methodology and Software Technology, 375\u2013390."},{"key":"S147106841300046X_ref25","unstructured":"Lierler Y. and Lifschitz V. 2009. One more decidable class of finitely ground programs. In International Conference on Logic Programming, 489\u2013493."},{"key":"S147106841300046X_ref23","unstructured":"Greco S. , Spezzano F. and Trubitsyna I. 2012b. On the termination of logic programs with function symbols. In International Conference on Logic Programming (Technical Communications), 323\u2013333."},{"key":"S147106841300046X_ref22","first-page":"1158","article-title":"Stratification criteria and rewriting techniques for checking chase termination.","volume":"4","author":"Greco","year":"2011","journal-title":"Proceeding of the Very Large Data Base Conference"},{"key":"S147106841300046X_ref20","unstructured":"Greco S. , Molinaro C. and Trubitsyna I. 2013. Bounded programs: A new decidable class of logic programs with function symbols. In International Joint Conference on Artificial Intelligence (to appear)."},{"key":"S147106841300046X_ref19","doi-asserted-by":"crossref","DOI":"10.2200\/S00435ED1V01Y201207DTM029","volume-title":"Incomplete Data and Data Dependencies in Relational Databases","author":"Greco","year":"2012"},{"key":"S147106841300046X_ref18","unstructured":"Grau B. C. , Horrocks I. , Kr\u00f6tzsch M. , Kupke C. , Magka D. , Motik B. and Wang Z. 2012. Acyclicity conditions and their application to query answering in description logics. In KR."},{"key":"S147106841300046X_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037169"},{"key":"S147106841300046X_ref16","unstructured":"Gelfond M. and Lifschitz V. 1988. The stable model semantics for logic programming. In International Joint Conference and Symposium on Logic Programming, 1070\u20131080."},{"key":"S147106841300046X_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/BF01191381"},{"key":"S147106841300046X_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.033"},{"key":"S147106841300046X_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9087-9"},{"key":"S147106841300046X_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90027-2"},{"key":"S147106841300046X_ref9","unstructured":"Codish M. , Lagoon V. and Stuckey P. J. 2005. Testing for termination with monotonicity constraints. In International Conference on Logic Programming, 326\u2013340."},{"key":"S147106841300046X_ref8","doi-asserted-by":"crossref","unstructured":"Calimeri F. , Cozza S. , Ianni G. and Leone N. 2010. Enhancing asp by functions: Decidable classes and implementation techniques. In AAAI Conference on Artificial Intelligence.","DOI":"10.1609\/aaai.v24i1.7702"},{"key":"S147106841300046X_ref7","unstructured":"Calimeri F. , Cozza S. , Ianni G. and Leone N. 2008. Computable functions in asp: Theory and implementation. In International Conference on Logic Programming, 407\u2013424."},{"key":"S147106841300046X_ref6","doi-asserted-by":"crossref","unstructured":"Calautti M. , Greco S. and Trubitsyna I. 2013. Detecting decidable classes of finitely ground logic programs with function symbols. In International Symposium on Principles and Practice of Declarative Programming (to appear).","DOI":"10.1145\/2505879.2505883"},{"key":"S147106841300046X_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"S147106841300046X_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.02.001"},{"key":"S147106841300046X_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"S147106841300046X_ref11","unstructured":"Deutsch A. , Nash A. and Remmel J. B. 2008. The chase revisited. In Symposium on Principles of Database Systems, 149\u2013158."},{"key":"S147106841300046X_ref27","unstructured":"Marnette B. 2009. Generalized schema-mappings: from termination to tractability. In Symposium on Principles of Database Systems, 13\u201322."},{"key":"S147106841300046X_ref24","unstructured":"Kr\u00f6tzsch M. and Rudolph S. 2011. Extending decidable existential rules by joining acyclicity and guardedness. In IJCAI, 963\u2013968."},{"key":"S147106841300046X_ref15","unstructured":"Gebser M. , Schaub T. and Thiele S. 2007. Gringo: A new grounder for answer set programming. In International Conference on Logic Programming and Nonmonotonic Reasoning, 266\u2013271."},{"key":"S147106841300046X_ref40","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":"S147106841300046X_ref38","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000159"},{"key":"S147106841300046X_ref39","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1994.1003"},{"key":"S147106841300046X_ref21","first-page":"93","article-title":"Chase termination: A constraints rewriting approach.","volume":"3","author":"Greco","year":"2010","journal-title":"Proceeding of the Very Large Data Base Conference"},{"key":"S147106841300046X_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S147106840900372X"},{"key":"S147106841300046X_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000244"}],"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\/S147106841300046X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T09:28:40Z","timestamp":1715592520000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S147106841300046X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":40,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["S147106841300046X"],"URL":"https:\/\/doi.org\/10.1017\/s147106841300046x","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}