© 1993 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Applying Linear Quantifier Elimination

1 Wilhelm-Schickard-Institut, Universita;t Tubingen, D-72076 Tubingen, Germany, 2 Lehrstuhl fur Mathematik, Universitat Passau, D-94030 Passau, Germany
The linear quantifier elimination algorithm for ordered fields in [15] is applicable to a wide range of examples involving even non-linear 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.
Received January 1993. revised May 1993.
* Wilhelm-Schickard-Institut, Universität Tübingen, D-72076 Tübingen, Germany
Lehrstuhl für Mathematik, Universität Passau, D-94030 Passau, Germany