Efficient preprocessing methods for quantifier elimination

Abstract

This paper presents a framework and prototype implementation for preprocessing quantified input formulas that are intended as input for quantifier elimination algorithms. The framework loosely follows the AI search paradigm - exploring the space of formulas derived from the input by applying various rewriting operators in search of a problem formulation that will be good input for the intended Q.E. program. The only operator provided by the prototype implementation presented here is substitution for variables constrained by equations in which they appear linearly, supported by factorization and a simple check for non-vanishing of denominators in substitutions. Yet we present examples of quantified formulas which can be reduced by our preprocessing method to problems solvable by current quantifier elimination packages, whereas the original formulas had been inaccessible to those. © Springer-Verlag Berlin Heidelberg 2006.