Mechanical Theorem Proving in Geometries : Basic Principles

Author's note to the English-language edition.- 1 Desarguesian geometry and the Desarguesian number system.- 1.1 Hilbert's axiom system of ordinary geometry.- 1.2 The axiom of infinity and Desargues' axioms.- 1.3 Rational points in a Desarguesian plane.- 1.4 The Desarguesian number system and rational number subsystem.- 1.5 The Desarguesian number system on a line.- 1.6 The Desarguesian number system associated with a Desarguesian plane.- 1.7 The coordinate system of Desarguesian plane geometry.- 2 Orthogonal geometry, metric geometry and ordinary geometry.- 2.1 The Pascalian axiom and commutative axiom of multiplication - (unordered) Pascalian geometry.- 2.2 Orthogonal axioms and (unordered) orthogonal geometry.- 2.3 The orthogonal coordinate system of (unordered) orthogonal geometry.- 2.4 (Unordered) metric geometry.- 2.5 The axioms of order and ordered metric geometry.- 2.6 Ordinary geometry and its subordinate geometries.- 3 Mechanization of theorem proving in geometry and Hilbert's mechanization theorem.- 3.1 Comments on Euclidean proof method.- 3.2 The standardization of coordinate representation of geometric concepts.- 3.3 The mechanization of theorem proving and Hilbert's mechanization theorem about pure point of intersection theorems in Pascalian geometry.- 3.4 Examples for Hilbert's mechanical method.- 3.5 Proof of Hilbert's mechanization theorem.- 4 The mechanization theorem of (ordinary) unordered geometry.- 4.1 Introduction.- 4.2 Factorization of polynomials.- 4.3 Well-ordering of polynomial sets.- 4.4 A constructive theory of algebraic varieties - irreducible ascending sets and irreducible algebraic varieties.- 4.5 A constructive theory of algebraic varieties - irreducible decomposition of algebraic varieties.- 4.6 A constructive theory of algebraic varieties - the notion of dimension and the dimension theorem.- 4.7 Proof of the mechanization theorem of unordered geometry.- 4.8 Examples for the mechanical method of unordered geometry.- 5 Mechanization theorems of (ordinary) ordered geometries.- 5.1 Introduction.- 5.2 Tarski's theorem and Seidenberg's method.- 5.3 Examples for the mechanical method of ordered geometries.- 6 Mechanization theorems of various geometries.- 6.1 Introduction.- 6.2 The mechanization of theorem proving in projective geometry.- 6.3 The mechanization of theorem proving in Bolyai-Lobachevsky's hyperbolic non-Euclidean geometry.- 6.4 The mechanization of theorem proving in Riemann's elliptic non-Euclidean geometry.- 6.5 The mechanization of theorem proving in two circle geometries.- 6.6 The mechanization of formula proving with transcendental functions.- References.