Fig. 3. Satisfiability check for Quantified Boolean Formulas

![0_image_0.png](0_image_0.png)

- Both FDNC and FP2 programs may have infinite and infinitely many answer sets.

- Unlike FP2 programs, the answer sets of FDNC programs can be finitely represented.

- Ground and nonground queries over FDNC programs are always computable; only call-safe queries are computable for FP2 programs.

- FDNC programs are safe, while FP2 programs admit unsafe rules.

- Odd-cycles may occur in FDNC programs but not in FP2 programs.

- FDNC programs are disjunctive.
Therefore, FDNC and FP2 programs are incomparable. The programs in Figures 1, 2 and 3 and in Example 4.5 are examples of FP2 programs that are not FDNC.

## 9 Summary And Conclusions

We have introduced FP2, a decidable class of well-behaved normal programs whose properties are orthogonal to those of the other decidable classes of ASP programs with function symbols.

Inference is decidable, too. We have shown a method based on a partial evaluation of the program w.r.t. a query Q (algorithm SUPPORTSUBPROGRAM) that produces a ground program S(**P, Q**) that can be fed to any ASP reasoner in order to answer Q. The query Q needs not be ground: it can be call-safe, and it is not hard to see that the method can produce answer substitutions by unifying Q with the stable models of S(**P, Q**).

Note that currently this mixed top-down/ASP solving method is not intended to be an efficient implementation; it is only a proof method for decidability results. In future work the potential of top-down computations as an implementation technique should be evaluated and compared with the magic-set approach adopted in (Calimeri et al. 2008).

The norm-based definition of FP2 programs is actually a simplification of the (approximate) static analysis method for recognizing U-bounded finitary programs described in
(Bonatti 2001; Bonatti 2004). The binding propagation analysis of the old recognizer is more powerful, and we are planning to improve FP2 to cover more programs accepted with the old method. Further interesting issues for future work comprise: a precise complexity analysis of FP2 membership checking and inference; support for disjunctive programs; more general forms of composition with persistently CFSP programs; integration with FDNC programs for more general support to odd-cycles.