The Basis Of Geometric Algebra And Readable Machine Proof For Mass Point Geometry

In the past thirty years since Wu's method published in 1977, the research and practice for automated proving of geometry theorems have been considerably developed. For statements in unordered geometry, the algebraic methods and the numerical parallel methods can effectively judge true and false, while the area method and the search methods can moreover generate readable proofs. As for readable machine proving methods for geometry theorems, later in time than the area method, there have been the vector method and the full-angle method, which have been developed as the geometric algebra method and the advanced invariants method. However, all these methods have been dealing with geometry problems using the geometric quantities other than the very basic geometric points, thus it is not so easy for these methods to be extended or combined. Furthermore, except for the area method, other methods have not been developed as the complete machine proving algorithms. Mass Point Geometry, whose basic idea is to establish algebraic operations among geometric points (other than coordinate points or geometric quantities), provides an operational model for developing the geometry theorem proving method based on geometric points. Mass Point Geometry supports the linear operations directly to geometric points, and also can express vector and area; each mass point expression has a clear geometric and physical interpretation. Thus, Mass Point Geometry can be regarded as a very basic geometric algebra.This paper proves the basic importance of Mass Point Geometry to geometric algebra, develops a new readable machine proving methods for geometry theorems based on geometric points, mass point method, and establishes two machine proving algorithms which can deal with the Hilbert intersection point statements and the linear constructive geometry statements respectively, and then implements the algorithms on Maple. Since we can do arithmetic operations directly to points, the algorithms and programming for the mass-point method are much more concise than that of the area method. The run results of hundreds of non-trivial statements show that our method is not only efficient, most proofs'readability are also very satisfactory. The paper is divided into five chapters:Chapter One briefly reviews the various readable machine proving methods for geometry theorems, gives an overview for geometric algebra, and explains the main objective of this paper.Chapter Two preliminarily studies the basis of the geometric algebra from a new perspective. The results show that the emergence of the concept and method, Mass Point Geometry and vector space, is not accidental. Both of Mass Point Geometry and vector space are, in some sense, bound to be a stage of development which the geometric algebra would experience.Chapter Three develops a new automated proving method based on the basic propositions of Mass Point Geometry, the mass point method, and establishes the affine-geometry- machine-proof algorithm which can deal with the Hilbert intersection point statements, Mass-Point-Method (MPM), and implements it as the MPM prover on Maple.Chapter Four develops the complex coefficient mass point geometry and the complex mass point method, establishes another complete algorithm which is effective against constructive statements in unordered geometry, Complex-Mass-Point-Method (CMPM), and implements it as the CMPM prover on Maple.Chapter Five collects statistics for the experimental data of 410 examples, summarizes this paper's work and points out the further work to be carried out.