Abstract. We present a new method for proving geometric theorems in the real plane or higher dimension. The method is derived from elimination set ideas for quantifier elimination in linear and quadratic formulas over the reals. In conrast to other approaches, our method can also prove theorems whose complex analogues fail. After specification of independent variables, non-degeneracy conditions are generated automatically. Moreover, when trying to prove conjectures that do-apart from non/degeneracy conditions-not hold in the claimed generality, missing premises are found automatically. We demonstrate the applicability of our method to non-trivial examples. In particular, we can treat a variety of examples for which quantifier elimination by partial CAD fails.
Key words: real quantifier elimination, real geometry, automatic theorem proving over the reals.
Ulrike Peiker, Martin Griebl