We present a new quantifier elimination procedure for the elementary formal theory of real numbers based on the counting of real zeros of multivariate polynomial systems in [Becker & Wörmann, Pedersen & Roy & Szpirglas] and the computation of comprehensive Gröbner bases in [Weispfenning 2]. In many cases the method may accomplish a simultaneous elimination of a whole block of quantifiers. In some small well-known benchmark exemples it appears to perform significantly better than the original Collin'CAD algorithm and not much worse than the highly optimized CAD-based quantifier elimination method of [Hong 3].
cetindag@fmi.uni-passau.de
Ulrike Peiker, Martin Griebl