This textbook presents various techniques of elimination based on Gröbner bases 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 easily be done with a ruler and compass.

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

Contents:

• 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