# A Decidable Subclass Of Finitary Programs

Sabrina Baselice, Piero A. Bonatti Universit`a di Napoli "Federico II", Italy submitted 1 January 2003; revised 1 January 2003; accepted 1 *January 2003*

## Abstract

Answer set programming - the most popular problem solving paradigm based on logic programs - has been recently extended to support uninterpreted function symbols (Syrj¨anen 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, Sec. 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 symbols, Infinite stable models, Norms.

## 1 Introduction

Answer set programming has become the most popular problem solving paradigm based on logic programs. It is founded on the stable model semantics (Gelfond and Lifschitz 1991) and supported by well-engineered implementations such as SMODELS (Niemel¨a and Simons 1997)
and DLV (Eiter et al. 1997), just to name a few. Recent developments of the paradigm and its implementations include support for uninterpreted function symbols, pioneered by the work on finitary programs (Bonatti 2004; Bonatti 2008). These works gave rise to further developments, including argument restricted programs (Lierler and Lifschitz 2009)
and FDNC programs (Simkus and Eiter 2007), that address three limitations of finitary programs: a restriction on the number of odd-cycles in the dependency graph; the undecidability of the class of finitary programs; the dependency of reasoning on the set of oddcycles, for which there is currently no general algorithm (Bonatti 2008). The drawback of these approaches, in turn, is that either they cannot express predicates with infinite extensions such as the standard list and tree manipulation predicates (Calimeri et al. 2008), or they have to restrict predicate arity and rule structure in such a way that - roughly speaking - only models shaped like labelled trees can be characterized (Simkus and Eiter 2007).

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 U-bounded programs (the extension of finitary normal programs with bounded local variables introduced in (Bonatti 2004, Sec. 5)). FP2 programs retain the ability of expressing predicates with infinite extensions, arXiv:1007.3663v1 [cs.AI] 21 Jul 2010