Declarative and Computational Properties of Logic Programs with Aggregates

We investigate the properties of logic programs with aggregates. We mainly focus on programs with monotone and antimonotone aggregates (LPAma programs). We define a new notion of unfounded set for LPAma programs, and prove that it is a sound generalization of the standard notion of unfounded set for aggregate-free programs. We show that the answer sets of an LPAma program are precisely its unfounded-free models.We define a well-founded operator WP for LPAma programs; we prove that its total fixpoints are precisely the answer sets of P, and its least fixpoint WP() is contained in the intersection of all answer sets (if P admits an answer set). WP() is efficiently computable, and for aggregate-free programs it coincides with the well-founded model.We carry out an in-depth complexity analysis in the general framework, including also nonmonotone aggregates. We prove that monotone and antimonotone aggregates do not increase the complexity of cautious reasoning, which remains in co-NP. Nonmonotone aggregates, instead, do increase the complexity by one level in the polynomial hierarchy. Our results allow also to generalize and speedup ASP systems with aggregates.