An Automated Theorem Prover

1. Geometric and Non-Geometric Drawing


In JGEX, The diagram generated by it is geometric. At the right beginning of developing the drawing part of JGEX, we have kept the proving and reasoning as our final goal since we treat geometric elements, such as points, lines, and circles symbolically. Then we can apply the reasoning methods developed for over a quarter of a century to proving and/or discovering properties of a geometric diagram constructed. We call this kind of drawing Geometric Drawing.


For a diagram generated by JGEX, we keep a set of algebraic equations of the geometry constraints, so that we can prove or disprove properties of it with our algebraic methods efficiently. Especially, with Geometric Drawing, all nondegenerate conditions can be generated automatically.

2. Use of Algebraic Equations

A geometrical constraint in the hypotheses can be represent as one or two polynomial equalities on the coordinates of points. For example, for predicate that A, B, C are collinear, the corresponding polynomial equation is: . In this way, the hypotheses can be expressed as a set of polynomial equations:


The next step is to triangulate 3 the polynomial set so that each polynomial introduces only one new (dependent) variable xi. Thus the polynomial set is transformed to triangular form:


The variables u1, . . . , ud can be arbitrarily chosen and once they are fixed, the variables x1, . . . , xr can be successively solved. When one or two of variables u1, . . . , ud are changed with the mouse, then the variables of x1, . . . , xr are updated to achieve the dynamic geometry effects.


One of advantages of this approach to drawing is that the reasoning with algebraic methods can be immediately applied to the diagram. Currently, we have implemented Wu’s method in JGEX and the Gr¨obner basis methods for various formulations (see [4]) are under implementing. Many
important and subtle geometry issues are closed related to Wu’s method which are impossible to discuss without the underlying theory of Wu’s method. Another important advantage of use of polynomials is that we can construct all diagrams or cases with the leading degree in xj ≤ 4, since JGEX implements the formulas for quadratic, cubic, and quartic equations.

3. Elimination of Duplicated Points
As a direct application of the JGEX algebraic proof engine, we can eliminate a newly constructed point if it is identical to one of the previously constructed points. The three commercial systems can only eliminate this point numerically. Since drawing a geometry diagram is so easy with a few mouse clicks, we repeatedly observed this phenomenon at the early stage of developing JGEX.

Example. Let ABC be an isosceles triangle with AB = AC. Reflecting AB with respect to (wrpt) BC, we get segment BA'; then reflecting AC wrpt BC, we get 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. Here is our approach. 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. Without the powerful algebraic proof engine, it could eliminate the redundant points with only approximate numerical computations. But approximate numerical computations does not prove points A and X to be identical.


4. Automated Generation of Nondegenerate conditions


A geometry theorem is true generally under some additional conditions called nondegenerate conditions. The identification of nondegenerate conditions is subtle.

Figure 2: One Form of the Nine-Point Circle Theorem
Example 1. (One form of the nine-point circle theorem) Let points D, E and F be the three feet of the altitudes of triangle ABC. Let N be such that NF = NE and NF = ND, and M be the midpoint of AB. Then NM = NF.


For this example, beside the condition that A, B and C are not collinear, we need at least the nondegenerate condition that triangle ABC is not a right triangle, a subtle condition which is not easy to detect. However, with geometric drawing and the reasoning ability of JGEX, we can generate the nondegenerate conditions for a class of geometry statements of the constructive type.


The existence of point N implies the nondegenerate condition that points D, E, F are not collinear. Since points D, E, F are fixed points, we need to generate nondegenerate conditions that only contains free points. This is not an easy work, however, we can generate the polynomial equations
for this nondegenerate condition and check if the hypotheses are consistent or not with Wu’s method. This is very useful for a theorem to be complete. For most of the theorems we encountered, the nondegenerate conditions with geometric meanings can be generated automatically and thus we can give a complete description of the geometry statements.


5. The Six Different Methods

Java Geometry Expert (JGEX) 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. JGEX also implements the the following methods. ( Note: in this beta version, the area method and vector method is under developing).


1. Wu's method is the most powerful method in terms of proving difficult geometry theorems. Wu's method is a coordinate-based method. It first transfers geometry conditions into poiynomial equations in the coordinates of the points involved, then deals with the polynomial equations with the characteristic set method.

2. The Groebner basis method is also a coordinate-based method. Instead of using the characteristic set method, it uses the Grobner basis method to deal with the polynomial equations.


3. The area method uses high-level geometric lemmas about geometry invariants such as the area and the Pythagorean difference as the basic tool of proving geometry theorems. The method has been used to produce short, elegant, and human- readable proofs for more than 500 geometry theorems.

4. The full-angle method is based on the calculation of full-angles. Full-angle method is not a decision procedure. But this method also has its advantages: all the proofs produced by the method are very short, and it has been used to prove several theorems that all the other methods fail to prove because of very large polynomials occurring in the proving process.

5. The Deductive Database Method based on Full-Angle.

6. Vector method This method is a variant of the area method and is based on the calculation of vectors and complex numbers.



To use more than one method in the prover, we can produce a variety of proofs with different styles. This might be important in using JGEX to geometry education, since different methods allow students to explore different and better proofs.

 
6. The Prove Pane

The prove pane is on the left of the JGEX main window. It has a toolbar on the top and a tabbed pane on the bottom.

 

See Also:


JGEX Help