Clearly enough, any non-valid clause δ is Lit-independent from L if and only if Lit ( δ ) ∩
L = 0. Since the conjunction of two formulas that are Lit-independent from L is Litindependent from L (see Proposition 2), and since every formula is equivalent to a CNF
formula, Proposition 16 shows ForgetLit(E, L) equivalent to the set of all clauses δ that are entailed by ∑ and are from { δ clause | Lit ( δ ) ∩ L = ∅} . Because { δ clause | Lit ( δ ) ∩ L = ∅} is closed under subsumption (i.e., it is a stable production field), it is possible to take advantage of consequence finding algorithms (see Marquis, 2000), to derive a CNF representation of For getLit( ). Especially, in the case where Σ is a CNF formula, resolution-based consequence finding algorithms like those reported in (Inoue, 1992) or (del Val, 1999) can be used; this is not very surprising since resolution is nothing but variable elimination.

In contrast to the disjunctive formulas situation, there is no guarantee that such consequencefinding algorithms run in time polynomial in the input size when the input is a conjunctive formula (otherwise, as explained in the following, we would have P = NP). Nevertheless, forgetting literals within a conjunctive formula Σ can be easy in some restricted cases, especially when Σ is given by the set of its prime implicates; in this situation, it is sufficient to give up those clauses containing a literal from L .

Proposition 19   Let Σ be a formula from PROP S and L ⊆ L P S .

I P(ForgetLit(Σ, L)) = {δ | δ ∈ I P(Σ) and Lit(δ) ∩ L = ∅}.

The notion of literal forgetting generalizes the notion of variable elimination from propositional logic (that was already known by Boole as elimination of middle terms and has been generalized to the first-order case in a more recent past by Lin & Reiter, 1994). Indeed, variable elimination is about variable forgetting, i.e., the one achieved not considering the literals signs: Definition 8 (variable forgetting) Let Σ be a formula from PROPps and let V be a subset of PS. ForgetVar(E,V) is the formula inductively defined as follows:
- ForgetVar(Σ, 0) = Σ,
- ForgetVar(Σ, {x}) = Σ x ← 1 V Σ x ← 0,
- ForgetVar(E, {x}UV) = ForgetVar(ForgetVar(E, V), {x}).

Example 13 Let Σ = (¬a Vb) ∧ (α Vc). We have ForgetVar(Σ, {α}) ≡ (bVc).

As a direct consequence of the definition, ForgetVar(Σ, { x 1 , ..., x n }) is equivalent to the quantified boolean formula (usually with free variables!) denoted ∃ x 1 ... ∃ x n Σ.

Clearly enough, forgetting a variable x amounts to forgetting both the literals x and
¬x.

Proposition 20   Let Σ be a formula from PROPps and V ⊆ PS.  We have ForgetVar(E,V) ≡ ForgetLit(E,Lv)
This result, together with the previous results on literal forgetting, gives us the following corollaries for variable forgetting: