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

• 作者: 张景中 李涛 邹宇
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 几何自动推理 可读机器证明 构造型几何命题 复系数质点法 CMPP
• 年，卷（期）: 2015,（8）
• 所属期刊栏目: 计算机理论与算法
• 页码范围: 1640-1647
• 页数: 8页
• 分类号: TP181
• 字数: 7076字
• 语种: 中文
• DOI: 10.11897/SP.J.1016.2015.01640

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张景中	广州大学计算机科学与教育软件学院	50	455	11.0	20.0
2	邹宇	广州大学计算机科学与教育软件学院	19	29	4.0	5.0
3	李涛	天津城建大学理学院	2	2	1.0	1.0