Java Geometry Expert and its Applications to Geometry Education

Abstract

Since the pioneering work by the eminent Chinese mathematician Wen-Tsun Wu, great achievements have been made by world-wide researchers in geometry theorem proving. Hundreds of difficult theorems whose traditional proofs require enormous amounts of human intelligence, such as Feuerbach's theorem, the Morley trisector theorem, etc., have been proved totally automatically by computer programs based on Wu's algorithm.

The software Geometry Expert (GEX) was originally developed around 1994. GEX uses Openwin under X-Window which is no longer supported by the Linux distributions after 2000. Thus we could not satisfy the requests for GEX from students and researchers after 2000.

The Java Geometry Expert (Java GEX) has been rewritten completely with emphasis on its ease of use by high school students and teachers in geometric drawing for educational purpose.

Java GEX consists of two parts: the proving part and the drawing part. The proving part is based on Wu's method. The dynamic nature of its drawing part is comparable to that of the Gabri and Geometer's Sketchpad. Since Java is platform-independent, people can use Java GEX at any platform.

There have been excellent pieces of software for geometric drawing, e.g., the Geometer's Sketchpad, Gabri and Cinderella. However, they lack the reasoning and proving abilities. Hence their drawing is non-geometric in the sense that if a new point constructed is identical to one of the previous constructed points, they can only eliminate this point numerically. Since drawing a geometry diagram is so easy with few mouse clicks, we repeatedly observe this phenomenon in the early stage of developing Java GEX.

Take an isosceles triangle ABC with the base segment BC as an example. If reflecting AB wrpt BC, we get a segment BA'; then reflecting AC wrpt BC, we get another segment CA". Points A' and A" are actually identical.

This is a simple example, but we have also encountered cases in which the identity itself is a relatively deep theorem.

Our approach is as following. Whenever a new point is constructed, we first check whether this point is identical to a previous one numerically. If so, we use Wu's method to check the identity. If the identity is valid, we eliminate this point. We will discuss this issue in depth.

The primary goal of Java GEX is to provide a piece of alternative and free software for dynamic geometry. We began this project in 2004 and plan to release the first official version early 2006.

We will present examples which are dynamic, vivid, and colorful.

Reference.

S. C. Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, Dordrecht, Netherlands, 1988.
S.C. Chou, X.S. Gao, and J.Z. Zhang, An Introduction to Geometry Expert, Proc. CADE-13, 235-239, 1996, Springer-Verlag.
W.T. Wu, On the Decision Problem and the Mechanization of Theorem in Elementary Geometry, Scientia Sinica 21(1978), 159--172; Also in Automated Theorem Proving: After 25 years, A.M.S. Contemporary Mathematics, 29(1984), 213--234.