位置:成果数据库 > 期刊 > 期刊详情页
几何定理机器证明复系数质点法的改进及其应用
  • ISSN号:0254-4164
  • 期刊名称:计算机学报
  • 时间:0
  • 页码:-
  • 分类:TP181[自动化与计算机技术—控制科学与工程;自动化与计算机技术—控制理论与控制工程]
  • 作者机构:[1]天津城建大学理学院,天津300384, [2]广州大学计算机科学与教育软件学院,广州510006
  • 相关基金:国家自然科学基金(11001228,11326212); 国家“九七三”重点基础研究发展规划项目基金(2011CB302412); 国家自然科学基金-广东省联合基金项目(U1201252); 广州市属高校科研计划(2012A019)资助
  • 相关项目:可构图几何定理向量法可读机器证明的完全性新算法
中文摘要:

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

英文摘要:

The complex mass point method is a new method for automated geometry theorem proving which is based on operations among geometric points.The complex mass point method can be used to prove most constructive geometry theorems efficiently,but so far it couldn't deal with nonlinear constructive geometry theorems.On the basis of our original work,we made improvements to the original algorithm of the complex mass point method.We added some new important constructions,implemented the improved algorithm again in software Mathematica to be a new prover CMPP(Complex Mass Point method Prover).The results of more than one hundred geometry statements show that CMPP can effectively deal with nonlinear constructive geometry theorems and many non-constructive geometry theorems in addition to linear constructive geometry theorems;moreover,CMPP runs more efficiently.Especially,CMPP can prove many difficult geometry theorems(such as five circles theorem and Morley's theorem)in a very short time and can generate human-readable machine proofs.

同期刊论文项目
同项目期刊论文
期刊信息
  • 《计算机学报》
  • 北大核心期刊(2011版)
  • 主管单位:中国科学院
  • 主办单位:中国计算机学会 中国科学院计算技术研究所
  • 主编:孙凝晖
  • 地址:北京中关村科学院南路6号
  • 邮编:100190
  • 邮箱:cjc@ict.ac.cn
  • 电话:010-62620695
  • 国际标准刊号:ISSN:0254-4164
  • 国内统一刊号:ISSN:11-1826/TP
  • 邮发代号:2-833
  • 获奖情况:
  • 中国期刊方阵“双效”期刊
  • 国内外数据库收录:
  • 美国数学评论(网络版),荷兰文摘与引文数据库,美国工程索引,美国剑桥科学文摘,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2011版),中国北大核心期刊(2014版),中国北大核心期刊(2000版)
  • 被引量:48433