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. Inspired by the success of Wu's method, researchers were also successfully in applying another algebraic method, the Grobner basis method, to the same class of geometry theorems that Wu's method addresses. The book [1] contains a collection of 512 theorems mechanically proved by Wu's method.
The proofs with algebraic methods are generally not readable because polynomials with hundreds or even thousands of terms are generated during the proof processes. During the 1990s the methods for generating human-readable proofs were introduced. Notably the area method [4] and the full-angle method [5] can generate elegant and short (sometimes even shorter than those given by geometry experts) proofs. Our deductive basis method based mainly on the full-angle method [6] can not only generate proofs, but also can discover (and prove) possibly new theorems.
The software Geometry Expert (GEX) was originally developed around 1994 at Wichita State University by S. C. Chou, X. S. Gao, and J. Z. Zhang. It consists
of two parts: the proving and reasoning part, and the drawing part. The dynamic nature of its
drawing part is comparable to that of Gabri and the Geometer's Sketchpad.
However, 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 in the world after 2000.
Java Geometry Expert
The Java Geometry Expert (Java GEX or JGEX) has been rewritten completely with emphasis on its ease
of use by high school students and teachers in geometric drawing for educational purpose.
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 in 2008.
Since Java is platform-independent, people can use Java GEX at any platform by downloading the compiled Java bytecode to their local machines. Also any user with a browser and the INTERNET connection can use a part of our JGEX at http://woody.cs.wichita.edu to see examples. We have prepared a few dozens of examples. Please click the example menu item to play with these examples. In these examples, points with the red or green color are free or semi-free points that can be dragged with the mouse.
[1] S. C. Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, Dordrecht,
Netherlands, 1988.
[2] S.C. Chou, X.S. Gao, & J.Z. Zhang, An Introduction to Geometry Expert, Proc. CADE-13,
p. 235-239, 1996, Springer-Verlag.
[3] S. C. Chou and W.F. Schelter, Proving Geometry Theorems with Rewrite Rules, Journal of
Automated Reasoning, 2(4) 1986, 253273.
[4] S. C. Chou, X .S. Gao, & J. Z. Zhang, Machine Proofs in Geometry, World Scientic,
Singapore, 1994.
[5] S.C. Chou, X.S. Gao, & J.Z. Zhang, Automated Generation of of Readable Proofs with Geometric
Invariants, Part II. Proving Theorems with Full-Angles, J. of Automated Reasoning,
17, 349-370, 1996.
[6] S. C. Chou, X. S. Gao, and J. Z. Zhang, A Deductive Database Approach To Automated
Geometry Theorem Proving and Discovering, J. Automated reasoning, 25(3), 219-246,
2000.
JGEX Help