"This textbook presents various automatic techniques based on Grobner 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."--Jacket.