期刊论文

Chen, Mao

中文

计算机学报

0254-4164

2014

37

8

1809-1819

10.3724/SP.J.1016.2014.01809

国家自然科学基金（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 ...