notion of formula-variable independence because, as we show, the result of forgetting the set of variables V in a formula Σ can be defined as the strongest consequence of Σ being independent from V. Both notions have appeared in the literature under various names and with several different (but equivalent) definitions, and are highly useful for many tasks in automated reasoning and many problems in artificial intelligence:

1. automated deduction and consequence finding. Formula-variable independence can be useful for cheing (un)satisfiability or for consequence finding. Indeed, structuring the knowledge base by finding useful independencies may be worth doing before running any search algorithm. This principle is at work in (Amir & McIlraith, 2000). In optimal cases, for example, a satisfiability problem will be decomposed into a small nmber of satisfiability problems on easier knowledge bases (with less variables) as shown by Park and Gelder (1996). As to improving inference, this can be particularly helpful in the situation where the set of queries under consideration is limited to formulas ϕ that are (syntactically or semantically) independent from a set V of variables.

2. query answering (see in particular Amir & McIlraith, 2000), diagnosis (see the work by Darwiche, 1998). Rendering a formula Σ independent from a set V of variables through variable forgetting gives rise to a formula that is query-equivalent to Σ w.r.t. V in the sense that every logical consequence ϕ of Σ that is independent from V also is a logical consequence of Σ once made independent from V, and the converse holds as well. Interestingly, the set of all the formulas independent from a set of variables is a stable production field (Siegel, 1987; Inoue, 1992), and focusing on such a production field is valuable for several reasoning schemes. For instance, in the consistency-based framework for diagnosis (Reiter, 1987), the queries we are interested
in are the conflicts of the system to be diagnosed, i.e., the clauses that are independent from every variable used to represent the system, except the abnormality propositions used to encode the component failures.

3. knowledge base structuring, topic-based reasoning. Formula-variable independence is a key notion for decomposing a propositional knowledge base (KB for short), i.e.,
a finite set of propositional formulas, into smaller subbases. Su a decomposition is all the more valuable as the number of variables the subbases depends on is low. Optimally, a knowledge base Σ = { ϕ 1 , ..., ϕ n } is fully decomposable if it can be written as Σ = Σ 1 ∪ ... ∪ Σ n where Σ i and Σ i depend on disjoint sets of variables for all i / j . Such decompositions were considered in several papers (Parikh, 1996; Amir & McIlraith, 2000; Marquis & Porquet, 2000) with somewhat different motivations. The most intuitive motivation for searching such decompositions is that it gives a better understanding of the knowledge base, by structuring it with respect to (possible
disjoint but not necessarily) sets of topics (Marquis & Porquet, 2000).