Removal of Quantifiers by Elimination of Boundary Points

Details Removal of Quantifiers by Elimination of Boundary Points Removal of Quantifiers by Elimination of Boundary Points

2012-04-08

arxiv.org/abs/1204.1746v1

Computer Science

Logic in Computer Science

16 pages

Scientific paper

We consider the problem of elimination of existential quantifiers from a Boolean CNF formula. Our approach is based on the following observation. One can get rid of dependency on a set of variables of a quantified CNF formula F by adding resolvent clauses of F eliminating boundary points. This approach is similar to the method of quantifier elimination described in [9]. The difference of the method described in the present paper is twofold: {\bullet} branching is performed only on quantified variables, {\bullet} an explicit search for boundary points is performed by calls to a SAT-solver Although we published the paper [9] before this one, chrono- logically the method of the present report was developed first. Preliminary presentations of this method were made in [10], [11]. We postponed a publication of this method due to preparation of a patent application [8].

Affiliated with

Also associated with

No associations

Rating

Removal of Quantifiers by Elimination of Boundary Points 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 Removal of Quantifiers by Elimination of Boundary Points, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Removal of Quantifiers by Elimination of Boundary Points will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-509973