Forgetting can also be used to characterize a dependence relation called definability
(Lang & Marquis, 1998b) as well as the strongest necessary (resp. weakest sufficient) conditions of a propositional variable on a set V of variables given a theory Σ (Lin, 2000; Doherty, Lukaszewicz, & Szalas, 2001). As shown in (Lang & Marquis, 1998b; Lin, 2000; Doherty et al., 2001), all these notions have many applications in various AI fields, including hypothesis discrimination, agent communication, theory approximation and abduction.

Finally, based on literal and variable forgetting, valuable equivalence relations over formulas can also be defined:
Definition 9 (Lit-equivalence, Var-equivalence) Let Σ, Φ be two formulas from PROPps, L be a subset of Lps, and V be a subset of PS.

- Σ and Φ are said to be Lit-equivalent given L, denoted Σ ≡ L Φ, if and only if ForgetLit(Σ, Lit(Σ) \ L) ≡ ForgetLit(Φ, Lit(Φ) \ L).

- Σ and Φ are said to be Var-equivalent given V , denoted Σ ≡ ν Φ, if and only if ForgetVar(E, Var(E) \ V) ≡ ForgetVar(Φ, Var(Φ) \ V).
Example 14  Let Σ = (α ⇒ b) ∧ (b ⇒ c) and Φ = (α ⇒ d) ∧ (d ⇒ c).  Let L = {¬α,c}.  Σ
and Φ are Lit-equivalent given L
Such equivalence relations capture some forms of dependence between formulas. They are useful in the various situations where it is required to formally characterize the fact that two knowledge bases share some theorems. Thus, two formulas are Lit-equivalent given L
whenever every clause containing literals from L only is a logical consequence of the first formula if and only if it is a logical consequence of the second formula. In the same vein, two Var-equivalent formulas given V have the same clausal consequences built up from V .

Clearly, Lit-equivalence is more fine-grained than Var-equivalence in the sense that two formulas Var-equivalent given V are also Lit-equivalent given L = L V, the set of literals built upon V, but the converse does not hold in the general case. Some applications are related to knowledge approximation ( Φ is a correct approximation of Σ over L if and only if Φ and Σ are Lit-equivalent given L ), normalization (turning a formula Σ into a CNF Φ
by introducing new symbols is acceptable as long as the two formulas are equivalent over the original language, i.e., Σ and Φ are Var-equivalent given V = Var(Σ)), and so on.

## 4.2 Complexity Results

It is quite easy to prove that forgetting is a computationally expensive operation in the general case. Indeed, since a formula Σ is consistent if and only if ForgetLit(Σ, Lit(Σ))
is consistent and since the latter formula is Lit-independent from every literal (i.e., it is equivalent to true or equivalent to false ), there is no way to compute a formula Φ equivalent to ForgetLit ( Σ, L ) in polynomial time, unless P = NP. Actually, we can derive the more constraining result, showing that the size of any formula equivalent to For getLit ( Σ, L ) may be superpolynomially larger than the size of Σ.

Proposition 23  Let E be a formula from PROPps and let L be a finite subset of Lps.

In the general case, there is no propositional formula Φ equivalent to ForgetLit(Σ, L) s.t.