We consider the problem of existential quantifier elimination for Boolean
formulas in Conjunctive Normal Form (CNF). We present a new method for solving
this problem called Derivation of Dependency-Sequents (DDS). A
Dependency-sequent (D-sequent) is used to record that a set of quantified
variables is redundant under a partial assignment. We show that D-sequents can
be resolved to obtain new, non-trivial D-sequents. We also show that DDS is
compositional, i.e. if our input formula is a conjunction of independent
formulas, DDS automatically recognizes and exploits this information.