Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang (Q1329538)

This is a brilliant presentation of computational geometry, which may also serve as introductory text to axiomatic geometry. First an introduction to different geometric systems is given starting with Desarguesian geometries. It is shown how to obtain an algebraization and a coordinate system for this geometry. Following the line of increasing complexity the author introduces orthogonal, metric, ordered and eventually ordinary (Euclidean) geometry. For all these geometries the corresponding number types and coordinate systems are defined and illustrated by well-known geometric problems. While chapter 2 presents some basic facts in geometry, chapter 3 introduces the key concept of this book, the mechanization problem and the mechanization theorem. Describing the history of this problem the author emphasizes the importance of Hilbert's ``Grundlagen der Geometrie'' to the development of mechanical methods in geometry. It is outlined that the Euclidean method to prove geometric theorems shows a problematic behavior in handling degenerate cases (e.g. triangles becoming line segments, circles becoming points etc.); this weakness makes the Euclidean proof method less rigorous in practice. It is shown how additional logical rigor is obtained in Hilbert's approach which directly leads to formulation of the so-called ``mechanization theorem''. This theorem -- expressible for various types of geometries -- defines the conceptual backbone of this book. It is the statement that there exists a mechanical method to (first) find all degeneracy conditions and to produce proofs for all provable statements (under these conditions). It is shown that Hilbert's method yields a mechanization theorem for pure point intersection theorems in Pascalian geometry. Chapter 4 is the real heart and principal chapter of the book; it contains a detailed and thorough presentation of the author's famous work on geometry theorem proving. In cases where the associated number system is a field, hypotheses and conclusions of theorems can (in most relevant cases) be represented by polynomial equality relations; merely the nondegeneracy conditions have to be expressed as inequalities. On the basis of J. F. Ritt's constructive algebraic geometry the author develops his method of geometry theorem proving; the key techniques and concepts are well-ordering of sets of polynomials and irreducible ascending sets of polynomials. The method is essentially based on division of the consequence polynomial over an irreducible ascending set of polynomials. The section culminates in the proof of the mechanization theorem of unordered ordinary geometry. In developing the method the author presents a constructive theory of algebraic varieties and of irreducible decomposition. This part of the book is also interesting from the purely algebraic point of view. At the end of the chapter some relevant examples illustrate the power of the method; particularly impressing is the handling of Feuerbach's theorem which clearly is a nontrivial one. In the area of ordered geometries there exist the well-known decision procedure for the theory of real closed fields by A. Tarski and its improvement by G. E. Collins. Although these methods are not very efficient in practice they are more general than the approach in this book (existential quantifiers are allowed!). Although Tarski's theorem is discussed in chapter 5.2 it would have deserved a little more attention. However the author presents an improvement of Tarski's method for the purely equational syntax type. The final chapter contains a description of mechanical theorem proving methods for several non-Euclidean geometries, among them the geometry of Bolyai and Lobachevsky. To some up, this book not only gives an introduction to axiomatic geometry and mechanical theorem proving in geometries but also presents modern advanced methods in a clear and intelligible way. Many things in the book, particularly the chapter on the author's method and on algebraic varieties, may also be of interest to the pure mathematician. The book clearly is a valuable source of knowledge to researchers and graduate students interested in symbolic computation, algebra and geometry.