Java Geometry Expert and its Applications to Geometry Education
Wichita State University
Institute of Systems Science, Academia Sinica
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
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.
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,