几何定理机器证明复系数质点法的改进及其应用 - 计算机学报.pdf

第 卷 第 期 计 算 机 学 报 ３８ ８ 　 　　 　　 　　 　　 Ｖｏｌ．３８ Ｎｏ．８ 年 月 ２０１５ ８ Ａｕ．２０１５ ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳ ｇ 　 几何定理机器证明复系数质点法的改进及其应用 １） ２） ２） 李 涛 邹 宇 张景中 　 　 　 　 １）（天津城建大学理学院 天津 ３００３８４） 　 　 ２）（广州大学计算机科学与教育软件学院 广州 ５１０００６） 　 　 摘 要 复系数质点法是以几何点的运算为基础而建立起来的一种新的几何定理机器证明方法 它能高效地证明 ． 　 　 大部分构造型几何命题，但现有的复系数质点法仍不能有效地处理一些非线性构造型几何命题 为此，该文在原有 ． 工作的基础上，对原复系数质点法机器证明算法进行了较大的改进，新添加了一些重要的构图方式，并选用 重新实现了改进的算法，创建了新的证明器 （ ）对上百个几 Ｍａｔｈｅｍａｔｉｃａ ＣＭＰＰＣｏｍ ｌｅｘＭａｓｓＰｏｉｎｔｍｅｔｈｏｄＰｒｏｖｅｒ． ｐ 何定理的运行结果显示，证明器 ＣＭＰＰ能有效地处理非线性构造型几何命题以及许多非构造型几何命题，在解题 能力及运行效率上均有所提高 特别地， 能在短时间内实现五圆定理、莫莱定理等一些难度较大的几何定理 ． ＣＭＰＰ 的可读机器证明． 关键词 几何自动推理；可读机器证明；构造型几何命题；复系数质点法； ＣＭＰＰ 　 中图法分类号 号 ／ ＴＰ１８１ 犇犗犐 １０．１１８９７ＳＰ．Ｊ．１０１６．２０１５．０１６４０ 　　　 犐犿 狉狅狏犲犿犲狀狋狅犳狋犺犲犆狅犿 犾犲狓犕犪狊狊犘狅犻狀狋犕犲狋犺狅犱 狆 狆 犪狀犱犐狋狊犃 犾犻犮犪狋犻狅狀犻狀犃狌狋狅犿犪狋犲犱犌犲狅犿犲狋狉犜犺犲狅狉犲犿犘狉狅狏犻狀 狆狆 狔 犵 １） ２） ２） ＬＩＴａｏ ＺＯＵＹｕ ＺＨＡＮＧＪｉｎ