Many equivalent characterizations of formula-variable independence have been given in the literature, each of which could serve as a definition (Definition 4, Corollary 1, each of the statements (2), (3) and (4) in Proposition 7 and of the statements (2), (3) in Proposition 9), so one may wonder which one has to be used in practice.

In many papers referring explicitly to formula-variable independence, the prime implicant/cate characterization (Proposition 9) is used as a definition (Boutilier, 1994; Doherty et al., 1998). Generally speaking, this is not the cheapest way to compute the set of variables a formula depends on, since the size of PI(E) is exponential in the size of E in the worst case. This characterization is to be used in practice only if the syntactical form of
∑ is such that its prime implicants or prime implicates can be computed easily from it
(this is the case for instance whenever Σ is a Krom formula). Clearly, the cheapest way to compute formula-variable independence consists in using any of the equivalent formulations of Proposition 7, which all consist of validity tests.

Checking whether a formula Σ is Var-independent from a variable x is coNP-complete, which implies that simplifying a knowledge base by getting rid of redundant variables needs |Var(E)| calls to an NP oracle, and is thus in FA, and not below (unless NP = coNP). This may look paradoxical (and sometimes useless) to preliminarily compute several instances of a NP or coNP-hard independence problem to help solving a (single) instance of a NP
or coNP-complete problem. However, this negative comment has a general scope only, and in many particular cases, this can prove quite efficient (indeed, even when Σ has no particular syntactical form, the satisfiability or the unsatisfiability of E x ← 0 ∧ ¬ ∑ x ← 1 may be particularly easy to check). Furthermore, if the knowledge base Σ is to be queried many times, then the preprocessing phase consisting in Var-simplifying Σ by ignoring useless variables is likely to be worthwhile.

## 4. Forgetting

In this section, we define what forgetting is, present some of its properties, and finally give some complexity results.

## 4.1 Definitions And Properties

A basic way to simplify a KB w.r.t. a set of literals or a set of variables consists in forgetting literals/variables in it. Beyond the simplification task, forgetting is a way to make a formula independent from literals/variables. Let us first start with literal forgetting:
Definition 7 (literal forgetting) Let Σ be a formula from PROPps and L be a subset of Lps. ForgetLit(E, L) is the formula inductively defined as follows:
1. ForgetLit(Σ, 0) = Σ,
2.  ForgetLit(Σ, {l}) = Σι← ι V(¬ ∧ Σ),
3. ForgetLit(E, {l}UL) = ForgetLit(ForgetLit(E, L), {l}),