Home > Geometry > Mechanical Geometry Theorem Proving

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

circulos

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:

h_1 = g_1 h_2=g_2 h_3=g_3 h_4=g_5
h_5 = g_7 h_6=g_8 h_7 = g_{10} h_8 = g_{11}
h_9 = g_3 h_{10} = g_6 h_{11}=g_9 h_{12} = g_{12}

The degenerate conditions are then reduced to vectors \nu and \omega being not nill:

\nu_1^2 + \nu_2^2 \neq 0\qquad \omega_1^2+\omega_2^2 \neq 0

Advertisements
  1. Tony
    September 7, 2013 at 4:04 pm

    This is a simple case of this theorem

    http://mathworld.wolfram.com/ThreeConicsTheorem.html

  1. No trackbacks yet.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: