Such elevated complexities may appear daunting, but the semantic similarities between HEF and HCF programs still exhibit that the syntactic concept of reachability merely gives a rough approximation of properties rendering disjunctive programs more difficult than nondisjunctive ones. As noted in (Fassetti and Palopoli 2010),
identifying subclasses of (not necessarily HCF) disjunctive programs for which verifying the HEF property is tractable may be an interesting line of future research.

## 5 Hef Programs And Inherent Tightness

When we add more rules to a program, a stable model of the original program remains to be a stable model of the extended program if it satisfies the new rules.

Proposition 9 For any disjunctive program Π and any model X of Π, X **is a stable model of Π iff**
there is a subset Π′ of Π such that X **is a stable model of Π**′.

## Proof**. From Left To Right Is Clear.**

From right to left: Assume that X **is not a stable model of Π. Then some proper**
subset Y of X is a model of ΠX . For each subset Π′ **of Π, we have that (Π**′)
X ⊆ ΠX,
so that Y **is a model of (Π**′)
X and X **is not a stable model of Π**′.

In view of Theoremd 1, Proposition 9 tells us that, provided that X **is a model**
of Π, in order to verify that X **is a stable model of Π, it is sufficient to identify a**
subset Π′ of Π such that X is a stable model of Π′**. Of course, one can trivially take** Π itself as the subset Π′**, but there are nontrivial subsets that deserve attention. In**
fact, if Π is nondisjunctive, it is known that the subset Π′**can be further restricted**
to a "tight" program (Fages 1994; Erdem and Lifschitz 2003)—the **result known**
as "inherently tight" (Lin and Zhao 2003) or "weakly tight" (You et al. 2003) program. In the following, we simplify these notions and show that they can be extended to HEF programs.

Recall that a loop of Π is called *trivial* **if it consists of a single atom such that the**
dependency graph of Π does not contain an edge from the atom to itself. In other words, a loop {a} **of Π is trivial if there is no rule (12) in Π such that** a ∈ A ∩ B. Definition 2 (**(Lee 2005)**) A disjunctive program Π is called *tight* **if every loop of Π is trivial.**
As defined previously (Apt et al. 1988; Baral and Gelfond 1994; Inoue and Sakama 1998; Lee 2005), we call a set X of atoms *supported* **by a disjunctive program Π if, for**
every a ∈ X, there is a rule (12) in ΠX such that A ∩ X = {a}**. Note that Definition 2 and the notion of support also apply to nondisjunctive programs as a special**
case.

The property of inherent tightness, introduced by Lin and Zhao (2003) for the case of nondisjunctive programs, can now be reformulated and generalized as follows.