Definition 17 Given a SOLP collection {P1, · · · ,Pn}**, we define the program** P
′u =S1≤i≤n Γ
′(Pˆi).

P
′u is obtained by combining the translations of all the SOLP programs in a given SOLP collection, where the social conditions are replaced by ρ**-atoms. The**
generation of P
′u concludes task (b**) of the translation process. Then, the program**
P
′u is merged with the LPA program C(P1, · · · ,Pn**) - obtained as a result of task**
(a) - in order to enable the social conditions (recall that C(P1, · · · ,Pn**) contains**
the ρ**-atoms as heads of rules, thus allowing the activation of some rule bodies in** P
′u). Finally, the social models of the SOLP collection {P1, · · · ,Pn} **can be found**
by computing the stable models of the logic program P
′u ∪ C(P1, **· · ·** ,Pn).

Once we have described how the translation mechanism proceeds, we need to demonstrate that it is sound and complete. To this aim, we have to prove the following results:
(1) The ρ-atoms occurring in C(P1, · · · ,Pn**) are in one-to-one correspondence**
with true SCs for {P1, **· · ·** ,Pn}.

(2) A one-to-one correspondence exists between the social models of P1, **· · ·** ,Pn and the stable models of the LPA **program** P
′u ∪ C(P1, **· · ·** ,Pn).

First, we prove item (1) above.

Lemma 1 Given a SOLP collection SP = {P1, · · · ,Pn}, an integer j (1 ≤ j ≤ n**), a SOLP**
program Pj ∈ SP, a social interpretation ¯I for SP **and a SC** s ∈ MSC Pj**, it holds**
that s is true for Pj w.r.t. ¯I iff ∃M ∈ SM (C(P1, · · · ,Pn) ∪ Q**) s.t.** ρ(s)Pj ∈ M ,
where Q = {a ←| a ∈ ¯I }.

## Proof See Appendix A.

Intuitively, a given social interpretation ¯I will infer rule heads in C(P1, **· · ·** ,Pn).

These are either labelled ρ-atoms or labelled g**-predicates. Lemma 1 states that**
the ρ-atoms occurring in C(P1, · · · ,Pn**) are in one-to-one correspondence with true**
social conditions. Now, since those ρ**-atoms occur also in rule bodies of** P
′u
, in order to replace the corresponding SCs (recall Definitions 16 and 17), they contribute to infer rule heads in P
′u
, which represent elements in a social model of the collection
{P1, **· · ·** ,Pn}.

Our intention is to compute the social models of P1, · · · ,Pn **in terms of the stable**
models of the logic program P
′u ∪ C(P1, **· · ·** ,Pn)
7**. Thus, we must prove item (2).**
To this aim, let us recall from (Buccafurri and Gottlob 2002) some definitions and results that we shall use later.

Definition 18 (Buccafurri and Gottlob 2002)
Let P **be a traditional logic program and** M ⊆ Var (P). We denote by [M ]P **the set** {aP | a ∈ M **} ∪ {**a
′
P | a ∈ Var (P) \ M **} ∪ {**saP | a ∈ M }.

7 This can be efficiently accomplished by using the DLV system (Leone et al. 2002)