Automatic Discovery of Elementary Geometry Theorems

A technique is presented, based on the computer algebra software CoCoA, for computer oriented exploration of elementary euclidean geometry theorems. By exploration we mean the search of plausible thesis and/or hypothesis in concrete geometric contexts. In both cases the program will find thesis and/or hypothesis and will, accordingly, check automatically the validity of the resulting theorem. Consider the following construction is performed: we draw (using Cabri-Geométrè, for instance) a triangle and its orthocenter, baricenter, circumcenter and incenter points. We know that the orthocenter, baricenter and circumcenter are always aligned but we want to find under which extra hypothesis it holds that the incenter lies in the same line. Our program concludes that it is necessary and sufficient that the triangle is isosceles.

A different kind of application appears in the next construction: an equilateral triangle and an arbitrary point in the plane are given. We consider the distances of this point to the three lines supporting the sides of the triangle. Our program will then tell us that there is just one possible theorem involving these data, namely, the sum of the distances (affected of certain signs) must be constant.

Didactically, this program could be thought as the core of an intelligent, interactive, learning environment, linked to a sketch tool such as Cabri-Geométrè, in order to allow students to explore elementary properties of geometric objects.

Back to ICME8-RECIO home page