Selected Topics In Geometry With Classical Vs. Computer Proving

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.