Quantifier Elimination by Dependency Sequents

Details Quantifier Elimination by Dependency Sequents Quantifier Elimination by Dependency Sequents

2012-01-26

arxiv.org/abs/1201.5653v1

Computer Science

Logic in Computer Science

27 pages, 5 figures, 2 tables

Scientific paper

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. We introduce an algorithm based on DDS and present experimental results demonstrating its potential.

Affiliated with

Also associated with

No associations

Rating

Quantifier Elimination by Dependency Sequents does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Quantifier Elimination by Dependency Sequents, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Quantifier Elimination by Dependency Sequents will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-343144