containing a minimal number of faulty components can be enumerated in (output) polynomial time. Interestingly, this work shows that the diagnosis task does not require the
(usually expensive) computation of prime implicates/implicants to be achieved (actually, computing prime implicates/implicants is just a way to achieve variable forgetting and not a goal in consistency-based diagnosis). Forgetting every variable from a formula allows for consistency checking since Σ is consistent if and only if ForgetVar (Σ,Var(Σ)) is consistent.

The well-known Davis and Putnam algorithm for satisfiability testing (Davis & Putnam, 1960) (recently revisited by Dechter and Rish (1994)under the name directional resolution)
basically consists in computing a clausal representation of ForgetVar(E,Var(E)) from a CNF Σ using resolution; if the empty clause is not generated, then Σ is consistent and the converse also holds.

Forgetting can also be used as a key concept in order to organize knowledge so as to replace one global inference into a number of local inferences as shown (among others) by Kohlas et al. (1999) and Amir and McIlraith (2000), McIlraith and Amir (2001). Loosely speaking, such approaches rely on the idea that exploiting all the pieces of information given in a knowledge base is typically not required for query answering. Focusing on what is relevant to the query is sufficient. While such techniques do not lower the complexity of inference from the theoretical side, they can lead to significant practical improvements. For instance, assume that Σ consists of three formulas Φ 1 , Φ 2 , and Φ 3 .

For any query ¥, let Vv = (U 3 = 1 Var( È i) \ Var( Ψ). We have Σ |= Ψ if and only if ForgetVar(Nj=1 Dj, Vv) = V. If Var(Dj) N(Uj=1 Var(Dj)) = 0, this amounts to test independently whether ForgetVar( Λ i = 1 Φ i , V v ) |= Ψ holds or ForgetVar( Φ 3 , V v ) |= Ψ holds.

This way, one global inference is replaced by two local inferences. Now, ForgetVar(Φ 1 ∧ Φ2, Vv) is equivalent to ForgetVar(Φ1 ∧ ForgetVar(Φ2, Vv Π(Var(Φ2) \ Var(Φ1))), Vv).

Accordingly, every variable from Φ 2 that is not a variable of Φ 1 or a variable of Ψ can be forgotten first within Φ 2 because it gives no information relevant to the query; thus, only a few pieces of knowledge have to be "propagated" from Φ 2 to Φ 1 before answering the query, and forgetting allows for characterizing them exactly.

As evoked in the introduction, another scenario in which forgetting is useful is that of belief update. Indeed, there are many formalizations of belief update that are based on a form of variable forgetting. The basic scenario is the following one: we have a formula Σ
that represents our knowledge; there are some changes in the world, and what we know is that after them a formula ϕ becomes true. The simplest way to deal with the update is to assume that ϕ represents all we know about the truth value of the variables in ϕ . As a result, we have to "forget" from Σ the value of the variables in Var(ϕ). There are different formalizations of this schema, based on whether formula ϕ is considered to carry information about variables it mentions (Winslett, 1990) or only on the variables it depends on (Hegner, 1987), or also on variables related to dependent variables via a dependence function (Herzig, 1996).  This kind of update schema, while less known than the Possible Models Approach by Winslett (1990), has proved to be suited for reasoning about actions (Doherty et al., 1998; Herzig & Rifi, 1999). Furthermore, the possibility to forget literals (and not variables) is also valuable in this framework to take account for persistent information, as shown recently by some of us (Herzig et al., 2001), since the polarity of information is often significant.

For instance, while forgetting the fluent alive from a knowledge base is not problematic, forgetting the persistent fluent ¬alive would surely be inadequate.