Example 6 Σ = (αΛ¬bΛ(bV¬b)) is fully Lit-dependent on {α, ¬b} and fully Var-dependent on {a, b}.  Contrastingly, ∑ is not fully Lit-dependent on {a, b}.

Clearly enough, whenever Σ is fully Lit-dependent on L , it is also fully Var-dependent on Var ( L ). However, the converse does not hold, as the previous example shows.

While full FL-dependence (resp.  full FV-dependence) can be checked in linear time once DepLit(E) (resp. DepVar(E)) is known, at the end of the section we prove that determining these sets is NP-hard, and that deciding full FL-dependence (as well as full FV-dependence) is NP-complete.

Let us now consider the particular case of full FL-dependence when L = Lit(E), or the full FV-dependence when V = Var(Σ). If full dependence holds in these cases, we say that Σ is Lit-simplified, or Var-simplified, respectively. Var-simplification is aieved when E contains no occurrence of any variable it is Var-independent from. Lit-simplification corresponds to the more restricted situation where the NNF of Σ does not contain any occurrence of a literal it is Lit-independent from.

If a formula Σ is not Lit-simplified (resp. Var-simplified), then there is some literal (resp.

variable) that occurs in the NNF of Σ, but Σ is not Lit-dependent (resp. Var-dependent) on it. This means that the syntactic form in which Σ is expressed contains a literal or variable that is indeed useless.

## Definition 6 (Simplified Formula) Let E Be A Formula From Propps.

- Σ is Lit-simplified if and only if Lit(Σ) = DepLit(Σ).

- Σ is Var-simplified if and only if Var(Σ) = DepVar(Σ).

As the following example illustrates, every formula that is Lit-simplified also is Varsimplified but the converse does not hold in the general case. Example 7 Σ = (αΛ¬bΛ(bV¬b)Λ(αVc)) neither is Lit-simplified nor Var-simplified.  The equivalent formula (a ∧ ¬ b ∧ (b ∨ ¬ b )) is Var-simplified but it is not Lit-simplified. Finally, the equivalent formula (a A ¬b) is both Lit-simplified and Var-simplified.

Simplified formulas do not incorporate any useless literals or variables. As the next proposition shows it, the notion of simplified formula actually is the point where syntactical independence and (semantical) independence coincide.

Proposition 4   Let Σ  be a  formula  from  PROPps.

- E is Lit-simplified if and only if the following equivalence holds: for every L C Lps, E is syntactically Lit-independent from L if and only if L H E holds.

- Σ is Var-simplified if and only if the following equivalence holds: for every V ⊆ P S,
E is syntactically Var-independent from V if and only if V + E holds.
Thus, while a formula can easily be Lit-independent from a set of literals without being syntactically Lit-independent from it, simplification is a way to join Lit-independence with its syntactical restriction (which is easier to grasp, and as we will see soon, easier