

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

modify a program/theory with the guarantee that stable models are preserved (more details in Section 2.4).

Nested expressions have already been used to express aggregates: [Ferraris and Lifschitz, 2005b]
showed that each weight constraint can be replaced by a nested expressions, preserving its stable models. As a consequence, theorems about nested expressions can be used for programs with weight constraints. It turns out, however, that nested expressions are not sufficiently general for defining a semantics for aggregates that overcomes the unintuitive features of the existing approaches. For this reason, we extend the syntax of rules with nested expressions, allowing implication in every part of a "rule", and not only as the outermost connective. (We understand a rule as an implication from the body to the head). A "rule" is then an arbitrary propositional formula, and a program an arbitrary propositional theory. Our new definition of a stable model, like all the other definitions, is based on the process of constructing a reduct. The process that we use looks very different from all the others, and in particular for programs with nested expressions. Nevertheless, it turns out that in application to programs with nested expressions, our definition is equivalent to the one from [Lifschitz *et al.*, 1999]. This new definition of a stable model also turns out to closely related to equilibrium logic [Pearce, 1997], a logic based on the concept of a Kripke-model in the logic of here-and-there. Also, we will show that many theorems about programs with nested expressions extend to arbitrary propositional theories.