to traditional logic programs6**, and then we apply such a transformation to each**
SOLP program in a given SOLP collection. Finally, we combine the traditional logic programs so obtained into a single program.

Before introducing the mapping, we need a preliminary processing of **all tolerance**
rules in a SOLP program. This is done by means of the following transformation: Definition 15 Given a SOLP program P, we define the SOLP program Pˆ = P \ TR(P) ∪ {p ←
p ∧ body(r ) | r ∈ TR(P) ∧ head(r ) = **okay**(p)}.

Note that Pˆ is obtained from P by replacing each tolerance rule okay(p) ← **body**
with the rule p ← p**, body**.

The next step is giving a mapping from a SOLP program to a traditional **logic**
program. Definition 16 Let P be a SOLP program. We define the program Γ′(P**ˆ) over the set of atoms**
Var (Γ′(P**ˆ)) =** {aP | a ∈ Var (A(Pˆ))**} ∪ {**a
′
P | a ∈ Var (A(Pˆ))**} ∪ {**saP | a ∈
Var (A(Pˆ))} ∪ {f ailP } as Γ′(P**ˆ) =** S
′
1
(Pˆ) ∪ S
′
2
(Pˆ) ∪ S
′
3
(P**ˆ), where** S
′
1
(Pˆ), S
′
2
(Pˆ)
and S
′
3
(P**ˆ) are defined as follows:**
S
′1(P**ˆ) =** {aP ←not a
′
P | a ∈ Var (A(Pˆ))**} ∪ {**a
′
P ←not aP | a ∈ Var (A(Pˆ))},
S
′2(P**ˆ) =** {saP ← b 1 P , **· · ·** , b n P , ρ(s1)P , · · · , ρ(sm )P | a ← b1, · · · bn, s1, · · · , sm **∈ P}**,
S
′3(Pˆ) = {**f ail**P ←not **f ail**P , saP ,not aP | a ∈ Var (A(Pˆ))}∪
{**f ail**P ←not **f ail**P , aP ,not saP | a ∈ Var (A(Pˆ))}
where A**() is the autonomous reduction operator (see page 9).**
In words, given a SOLP program P, first a program Pˆ **is produced (according**
to Definition 15) such that all the predicates okay**() occurring in it are suitably** translated. Then, according to Definition 16, three sets of standard logic rules are generated from P**ˆ, referenced as** S
′1(Pˆ), S
′2(P**ˆ) and** S
′3(Pˆ). Observe that atoms occurring in these sets are labelled w.t.r. the source program P **in order not to generate**
name mismatch in the final merging phase. Informally, the set S
′1(P**ˆ) guesses atoms**
that are candidates to be included in a social model. By means of the rules included in the set S
′
2(P**ˆ), atoms that are supported by a social rule are inferred. The atoms**
denoted by ρ(si)P (1 ≤ i ≤ m) are in one-to-one correspondence with those generated by W P **(see Definition 14) and represent the social conditions occurring in**
P**. Finally, the set** S
′
3
(P**ˆ) ensures that an atom is derived by means of some rule in**
S
′
2
(P**ˆ) iff it is also guessed by some rule in** S
′
1
(Pˆ).

The next definition introduces a logic program representing the translation of the whole SOLP collection.

6 Note that, differently from task (a), the logic program here generated do not contain aggregates.