Quantifier elimination for real algebra – the quadratic case and beyond. (English) Zbl 0867.03003

Weispfenning, V.

Appl. Algebra Eng. Commun. Comput. 8, No. 2, 85-101 (1997).

Summary: We present a new, “elementary” quantifier elimination method for various special cases of the general quantifier elimination problem for the first-order theory of real numbers. These include the elimination of one existential quantifier \(\exists x\) in front of quantifier-free formulas restricted by a non-trivial quadratic equation in \(x\) (the case considered also by H. Hong [Comput. J. 36, No. 5, 439-449 (1993; Zbl 0788.68075)]), and more generally in front of arbitrary quantifier-free formulas involving only polynomials that are quadratic in \(x\). The method generalizes the linear quantifier elimination method by virtual substitution of test terms [see R. Loos and the author, ibid. 36, No. 5, 450-462 (1993; Zbl 0787.03021)]. It yields a quantifier elimination method for an arbitrary number of quantifiers in certain formulas involving only linear and quadratic occurrences of the quantified variables. Moreover, for existential formulas \(\varphi\) of this kind it yields sample answers to the query represented by \(\varphi\). The method is implemented in REDUCE as part of the REDLOG package [see A. Dolzmann and T. Sturm, “Simplification of quantifier-free formulas over ordered fields”, Techn. Rep. MIP-9517, Univ Passau (1995), to appear in J. Symb. Comput.; “REDLOG, computer algebra meets computer logic”, Techn. Rep. MIP-9603, Univ. Passau (1996), submitted]. Experiments show that the method is applicable to a range of benchmark examples, where it runs in most cases significantly faster than the QEPCAD package of Collins and Hong. An extension of the method to higher degree polynomials using Thom’s lemma is sketched.

MSC:

03B35	Mechanization of proofs and logical operations
03C10	Quantifier elimination, model completeness, and related topics
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30	Symbolic computation and algebraic computation
68Q25	Analysis of algorithms and problem complexity

Keywords:

constraint solving; quantifier elimination method; first-order theory of real numbers; REDUCE; REDLOG package

Citations:

Zbl 0788.68075; Zbl 0787.03021

Software:

REDUCE; QEPCAD; REDLOG