Interestingly, FL-independence and FV-independence can be determined in an efficient way when Σ is given in some specific normal forms, namely, prime implicate normal form or prime implicant normal form. For such normal forms, Lit-independence and Var-independence come down to their corresponding syntactical forms.

Proposition 8  Let Σ  be a formula from PROPps and L  be a  subset of Lps.  The next statements are equivalent:
(1) L A L ;
(2) PI(E) E {7 | 7 is a term that does not contain any literal from L};
(3) I P(Σ) ⊆ {δ | δ is a clause that does not contain any literal from L}.

Proposition 9 Let Σ be a formula from PROPρς and V be a subset of PS. The next statements are equivalent:
(1) V H È È ;
(2) PI(E) C {7 | 7 is a term that does not contain any variable from V};
(3) IP(Σ) ⊆ {δ | δ is a clause that does not contain any variable from V}. Example 10  Let Σ = (αΛ¬bΛ(bV¬b)).  We have PI(Σ) = {(αΛ¬b)} and I P(Σ) = {α, ¬b}
(up to logical equivalence). We can easily observe that Σ is Lit-independent from b looking at PI(E) (or IP(E)).  We can also easily state that E is Lit-dependent on ¬b and Varindependent from c by considering any of these normal forms.

Proposition 7 shows that a KB can be easily Var-simplified (i.e., in polynomial time)
as soon as the variables it is Var-independent from have been determined. Indeed, we can easily design a greedy algorithm for simplifying KBs.  This algorithm consists in considering ery variable x of Var(E) in a successive way, while replacing E by Ex~o whenever E is Var-independent from x . This algorithm runs in time polynomial in the size of Σ once the variables Σ is Var-independent from have been computed. At the end, the resulting KB is Var-simplified.

Lit-simplifying a KB is not so easy if no assumptions are made about its syntax, due to the fact that literals signs are crucial here. Indeed, looking only at the occurrence of a variable inside a formula is not sufficient to state whether or not this is a positive occurrence (or a negative one). Fortunately, turning a formula into its NNF is computationally easy (as long as it does not contain any occurrence of connectives like $ or ⊕) and it proves sufficient to design a greedy algorithm for Lit-simplifying a KB when the literals it is Lit-independent from have been identified. Indeed, within an NNF formula, every literal can be considered easily as an atomic object. This algorithm consists in considering every literal l of Lit(Σ)
in a successive way, while replacing every occurrence of I in E by false considering every literal of Lit ( ) as an atom. Stated otherwise, when l is a positive (resp. negative) literal x (resp. ¬ x ), replacing l by false does not mean replacing ¬ x (resp. x ) by true : only the occurrences of l with the right sign are considered. This algorithm runs in time polynomial in the size of Σ once the literals Σ is Lit-independent from have been computed. At the end, the resulting KB is Lit-simplified.