论文部分内容阅读
几何学具有悠久的历史,两千多年来积累下来的几何知识是人类的宝贵财富。其中,几何证明是几何学的精华之一。几何题的证法,没有统一的方法可依循,有赖于个人的灵感和技巧,一直是数学教学中的难点和重点内容。用机器来模仿人的思维活动,来帮助人证明几何命题,是历史上一些卓越科学家的梦想,也是具有重要研究价值和应用价值的研究方向。吴文俊建立的数学机械化方法,极大的推动了几何定理机器证明领域的研究。目前,基于不同推理算法的自动推理系统已经出现,在科学研究和工程计算中发挥着重要的作用。但是,几何定理自动推理领域中的丰富成果,在教育中并没有得到充分应用,其教育价值远远没能得到充分体现。原因一方面在于中学教育阶段涉及到的几何知识比较初等,而现有的几何自动推理方法给出的证明过程难于被中学生理解；另一方面,几何知识的教学又涉及语言表达与作图、从图形发现问题、问题分析与解答等多个方面,不仅仅是单纯的几何定理机器证明。面对中学几何教学的应用需求,几何自动推理的研究面临着中学几何知识范围、解答步骤长度、推理时间和推理方法等多方面的限制。针对这些限制条件,本文开展了面向中学几何教学的几何自动推理的研究工作,涉及几何自动推理在动态几何作图、几何问题生成、向量法解题等方面的理论方法与应用,研究成果(创新点)包括以下几个方面：第一：提出动态几何作图中的枢点概念,建立了以枢点为基础的动态几何机制,设计了包括智能作图方法,语义作图方法和文本作图等几何作图方法。实现了相应的动态几何作图系统,拓展了动态几何理论。第二：提出并实现基于向量法的自动推理算法。该自动推理方法基于向量的回路特征,对构造型交点类几何命题能迅速地给出可读的向量式证明,证明过程简洁优美。这种自动推理方法能够在限制条件内能达到推理不动点,在构造型交点类的题目上表现出较高的效率。第三：提出并实现了基于自动推理的几何问题自动生成与答案验证方法。以自动推理为基础,设计了可以生成填空、判断、选择、计算和证明等多种题型的自动出题方法,并实现对用户的解答进行实时验证。这种方法创新了几何学出题方式,提高了测试效率。综合应用上述研究成果,实现了一个面向中学教学应用的几何自动推理原型系统,其主要功能包括动态几何作图、几何自动推理和题目自动生成。这三种主要功能有机集成,可满足教师课堂教学和学生课下自学的需求。最后提出了值得进一步研究的问题和对此方向未来的展望。