Using geometric rewrite rules for solving geometric problems symbolically (Q685375)

The paper develops a rewrite rule system operating on geometric predicates. The system is able to derive symbolic prescriptions for compass and ruler construction of configurations satisfying given constraints and to reason about congruence relation. Completeness and termination of the system are obtained by making the set of rewrite rules locally confluent and by introducing a simple, well-founded ordering of the terms of language. While the system is not fully presented (we assume this is realized in the author's thesis), enough details are given to make the reader fell how it works and what its capabilities are.