It is important to stress here that some languages are closed under a logical operator, only if the number of operands is bounded by a constant. We will refer to this as **bounded closure.**
Definition 5.3 (∧BC,∨BC) Let L **be a subset of** NNF. L satisfies ∧BC (∨BC**) iff there exists**
a polytime algorithm that maps every pair of formulas Σ and Φ from L to a formula of L **that is**
logically equivalent to Σ ∧ Φ (Σ ∨ Φ).

We now turn to another important transformation:
Definition 5.4 (Conditioning) (Darwiche, 1999) Let Σ **be a propositional formula, and let** γ be a consistent term. The conditioning of Σ on γ, noted Σ | γ**, is the formula obtained by replacing** each variable X of Σ by true (resp. false) if X (resp. ¬X**) is a positive (resp. negative) literal of** γ.

Definition 5.5 (CD) Let L **be a subset of** NNF. L satisfies CD **iff there exists a polytime algorithm**
that maps every formula Σ from L and every consistent term γ to a formula from L **that is logically**
equivalent to Σ | γ.

Conditioning has a number of applications, and corresponds to restriction **in the literature on**
Boolean functions. The main application of conditioning is due to a theorem, which says that Σ ∧ γ is consistent iff Σ | γ **is consistent (Darwiche, 2001a, 1999). Therefore, if a language satisfies** CO
and CD, then it must also satisfy CE**. Conditioning also plays a key role in building compilers**
that enforce decomposability. If two sentences ∆1 and ∆2 **are both decomposable (belong to** DNNF),
their conjunction ∆1 ∧ ∆2 **is not necessarily decomposable since the sentences may share variables.** Conditioning can be used to ensure decomposability in this case since ∆1 ∧ ∆2 **is equivalent to**
Wγ
(∆1 | γ) ∧ (∆2 | γ) ∧ γ, where γ is a term covering all variables shared by ∆1 and ∆2**. Note that**
Wγ
(∆1 | γ) ∧ (∆2 | γ) ∧ γ must be decomposable since ∆1 | γ and ∆2 | γ **do not mention variables**
in γ**. The previous proposition is indeed a generalization to multiple variables of the well-known**
Shannon expansion in the literature on Boolean functions. It is also the basis for compiling CNF **into**
DNNF **(Darwiche, 1999, 2001a).**
Another critical transformation we shall consider is that of forgetting **(also referred to as marginalization, or elimination of middle terms (Boole, 1854)):**
Definition 5.6 (Forgetting) Let Σ be a propositional formula, and let X **be a subset of variables**
from PS. The forgetting of X from Σ, denoted ∃X.Σ**, is a formula that does not mention any variable** from X and for every formula α that does not mention any variable from X, we have Σ |= α **precisely** when ∃X.Σ |= α.

Therefore, to forget variables from X is to remove any reference to X **from Σ, while maintaining all**
information that Σ captures about the complement of X. Note that ∃X.**Σ is unique up to logical**
equivalence.

Definition 5.7 (FO, SFO) Let L **be a subset of** NNF. L satisfies FO **iff there exists a polytime**
algorithm that maps every formula Σ from L and every subset X **of variables from PS to a formula**
from L equivalent to ∃X.Σ. If the property holds for singleton X, we say that L satisfies SFO.

Forgetting is an important transformation as it allows us to focus/project a theory on a set of variables. For example, if we know that some variables X **will never appear in entailment queries,** we can forget these variables from the compiled theory while maintaining its ability to answer such queries correctly. Another application of forgetting is in counting/enumerating the instantiations of some variables Y**, which are consistent with a theory ∆. This query can be answered by**
counting/enumerating the models of ∃X.∆, where X is the complement of Y**. Forgetting also has**
applications to planning, diagnosis and belief revision. For instance, in the SATPLAN framework,