Definition 19 (Buccafurri and Gottlob 2002) Let P be a positive program. We define the program Γ(P**) over the set of atoms**
Var (Γ(P**)) =** {aP | a ∈ Var (P)}∪{a
′
P | a ∈ Var (P)}∪{saP | a ∈ Var (P)}∪{**f ail**P }
as the union of the sets of rules S1, S2 and S3**, defined as follows:**

$$\begin{array}{r l}{S_{1}=}&{{}\left\{\,a_{P}\leftarrow\mathrm{not}\ a_{P}^{\prime}\ |\ a\in V\right.}\end{array}$$
$\left(\frac{1}{2}\right)^{2}+\left(\frac{1}{2}\right)^{2}+\left(\frac{1}{2}\right)^{2}+\left(\frac{1}{2}\right)^{2}+\left(\frac{1}{2}\right)^{2}$ 4. 
P | a ∈ Var (P)**} ∪ {**a
′
P ←not aP | a ∈ Var (P)}

$S_{2}=\quad\{\,s_{ap}\gets b_{p}^{1},\cdots,b_{p}^{n}\mid a\gets b_{1},\ldots b_{n}\in{\cal P}\}$  $S_{3}=\quad\{\,fail_{\cal P}\leftarrow$_not fail${}_{\cal P},s_{ap},$not a${}_{\cal P}\mid a\in$_Var_(${\cal P}$)$\}\cup$  $\{\,fail_{\cal P}\leftarrow$_not fail${}_{\cal P},$_not s_{ap}\mid a\in$_Var_(${\cal P}$)$\}$.  
Note that Definition 16 (introducing Γ′**) can be viewed as an extension of the**
above definition, since the former takes into account social conditions, while the latter does not. In fact, the transformations Γ′ **and Γ produce the same result in**
case of programs with no social conditions.

Proposition 1 Given a SOLP program P, it holds that Γ′(A(Pˆ)) = Γ(A(P**ˆ)).**

## Proof

Since A(P**ˆ) contains no social condition, it is easy to see that, according to Definitions 16 and 19 (pages 17 and 19),** S
′
1
(A(Pˆ)) = S1(A(P**ˆ)),** S
′
2
(A(Pˆ)) = S2(A(Pˆ))
and S
′
3
(A(Pˆ)) = S3(A(Pˆ)). As a consequence, Γ′(A(Pˆ)) = Γ(A(P**ˆ)).**
Lemma 2 (Buccafurri and Gottlob 2002) Let P **be a traditional logic program. Then**

$$S M(\Gamma({\mathcal{P}}))=\bigcup_{F\in F P({\mathcal{P}})}\{[F]_{{\mathcal{P}}}\}.$$

Once we have recalled the results from (Buccafurri and Gottlob 2002), we introduce some more results that we shall use in order to prove item (2).

Proposition 2 Let P be a SOLP program. Then FP(A(P**ˆ)) =** AFP(P).

## Proof

First observe that, given a SOLP program P, it holds that A(Pˆ) = Qˆ **where** Q =
A(P), i.e. the result of the joint application of the two operators A**() and ˆ is**
invariant w.r.t. to the order of application. In fact, according to the definitions of both A**() (see page 9) and ˆ (see Definition 15 on page 17), it is easy to see that**
the former operates only on social conditions, while the latter does **not, since it**
operates on both standard atoms and okay **predicates. Thus, the two operators** have disjoint application domains. Hence, the order of application is not relevant.

As a result it holds that, FP(A(Pˆ)) = FP(Qˆ ) where Q = A(P**) and, according**
to the traditional definition of fixpoint of a logic program (page 9), FP(Qˆ ) = {X | TQˆ (X ) = X ∧ X ∈ 2 Var(Qˆ )}.

Now, according to the definition of the classical immediate consequence operator