Proof. It is easy to see that if X 6|= Π then X 6|= ΠX and X 6|= ΠX, so that X
is not a stable model under either semantics. Now assume that X |= Π. We will show that the two reducts are satisfied by the same subsets of X. It is sufficient to consider the case in which Π contains only one rule

$$A_{1}\land\cdots\wedge A_{m}\to a_{1}\lor\cdots\lor a_{n}.$$
A1 ∧ · · · ∧ Am → a1 **∨ · · · ∨** an. (44)
$\colon X\not\equiv A_1\land$. 
If X 6|= A1 **∧ · · · ∧** Am then Π
X = ∅, and ΠX is the tautology

$$(44)^{\frac{1}{2}}$$
$\mathrm{s}$ the tautology. 
⊥ → (a1 **∨ · · · ∨** an)
X.

Otherwise, Π
X is rule (44), and ΠX is A
X
1 **∧ · · · ∧** A
X
m → (a1 **∨ · · · ∨** an)
X .

These two reducts are satisfied by the same subsets of X by Lemmas 22 and 23.

## 5 Conclusions

We have proposed a new definition of stable model - for proposition theories —
that is simple, very general, and that inherits several properties from logic programs with nested expressions. On top of that, we have defined the concept of an aggregate, both as an atomic operator and as a propositional formula. We hope that this very general framework may be useful in the heterogeneous world of aggregates in answer set programming.

## Acknowledgements

We thank Vladimir Lifschitz for many useful comments on a draft of this paper.

## References

[Baral and Uyan, 2001] Chitta Baral and Cenk Uyan. Declarative specification and solution of combinatorial auctions using logic programming. *Lecture Notes* in Computer Science, 2173:186–199, 2001.

[Cabalar and Ferraris, 2007] Pedro Cabalar and Paolo Ferraris. Propositional theories are strongly equivalent to logic programs. *Theory Pract. Log. Program.*,
7(6):745–759, 2007.