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 A, B that intersect each other in points C and D, and given points E, F in circle A, consider line a through E and C, and line b through F and D. The intersections of line a with circle B are C and G. The intersections of line b with circle B are D and H. Consider the segments c (connecting E with F) and d (connecting G with H). To prove: Segments c and d are parallel.