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

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

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

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

3、MethodandItsApplicationinAutomatedGeometryTheoremProving１）２）２）ＬＩＴａｏＺＯＵＹｕＺＨＡＮＧＪｉｎｇ-Ｚｈｏｎｇ１）（ＦacultyofＳcience，TianjinChengjianUniversity，Tianjin３００３８４）２）（CollegeofComputerＳcienceandＥducationalＳoftware，GuangzhouUniversity，Guangzhou５１０００６）AbstractＴｈｅｃｏｍｐｌｅｘｍａｓｓｐｏｉｎｔｍｅｔｈｏｄｉｓａｎｅｗｍｅｔｈｏｄｆｏｒａｕｔｏｍａｔｅ

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

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

6、ｎｙｎｏｎ-ｃｏｎｓｔｒｕｃｔｉｖｅｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｓｉｎａｄｄｉｔｉｏｎｔｏｌｉｎｅａｒｃｏｎｓｔｒｕｃｔｉｖｅｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｓ；ｍｏｒｅｏｖｅｒ，ＣＭＰＰｒｕｎｓｍｏｒｅｅｆｆｉｃｉｅｎｔｌｙ．Ｅｓｐｅｃｉａｌｌｙ，ＣＭＰＰｃａｎｐｒｏｖｅｍａｎｙｄｉｆｆｉｃｕｌｔｇｅｏｍｅｔｒｙｔｈｅｏｒｅｍｓ（ｓｕｃｈａｓｆｉｖｅｃｉｒｃｌｅｓｔｈｅｏｒｅｍａｎｄＭｏｒｌｅｙ’ｓｔｈｅｏｒｅｍ）ｉｎａｖｅｒｙｓｈｏｒｔｔｉｍｅａｎｄｃａｎｇｅｎｅｒａｔｅｈｕｍａｎ-ｒｅａｄａｂｌｅｍａｃｈｉｎｅｐｒｏｏｆｓ．Keywordsａｕｔｏｍａｔｅｄｇｅｏｍｅ

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