Applying linear quantifier elimination. (English) Zbl 0787.03021

Loos, Rüdiger; Weispfenning, Volker

Comput. J. 36, No. 5, 450-462 (1993).

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.

MSC:

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

Keywords:

linear quantifier elimination algorithm for ordered fields; Skolem sets; elimination sets; non-standard terms

Citations:

Zbl 0646.03005