by Pavel Pech (University of South Bohemia, Czech Republic)

Table of Contents (70k)
Preface (57k)
Chapter 1: Introduction (87k)

This textbook presents various automatic techniques based on Gröbner bases elimination to prove well-known geometrical theorems and formulas. Besides proving theorems, these methods are used to discover new formulas, solve geometric inequalities, and construct objects — which cannot be easily done with a ruler and compass.

Each problem is firstly solved by an automatic theorem proving method. Secondly, problems are solved classically — without using computer where possible — so that readers can compare the strengths and weaknesses of both approaches.

• Automatic Theorem Proving
• Generalization of the Formula of Heron
• Simson-Wallace Theorem
• Transversals in a Polygon
• Petr-Douglas-Neumann's Theorem
• Geometric Inequalities
• Regular Polygons