Contents

1  Introduction	    5

1.1 Goals of the Thesis	    5

1.2 Achievements of the Thesis	    5

2  Historical Overview	    7

2.1 First Steps: Axiomatic Systems	    7

2.2 Algebraic Techniques	    8

2.2.1 Wu's Method	    8

2.2.2 Gröbner Bases Method	    9

2.2.3 Cylindrical Algebraic Decomposition	    9

2.3 Coordinate–Free Techniques	  10

2.3.1 The Area Method	  10

2.3.2 The Full–Angle Method	  11

2.3.3 The Vector Method	  11

2.3.4 Clifford Algebra	  11

2.4 Implementations	  11

3  Preliminaries	  13

3.1 Mechanization of Geometry	  13

3.2 Constructive Geometry Statements	  13

3.3 Constructive Geometry Statements Possibly Involving Inequalities	  15

4  Basic Elements of the Theorema System 	  16

4.1 Theorema	  16

4.2 Theorema Constructs as Input	  16

4.3 Simplify, Prove, Compute, Explore	  17

4.4 Theorema Notebooks as Output	  17

5  Implementation  of Known Proving Methods	  19

5.1 Main Functionalities	  19

5.1.1 Proving with GeometryProver	  19

5.1.2 Computation Problems	  19

5.1.3 Obtaining Different Forms of the Input Problem	  20

5.1.4 Systematic Exploration 	  21

5.2 Problem Input	  22

5.2.1 Input Formats Supported	  22

5.2.2 Supported Constructions and Conclusions	  24

5.2.3 Implementation	  26

5.2.4 GeomPalette	  26

5.3 Graphical Interface	  30

5.3.1 Graphical Representation of Geometric Configurations	  30

5.3.2 Visualization of Conditions Described by Inequalities	  33

5.3.3 Checking Conjectures by Examples	  34

5.3.4 Implementation	  36

5.4 Algebraic Methods	  39

5.4.1 Formulation  of  the Problem	  39

5.4.2 Algebraic Form – Algebraic Simplifier	  40

5.4.3 Wu's Method	  42

5.4.4 Gröbner Bases Method	  45

5.5 Coordinate–free Techniques – the Area Method	  50

5.5.1 Basic Notions	  50

5.5.2 Area Form – Area Simplifier	  51

5.5.3 Proving by the Area Method	  53

5.5.4 Computing Expressions Containing Geometric Quantities 
                        Using the Area Method	  60

6  Subalgorithms and Heuristics for Improving Existing Methods	  64

6.1 Choice of an Appropriate Coordinate System	  64

6.2 Incremental Wu's Method	  67

6.2.2 Method	  67

6.2.3 Example	  67

7  Combining Methods	  72

7.1 Proving Geometrical Theorems Involving Order Relation	  72

7.2 AreaCAD Method	  72

7.2.1 The Method	  72

7.2.2 Problem Input	  73

7.2.3 Step 1: Simplifying Expressions by the Area Method	  73

7.2.4 Step 2: Solving theProblem Using the CAD Method	  76

7.2,5 Output of the Proof	  77

8  Systematic Exploration of Geometric Configurations	  82

8.1 Proving ⟹ exploring	  82

8.2 Exploring by AreaExplore	  83

8.2.1 Problem Input 	  83

8.2.2 Computing Geometric Quantities 	  84

8.2.3 Finding Basic Properties	  84

8.2.4 Building the Knowledge Base 	  85

8.2.5 Output of the Results	  85

8.3 Implementation	  88

9  Conclusions	  94

References	  95

Appendix	  99

Pappus' Theorem	  99

The Butterfly Theorem	107

Line Intersections	117

Exploring the Trapezoid	127

Interior Bisector	131

Incircle and Circumcircle	135

OG ≤ OI ≤ OH	141

0.4<(r/h) <0.5.	147