Mechanical Geometry Theorem Proving

Foreword by Larry Wos ix
Preface by the Author xi
Part I: Methods in Mechanical Geometry Theorem Proving 1
Chapter 1. An Introduction to Wu's Method 3
1. The Defects in Traditional Proofs 3
1.1. The Traditional Euclidean Proof 3
1.2. The Traditional Analytic Proof 4
2. Four Examples 5
3. A Summary of Wu's Method 12
4. Pseudo Division and Successive Pseudo Division 12
5. A Simple Triangulation Procedure 14
6. Geometry Statements of Constructive Type 15
7. Further Discussion of Geometry Statements of Constructive Type 19
Chapter 2. Ritt's Characteristic Set Method 23
1. The Prerequisite in Algebra 23
2. Ascending Chains and Characteristic Sets 26
3. Irreducible Ascending Chains 28
4. A Complete Triangulation Procedure: Ritt's Principle 31
5. Ritt's Decomposition Algorithm 32
Chapter 3. Algebra and Geometry 34
1. Axiomatic Geometries and Number Systems 34
1.1. Affine Geometry 35
1.2. Metric Geometry 39
1.3. Hilbert Geometry 41
1.4. Tarski Geometry 41
2. On the Algebraic formulation of Geometry Statements 42
2.1. Formulation F1 43
2.2. Formulation F2 45
3. Formulation F3 46
3.1. The Generic Validity of a Geometry Statement 47
3.2. Identifying Nondegenerate Conditions 49
3.3. The Generic Validity of a Geometry Statement in an Arbitrary Field 51
Chapter 4. The Complete Method of Wu 52
1. Ritt's Principle Revised 52
2. Ritt's Decomposition Algorithm Revised 53
3. Complete Method of Wu - Irreducible Cases 54
4. Complete Method of Wu - General Case 57
5. Examples 58
Chapter 5. Geometry Theorem Proving Using The Groebner Basis Method 75
1. A Review of the Grobner Basis Method 75
2. Proof Methods for Formulation F3 77
3. A Proof Method for Formulation F1 81
4. Connections Between Characteristic Sets and Grabner Bases 83
5. A Comparison of the Groebner Basis Method with Wu's Method 88
5.1. The Scope 88
5.2. The Efficiency 88
References 90