
## 4 Translation To Logic Programming With Aggregates

In this section we give the translation from SOLP under the Social Semantics to logic programming with aggregates5 **under the Stable Model Semantics. We assume**
that the reader is familiar with the Stable Model Semantics (Gelfond and Lifschitz 1988).

Given a traditional logic program P, we denote by SM (P**) the set of all the stable**
models of P**. For the sake of presentation, the most complicated proofs are placed**
in Appendix A.

Our goal is the following: given a collection of SOLP programs we have to generate a single LPA **program whose stable models are in one-to-one correspondence with**
the social models of the collection. To this aim we perform the two following tasks:
(a) we generate a LPA **program by means of a suitable transformation of all the**
SCs occurring in the SOLP programs of the collection; (b**) we obtain another logic** program by processing the original SOLP programs in such a way that the SCs are replaced by suitable atoms. Finally, we merge the two programs obtained from tasks (a) and (b) into a single LPA **program. At the end of the section, we present**
a comprehensive example (Example 13) describing the whole translation process.

Next we describe how task (a**) is performed. The first step is the translation of a**
single SC and the extension of such a translation to all the SCs included in a social rule, a SOLP program and a SOLP collection, respectively. As a result **of task (**a),
a single LPA **program is generated which represents the translation of the social**
conditions occurring in the SOLP collection. In order to have fresh literals that allow us to encode - in such a program - the truth of social conditions, we need a mechanism to generate auxiliary atoms that are in one-to-one correspondence with the social conditions occurring in a SOLP program.

## Definition 12

Given a SOLP program P**, we define** USC P =Sr∈P
Sn≥0 MSChP,r,ni**. Moreover,**
let L
ρ and L
g **be two sets of literals such that both (1)** Var (P), L
ρ**, and** L
g are disjoint sets and (2) |L
ρ| = |L
g| = |USC P |**. We define two one-to-one mappings:**
ρ : USC P → L
ρ and g : USC P → L
g.

Observe that, according to the definition of the set MSChP,r,ni**(see page 11),**
USC P is the set of all the SCs (at any nesting depth) in P**. Thus, given a SC** s included in a SOLP program P, the mapping ρ (resp. g**), returns the auxiliary atom**
ρ(s) (resp. the predicate g(s)) such that it is fresh, i.e. it does not occur in P**. We** will explain next how ρ(s) and g(s**) are exploited by the translation process.**
The following definition enables the translation of a single social condition s **of a**
given program P of a SOLP collection C**. Observe that this definition is recursive in**
order to produce the translation of every social condition nested in s**. Such a translation produces two sets of rules that we reference as** GUESS P (s**) and** CHECK P (s),
respectively. Informally, the rules in the set GUESS P (s) aim at verifying properties concerning atoms belonging to other SOLP programs different from P**. These**