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.
- 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.
- 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.
- 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.
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.
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 Also:
- GEX and JGEX
- A Dynamic Geometry Software
- An Automated Geometry Theorem Prover
- A Tool for Visually Dynamic Presentation of Proofs
The JGEX is written in Java, so you need a JDK in order to compile the code. The prefered IDE for development is NetBeans: https://netbeans.org/
Some interesting animations
|
How to install & develop
It's suggested to use Netbeans to open Java Geometry Expert. The main class is in wprover. GExpert. The build.xml contains all the scripts to build the jar file. If you choose to run "all", this will do the compile, copy resources, generate jar file. You can also choose to generate applet for web use (unfortunately it's not supported anymore by the browser).