Using geometric rewrite rules for solving geometric problems symbolically

AbstractThis paper describes the theoretical framework of a geometric problem solver based on rewrite rules which were directly derived from axioms of Euclidean geometry. Completeness and termination of the system were obtained by making the set of rewrite rules locally confluent and by introducing a simple, well-founded ordering. This research presents a first step in finding a geometric alternative to the numerical and computer algebra methods currently used for such problems and, thus, has the potential of supporting geometric applications such as computer-aided geometric design