and fully support predicates with arbitrary arity; moreover, deciding whether a program belongs to FP2 is decidable, as well as skeptical and credulous stable model reasoning, provided that the query is *call-safe*. Odd cycles are supported by composing FP2 programs with argument restricted programs.

The paper is organized as follows. After some preliminaries on logic programming, in Sec. 3 we introduce *term comparison* relations based on a measure of term size called norm, and show how to compute those relations. In Sec. 4 we apply the term comparison relations to define *recursion patterns*, that is, distinguished sets of arguments whose size almost never increases during recursion; we prove that if a recursion pattern exists then acyclic recursion depth is bounded, and there can be no odd-cycles. Then, in Sec. 6 we define FP2 and show that a form of SLD resolution with loop checking called *acyclic* derivations suffice to compute a representative set of supports for each subgoal relevant to a given query. The output of this phase is a finite ground program that can be fed to an ASP
solver to answer credulous and skeptical queries, in the same spirit as finitary programs.

To re-introduce odd-cycles (and hence the ability to express constraints) in FP2, we show in Sec. 7 how to compose FP2 programs with argument restricted programs. Two sections, on related work and a final discussion, conclude the paper. Many proofs are omitted due to space limitations.

## 2 Preliminaries And Notation

We assume the reader to be familiar with classical logic programming (Lloyd 1984). *(Normal) logic programs* are finite sets of rules A ← L1**, ..., L**n (n ≥ 0), where A is a logical atom and each Li (i = 1**, ..., n**) is a *literal*, that is, either a logical atom B or a negated atom not B. If R is a rule with the above structure, then let head(R) = A and body(R) = {L1**, ..., L**n}. Moreover, let **body**+(R) (respectively **body**−(R)) be the set of all atoms B s.t. B (respectively notB) belongs to **body**(R). For all predicate symbols p, a p-atom A is an atom whose predicate, denoted by pred(A), is p. Similarly a p-literal L
is a literal whose predicate, denoted by pred(L), is p. The ground instantiation of a program P is denoted by Ground(P). A Herbrand model M of P is a *stable model* of P iff M is the least Herbrand model of P M and P M is the *Gelfond-Lifschitz transformation* of P (Gelfond and Lifschitz 1991), obtained from Ground(P) by (i) removing all rules R
such that **body**−(R) ∩ M 6= ∅, and (ii) removing all negative literals from the body of the remaining rules. A *skeptical* consequence of a program P is a formula satisfied by all the stable models of P. A *credulous* consequence of P is a formula satisfied by at least one stable model of P.

The *atom dependency graph of a program* P is a labelled directed graph, denoted by DGa(P), whose vertices are the ground atoms of P's language. Moreover, i) there exists an edge labelled '+' (called positive edge) from A to B iff for some rule R ∈ Ground(P), A = head(R) and B ∈ **body**(R);
ii) there exists an edge labelled '-' (called negative edge) from A to B iff for some rule R ∈ Ground(P), A = head(R) and not B ∈ **body**(R).

An atom A *depends* on B if there is a directed path from A to B in DGa(P). Similarly, the *predicate dependency graph of a program* P is a labelled directed graph, denoted by