EJMT Abstract

Derivation of geometry theorems belongs to mighty tools of automated geometry theorem proving. By elimination of suitable variables in the system of algebraic equations describing a geometric situation we get required formulas. The power of derivation is presented on computation of the area of planar polygons given by their lengths of sides and diagonals. This part we conclude with derivation of a formula of Robbins for the area of a cyclic pentagon given by its side lengths. Searching for loci of points of given properties is a special case of derivation. This topic belongs to the most difficult parts of school mathematics all over the world. New technologies DGS and CAS enable to overcome this problem. We demonstrate it in a few examples from elementary geometry.