This technical note describes a monotone and continuous fixpoint operator to compute the answer sets of programs with aggregates. The fixpoint operator relies on the notion of aggregate solution. Under certain conditions, this operator behaves identically to the three-valued immediate consequence operator @math for aggregate programs, independently proposed This operator allows us to closely tie the computational complexity of the answer set checking and answer sets existence problems to the cost of checking a solution of the aggregates in the program. Finally, we relate the semantics described by the operator to other proposals for logic programming with aggregates. To appear in Theory and Practice of Logic Programming (TPLP).
For the sake of completeness, we will review the translation of @cite_5 , presented using the notation of our paper. Given a ground logic program with aggregates @math , @math denotes the ground normal logic program obtained after the translation. The process begins with the translation of each aggregate atom @math of the form @math into a disjunction @math , where @math , and each @math is a conjunction of the form [ l s_1 l l H ( ) s_2 l ] The construction of @math considers only the pairs @math that satisfy the following condition: each interpretation @math such that @math and @math must satisfy @math . The translation @math is then created by replacing rules with disjunction in the body by a set of standard rules in a straightforward way. For example, the rule [ a (b c), d ] is replaced by the two rules [ ] From the definitions of @math and of aggregate solutions, we have the following simple lemma: We next show that fixed point answer sets of @math are answer sets of @math .
@cite_5
2064864283 2004414305 2010968193 80590317
The addition of aggregates has been one of the most relevant enhancements to the language of answer set programming (ASP). They strengthen the modelling power of ASP in terms of natural and concise problem representations. Previous semantic definitions typically agree in the case of non-recursive aggregates, but the picture is less clear for aggregates involved in recursion. Some proposals explicitly avoid recursive aggregates, most others differ, and many of them do not satisfy desirable criteria, such as minimality or coincidence with answer sets in the aggregate-free case. In this paper we define a semantics for programs with arbitrary aggregates (including monotone, antimonotone, and nonmonotone aggregates) in the full ASP language allowing also for disjunction in the head (disjunctive logic programming - DLP). This semantics is a genuine generalization of the answer set semantics for DLP, it is defined by a natural variant of the Gelfond-Lifschitz transformation, and treats aggregate and non-aggregate literals in a uniform way. This novel transformation is interesting per se also in the aggregate-free case, since it is simpler than the original transformation and does not need to differentiate between positive and negative literals. We prove that our semantics guarantees the minimality (and therefore the incomparability) of answer sets, and we demonstrate that it coincides with the standard answer set semantics on aggregate-free programs. Moreover, we carry out an in-depth study of the computational complexity of the language. The analysis pays particular attention to the impact of syntactical restrictions on programs in the form of limited use of aggregates, disjunction, and negation. While the addition of aggregates does not affect the complexity of the full DLP language, it turns out that their presence does increase the complexity of normal (i.e., non-disjunctive) ASP programs up to the second level of the polynomial hierarchy. However, we show that there are large classes of aggregates the addition of which does not cause any complexity gap even for normal programs, including the fragment allowing for arbitrary monotone, arbitrary antimonotone, and stratified (i.e., non-recursive) nonmonotone aggregates. The analysis provides some useful indications on the possibility to implement aggregates in existing reasoning engines. We propose a new translation from normal logic programs with constraints under the answer set semantics to propositional logic. Given a normal logic program, we show that by adding, for each loop in the program, a corresponding loop formula to the program's completion, we obtain a one-to-one correspondence between the answer sets of the program and the models of the resulting propositional theory. In the worst case, there may be an exponential number of loops in a logic program. To address this problem, we propose an approach that adds loop formulas a few at a time, selectively. Based on these results, we implement a system called ASSAT(X), depending on the SAT solver X used, for computing one answer set of a normal logic program with constraints. We test the system on a variety of benchmarks including the graph coloring, the blocks world planning, and Hamiltonian Circuit domains. Our experimental results show that in these domains, for the task of generating one answer set of a normal logic program, our system has a clear edge over the state-of-art answer set programming systems Smodels and DLV. Let P be an arbitrary theory and let X be any given logic. Let M be a set of atoms. We say that M is a X-stable model of P if M is a classical model of P and P∪¬M proves in logic X all atoms in M, this is denoted by P∪¬M ⊩xM. We prove that being an X-stable model is an invariant property for disjunctive programmes under a large class of logics. Two kinds of logics are mainly considered: paraconsistent logics and normal modal logics. For modal logics we use a translation proposed by Gelfond that replaces ¬a with ¬□a. As a consequence we prove that several semantics (recently introduced) for non-monotonic reasoning are equivalent for disjunctive programmes. In addition, we show that such semantics can be characterized by a fixed-point operator in terms of classical logic. We also present a simple translation of a disjunctive programme D into a normal programme N, such that the PStable model semantics of N corresponds to the stable semantics of D over the common language. We present the formal proof of this statement. Dept. of Computer Science, K.U.LeuvenCelestijnenlaan 200A, B-3001 Heverlee, BelgiumE-mail: pelov,marcd,maurice @cs.kuleuven.ac.beAbstract. We deﬁne a translation of aggregate programs to normal lo-gic programs which preserves the set of partial stable models. We thendeﬁne the classes of deﬁnite and stratiﬁed aggregate programs and showthat the translation of such programs are, respectively, deﬁnite and strat-iﬁed logic programs. Consequently these two classes of programs havea single partial stable model which is two-valued and is also the well-founded model. Our deﬁnition of stratiﬁcation is more general than theexisting one and covers a strictly larger class of programs.