基于向量的几何可读自动证明  

Automated Geometry Readable Proving Based on Vector

作　　者：葛强[1,2] 张景中[2] 陈矛[2] 彭翕成[2] 

机构地区：[1]河南大学数据与知识工程研究所,河南开封475004 [2]华中师范大学国家数字化学习工程技术研究中心,武汉430079

出　　处：《计算机学报》2014年第8期1809-1819,共11页Chinese Journal of Computers

基　　金：国家自然科学基金(60903023;61304132);国家"八六三"高技术研究发展计划项目基金(2008AA01Z127);国家科技支撑计划课题(2013BAH18F02);河南省科技攻关计划项目(142102210397)资助~~

摘　　要：几何定理机器证明已经成功发展了多种新方法,但其中对中学几何中向量的机器证明研究没有抓住其回路的基本特征.文中以向量的回路为出发点,提出了基于回路的向量可读证明新方法,开发了机器证明新程序.该程序对常见的构造类型欧氏几何题目能快速作图,并依据题目类型的不同,分别用不同的向量方法对其进行自动推理,证明结果简短可读.经过大量实例测试,证明将向量用于几何自动推理是可行和高效的.与《超级画板》等中的证明器相比,文中算法在自动推理能力和证明过程可读性方面有较大提高.文中给出的基于向量的几何可读证明算法丰富了几何定理自动推理方法,并且具有应用于几何教学实践的价值.Many novel methods have been successfully developed in the field of automated geometry theorem proving,however,those based on the vector representations did not seize some basic characteristics of geometric vectors,and therefore have not given full play to the advantages of the vector method.To solve this problem,upon the concept of loop of vectors,we propose a new vector based readable automated geometry reasoning method in this paper.Moreover,we have implemented the corresponding software for automated theorem proving.For conventional Euclidean geometric problems,this software can construct geometry figure instantly.Furthermore,it can perform automated reasoning with various rules in the vector method according to the corresponding types of constructions.More importantly,the proofs generated by our software are concise and readable.The Experimental results show that the proposed method is efficient and effective.Compared with other provers such as Super Sketchpad,our prover greatly improves the proving ability and readability.Hence,our method not only enriches the current methods for geometry theorem proving,it also could be further developed into an education software and used in geometry education.

关 键 词：机器证明 可读证明 前推法 向量 回路 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]