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

《几何定理机器证明复系数质点法的改进及其应用》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、第３８卷第８期计算机学报Ｖｏｌ．３８Ｎｏ．８２０１５年８月ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳＡｕｇ．２０１５几何定理机器证明复系数质点法的改进及其应用李涛１）２）２）邹宇张景中１）（天津城建大学理学院天津３００３８４）２）（广州大学计算机科学与教育软件学院广州５１０００６）摘要复系数质点法是以几何点的运算为基础而建立起来的一种新的几何定理机器证明方法．它能高效地证明大部分构造型几何命题，但现有的复系数质点法仍不能有效地处理一些非线性构造型几何命题．为此，该文在原有工作的基础上，对原复系

2、数质点法机器证明算法进行了较大的改进，新添加了一些重要的构图方式，并选用Ｍａｔｈｅｍａｔｉｃａ重新实现了改进的算法，创建了新的证明器ＣＭＰＰ（ＣｏｍｐｌｅｘＭａｓｓＰｏｉｎｔｍｅｔｈｏｄＰｒｏｖｅｒ）．对上百个几何定理的运行结果显示，证明器ＣＭＰＰ能有效地处理非线性构造型几何命题以及许多非构造型几何命题，在解题能力及运行效率上均有所提高．特别地，ＣＭＰＰ能在短时间内实现五圆定理、莫莱定理等一些难度较大的几何定理的可读机器证明．关键词几何自动推理；可读机器证明；构造型几何命题；复系数质点法；ＣＭＰＰ中图

3、法分类号ＴＰ１８１犇犗犐号１０．１１８９７／ＳＰ．Ｊ．１０１６．２０１５．０１６４０犐犿狆狉狅狏犲犿犲狀狋狅犳狋犺犲犆狅犿狆犾犲狓犕犪狊狊犘狅犻狀狋犕犲狋犺狅犱犪狀犱犐狋狊犃狆狆犾犻犮犪狋犻狅狀犻狀犃狌狋狅犿犪狋犲犱犌犲狅犿犲狋狉狔犜犺犲狅狉犲犿犘狉狅狏犻狀犵１）２）２）ＬＩＴａｏＺＯＵＹｕＺＨＡＮＧＪｉｎｇＺｈｏｎｇ１）（犉犪犮狌犾狋狔狅犳犛犮犻犲狀犮犲，犜犻犪狀犼犻狀犆犺犲狀犵犼犻犪狀犝狀犻狏犲狉狊犻狋狔，犜犻犪狀犼犻狀３００３８４）２）（犆狅犾犾犲犵犲狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲犪狀犱犈

4、犱狌犮犪狋犻狅狀犪犾犛狅犳狋狑犪狉犲，犌狌犪狀犵狕犺狅狌犝狀犻狏犲狉狊犻狋狔，犌狌犪狀犵狕犺狅狌５１０００６）犃犫狊狋狉犪犮狋Ｔｈｅｃｏｍｐｌｅｘｍａｓｓｐｏｉｎｔｍｅｔｈｏｄｉｓａｎｅｗｍｅｔｈｏｄｆｏｒａｕｔｏｍａｔｅｄｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｐｒｏｖｉｎｇｗｈｉｃｈｉｓｂａｓｅｄｏｎｏｐｅｒａｔｉｏｎｓａｍｏｎｇｇｅｏｍｅｔｒｉｃｐｏｉｎｔｓ．Ｔｈｅｃｏｍｐｌｅｘｍａｓｓｐｏｉｎｔｍｅｔｈｏｄｃａｎｂｅｕｓｅｄｔｏｐｒｏｖｅｍｏｓｔｃｏｎｓｔｒｕｃｔｉｖｅｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｓｅ

5、ｆｆｉｃｉｅｎｔｌｙ，ｂｕｔｓｏｆａｒｉｔｃｏｕｌｄｎ’ｔｄｅａｌｗｉｔｈｎｏｎｌｉｎｅａｒｃｏｎｓｔｒｕｃｔｉｖｅｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｓ．Ｏｎｔｈｅｂａｓｉｓｏｆｏｕｒｏｒｉｇｉｎａｌｗｏｒｋ，ｗｅｍａｄｅｉｍｐｒｏｖｅｍｅｎｔｓｔｏｔｈｅｏｒｉｇｉｎａｌａｌｇｏｒｉｔｈｍｏｆｔｈｅｃｏｍｐｌｅｘｍａｓｓｐｏｉｎｔｍｅｔｈｏｄ．Ｗｅａｄｄｅｄｓｏｍｅｎｅｗｉｍｐｏｒｔａｎｔｃｏｎｓｔｒｕｃｔｉｏｎｓ，ｉｍｐｌｅｍｅｎｔｅｄｔｈｅｉｍｐｒｏｖｅｄａｌｇｏｒｉｔｈｍａｇａｉｎｉｎｓｏｆｔｗａｒ

6、ｅＭａｔｈｅｍａｔｉｃａｔｏｂｅａｎｅｗｐｒｏｖｅｒＣＭＰＰ（ＣｏｍｐｌｅｘＭａｓｓＰｏｉｎｔｍｅｔｈｏｄＰｒｏｖｅｒ）．ＴｈｅｒｅｓｕｌｔｓｏｆｍｏｒｅｔｈａｎｏｎｅｈｕｎｄｒｅｄｇｅｏｍｅｔｒｙｓｔａｔｅｍｅｎｔｓｓｈｏｗｔｈａｔＣＭＰＰｃａｎｅｆｆｅｃｔｉｖｅｌｙｄｅａｌｗｉｔｈｎｏｎｌｉｎｅａｒｃｏｎｓｔｒｕｃｔｉｖｅｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｓａｎｄｍａｎｙｎｏｎｃｏｎｓｔｒｕｃｔｉｖｅｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｓｉｎａｄｄｉｔｉｏｎｔｏｌｉｎｅａｒｃｏｎｓｔｒｕｃｔｉｖｅｇｅｏｍ

7、ｅｔｒｙｔｈｅｏｒｅｍｓ；ｍｏｒｅｏｖｅｒ，ＣＭＰＰｒｕｎｓｍｏｒｅｅｆｆｉｃｉｅｎｔｌｙ．Ｅｓｐｅｃｉａｌｌｙ，ＣＭＰＰｃａｎｐｒｏｖｅｍａｎｙｄｉｆｆｉｃｕｌｔｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｓ（ｓｕｃｈａｓｆｉｖｅｃｉｒｃｌｅｓｔｈｅｏｒｅｍａｎｄＭｏｒｌｅｙ’ｓｔｈｅｏｒｅｍ）ｉｎａｖｅｒｙｓｈｏｒｔｔｉｍｅａｎｄｃａｎｇｅｎｅｒａｔｅｈｕｍａｎｒｅａｄａｂｌｅｍａｃｈｉｎｅｐｒｏｏｆｓ．犓犲狔狑狅狉犱狊ａｕｔｏｍａｔｅｄｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｐｒｏｖｉｎｇ；ｒｅａｄａｂｌｅｍａｃｈｉ

8、ｎｅｐｒｏｏｆｓ；ｃｏｎｓｔｒｕｃｔｉｖｅｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｓ；ｔｈｅｃｏｍｐｌｅｘｍａｓｓｐｏｉｎｔｍｅｔｈｏｄ；ＣＭＰＰ收稿日期：２０１３１２２３；最终修改稿收到日期：２０１４１０３０．本课题得到国家自然科学基金（１１００１２２８，１１３２６２１２）、国家“九七三”重点基础研究发展规划项目基金（２０１１ＣＢ３０２４１２）、国家自然科学基金广东省联合基金项目（Ｕ１２０１２５２）及广州市属高校科研计划（２０１２Ａ０１９）资助．李涛，