Finitely recursive programs: Decidability and bottom-up computation

The support for function symbols in logic programming under answer set semantics allows us to overcome some modeling limitations of traditional Answer Set Programming (ASP) systems, such as the inability of handling infinite domains. On the other hand, admitting function symbols in ASP makes inference undecidable in the general case. Recently, the research community has been focusing on finding proper subclasses of programs with functions for which decidability of inference is guaranteed. The two major proposals, so far, are finitary programs and finitely-ground programs. These two proposals are somehow complementary: indeed, the former is conceived to allow decidable querying (by means of a top-down evaluation strategy), while the latter supports the computability of answer sets (by means of a bottom-up evaluation strategy). One of the main advantages of finitely-ground programs is that they can be "directly" evaluated by current ASP systems, which are based on a bottom-up computational model. However, there are also some interesting programs which are suitable for top-down query evaluation; but they do not fall in the class of finitely-ground programs. In this paper, we focus on disjunctive finitely recursive positive (DFRP) programs. We design a version of the magic sets technique for DFRP programs, which ensures query equivalence under both brave and cautious reasoning. We show that, if the input program is DFRP, then its magic-sets rewriting is guaranteed to be finitely ground. Reasoning on DFRP programs turns out to be decidable; and we provide also an effective method that allows one to simply perform this reasoning by using the ASP system DLV.