Hostname: page-component-cd9895bd7-lnqnp Total loading time: 0 Render date: 2024-12-17T22:27:58.729Z Has data issue: false hasContentIssue false
  • English
  • Français

A decidable subclass of finitary programs

Published online by Cambridge University Press:  09 July 2010

SABRINA BASELICE  and
PIERO A. BONATTI
SABRINA BASELICE
Affiliation:
Università di Napoli “Federico II”, Italy
PIERO A. BONATTI
Affiliation:
Università di Napoli “Federico II”, Italy
Get access Rights & Permissions [Opens in a new window]

Abstract

Answer set programming—the most popular problem solving paradigm based on logic programs—has been recently extended to support uninterpreted function symbols (Syrjänen 2001, Bonatti 2004; Simkus and Eiter 2007; Gebser et al. 2007; Baselice et al. 2009; Calimeri et al. 2008). All of these approaches have some limitation. In this paper we propose a class of programs called FP2 that enjoys a different trade-off between expressiveness and complexity. FP2 is inspired by the extension of finitary normal programs with local variables introduced in (Bonatti 2004, Section 5). FP2 programs enjoy the following unique combination of properties: (i) the ability of expressing predicates with infinite extensions; (ii) full support for predicates with arbitrary arity; (iii) decidability of FP2 membership checking; (iv) decidability of skeptical and credulous stable model reasoning for call-safe queries. Odd cycles are supported by composing FP2 programs with argument restricted programs.

Keywords

answer set programming with function symbolsinfinite stable modelsnorms
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 10 , Special Issue 4-6: 26th International Conference on Logic Programming , July 2010 , pp. 481 - 496
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Baselice, S. and Bonatti, P. A. 2008. Composing normal programs with function symbols. See de la Banda and Pontelli (2008), 425–439.Google Scholar
Baselice, S., Bonatti, P. A., and Criscuolo, G. 2009. On finitely recursive programs. Theory and Practice of Logic Programming 9, 2, 213–238.CrossRefGoogle Scholar
Bonatti, P. 2001. Prototypes for reasoning with infinite stable models and function symbols. In Logic Programming and Nonmonotonic Reasoning, 6th International Conference, LPNMR 2001. LNCS, vol. 2173. Springer, 416–419.Google Scholar
Bonatti, P. A. 2004. Reasoning with infinite stable models. Artificial Intelligence 156, 1, 75–111.CrossRefGoogle Scholar
Bonatti, P. A. 2008. Erratum to: Reasoning with infinite stable models [Artificial Intelligence 156 (1) (2004) 75–111]. Artificial Intelligence 172, 15, 1833–1835.CrossRefGoogle Scholar
Bossi, A., Cocco, N., and Fabris, M. 1994. Norms on terms and their use in proving universal termination of a logic program. Theoretical Computer Science 124, 2, 297–328.CrossRefGoogle Scholar
Calimeri, F., Cozza, S., Ianni, G., and Leone, N. 2008. Computable functions in ASP: Theory and implementation. See de la Banda and Pontelli (2008), 407–424.Google Scholar
Calimeri, F., Cozza, S., Ianni, G., and Leone, N. 2009. Magic sets for the bottom-up evaluation of finitely recursive programs. In LPNMR, Erdem, E., Lin, F., and Schaub, T., Eds. Lecture Notes in Computer Science, vol. 5753. Springer, 71–86.Google Scholar
de la Banda, M. G. and Pontelli, E., Eds. 2008. Logic Programming, 24th International Conference, ICLP 2008, Udine, Italy, December 9–13, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5366. Springer.Google Scholar
Eiter, T., Leone, N., Mateis, C., Pfeifer, G., and Scarcello, F. 1997. A Deductive System For Non-Monotonic Reasoning. In Logic Programming and Nonmonotonic Reasoning, 4th International Conference, LPNMR'97, Proceedings. Lecture Notes in Computer Science, vol. 1265. Springer, 364–375.Google Scholar
Gebser, M., Schaub, T., and Thiele, S. 2007. Gringo: A new grounder for answer set programming. In LPNMR, Baral, C., Brewka, G., and Schlipf, J. S., Eds. Lecture Notes in Computer Science, vol. 4483. Springer, 266–271.Google Scholar
Gelfond, M. and Lifschitz, V. 1991. Classical negation in logic programs and disjunctive databases. New Generation Computing 9, 3–4, 365–386.CrossRefGoogle Scholar
Genaim, S., Codish, M., Gallagher, J., and Lagoon, V. 2002. Combining norms to prove termination. In Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002. Lecture Notes in Computer Science, vol. 2294. Springer, 126–138.Google Scholar
Lierler, Y. and Lifschitz, V. 2009. One more decidable class of finitely ground programs. In ICLP, Hill, P. M. and Warren, D. S., Eds. Lecture Notes in Computer Science, vol. 5649. Springer, 489–493.Google Scholar
Lloyd, J. W. 1984. Foundations of Logic Programming, 1st ed.Springer.CrossRefGoogle Scholar
Marek, V. W. and Remmel, J. B. 2008. On the continuity of Gelfond-Lifschitz operator and other applications of proof-theory in ASP. See de la Banda and Pontelli (2008), 223–237.Google Scholar
Niemelä, I. and Simons, P. 1997. Smodels—an implementation of the stable model and well-founded semantics for normal LP. In Logic Programming and Nonmonotonic Reasoning, 4th International Conference, LPNMR'97, Proceedings. Lecture Notes in Computer Science, vol. 1265. Springer, 421–430.Google Scholar
Simkus, M. and Eiter, T. 2007. FDNC: Decidable non-monotonic disjunctive logic programs with function symbols. In 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007. Lecture Notes in Computer Science, vol. 4790. Springer, 514–530.Google Scholar
Syrjänen, T. 2001. Omega-restricted logic programs. In LPNMR, Eiter, T., Faber, W., and Truszczynski, M., Eds. Lecture Notes in Computer Science, vol. 2173. Springer, 267–279.Google Scholar