智能解答是人工智能中的重要研究领域。随着教育信息化的深入发展,要求教育资源智能化,而不是简单的“电子化”。教育软件缺少智能性或智能化程度不高,导致难以满足教学需求。研发高智能的教育软件已成为解决问题的关键,智能解答是其中的核心技术。本文研究的几何自动推理属于智能解答的分支。通过文献梳理和调研,我们发现几何自动推理领域研究成果丰富,但已有推理算法对产生的证明是否足够简短易于理解掌握,其几何意义是否足够丰富易于揭示几何关系、发现新的定理,关注还不够。因此有必要探索新的推理算法,主要围绕两个目标努力,一是提高机器解答的可读性,实现“明证”(即一目了然的证明);二是更多地发现新的几何定理。本文具体研究内容和主要贡献如下:一、提出了点几何恒等式算法。在学习吴方法的基础上,用点几何运算方式简明地表示几何关系,并转化为向量多项式,通过待定系数法解方程,探寻能关联命题条件和结论关系的恒等式。生成的代数恒等式,有明显的几何意义,在数形之间架构了一座新的桥梁。此方法原理简单,计算简便,给出的证明易于理解,读者需要的基础知识少,基本实现“明证”的目标。多数证明甚至比原题更简短,且清楚展现了条件和结论之间的关系,因此既能由一题扩展到多题,还能从低维扩展到高维。二、提出了基于点几何恒等式的混合推理算法。为了更好地利用不同解答方法的优势,结合代数计算和搜索思想,提出两种挖掘隐藏关系的算法,大大扩展了恒等式方法的解题范围。对长期讨论的某些有序几何问题,给出简短的恒等式证明,指出命题成立的充要条件,并将命题多角度扩展;而以往的解决方案需要引入较多的新概念,复杂运算,还达不到这样的效果。开发了点几何解答系统,针对可构图几何问题,能生成有详细步骤的可读证明,其中的遍历搜索功能与延伸作图功能相结合,可批量发现并证明几何定理,所发现的结论为恒等式算法提供补充。三、提出了向量方程消元算法。基于复数形式的欧拉公式,将几何关系转化成向量方程组,然后利用线性方程组的基础性质消去向量,从而抽取出含有边长和角度关系的系数矩阵,计算行列式并化简,调用消元法消去不感兴趣的变量,得到一些几何意义鲜明的关系式。这是将代数方法和不变量相结合的新思路。应用此方法研究一些经典几何图形,不但能重现经典结论,还能发现图形中蕴藏但前人疏漏的结论。此方法擅长发现和证明多项式形式的边角关系,这是以往研究所欠缺的。特别是对单个三角形的研究,能自动生成或强制生成大量三角恒等式。四、建立了一个几何题库。为检验算法的有效性,我们整理研究了 1000余例有代表性的几何问题。这些典型案例经本文算法处理之后,发现了许多新的结论,使得题目的内涵变得丰富,题目质量大大增强。有助于学生实行变式练习,加强巩固重点难点。为方便一线师生使用,我们基于题库出版了系列文章和著作,其中的题目,大部分来自人工收集,少部分由计算机自动生成,解答则几乎由机器完成,人只在其中增加少量连词和分析,使得读起来更加顺畅。而这些主要由计算机自动生成的命题和解答,审稿人和读者都没察觉是机器所为,充分说明能被教育领域理解和接受。同时也表明本文给出的机器解答,从某种程度上可认为通过了图灵测试。本文研究了基于点几何的自动推理方法,并指出它在数学教育上的种种应用,为基础数学教育内容的改进提供了一种新的途径。此外,本文研究也引人思考,人类的解答未必最佳,计算机可能给出让人惊讶的解答。计算机给出解答甚至比题干还短,这看似“有悖”常识,但又引起思考,如何知识表示才能尽量简洁而又方便推理。知识的创新表示,要尽量符合信息时代的要求,同时也可能造成原有知识体系的重新定位。