几何定理机器证明是用计算机来完成数学命题的证明,它是现代数学中一种新兴的边缘性学科,是现代人工智能发展的一个重要方向.经过多年来卓越科学家们的努力,几何定理机器证明的研究在七十年代已经取得突破,可读证明的实现也十多年了.事实证明,机器证明的研究已经取得了骄人的成绩.但从目前的推理软件来看,关于几何定理可读证明自动生成的研究,还不完善,这是由于,机器生成的证明与两千多年来人们所创造的巧妙证明相比,仍有一定的差距,应当把几何学家所掌握的更多方法<[8]>,如添加辅助线、辅助点等需要相当技巧的方法"教给"计算机,使计算机产生的解法可以与几何学家相比.在证明中使用辅助线和辅助点,是传统几何的特色,是高智能的几何解题方法,这一特色使传统几何证题方法显得格外美妙,但却给几何证明的机械化增添了很大的困难.辅助线、辅助点在解题中的必要性,是由于欧氏几何传统方法以全等三角形和相似三角形为基本工具.多数几何题中,常常没有现成的全等三角形和相似三角形,因而要添加辅助线、辅助点为基本工具创造条件.寻找添加辅助线、辅助点的规律是实现机器证明所要解决的一个问题之一<[9]>.该文工作的核心部分是第三和第四部分,分别解决添加辅助线和辅助点两方面的问题.第三部分实现区分连线,自动添加辅助线功能,由此大大减少了推理信息量,尤其对图形复杂的几何问题,推理时间的缩短更为明显,而且计算机自动添加的辅助线可以与手工添加效果相媲美;第四部分实现添加辅助点问题,根据边添加边删除的思想实现了几种类型的辅助点的添加,不仅提高了推理效率,而且进一步增强了计算机解题能力和解题灵活性.为了使解题过程符合传统阅读习惯,该文采用了前推式几何信息搜索法.该文程序用Miscrosoft Visual C++6.0开发完成.