Applying Linear Quantifier Elimination

Abstract

The linear quantifier elimination algorithm for ordered fields in[15] is applicable to a wide range of examples involving even non-linearparameters. The Skolem sets of the original algorithm are generalized toelimination sets whose size is linear in the number of atomic formulas,whereas the size of Skolem sets is quadratic in this number. Eliminationsets may contain non-standard terms which enter the computation symbolically.Many cases can be treated by special methods improving further the empiricalcomputing times.