zbMATH — the first resource for mathematics

Selected topics in geometry with classical vs. computer proving. (English) Zbl 1149.51007
Hackensack, NJ: World Scientific (ISBN 978-981-270-942-4/hbk). xi, 239 p. (2007).
The book under review presents the method of automatic theorem proving based on Gröbner bases elimination. It does so by selecting several well known theorems from Euclidean Geometry, presenting the traditional proof of each, then writing a program for an automatic computer proof that can be run on the freely distributed software CoCoA. The selection of the theorems is very nice, making the book quite interesting even to those with no interest in computer-based proofs.
After an introduction in Chapter 1, Chapter 2 describes the mathematical theory behind the method of automatic theorem proving, describes the method itself, and applies it to simple examples. Chapter 3 considers Heron’s and Brahmagupta’s formulas for the areas of triangles and cyclic quadrilaterals and investigates possible generalizations to cyclic pentagons and hexagons along the line of the work of late D. P. Robbins in [Discrete Comput. Geom. 12, No. 2, 223–236 (1994; Zbl 0806.52008)] and his work with M. Malley and J. Roskies in [Adv. Appl. Math. 34, No. 4, 669–689 (2005; Zbl 1088.52005)].
Chapter 4 deals with the Simson-Wallace theorem and presents the beautiful and not so well known generalization attributed to Gergonne and the recent generalization by Guzmán. It also presents generalization to tetrahedra. Chapter 5 treats the theorems of Ceva and Menelaus, generalizations to quadrilaterals and pentagons, several consequences, and generalizations to three-dimensional space. Chapter 6 is concerned with the celebrated Petr-Douglas-Neumann theorem and the many interesting theorems connected with it. These include the theorems of Napoleon, Finney, Thébault, van Aubel, and Finsler-Hadwiger. The only spatial version of the Petr-Douglas-Neumann treated in this chapter is the theorem of Douglas that deals with a skew pentagon. Obviously, the author is not aware of the generalizations to \(d\)-simplices of Napoleon’s theorem that are proved by H. Martini and B. Weissbach in [Geom. Dedicata 74, No. 2, 213–223 (1999; Zbl 0920.51008)] and by M. Hajja, H. Martini, and M. Spirova in [Beitr. Algebra Geom. 47, No. 2, 363–383 (2006; Zbl 1116.51013) and Beitr. Algebra Geom. 49, No. 1, 253–264 (2008; Zbl 1142.51015)]. These, too, would form a suitable topic to add to this chapter.
Chapter 7 is on geometric inequalities. These include inequalities among sides and diagonals of quadrilaterals (and general polygons), the Neuberg-Pedoe inequality, the Wirtinger’ s inequality, the isoperimetric inequality, and Euler’s inequality between the circumradius and inradius of a triangle and a \(d\)-simplex. Chapter 8 is about certain skew regular polygons and conditions that guarantee their planarity. Chapter 9 discusses miscellaneous issues that include certain difficult and impossible Euclidean constructions.
The book has its share of misprints and uncommon usage of some terminology. A very careful revision will be necessary for a second edition, which may also be accompanied by a CD-ROM that contains the software CoCoA together with examples.
Beside being extremely useful to those who would like to benefit from automatic theorem proving and discovering, the book is also of great interest to anyone interested in geometry, thanks to the beautiful selection of topics it covers.

51M05 Euclidean geometries (general) and generalizations
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
51M04 Elementary problems in Euclidean geometries
51-02 Research exposition (monographs, survey articles) pertaining to geometry
68-02 Research exposition (monographs, survey articles) pertaining to computer science
CoCoA; Lugares