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.