A New Approach for Automatic Theorem Proving in Real Geometry

Résumé du livre

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 contrast 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."