from [Lifschitz *et al.*, 1999], as the definitions from [Gelfond and Lifschitz, 1988, 1991] are essentially its special cases.

The *reduct* ΠX of a program Π with nested expressions relative to a set X of atoms is the result of replacing, in each rule of Π, each maximal subformula of the form ¬F with ⊤ if X |= ¬F, and with ⊥ otherwise. Set X is a *stable model* of Π
if it is a minimal model of ΠX.

7 For instance, if Π is (3) then the reduct Π
{p}is

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

q ← ⊥,

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

while Π∅is

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

p ← ⊤
q ← ⊤,
The stable models of Π - based on this definition of the reduct - are the same ones that we computed in the previous section using the newer definition of a reduct: {p} and {q}. On the other hand, there are differences in the value of the reducts: for instance, we have just seen that Π∅is classically equivalent to {p, q},
while Π∅ = {⊥, ⊥}. However, some similarities between these definitions exist.

For instance, negations are treated essentially in the same way: a nested expression
¬F is transformed into ⊥ if X |= F, and into ⊤ otherwise, under both definitions of a reduct.

The following proposition states a more general relationship between the new definition and the 1999 definition of a reduct.

Proposition 1. For any program Π with nested expressions and any set X *of atoms,*
ΠX *is equivalent, in the sense of classical logic,*
- to ⊥*, if* X 6|= Π*, and*

- to the program obtained from ΠX *by replacing all atoms that do not belong* to X by ⊥*, otherwise.*
Corollary 1. Given two sets of atoms X and Y with Y ⊆ X *and any program* Π
with nested expressions, Y |= ΠX iff X |= Π and Y |= ΠX.

From the corollary above, one of the main claims of this paper follows, that our definition of a stable model is an extension of the definition for programs with nested expressions.

7We underline the set X in Π
X to distinguish this definition of a reduct from the one from the previous section.