几何定理机器证明复系数质点法的改进及其应用

摘要：

复系数质点法是以几何点的运算为基础而建立起来的一种新的几何定理机器证明方法。它能高效地证明大部分构造型几何命题，但现有的复系数质点法仍不能有效地处理一些非线性构造型几何命题。为此，该文在原有工作的基础上，对原复系数质点法机器证明算法进行了较大的改进，新添加了一些重要的构图方式，并选用Mathematica 重新实现了改进的算法，创建了新的证明器 CMPP（Complex Mass Point method Prover）。对上百个几何定理的运行结果显示，证明器 CMPP 能有效地处理非线性构造型几何命题以及许多非构造型几何命题，在解题能力及运行效率上均有所提高。特别地，CMPP 能在短时间内实现五圆定理、莫莱定理等一些难度较大的几何定理的可读机器证明。

关键词：几何自动推理、可读机器证明、构造型几何命题、复系数质点法、CMPP

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

资助基金：国家自然科学基金11001228，11326212;国家“九七三”重点基础研究发展规划项目基金2011CB302412;国家自然科学基金-广东省联合基金项目U1201252;广州市属高校科研计划2012A019资助．

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

页数：共8页

页码：1640-1647