THE DIMENSION METHOD IN ELEMENTARY AND DIFFERENTIAL GEOMETRY

The paper discusses the dimension method, introduced by Carra and Gall o, to prove theorems in elementary and differential geometry. The meth od, based on the computation of the dimension of algebraic varieties, which is carried out by first determining Grobner bases, introduces di fferent levels of validity of geometric statements. The paper compares the outcome of this approach with that of Wu's method, discusses its theoretical bases and presents a refined decision algorithm for the di fferential case, which improves a previous version. A software environ ment that allows to experiment with the two different theorem provers has been designed and is presented in the paper. The environment inter face provides a specification language that enables users to easily de scribe geometric relationships among the geometric entities involved i n a problem, A problem description is then interpreted to yield a grap hic representation of the problem and to provide polynomial equations which constitute the input to the provers.