Applying linear quantifier elimination. (English) Zbl 0787.03021

Summary: The linear quantifier elimination algorithm for ordered fields of the second author [J. Symb. Comput. 5, 3-27 (1988; Zbl 0646.03005)] is applicable to a wide range of examples involving even nonlinear parameters. The Skolem sets of the original algorithm are generalized to elimination sets whose size is linear in the number of atomic formulas, whereas the size of Skolem sets is quadratic in this number. Elimination sets may contain non-standard terms which enter the computation symbolically. Many cases can be treated by special methods improving further the empirical computing times.


03C10 Quantifier elimination, model completeness, and related topics
68W30 Symbolic computation and algebraic computation
68Q25 Analysis of algorithms and problem complexity


Zbl 0646.03005
Full Text: DOI