Abstract:
SGARP (sustainable geometry automated reasoning platform) enables users to add or change the knowledge involved in automated geometry theorem proving, such as geometry objects, predicates, theorems or reasoning rules, so that varieties of rule-based machine proving methods or human-machine interactive reasoning methods could be developed. In order to further enhance the automated reasoning power of SGARP and to expand its scope of application, this paper proposes a convenient way of implementing the symbolic computation modules in SGARP. Based on the embedded symbolic computation modules, the mass point method and the analytic method are successfully added into SGARP. The mass point method can prove the Hilbert intersection point statements, and the analytic method can assist in proving all types of difficult geometric theorems, such as the famous Thebault's Theorem. As for the two embedded methods, we test them with 180 geometry problems in TGTP (thousands of geometric problems for geometric theorem provers) which is a Web-based library of problems in geometry. The results show that all of the 180 geometry problems could be proved within a reasonable time with readable machine proofs, which shows that the upgraded SGARP can better satisfy the users' requirements for learning and developing automated geometry reasoning.