ISSN:
1573-0670
Keywords:
real quantifier elimination
;
real geometry
;
automatic theorem proving over the reals
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
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. Moreover, the problem formulation may involve order inequalities. After specification of independent variables, nondegeneracy conditions are generated automatically. Moreover, when trying to prove conjectures that – apart from nondegeneracy conditions – do not hold in the claimed generality, missing premises are found automatically. We demonstrate the applicability of our method to nontrivial examples.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1006031329384
Permalink