theorem on loop formulas characterizes the stable models of a nondisjunctive program in terms of the models of its completion that satisfy the loop formulas of all loops of the program. This allows us to compute stable models using SAT solvers, which led to the design of answer set solvers assat1**(Lin and Zhao 2004) and**
cmodels2**(Giunchiglia et al. 2004). Due to its importance in semantic understanding as well as in stable model computation, the theorem on loop formulas has been**
extended to more general classes of logic programs, such as disjunctive programs
(Lee and Lifschitz 2003), infinite programs and programs containing classical negation (Lee 2005), and programs containing aggregates (Liu and Truszczynski 2006; You and Liu 2008; Lee and Meng 2009). Moreover, it has been applied **to other**
nonmonotonic logics, such as circumscription (Lee and Lin 2006) and **nonmonotonic causal logic (Lee 2004). The stable model semantics for first-order formulas**
given in (Ferraris et al. 2007; Ferraris et al. 2011) is also closely related to the idea of loop formulas, as described in (Lee and Meng 2008).

By slightly modifying the definition of a loop, Lee (2005) showed that loop formulas can be viewed as a generalization of completion (Clark 1978). The modeltheoretic account of loop formulas give in (Lee 2005) also tells us that the idea of loop formulas is closely related to assumption sets (Sacc´a and Zaniolo 1990) or unfounded sets (Leone et al. 1997). In a sense, the theorem by Lin and Zhao is an enhancement of the unfounded set based characterization of **stable models given**
in (Sacc´a and Zaniolo 1990; Leone et al. 1997). The unfounded set based characterization takes into account the loop formulas of *all sets of atoms***, while the theorem**
by Lin and Zhao considers the loop formulas of *loops* **only. Gebser and Schaub**
(2005) improved this enhancement even further. They defined the notion of an elementary loop of a nondisjunctive program and showed that the theorem by Lin and Zhao remains correct even if we consider loop formulas of *elementary loops* **only.**
In this article, we reformulate the definition of an elementary loop of **a nondisjunctive program by Gebser and Schaub, extend it to disjunctive programs, and study**
several properties of elementary loops, including how maximal elementary loops are related to minimal unfounded sets. Based on the notion of an elementary loop, we present the class of Head-Elementary-loop-Free (HEF) program, which strictly generalizes the class of Head-Cycle-Free (HCF) programs due to Ben-Eliyahu and Dechter (1994). Like an HCF program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head **atoms into** the body—a simple transformation defined in (Gelfond et al. 1991). This tells us that an HEF program is an "easy" disjunctive program, which is merely a syntactic variant of a nondisjunctive program. We also observe that several other properties of nondisjunctive and HCF programs can be generalized to HEF programs. The main results from (Lin and Zhao 2003) and (You et al. 2003), characterizing stable models in terms of inherent tightness and weak tightness**, respectively, can be**
extended to HEF programs, and likewise the operational characterization of stable models of HCF programs due to Leone *et al.* (1997) can be extended to HEF pro1 http://assat.cs.ust.hk/
2 http://www.cs.utexas.edu/users/tag/cmodels/