The set of all the resulting clauses and of those in Πcl forms the clausified completion of Π, which we will denote by *Comp*(Π).

The theory *Comp*(Π) does not involve any new atoms but it can be exponentially larger than the completion formula before clausification. We can avoid the exponential blowup by introducing new atoms. Namely, for each body B of a rule in Π with |B| > 1, we introduce a fresh atom fB. If |B| = 1, then we define fB = s(l), where l is the only element of B. By *ED-Comp*(Π), we denote the set of the following clauses:
1. all clauses in Πcl 2. all clauses ¬a∨WB∈*Bodies*(Π,a)
fB, for every a ∈ At(Π) such that a is not a fact in Π
and |*Bodies*(Π,a)| > 1 3. all clauses ¬a∨s(l), where a ∈ At(Π), *Bodies*(Π,a) = {B} and l ∈ B,
4. all clauses ¬a, where |*Bodies*(Π,a)| = 0 5. all clauses obtained by clausifying in the obvious way formulas fB ↔ B, where B ∈
Bodies(Π,a), for some atom a that is not a fact in Π and |*Bodies*(Π,a)| > 1.

Clearly, the restrictions of models of the theory *ED-Comp*(Π) to the original set of atoms are precisely the models of *Comp*(Π) (and of the completion of Π). However, the size of ED-Comp(Π) is linear in the size of Π. The theory *ED-Comp*(Π) has long been used in answer-set computation. Answer set solvers such as CMODELS (Giunchiglia et al. 2004)
and CLASP (Gebser et al. 2007) start their computation by transforming the given program Π into *ED-Comp*(Π).

For instance, let Π be program (3). The completion of Π is the formula
(a∨ ¬b∨c)∧b∧ ¬c∧(¬a∨(b∧ ¬c)),
its clausified completion *Comp*(Π) is the formula
(a∨ ¬b∨c)∧(¬a∨b)∧(¬a∨ ¬c)∧b∧ ¬c, and, finally, *ED-Comp*(Π) is the formula
(a∨ ¬b∨c)∧(¬a∨fb∧¬c)∧(fb∧¬c ∨ ¬b∨c)∧
(¬fb∧¬c ∨b)∧(¬fb∧¬c ∨ ¬c)∧b∧ ¬c.

We now have the following corollary from Proposition 5.

Corollary 1 For a logic program Π and a set X of atoms, the following conditions are equivalent:
(a) X is an answer set of Π,
(b) X = M+ for some model M of the SM(ASP) theory [{¬a | a ∈ O
Π
At(Π)
},Π],
(c) X = M+ for some model M of the SM(ASP) theory [*Comp*(Π),Π],
(d) X = M+ ∩At(Π) for some model M of the SM(ASP) theory [*ED-Comp*(Π),Π].

It is in this sense that ASP can be regarded as a fragment of SM(ASP). Answer sets of a program Π can be described in terms of models of SM(ASP) theories. Moreover, answerset computation can be reduced in a straightforward way to the task of computing models of SM(ASP) theories.