SGARP中符号计算模块的实现及其应用

The Realization and Application of Symbolic Computation Modules in SGARP

可持续发展的几何自动推理平台(sustainable geometry automated reasoning platform,SGARP)支持用户按需添加或修改几何定理机器证明所涉及的几何对象、谓词、定理和规则,以发展多种多样基于规则的机器自动推理或人机交互推理方法.为进一步提高SGARP的推理能力和扩展其适用范围,提出一种在SGARP中实现符号计算功能的快捷方法,并成功添加了质点法和解析法推理模块.质点法可证明希尔伯特交点类几何命题,解析法能用于辅助证明各种类型有一定难度的几何定理,如著名的Thebault定理.对这两种方法用基于Web的机器证明测试用的几何问题库(thousands of geometric problems for geometric theorem provers,TGTP)中180道几何题进行评估,均在合理时间内给出令人满意的可读机器证明,表明升级后的SGARP能更好地满足用户学习与发展几何机器推理的需求.

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.