On the automatic derivation of a set of geometric formulae

Leta, b, andc be the three sides of a triangleABC, a_i,b_i,c_i anda_e,b_e, c_e be the lengths of the three internal and external bisectors of the three anglesA, B, andC respectively. It is easy to express the bisectors as formulae of the sides. In this paper, we solve a problem proposed by H. Zassenhaus: for any three different bisectors in {a_i, b_i, c_i, a_e, b_e, c_e}, finding the relations between each side of the triangle and the three chosen bisectors. We also prove that given any general values for three different bisectors (internal or external) of a triangle, we can not draw the triangle using a ruler and a pair of compasses alone. The formulae mentioned above are derived automatically using a general method of mechanical formula derivation.This work was partially supported by a Grant from Chinese NSF and by the NSF Grant CCR-917870.