Geometry Expert (GEX)

Geometry Expert (GEX) is a software for dynamic diagram drawing and automated geometry theorem proving and discovering. As a dynamic geometry software, GEX can be used to build dynamic visual models to assist teaching and learning of various mathematical concepts. As an automated reasoning software, we can build dynamic logic models which can do reasoning themselves.

Geometry Expert (GEX) is a powerful computer program for geometric reasoning. Within its domain, it invites comparison with the best of human geometry provers. It implements most of the effective methods for geometric reasoning introduced in the past twenty years, including the deductive base method, Wu's method, the area method, the Groebner basis method, the vector method, and the full-angle method. With these methods, users may automated prove geometry theorems, to discover new properties of theorems, and to generate readable proofs for many geometry theorems.
A Chinese version of GEX: MMP also implements several state of the art methods for geometric constraint solving, that is, the user can input the geometric properties satisfied by a geometric diagram, and the software will automatically generate a constructive way to draw the diagram. Geometric constraint solving is a key property of so-called intelligent computer-aided design (CAD).
By dynamic visual models, we mean models built by computer softwares that can be changed dynamically. With GEX, we can build four classes of dynamic visual models: geometric transformations, loci generation, diagrams of functions, and loci generation.

Documents and Softwares

An introductory paper for GEX can be obtained here
An experimental Windows version of GEX, with a set of examples, can be obtained here

Java Geometry Expert

Java GEX is an internet based version of Geometry Expert.

MMP/Geometer

MMP/Geometer is a new Chinese version of GEX with ability of automated geometric diagram construction.

X.S. Gao and Q. Lin, MMP/Geometer - A Software Package for Automated Geometry Reasoning, Automated Deduction in Geometry, 44-66, Springer, Berlin, 2004.

References for Automated Geometry Reasoning

S.C. Chou, X.S. Gao, and J.Z. Zhang, Machine Proofs in Geometry, World Scientific, Singapore, 1994.
S.C. Chou, X.S. Gao, and J.Z. Zhang, A Deductive Database Approach To Automated Geometry Theorem Proving and Discovering, Journal of Automated Reasoning, 25(3), 219-246, 2000.
S.C. Chou, X.S. Gao, and J.Z. Zhang, Automated Generation of Readable Proofs with Geometric Invariants, I. Multiple and Shortest Proof Generation, Journal of of Automated Reasoning, 17, 325-347, 1996.
S.C. Chou, X.S. Gao, and J.Z. Zhang, Automated Generation of Readable Proofs with Geometric Invariants, II. Proving Theorems with Full-Angles, Journal of of Automated Reasoning, 17, 349-370, 1996.

References for Geometric Constraint Solving

X.S. Gao, D. Lei, Q. Liao, and G. Zhang, Generalized Stewart Platforms and their Direct Kinematics, IEEE Trans. Robotics, vol 21, 141-151, 2005.
X.S. Gao, Q. Lin, and G. Zhang, A C-tree Decomposition Algorithm for 2D and 3D Geometric Constraint Solving, Computer-Aided Design, 38(1), 1-13, 2006.
X.S. Gao, C.M. Hoffmann and W. Yang, Solving spatial basic geometric constraint configurations with locus intersection, Computer Aided Design, 111-122, 36(2), 2004.
J. Ge, S.C. Chou and X.S. Gao, Geometric Constraint Satisfaction Using Optimization Methods, Computer Aided Design, 31(14), 867-879, 2000.
X.S. Gao and S. C. Chou, Solving Geometric Constraint Systems, I. A Global Propagation Approach, Computer Aided Design, Vol. 30, No. 1, 47-54, 1998.
X.S. Gao and S. C. Chou, Solving Geometric Constraint Systems, II. A Symbolic Computational Approach, Computer Aided Design, Vol. 30, No.2, 115-122, 1998.

Using GEX for Mathematics Instruction

X.S. Gao, J.Z. Zhang, and S.C. Chou, Geometry Expert (in Chinese) , Nine Chapters, Taipei, 1998.
X. S. Gao, C.C. Zhu, and Y. Huang, Building Dynamic Mathematical Models with Geometry Expert, I. Geometric Transformations, Functions and Plane Curves, Proceedings of the Third Asian Technology Conference in Mathematics, eds W.C. Yang, pp. 216-224, Springer, 1998.
X.S. Gao, C.C. Zhu, and Y. Huang, Building Dynamic Mathematical Models with Geometry Expert, II. Linkages, Proc. of the Third Asian Symposium on Computer Mathematics, eds Z. B. Li, pp. 15-22, LanZhou University Press, 1998.
X.S. Gao, Building Dynamic Mathematical Models with Geometry Expert, III. A Geometry Deductive Database Proc. Of ATCM'99, 153-162, 1999, ATCM Inc., USA (Best paper Award of ATCM'99).