# Mechanical Theorem Proving in Geometries: Basic Principles

Springer Science & Business Media, Apr 14, 1994 - Computers - 288 pages
There seems to be no doubt that geometry originates from such practical activ ities as weather observation and terrain survey. But there are different manners, methods, and ways to raise the various experiences to the level of theory so that they finally constitute a science. F. Engels said, "The objective of mathematics is the study of space forms and quantitative relations of the real world. " Dur ing the time of the ancient Greeks, there were two different methods dealing with geometry: one, represented by the Euclid's "Elements," purely pursued the logical relations among geometric entities, excluding completely the quantita tive relations, as to establish the axiom system of geometry. This method has become a model of deduction methods in mathematics. The other, represented by the relevant work of Archimedes, focused on the study of quantitative re lations of geometric objects as well as their measures such as the ratio of the circumference of a circle to its diameter and the area of a spherical surface and of a parabolic sector. Though these approaches vary in style, have their own features, and reflect different viewpoints in the development of geometry, both have made great contributions to the development of mathematics. The development of geometry in China was all along concerned with quanti tative relations.

### What people are saying -Write a review

We haven't found any reviews in the usual places.

### Contents

 Desarguesian geometry and the Desarguesian number system 13 12 The axiom of infinity and Desargues axioms 18 13 Rational points in a Desarguesian plane 25 14 The Desarguesian number system and rational number subsystem 30 15 The Desarguesian number system on a line 37 16 The Desarguesian number system associated with a Desarguesian plane 42 17 The coordinate system of Desarguesian plane geometry 55 Orthogonal geometry metric geometry and ordinary geometry 63
 42 Factorization of polynomials 152 43 Wellordering of polynomial sets 159 44 A constructive theory of algebraic varieties irreducible ascending sets and irreducible algebraic varieties 169 45 A constructive theory of algebraic varieties irreducible decomposition of algebraic varieties 178 46 A constructive theory of algebraic varieties the notion of dimension and the dimension theorem 183 47 Proof of the mechanization theorem of unordered geometry 187 48 Examples for the mechanical method of unordered geometry 195 Mechanization theorems of ordinary ordered geometries 213

 22 Orthogonal axioms and unordered orthogonal geometry 70 23 The orthogonal coordinate system of unordered orthogonal geometry 80 24 Unordered metric geometry 91 25 The axioms of order and ordered metric geometry 102 26 Ordinary geometry and its subordinate geometries 109 Mechanization of theorem proving in geometry and Hilberts mechanization theorem 115 32 The standardization of coordinate representation of geometric concepts 118 33 The mechanization of theorem proving and Hilberts mechanization theorem about pure point of intersection theorems in Pascalian geometry 124 34 Examples for Hilberts mechanical method 128 35 Proof of Hilberts mechanization theorem 139 The mechanization theorem of ordinary unordered geometry 149
 52 Tarskis theorem and Seidenbergs method 220 53 Examples for the mechanical method of ordered geometries 228 Mechanization theorems of various geometries 235 62 The mechanization of theorem proving in projective geometry 236 63 The mechanization of theorem proving in BolyaiLobachevskys hyperbolic nonEuclidean geometry 246 64 The mechanization of theorem proving in Riemanns elliptic nonEuclidean geometry 258 65 The mechanization of theorem proving in two circle geometries 264 66 The mechanization of formula proving with transcendental functions 267 References 281 Subject index 285 Copyright