The reduct ΠX of a disjunctive program Π w.r.t. a set X **of atoms is obtained**
from Π by deleting each rule (12) such that X 6|= F**, and replacing each remaining** rule (12) with A ← B. A set X of atoms is a stable model, also called an **answer**
set, of Π if X **is minimal among the sets of atoms that satisfy Π**X .

The definition of a *(positive) dependency graph* **is extended to a disjunctive**
program Π in the straightforward way: the vertices of the graph are the atoms occurring in Π, and its edges go from the elements of A to the elements of B **for all**
rules (12) of Π. With this extended definition of a dependency graph, the definition of a loop for a nondisjunctive program is straightforwardly extended to a disjunctive program.

For any set Y of atoms, the *external support formula* of Y **for a disjunctive**
program Π, denoted by ES Π(Y **), is the disjunction of conjunctions**

$$B\wedge F\land\bigwedge_{a\in A\setminus Y}\neg a$$

for all rules (12) of Π such that A∩Y 6= ∅ and B∩Y = ∅**. When Π is a nondisjunctive**
program, this definition reduces to the definition of ES Π(Y **) for nondisjunctive**
programs given earlier. As before, we say that Y is externally supported **by Π w.r.t.**
a set X of atoms if X |= ES Π(Y ); Y is unfounded **Π w.r.t.** X if X 6|= ES Π(Y ).

The notion of LF Π(Y ) and the term *(conjunctive) loop formula* **similarly apply**
to formulas (4) when Π is a disjunctive program.

As shown in (Lee 2005), Theorem 1 remains correct after replacing **"nondisjunctive program" in its statement with "disjunctive program."**
Theoremd 1 (**(Lee 2005)**)
For any disjunctive program Π and any set X of atoms that occur in Π, if X **is a**
model of Π, then the following conditions are equivalent: 9
(a) X **is a stable model of Π;**
(b) X satisfies LF Π(Y ) for all nonempty sets Y **of atoms that occur in Π;**
(b′) X **contains no nonempty unfounded sets for Π w.r.t.** X;
(c) X satisfies LF Π(Y ) for all loops Y **of Π.**
For instance, the loop formulas of the seven loops of the program in **(10) are:**
p → (r ∧ ¬q) ∨ (q ∧ ¬r)
q → (r ∧ ¬p) ∨ (p ∧ ¬r) r → (q ∧ ¬p) ∨ (p ∧ ¬q) p ∧ q → r p ∧ r → q q ∧ r → p p ∧ q ∧ r → ⊥ .

(13)
∅ **is the only model of (13) and it is the only stable model of (10) in accordance**
with the equivalence between (a) and (c) in Theoremd 1.

9 Superscript d indicates that the statement is a generalization to disjunctive programs.