Formula Simplification for Real Quantifier Elimination Using Geometric Invariance (Computer Algebra --Theory and its Applications)

Abstract

Formulating a simple and adequate quantified first-order formula is crucial for applying real quantifier elimination (QE) efficiently. In general, generating simple formulas or simplifying formulas for efficient QE involves human interaction. In this paper, we present simplification algorithms for quantified first-order formulas over the real numbers to speed up QE. We present experimental results for more than 10, 000 benchmark problems to examine the effectiveness of our simplification algorithms.