Mechanical Geometry Theorem Proving

I: Methods in Mechanical Geometry Theorem Proving.- 1. An Introduction to Wu's Method.- 1. The Defects in Traditional Proofs.- 1.1. The Traditional Euclidean Proof.- 1.2. The Traditional Analytic Proof.- 2. Four Examples.- 3. A Summary of Wu's Method.- 4. Pseudo Division and Successive Pseudo Division.- 5. A Simple Triangulation Procedure.- 6. Geometry Statements of Constructive Type.- 7. Further Discussion of Geometry Statements of Constructive Type.- 2. Ritt's Characteristic Set Method.- 1. The Prerequisite in Algebra.- 2. Ascending Chains and Characteristic Sets.- 3. Irreducible Ascending Chains.- 4. A Complete Triangulation Procedure: Ritt's Principle.- 5. Ritt's Decomposition Algorithm.- 3. Algebra and Geometry.- 1. Axiomatic Geometries and Number Systems.- 1.1. Affine Geometry.- 1.2. Metric Geometry.- 1.3. Hilbert Geometry.- 1.4. Tarski Geometry.- 2. On the Algebraic formulation of Geometry Statements.- 2.1. Formulation Fl.- 2.2. Formulation F2.- 3. Formulation F3.- 3.1. The Generic Validity of a Geometry Statement.- 3.2. Identifying Nondegenerate Conditions.- 3.3. The Generic Validity of a Geometry Statement in an Arbitrary Field.- 4. The Complete Method of Wu.- 1. Ritt's Principle Revised.- 2. Ritt's Decomposition Algorithm Revised.- 3. Complete Method of Wu - Irreducible Cases.- 4. Complete Method of Wu - General Cases.- 5. Examples.- 5. Geometry Theorem Proving Using The Grobner Basis Method.- 1. A Review of the Grobner Basis Method.- 2. Proof Methods for Formulation F3.- 3. A Proof Method for Formulation Fl.- 4. Connections Between Characteristic Sets and Grobner Bases.- 5. A Comparison of the Grobner Basis Method with Wu's Method.- 5.1. The Scope.- 5.2. The Efficiency.- References.- II: 512 Theorems Mechanically Proved.- Explanations.- 1. General Remarks.- 2. Algebraic Representations of Geometric Conditions.- Theorems Proved Mechanically by Wu's Method.- 2. Algebraic Representations of Geometric Conditions.- Appendix. The Timing For the Grobner Basis Method.- Index of Examples.