ISSN:
1573-0670
Keywords:
automated theorem proving
;
Euclidean traditional proofs
;
volume method
;
constructive geometry statements
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract This paper presents a method of producing readable proofs for theorems in solid geometry. The method is for a class of constructive geometry statements about straight lines, planes, circles, and spheres. The key idea of the method is to eliminate points from the conclusion of a geometric statement using several (fixed) high-level basic propositions about the signed volumes of tetrahedrons and Pythagorean differences of triangles. We have implemented the algorithm, and more than 80 examples from solid geometry have been used to test the program. Our program is efficient and the proofs produced by it are generally short and readable.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00881858
Permalink
