有限制条件的几何定理机器证明

中学几何教学对具有几何定理自动推理功能的智能教育软件有强烈需求，但现有"几何定理机器证明"的研究成果还不能满足中学几何教学的实际需求。为了充分挖掘"几何定理机器证明"的教学价值，满足中学几何教学的实际需求，本项目开展有限制条件的"几何定理机器证明"研究，在提高算法推理能力使之能满足教学需求的同时，对算法的推理规则、证明的长度和证明的表达形式等进行限制。主要研究内容包括(1)将向量法、辅助线法和反证法等中学课本上的证题方法设计为算法；(2)设计推理规则库和谓词库；(3)将前推法和后推法结合起来形成一个双向搜索算法；(4)设计算例库，对"有限制条件的几何定理机器证明"算法进行测试。本项目可进一步深入研究"几何定理机器证明"，也将对数学机械化在几何教学中的应用起到一定推动作用，为设计开发智能教育软件奠定理论和技术基础。

中学几何教学对具有几何定理自动推理功能的智能教育软件有强烈需求，但现有“几何定理机器证明”的研究成果还不能满足中学几何教学的需求。本项目系统深入地开展有限制条件的“几何定理机器证明”研究，旨在充分挖掘“几何定理机器证明”的教学价值，满足中学几何教学的需求。本项目在分析中学几何定理以及推理法、添加辅助线法和向量法等几何证明常用方法的基础上，将这些几何定理和证题规律总结为一系列谓词和推理规则，并将前推法和后推法结合起来，设计了一个高效的双向搜索算法。在算法设计中，我们对算法的推理规则、证明的长度和证明的表达形式等进行限制，使之不超出中学几何教学大纲的范畴，以充分满足实际教学的需求。为验证本项目给出的算法和方法，我们研发了一款几何定理自动推理原型系统，并基于中学几何课本上的练习题、习题集和数学竞赛题设计了一套测试算例集。测试结果表明，本项目给出的自动推理算法能对算例集中82%的题目给予成功证明。除了一些较难的竞赛题，绝大多数题目的推理长度不超过13步，推理时间在3秒以内，可满足中学几何教学的实际需求。基于几何定理自动推理过程中形成的推理链，我们还研究了几何证明题的自动出题及解答验证机制，实现了包括填空、判断、选择、计算和证明等多种题型在内的自动出题和解答验证功能。本项目的研究成果丰富了几何定理机器证明研究的方法和手段，对数学机械化在几何教学中的应用起到一定推动作用，为设计开发数学学科相关的智能教育软件奠定了理论和技术基础。