ISSN:
1573-7470
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
,
Mathematics
Notes:
Abstract The paper discusses the dimension method, introduced by Carrà and 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 Gröbner 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 enables users to easily describe geometric relationships among the geometric entities involved in a problem. A problem description is then interpreted to yield a graphic representation of the problem and to provide polynomial equations which constitute the input to the provers.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01531323
Permalink