Mechanical Geometry Theorem Proving

Home > Geometry > Mechanical Geometry Theorem Proving

Mechanical Geometry Theorem Proving

August 5, 2007 Leave a comment Go to comments

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 $A$ 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.

Proposed Solution

Let us assume the points $C$ and $D$ have coordinates $C=(0,1)$ and $D=(0,-1)$ , and the centers of the circles are $A=(a,0)$ , $B=(b,0)$ . Let us consider a vector $\nu = (\nu_1, \nu_2)$ supported in the point $C$ , and a vector $\omega = (\omega_1, \omega_2)$ supported in the point $D$ .

A line through $C$ with leading vector $\nu$ intersects the circle $A$ at the point $E=(x_1,y_1)$ . In order to compute its coordinates, we consider the equations of the line and the circle:

(1)	$x_1 - \alpha \nu_1 = 0$
(2)	$y_1 - 1 - \alpha\nu_2 = 0$
	$(x_1-a)^2 + y_1^2 = 1+a^2$

By simple substitution, we obtain the following second-degree equation, stating the condition:

$(\nu_1^2 + \nu_2^2) \alpha^2 + 2(\nu_2 - \nu_1)\alpha = 0$

One of the solutions is the trivial $\alpha=0$ (the point $C$ ). The other solution is what we need:

(3)	$(\nu_1^2 + \nu_2^2)\alpha + 2(\nu_2 - \nu_1) = 0$

Let $g_1(x_1,\alpha)$ , $g_2(y_1,\alpha)$ and $g_3(\alpha)$ be polynomials obtained from (1), (2) and (3). We obtain polynomials $g_4(x_2,\beta)$ , $g_5(y_2, \beta)$ and $g_6(\beta)$ in a similar way, considering the condition of point $F$ belonging in the line through $D$ with leading vector $\omega$ and the circle $A$ . We also obtain polynomials $g_7(x_3, \gamma)$ , $g_8(y_3,\gamma)$ and $g_9(\gamma)$ for the point $G$ in circle $B$ and line through $C$ with leading vector $\nu$ . Finally, obtain polynomials $g_{10}(x_4,\delta)$ , $g_{11}(y_4,\delta)$ and $g_{12}(\delta)$ for point $H$ belonging to circle $B$ and the line through point $D$ with leading vector $\omega$ .

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: