Mechanical Geometry Theorem Proving
In 1977, Professor Wen-Tsun Wu succeeded in developing a method of mechanical geometry theorem proving. This method has been applied to prove or even discover hundreds of non-trivial difficult theorems in elementary and differential geometries on a computer in an almost trivial manner. Usign Ritt’s differential algebra, Wu established a method for solving algebraic and differential equations by transforming an equation system in the general form to equation systems in triangular form. This is the Ritt-Wu decomposition algorithm, that later on was shown to be equivalent to perform a series of operations on ideals, very easily carried out by means of Gröbner basis manipulation.
I wrote a script in
MAPLE to perform evaluations of the validity of some simple theorems in Euclidean Geometry, and wrote a small paper (in Spanish) on one of my findings, that was published in Bol. Asoc. Prof. Puig Adams, in October’99: “Sobre demostración automática de un problema geométrico“.
The example I cover in that short article can be seen below.
Given: Circles , that intersect each other in points and , and given points , in circle , consider line through and , and line through and . The intersections of line with circle are and . The intersections of line with circle are and . Consider the segments (connecting with ) and (connecting with ).
To prove: Segments and are parallel.
Let us assume the points and have coordinates and , and the centers of the circles are , . Let us consider a vector supported in the point , and a vector supported in the point .
A line through with leading vector intersects the circle at the point . In order to compute its coordinates, we consider the equations of the line and the circle:
By simple substitution, we obtain the following second-degree equation, stating the condition:
One of the solutions is the trivial (the point ). The other solution is what we need:
Let , and be polynomials obtained from (1), (2) and (3). We obtain polynomials , and in a similar way, considering the condition of point belonging in the line through with leading vector and the circle . We also obtain polynomials , and for the point in circle and line through with leading vector . Finally, obtain polynomials , and for point belonging to circle and the line through point with leading vector .
We use the Ritt-Wu method on those polynomials (notice it is not necessary to turn the system in triangular, since by a simple re-ordering of the polynomials we accomplish this state). The proof follows:
The degenerate conditions are then reduced to vectors and being not nill: