The dimension method in elementary and differential geometry
M.A. Alberti, G. Carrà Ferro, B. Lammoglia, M. Torelli
The paper discusses the dimension method, introduced by Carrà & Gallo, to prove
theorems in elementary and
differential geometry. The method, based on the computation of the dimension of
algebraic varieties, which is
carried out by first determining Groebner bases, introduces different 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 differential case, which improves
a previous version. A software
environment that allows to experiment with the two different theorem provers has
been designed and is presented
in the paper. The environment interface provides a specification language that e
nables users to easily describe
geometric relationships among the geometric entities involved in a problem. A pr
oblem description is then
interpreted to yield a graphic representation of the problem and to provide poly
nomial equations which constitute
the input to the provers.
novembre 94, M.A.Alberti,
alberti@dsi.unimi.it