Partial Quantifier Elimination With Learning

Eugene Goldberg

We consider a modification of the Quantifier Elimination (QE) problem called Partial QE (PQE). In PQE, only a small part of the formula is taken out of the scope of quantifiers. Th…