Quantifier Elimination by Dependency Sequents
Abstract
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 introduce a resolution-like operation called join that produces a new D-sequent from two existing 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. We introduce an algorithm based on DDS and present experimental results demonstrating its potential.
Cite
@article{arxiv.1201.5653,
title = {Quantifier Elimination by Dependency Sequents},
author = {Eugene Goldberg and Panagiotis Manolios},
journal= {arXiv preprint arXiv:1201.5653},
year = {2013}
}
Comments
All the changes we made with respect to the previous versions are listed in the footnotes. The main change is that we modified the definition of a D-sequent using the notion of scoped redundancy of variables. We modified a few proofs of propositions affected by this change