Example 6.3 The append program of Example 4.5 is in FP2. It is easy to verify that if τappend = {3} then τ is not only a recursion pattern (see Ex. 4.5), but also a call pattern. On the contrary, the recursion pattern yielded by τappend = {1} is not a call pattern because the variable L in the first rule occurs neither in the selected argument (the first one) nor in the body. However this recursion pattern is contained in two call patterns, defined by τappend = {1, 2} and τappend = {1, 3}.

For an example of a cyclic FP2 program with negation see the blocks world program in
(Bonatti 2004, Fig.4). To make it an FP2 program, uniformly replace T + 1 with T in the second arguments of predicate ab. Then the (unique) selection index that is complete for all predicates is a call pattern for the program.

In general, it may be necessary to use different call patterns for different initial goals, in order to satisfy call safeness. In the above example a goal append(t1, t2, t3) is call safe w.r.t. some call pattern iff either t3 is ground or at least two arguments are ground; different situations require different call patterns.

## 6.1 Inference In Fp2

The ground skeptical and credulous consequences of finitary programs can be computed by using a ground "relevant" fragment of their ground instantiation (Bonatti 2004). Similarly, we can reason over FP2 programs by answering queries over finite and ground programs called support subprograms.

We start by defining a function Ssup(**G, P**) that, for all call-safe a-goals G and FP2 programs P, returns a representative set of supports for G w.r.t. P. More precisely, let Ssup(**G, P**) be the set of all pairs (**θ, s**) such that s is an acyclic support of G in P with global answer θ.

## Proposition 6.4

Let P ∈ FP2 be a program with a call pattern τ. The restriction of Ssup(**G, P**) to all G
that are call-safe w.r.t. τ is computable.

Proof. (Sketch) By Corollary 5.10, acyclic a-derivations of G from P are finite and finitely many. Then, it suffices to enumerate all acyclic a-derivations of G from P. ✷

## Definition 6.5

Let P be a program and Q be an atom. The *support subprogram* S(**P, Q**) for Q w.r.t. P is the set computed by the algorithm SUPPORTSUBPROGRAM (**P, Q**) below.

For all FP2 programs and suitably instantiated atoms Q, the support subprogram S(**P, Q**)
is finite, ground, and computable.

## Theorem 6.6

Let P ∈ FP2 be a program with a call pattern τ. For all atoms Q such that Q[τ] is ground, the algorithm SUPPORTSUBPROGRAM (**P, Q**) terminates and returns a ground program.