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

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 |