zbMATH — the first resource for mathematics

A Maple package for automatic theorem proving and discovery in 3D-geometry. (English) Zbl 1195.68095
Botana, Francisco (ed.) et al., Automated deduction in geometry. 6th international workshop, ADG 2006, Pontevedra, Spain, August 31–September 2, 2006. Revised papers. Berlin: Springer (ISBN 978-3-540-77355-9/pbk). Lecture Notes in Computer Science 4869. Lecture Notes in Artificial Intelligence, 171-188 (2007).
Summary: A package for investigating problems about configuration theorems in 3D-geometry and performing mechanical theorem proving and discovery is presented. It includes the preparation of the problem, consisting of three processes: defining the geometric objects in the configuration; determining the hypothesis conditions through a point-on-object declaration method; and fixing the thesis conditions. After this preparation, methods based both on Groebner Bases and Wu’s method can be applied to prove thesis conditions or to complete hypothesis conditions. Homogeneous coordinates are used in order to treat projective problems (although affine and Euclidean problems can also be treated). A Maple implementation of the method has been developed. It has been used to extend to 3D some classic 2D theorems.
For the entire collection see [Zbl 1132.68006].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
Full Text: DOI