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

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

SGARP中全角法的实现

在可持续发展的几何自动推理平台SGARP中,通过添加全角法相关的对象、谓词和定理,在SGARP中成功实现了全角法.添加了全角法的SGARP测试证明了100个几何定理.

质点法在SGARP中的新实现

可持续发展的几何自动推理平台(SGARP)支持用户发展多种多样基于规则的机器自动推理或人机交互推理方法,但缺乏处理符号计算的模块,其解题能力仍有待加强.质点法是最近发展的继面积法之后又一个能对可构造型几何命题生成可读机器证明的具有完全性的算法.基于一种在SGARP中快捷实现符号计算功能的方法,对质点法机器证明算法进行了新的实现.新添加的质点法模块使得用户能更便捷地验证更多的几何定理,从而使SGARP能更好地满足用户学习与发展几何机器推理的需求.

复系数质点法在SGARP中的新实现

在可持续发展的几何自动推理平台SGARP上添加了符号计算、解析法和实系数质点法推理模块的基础上添加了证明涉及度量几何问题的复系数质点法推理模块.根据复系数质点法的基本理论,建立了复系数质点法的算法、编写了Python和Visual C++的混合程序,在SGARP中建立了两个方便用户使用的相对独立的推理模块--复系数质点法鼠标作图自动推理模块和复系数质点法构图语句自动推理模块.使得用户能更便捷地验证更多的几何定理,从而使SGARP能更好地满足用户学习与发展几何机器推理的需求.