

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

ing properties of programs with aggregates, in particular for reasoning about the correctness of programs with aggregates.

This paper addresses the problems of aggregates mentioned above by (i) giving a new semantics of aggregates that, we argue, is more satisfactory than the existing alternatives, and (ii) providing tools for studying properties of logic programs with aggregates.

Our approach is based on a relationship between two directions of research on extending the stable model semantics: the work on aggregates, mentioned above, and the work on "propositional extensions" (see Figure 1). The latter makes the syntax of rules more and more similar to the syntax of propositional formulas.

In disjunctive programs, the head of each rule is a (possibly empty) disjunction of atoms, while in programs with nested expressions the head and body of each rule can be any arbitrary formula built with connectives AND, OR and NOT. For instance,
¬(p ∨ ¬q) ← p **∨ ¬¬**r is a rule with nested expressions. Programs with nested expressions are quite attractive especially relative to point (ii) above, because many theorems about properties of logic programs have been proved for programs of this kind. For instance, the splitting set theorem [Lifschitz and Turner, 1994; Erdo˘gan and Lifschitz, 2004]
simplifies the task of computing the stable models of a program/theory by breaking it into two parts. Work on strong equivalence [Lifschitz *et al.*, 2001] allows us to