Unfounded Sets and Well-Founded Semantics of Answer Set Programs with Aggregates

Logic programs with aggregates (LPA) are one of the major linguistic extensions to Logic Programming (LP). In this work, we propose an extension of the notions of unfounded set and the well-founded semantics for programs with monotone and antimonotone aggregates (LPAm,a programs). The restriction on monotone and antimonotone aggregates allows for a clean extension that, as it turns out, keeps almost all of the important properties of the aggregate-free setting. In more detail, a new notion of unfounded set for LPAm,a programs is presented, which is a sound generalization of the original definition for standard LP provided by Van Gelder, Ross, and Schlipf (1988). On this basis, a well-founded operator for LPAm,a programs is defined, the fixpoint of which is called well-founded model (or well-founded semantics) for LPAm,a programs. The most important properties of unfounded sets and the well-founded semantics are retained by this generalization, notably existence and uniqueness, and a strong relationship to the answer set semantics for LPAm,a programs. Also complexity issues are discussed in detail, most importantly a formal proof of tractable computation of the well-founded model for LPAm,a programs is given. It also turns out that one ˜D -well-founded semantics, defined by Pelov, Denecker, and Bruynooghe (2007) for a broader class of aggregates using approximating operators, coincides with the well-founded model as defined in this work on LPAm,a programs. This implies that the results in this paper carry over to that semantics as well, and, vice versa, some of the results of Pelov et al. (2007) are confirmed by ours. In order to justify the restriction on LPAm,a programs, it is shown that for general LPA programs, which may contain aggregates that are neither monotone nor antimonotone, deciding satisfaction of aggregate expressions with respect to partial interpretations is coNP-complete. As a consequence, a well-founded semantics for general LPA programs that allows for tractable computation is unlikely to exist. In general, most obvious extensions of LPAm,a programs appear to necessitate a substantial change in the definition of unfounded sets, and do no longer satisfy some of their important properties and those of the resulting well-founded semantics. Finally, a prototype system extending DLV is presented, which supports the wellfounded semantics for LPAm,a programs, at the time of writing the only implemented system that does so. Experiments with this prototype show significant computational advantages of aggregate constructs over equivalent aggregate-free encodings.