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

项目名称： 有限制条件的几何定理机器证明

项目编号： No.60903023

项目类型： 青年科学基金项目

立项/批准年度： 2010

项目学科： 矿业工程

项目作者： 陈矛

作者单位： 华中师范大学

项目金额： 17万元

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

中文关键词： 自动推理；几何定理；双向推理算法；自动出题；动态几何

英文摘要：

英文关键词： Automated reasoning；Geometric theorems；Two-way reasoning algorithm；Auto-generation of problems；Dynamic geometry