On Wu's Method for Proving Constructive Geometric Theorems

1 Introduction

The idea of proving mathematical theorems mechani­ cally can be traced back to Leibniz early in the seven­ teenth century. The first one who pointed out precisely the mechanical methods, in particular, for geometry, is Hilbert. His classic work Grundlagen der Geometrie [Hilbert, 1956] is not only a model of axiomatization sys­ tem but also a tremendous contribution to the mecha­ nization of geometry. A complete decision method for el­ ementary geometry and algebra was then given by Tarski [1948-1951]. Unfortunately, his method, even with the great simplifications due to Seidenberg [1954], is too complicated to be feasible. In fact, no theorems of any geometric interest have been proved in this way. A early geometry machine written up by Gelernter [1959] might prove only some trivial theorems. In 1977 Wu Wen­ tsi.in discovered an algorithmic method which has been successfully applied to theorem proving in many kinds of elementary geometries involving ordinary Euclidean geometry, non-Euclidean geometry and circle geometry. Using Wu's method, a number of non-trivial geometric theorems have been proved and discovered by several research groups [Chou, 1986, Kutzler and Stifter, 1986, Wang and Gao, 1987]. The application of the Grobner basis method to geometry theorem proving has been in­ vestigated in the past few years [Kapur, 1986, Kutzler and Stifter, 1986].

cal theorem proving since 1977. This theory solves the mechanization decision problem of various kinds of ge­ ometries and provides the feasible methods for theorem proving and theorem discovering. The first step of Wu's approach, in starting from the defining axiomatic system of geometry as shown in the Grundlagen of Hilbert , is to introduce some number systems and coordinate sys­ tems so that the geometric entities and relations will be turned into algebraic ones, the coordinatization and algebraization of geometric problems . Then the alge­ braic relations corresponding to geometric ones occuring in the theorems under the consideration will be ( differen­ tial) polynomial equations, (differential) polynomial in­ equations and (differential) polynomial inequalities. The next step of Wu's approach, restricted on the classes of theorems, particularly, in which no order relations are involved (i .e., there will appear only (differential) poly­ nomial equations and inequations but not any ( differen­ tial) polynomial inequalities in the algebraic relations) , is to decide in an algorithmic manner whether the al­ gebraic relations corresponding to the conclusion of a geometric theorem are formal consequences of the re­ lations corresponding to the hypothesis of the theorem under some non-degenerate conditions. Note that these non-degenerate conditions play a very important rule in Wu's theory. If we leave them aside, then this de­ cision problem may be reduced , by Hilbert's N ullstel­ lensatz, to determine the membership of a radical ideal. However, only a few geometric theorems may be proved in that way because most of the theorems are actually only generically true. The degenerate cases in geome­ try cannot be indicated explicitly by the algebraic rela­ tions. Hence for geometry, before solving the algebraic problem, we have first to determine the non-degenerate conditions.

Wu has extended his method to elementary differential geometry and established a general theory of mechani- Among those involving no order relations , there are a type of theorems for which the hypotheses may be stated successively according to certain constructive types by introducing new geometric entities, and in the state­ ments of each step the algebraic relations corresponding to the geometric ones are linear equations in the new in­ troduced geometric dependents as variables. This type of theorems , as an extension of Hilbert pure intersec­ tion theorems, will be called constructive geometric the­ orems. The main part of this paper aims to discuss the mechanical proving of constructive geometric theorems.

2 An Extension of Hilbert Mechanization Theorem

As theorem 62 in a later edition of the Grundlagen, Hi b­ ert pointed out that if a pure intersection theroem holds in Pascal geometry, then this theorem may be proved successively by adjoining some suitable constructions of points and lines, as a combination of finite number of Pascal configurations. This theorem so-called Hilbert Mechanization Theorem by Wu indicates that the pure intersection theorems may be proved mechanically. As one of his methods, Wu gave a constructive proof of the Hilbert mechanization theorem by presenting an algo­ rithmic procedure [Wu, 1982, 1984b]. In view of the Hilbert explanation of pure intersection theorems, Wu discovered that the constructions of points (replacing a line by two points) occurring in the theorems are of not more than 10 types. In each of these 10 types, the corresponding algebraic relations are linear equations in the newly introduced geometric dependents. Thus they may be found successively from the linear equations as a rational function which has the parameters only as vari­ ables.

It is easy to see that there are actually only two geo­ metric objects collinear and parallel occurring in Wu's 10 constructive types. The author [Wang, 1987] noticed that there are other important geometric objects such as perpendicular in ordinary geometry for which the corresponding algebraic relations are linear equations too. Hence the theorems involving the constructive man­ ner related to perpendicular may also be proved in the same algorithmic procedure as pure intersection theo­ rems. This means that Hilbert mechanization theorem may be extended to suit more geometric theorems. We shall not distinguish the kinds of geometries. The in­ volved notions are directed against certain geometry for which they have definite meaning. Thus we may add five new ones following Wu's 10 constructive types.

11. Construct a division point of two constructed points;

Suppose the coordinates of two constructed points are ( o:;, o: j) and ( O:k, 0:1) respectively. Then the coordinates of the division point (x9, xh) of these two points with di­ vision ratio m : n 1 to be constructed satisfy the following equations

12. Through a constructed point, construct a line to be perpendicular to a constructed line;

Suppose the constructed line is determined by two points (o:; ,o:j ), (o:k>o:l) and the constructed point is given by (a:., O:t)· Then the coordinates of another point ( 1Lr, x 9 ) or ( x 9 , Ur) on the perpendicular line to be con­ structed must satisfy the following equation

or

1 m and n may be positive, negative integers or variables.

13. Construct the square of the distance between two constructed points;

Suppose two constructed points are given by ( o:;, O:j) and ( o:k, 0:1) respectively and denote the square of the distance to be constructed by x 9 . Then we have

14. Construct the square of the cosine of the angle between two constructed lines;

Suppose two constructed lines are given by (a:;, O:j), (o:k>o:l) and (o:.,o:t), (o:p,o:q) respectively. Then the square x 9 of the cosine to be constructed satisfies

15. Construct the area of a triangle determined by three constructed points.

Suppose three constructed points are given by (a:;, O:j), (o:k> 0:1) and (a:., O:t) respectively. Let x9 be the area of the triangle determined by these three points. Then x 9 satisfies

Since the distance and cosine themselves cannot be ex­ pressed as algebraic equations, we thus need to consider the squares as their alternative algebraic expressions . In fact, this change does not influence the characters of ge­ ometric entities [Wu, 1984b].

3 Method for Proving Constructive Geometric Theorems and Prover CPS

If the hypothesis of a geometric theorem may be stated step by step according to a certain constructive manner such that in the statement of each step the correspond­ ing algebraic relations are linear equations in the new introduced geometric dependents as variables and the conclusion of the theorem may be expressed as a set of polynomial equations, this theorem is then called a con­ structive geometric theorem. Certainly, the theorem, of which the hypothesis may be stated step by step accord­ ing to the given 15 constructive types and the conclusion may be expressed as polynomial equations, is a construc­ tive one.

Evidently, the algorithmic procedure given by Wu for proving Hilbert pure intersection theorems works also for constructive geometric theorems . By experiments on computers, the author found that it is not very efficient to prove theorems in accordance with Wu's original pro­ cedure. A suitable adjustment of Wu's algorithmic steps is thus required 2 . To do this, we will not attempt to find out each geometric dependent as a rational function only in the parameters as variables.

2 In fact, this adjustment was pointed out by Professor Wu himself when the author discussed his algorithm with him in spring 1984.

Suppose the hypothesis of a constructive geometric theorem is stated by m steps. The conclusion of this theorem may be expressed as, without loss of the gener­ ality, a single polynomial equation

To prove this geometric theorem, we proceed as fol­ lows. Start from polynomial g and let the polynomial set (DS) = ¢. By induction on i, suppose we have al­ ready done for m,m- 1, ... , i + 1. Do next fori.

Let the parameters and geometric depen­ dents obtained from the first i-1 steps and the parameters newly introduced in the ith step be a 1 , ... , ae in all. Suppose in the ith step the geometric dependents x1 , ... , Xr are introduced (if no dependents are introduced, we will jump this step). Then the algebraic relations corre­ sponding to the satement of this step will be a system of linear equations of the form

fr = /r1X1 + fr2X2 + ... + frrXr +fro= 0, where all /ik are polynomials in variables a 1 , ... , a ·.

Suppose our choice of parameters and de­ pendents are suitable, i.e., det(fjk) 1. 0. Other­ wise, there must be some x; that can be chosen as a parameter or the statement of this step is self-contradictory. Then by the Gauss elimina­ tion method 3 , we may transform the above sys­ tem of linear equations into a triangular form

Suppose the parameters introduced in the last m-i steps are u1 , ... , uM, (in the case i = m no such u's exist). Then up to i, the obtained polynomial g may be assumed by induction to be of the form

Set hr = g. Under the subsidiary condition Cj j i= 0, finding

from Cj = 0 and substituting it into hj, we have successively

3 This method appeared actually in "Nine Chapters on Mathematical Art ( Jiu-Zhang-Suan-Shu)", an ancient Chi­ nese un-au tho red book, in 50 AD. It is much earlier than tha t discovered by Gauss in 1826, and will be called China­ Gauss elimination method.

where hj_1 is still a polynomial and integer Sj 2: 0, for j = r, r- 1, ... , 1. Finally, we shall obtain an ho = ho(a1 , .. . , a., u1, ... , uM.). Reset g = ho and let ( D S) = ( D S) U { cu , ... , Crr}. We complete then the induction on i .

In this way, we will get finally a polynomial g, namely, R, of the form

and a polynomial set (DS) = {D1 , ... , Dt}. Then un­ der the subsidiary conditions Dk i= 0, k = 1, ... , t, the geometric theorem is true if and only if R = 0.

The conditions Dk = 0, k = 1, ... , t, usually, just in­ dicate the degenerate cases. The next step (however, indispensable for consistency) is to verify whether the hypothesis implies certain Dk = 0. This may be done, but simpler, in the same manner by regarding Dk as g. In the case some Dk = 0 or it follows from the hypothesis, we need to check whether the hypothesis of the theorem is self-contradictory or to rearrange the parameters and geometric dependents. On the other hand, if one is in­ terested in the case Dk = 0, some further consideration by regarding this relation as one of the statements of hypothesis is required.

Based on the principle of the above procedure, the au­ thor implemented a prover CPS using Fortran 77 and experimented on several computers such as HP 1000, IBM4341 and IBM-PC. In this prover, the input in­ cludes two manners command input and polynomial input. The command input is used to enter directly cer­ tain geometric statements in coordinate form involving the considered 15 constructive types by some appointed commands. The polynomial input is used to enter the al­ gebraic relations of the constructive manners to which no commands correspond in the command directory. The output of the prover includes a translation of each com­ mand to the natural language statement, the successive reductions of the proof using either polynomials or in­ dex sets and the non-degenerate conditions as required. The verifications of the suitablity of the choice of pa­ rameters and geometric dependents and the consistency of the non-degenerate conditions and the hypotheses of theorems are involved in the prover.

4 Wu's Method for Proving Theorems of Equation Type

For Wu's general theory of mechanical theorem prov­ ing, the readers are referred to his Chinese monograph [Wu, 1984b]. By a theorem of equation type we shall mean anyone for which the hypothesis and conclusion may be algebraized or formulated as systems of polyno­ mial equations. The basic algorithmic principles of Wu's method for proving theorems of equation type were writ­ ten in English [Wu, 1984a] as a abbreviation of chapter 4 in his monograph. We give in this sec tion only a brief review of Wu's method and add a few remarks on the non-degenerate conditions.

In what follows, we consider the case of geometry and suppose the hypothesis of a theorem, by intruducing number system and coordinate system, is given by a sys­ tem of polynomial equations, with coefficients in ceratin basic field K (regarding as rational field Q for ordinary geometry) associated to the geometry, as follows

where variables x 1 , ... , Xn are some geometric entities such as coordinates of points, areas of triangles and radii of circles. The conclusion of the theorem to be proved is given by a polynomial equation

Then the geometric decision problem is to determine ei­ ther a polynomial set (DS) = {D1 , ... , D1}, called the non-degenerate condition set, or no such set exists, such that g = 0 is a formal consequence of the system (HY P) under the conditions D; f:. 0 but D; = 0 themselves are not consequences of the system (HY P) .

For solving this decision problem, Wu [1984a, 1984b] developed a well ordering principle of polynomial set based on the classic work of Ritt [1950]. This prin­ ciple aims mainly to triangulate a system of polyno­ mials (a generalization of the China-Gauss elimination method). Let Zero(PS) be the totality of zeros of all polynomials in a polynomial set (PS). If G is another non-zero polynomial, then the subset of Zero(PS) for which G f:. 0 will be denoted as Zero(PS/G). Now, let ( P S) = {h , ... , f.}. Then the well ordering principle shows that one can transform ( P S) in an algorithmic manner into another polynomial set of certain form

where u1, ... , ud, Y1, ... , Yr (d + r = n) is a rearrangement of x1, ... , Xn, such that

in which J = h · · · In each I; is the leading coefficient of c; as polynomial in y; and (PS;) = (PS) U {I;}.

The obtained ( C S) will be called the characteristic set, weak characteristic set or triangular form of(PS) if degy,(cj) < degy,(c;) for j > i, degy,(Ij) < degy,(c;) for j > i or no further requirements, respectively. A characteristic set is called to be irreducible if c1 as a poly­ nomial in Yl is irreducible over K(u1, ... , ud)[yl], c2 as a polynomial in Y2 is irreducible over K( u1, ... , ud, Y1HY2J with y1 adjoined as an algebraic extension by the equa­ tion c1 = 0 and so on.

In proceeding further with each (PS;) as (PS) , we may decompose (PS) into a system of polynomial sets of the same form as the characteristic set, weak characteristic set or triangular form as required. Furthermore, one can decide whether a characteristic set is irreducible, and in the case it is not, determine an irreducible decomposi­ tion aided by polynomial factorization , see [Wu, 1984a] for details.

From the above structure of zeros, we know in the case J f:. 0, Zero(PS) = Zero(CS). Hence under this condi­ tion, to prove the geometric theorem, we need only to de­ cide whether g = 0 is a consequence of ( C S) = 0. Using the division algorithm, let us divide g by c,., Cr-1, ... , c1 successively, considered successively as · polynomials in Yr,Yr-l>···,Yl, and denote the finial remainder by R . We have thus a remainder formula of the form

where A; and R are all polynomials and degy, (R) < degy,(c;) for each i. Then the decision method is based on the following

Wu's Principle If the remainder R = 0, then under the subsidiary conditions I; f:. 0, g = 0 is a formal con­ sequence of (HY P) and thus the geometric theorem is true. If R ;t 0 and the characteristic set ( CS) is irre­ ducible, then under the conditions I; f:. 0, g = 0 is not a consequence of(HY P) and thus the theorem is not true.

The first half of this principle is enough to prove a large number of geometric theorems. The irreducibility and further decomposition have to be considered only if the remainder R ;t 0. Usually, the subsidiary conditions I; :j:. 0 are just the non-degenerate conditions of the theorem to be true and I; = 0 themselves are not consequences of the system (HY P) in either case. In practice, if we use only the triangular form or weak characteristic set, the proof efficiency may be greatly inproved. However, it cannot be theoretically guaranteed that the conditions I; = 0 themselves are not consequences of (HY P) in this case. As a altered way, we may first triangulate the hypothesis polynomial set and verify whether some condition I; = 0 is a consequence of the hypothesis, and if not, then compute the remainder R of g with respect to the triangular form, since the former is relatively simpler. Anyhow, even for the characteristic set, the ·verification is still required unless it is irreducible.

On the other hand, each degenerate case may be fur­ ther considered as interesting. For the completeness of theory, the irreducible decomposition of the algebraic variety has to be considered. So-called degenerate cases, they should correspond to a small part of the whole geo­ metric figure, i.e., from the point of algebraic geometry, this part should have a lower dimension. The only way is to analyse each irreducible component of the whole algebraic variety. For a penetrating description and ex­ planation, see [Wu, 1984a, 1984b].

Wu's general method for proving theorems of equa­ tion type, concerning the irreducible decomposition of algebraic varieties, is theoretically complete and quite simple in appearance. For the practicability of proving concrete theorems, Wu proposed also a modified but very efficient mechanical procedure [Wu , 1984a, 1984b] and , proved and discovered himself a number of non-trivial theorems such as the Morley Theorem, the Pascal-Conic Theorem and the Thebault-Taylor Theorem using an im­ plementation on some small computers.

Based on Wu's method, the author implemented also a general prover (PS) on HP1000 and IBM-PC using Fortran 77 for proving theorems of equation type. How­ ever, the prover is not complete. Some facilities such as characteristic set computation, irreducible decompo­ sition and command input of geometric statements need to be further improved.

5 Proving and Discovering Geometric Theorems

Using the implemented prover CPS, as well as PS, we have experimented on several computers for proving and discovering geometric theorems since 1984. More than one hundred non-trivial theorems have been proved. Part of these theorems was collected as appendix A in my doctoral dissertation [Wang, 1987) and written up in English in [Wang and Gao, 1987). Among them, there are several interesting ones discovered independently by t.he author. Most of the discovered theorems were al­ r.oady found later from certain books and papers. So far, a seemingly new one [Wang, 1986) concerning Pap­ pus lines and Leisenring lines has not been found in any literatures.

CPS is a complete and very efficient prover. It may be applied to prove many more geometric theorems over the applicability domain of Hilbert mechanization the­ orem. In fact, some theorems in solid geometry have also been proved by this prover . As noticed in [Chou, 1986], most theorems in elementary geometries may be expressed as linear constructive geometric theorems dis­ cussed . In fact, by choosing appropriate coordinate sys­ tems or changing the manner of geometric statements, many seemingly inconstructive geometric theorems, es­ pecially those involving quadratic relations or reducibil­ ity problems, may also be restated as constructive geo­ metric theorems. Consider the following example.

Ex (Secant Theorem) From a point S two secants are drawn to cut a circle at points A, C and B, D respec­ tively. Then SA 2 · SC 2 = SB 2 . SD 2 .

This theorem is related to a quadratic relation and re­ ducibility problem about distinguishing two intersection points of a line and a circle from each other [Wu, 1987). To deal with this problem, we do the following: first fix one of the two points of intersection, drawing the perpen­ dicular from the center of the circle to the line, and then determine the point symmetric to the first intersection point with respect to the perpendicular. In this way, the secant theorem may be stated as a constructive theo­ rem and proved easily by our prover. In fact, the prover CPS may treat various metric relations involving angle, area. and so on as given in the constructive types. As we know, the different description of the geometric theorem and different choice of coordinate system affect directly the efficiency of the proof. Whether the algebraic re­ lations corresponding to the hypothesis of a geometric theorem have lower degrees or a better triangular form depends closely on the description of the theorem and the introduction of geometric entities, which are thus Vt'ry important, not in principle but in practice.

By the general prover PS, the author has proved a number of non-trivial geometric theorems as illustrative examples, such as the Apollonian circle theorem which is one of the most difficult theorems proved by Chou [1986) using Wu's method. Our proof of this theorem was car­ ried out on a small computer HP1000. The maximal number of terms of polynomials appearing in the reduc­ tions is 1044. Some non-trivial theorems have also been proved by PS on an IBM-PC. However, using the prover, theorem proving becomes a relatively simple work be­ sides certain techniques such as the suitable choice of coordinates (in fact, which may be done mechanically too).

For discovering geometric theorems , there are several different ways, for example, numerical searching, guess­ ing and then proving as discussed in [Chou, 1985). The CPS involves also a sub-program for the first goal. A sys­ tematic way for theorem discovering is by means of cre­ ating first a geometric proposition and finding then the triangular form and the remainder using Wu's method. If the obtained remainder itself is identically equal to 0, then this proposition forms, of course, a true geometric theorem. Otherwise, if any factor of the remainder to be 0 has some geometric meaning, we may regard the geo­ metric statement correspoinding to that algebraic rela­ tion as a new additional hypothesis of the created propo­ sition and discover thus a new geometric theorem.

The author was trying to discover new theorems by different ways for a period of time after the implementa­ tion in 1985 and discovered independently several inter­ esting theorems. As examples, we may list four of them as follows.

1. If four lines in a plane form four triangles, then the orthocenters of these four triangles are collinear;

2. The five Gauss lines determined by five given lines in a plane, taken four at a time , are concurrent;

3. In the Pappus point theorem, two intersection points of every three Pappus lines are harmonically separated by the two basic lines, as are two intersection points of every three Leisenring lines;

4. The angle formed by the Simson lines of two points for a same triangle does not depend on the choice of the triangle and is measured by half the arc between the two points.

Among the above theorems, the second one has been called Wang's Theorem by several authors [Chou, 1985, Kapur, 1986, Kutzler and Stifter, 1986]. However, this theorem, even a more general theorem based on this one discovered by Chou [1986), is not a new one and thus not due to me at all. In fact , the above four theorems are all known.

About Pappus lines and Leisenring lines, Rigby pub­ lished a paper in Journal of Geometry in 1983. In his paper, there are some interesting geometric theorems involving the Pappus point theorem discovered by Wu [1984b) independently in 1980 and the above third the­ orem discovered by myself. The author [Wang, 1986] reproved a set of theorems appeared in Rigby's paper using prover CPS and in the meantime, conjectured and proved the following Theorem The six intersection points of every Pappus line and its corresponding Leisenring line are collinear.

This theorem is probably a new one. The proofs of other theorems concerning the Pappus lines and Leisen­ ring lines are quite simple by our prover. However, the proof of this theorem is not so simple as expected. It took about 14 hours CPU time on an IBM4341 com­ puter. The hypothesis of this theorem involves 30 poly­ nomials in 36 variables. The maximal number of terms of polynomials appearing in the reductions is 10980.

Acknowledgement

The author is deeply grateful to Professor Wu Wen-tsiin for his guidance, encourgement and valuable help on this work. This paper is written in part during author's visit at Computing Laboratory, Oxford University. The thanks are to Professor C. A. R. Hoare for the invitation and to Dr. S. A. Cameron for the arrangements.