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

摘要：

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

关键词：可由用户持续发展的几何自动推理平台(SGARP)、几何定理机器证明、符号计算、Python语言、质点法、Thebault定理

所属期刊栏目：51

分类号：TP181(自动化基础理论)

资助基金：国家“九七三”重点基础研究发展计划基金项目2011CB302412;国家自然科学基金-广东联合基金项目U1201252;国家自然科学基金项目11001228,11326212;广州市教育局科技项目2012A019

在线出版日期：2014-08-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：1341-1351