JGEX is a software which combines dynamic geometry software (DGS), automated geometry theorem prover (GTP) and our approach for visually dynamic presentation of proofs. As a dynamic geometry software, JGEX 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. As a tool for dynamic presentation of proofs, JGEX is a valuable for teachers and students to write and present proofs of geometry theorems with various dynamic visual effects.

1. JGEX is a powerful software 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, and the full-angle method, etc. With these methods, users may automated prove geometry theorems, to discover new properties of theorems, and to generate readable proofs for many geometry theorems.
2. By its dynamic nature, the diagram built by this softwares can be changed dynamically. With JGEX, we can drag part of the diagram with mouse and see immediately how the diagram changes accordingly.
3. JGEX can be used to create proofs either manually and automatically. It provides a series of visual effects for presenting of these proof.

JGEX consists of three parts: the drawing part, the reasoning and proving part, and the part of the visual presentation of proofs. In the drawing part, JGEX provides a graphical interface for the user to draw the diagram step by step with predefined constructions. Wu's method, the Full Angle Method and the Deductive Database Method based on Full Angle are implemented in JGEX as reasoning and proving tool.

The part of visual presentation of proofs makes JGEX most distinctive from other geometry drawing systems on one side, and from other geometry reasoning systems, including our previous versions of GEX, on the other side. It is based on our work on automated generation of readable proofs and on our approach to geometric drawing.

There have been excellent commercial geometry theorem drawing systems such as the Geometer’s Sketchpad in the US, Cabri in France, and Cinderella in Germany. All of them are capable of doing dynamic geometry. Each of them has its own advantages and extends to other areas such as drawing in 3D geometry, etc. The name “dynamic geometry” was introduced as early as 1950 in the book:

By a dynamic geometry we simply mean a study of the parts of space andtheir relations to one another while they are in motion and changing.

The drawing part of JGEX allows the user to construct the diagram interactively and manipulate the diagram in a dynamic way, so JGEX is first a DGS. Starting from free points, the user can create elements which is dependent on existed elements. With the mouse, the user can place points, draw lines, introduce marks, etc. In this way, the diagram is constructed step by step. Much more important is the fact that the user can explore the dynamic nature of the diagram. The user can drag part of the diagram with mouse and see immediately how the diagram changes accordingly. However, JGEX has its distinctive features comparing to the three commercial geometry drawing systems.

See Detail >>>

Wu's method, the Full Angle Method and the Deductive Database Method based on Full Angle are implemented in JGEX as reasoning and proving tool.

See Detail >>>

The part of visual presentation of proofs makes JGEX most distinctive from other geometry drawing systems on one side, and from other geometry reasoning systems, including our previous versions of GEX, on the other side. It is based on our work on automated generation of readable proofs and on our approach to geometric drawing.

However, as a first step, instead of automated generation of visual presentations of proofs, we implement the manual input method for creating visual presentations of proofs. This gives us first-hand experience with the approach we propose. It is also an important preparation for our future work on the proof checker. Especially, we have a collection of over 100 examples created manually with JGEX. We collect mainly those examples that do not mix algebraic expressions or computations with the geometry diagrams.

See Detail >>>

See Also:

• GEX and JGEX
• A Dynamic Geometry Software
• An Automated Geometry Theorem Prover
• A Tool for Visually Dynamic Presentation of Proofs

Download JGEX for your platform and just start it. In case you want to contribute to the development, you need to have some experience in the Java language. JGEX is written in Java, so you need a JDK in order to compile the code. The preferred IDE for development is IntelliJ IDEA. Alternatively, you can use Gradle on command line to compile and run the application: you need to type gradlew run in the root folder of JGEX.

Some interesting animations

How to install and develop

Since version 0.81, JGEX comes with a Gradle configuration. It is suggested using IntelliJ IDEA to open Java Geometry Expert. The main class is in wprover.GExpert.

The newest versions of JGEX use the gettext internationalization system for translating the texts. You need to install the gettext utility before starting a build. The msgfmt utility must be available in the system path.

JGEX uses a couple of additional third-party libraries, including graph-support (which requires slf4j and logback) and batik (which uses xml-apis and xmlgraphics).