PROVING AND DISCOVERING GEOMETRY THEOREMS USING WU'S METHOD

The present dissertation is based on the pioneering work of the prominent Chinese mathematician Wu Wen-tsun on mechanical theorem proving in geometry.;We implement a new prover based on our studies of Wu's method and practical experience with previous provers. Our contributions to the method are: (1) A feasible algorithm for dealing with reducibility when the leading degrees of all hypotheses are less than or equal to 2 has been found and implemented. Our prover is the first that deals with reducible cases. (2) The prover is complete for a class of geometric statements in the sense that if the prover proves a theorem then there is a formal deduction from the theory of Wu's metric geometry; if it fails to prove a geometric statement then there are no such deductions. Nondegenerate conditions are either proved to be redundant or to be of clear geometric meaning. (3) The sources of irreducibility have been extensively studied based on many interesting practical theorems in geometry. A new method for removing one kind of reducibility has been found. (4) Several techniques have been developed for the discovery of new theorems, and a few new theorems have been found. In particular, the use of Ritt-Wu's decomposition algorithm provides a systematic way for discovering new theorems. (5) Problems involving such concepts as the addition of lengths of segments seem beyond the scope of Wu's method. However, a new technique is given to handle some of these problems and about ten theorems have been proved using this technique. A method for dealing with problems in which only the hypotheses involve order has been discussed. The famous theorem about equal internal bisectors is used as an example to show what parts of the proof can be mechanized and which ones have to be done manually at present.;We classify all models for the theory of Wu's metric geometry and hence establish the connection between Wu's method for proving theorems in geometry and the formal proofs of those theorems in the theory.