【作者】 葛强；

【导师】 张景中；

【作者基本信息】 华中师范大学 ， 教育技术学， 2011， 博士

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

【Abstract】 With a long history, the knowledge of geometry is a valuable wealth of mankind, which has accumulated two thousand years. In which, the proof of geometry is one of the elites. The proving methods with no uniform methods have been a difficult and key content in mathematics teaching, which depend on the personal inspiration and skills. Using machines to mimic human thinking to help people prove geometric propositions is the dream of some of the outstanding scientists in history, but also has important value of research and application. Wu-method greatly contributes to geometry theorem proving research in the field. Currently, the automated reasoning systems based on different reasoning algorithms has emerged in scientific research and engineering calculations and it plays an important role.However, the rich achievements of the field of automated reasoning in geometry theorem have not been fully applied in education, their educational value is far failed to be fully reflected. The reason is that, on the one hand, the knowledge of geometry in secondary education is elementary compared to mathematics, the given process by existing methods of automated reasoning of geometry is so difficult that students couldn’t understand. On the the other hand, knowledge of geometry teaching involves the expression and construction of geometry, generating geometric problem from given construction, analysis and solving for a problem and other aspects, not just a simple geometric theorem proving. For the application requirements of geometry teaching in high schools, the study of geometry automated reasoning faces the restrictions of the scope of geometry knowledge in secondary schools, the length of working steps, time and reasoning methods. In response to these limitations, this paper carried out the research on automated reasoning about the teaching of geometry in secondary schools, which involves the theory and application of the dynamic geometry construction, generating geometry problem, problem-solving with vector approach and other aspects, the research results and innovation include the following:First:this paper proposes the pivot concept in dynamic geometry construction and the dynamic geometry mechanism based on the pivot idea. Several methods of the dynamic geometric construction based on pivot concept have been designed, which include the manual method of intelligent construction, semantic construction and construction method of the text. The function of dynamic geometric construction in a prototype system has been implemented, and it extends the thoeries of dynamic geometry.Second:the paper proposes and implements automated reasoning algorithms based a vector method. The method is based on the characteristics of the vector loop, which can quickly generate the readable vector-proof of given proposition with the constructed type and intersection class for students, and the proof is simple and readable. This method of automated reasoning can achieve a fixed point, and it shows higher efficiency in a large class of subjects.Third:The paper proposes and implements an automated method of generation and verification for a given geometric proposition based on automated reasoning. The mechanism of multi-kinds of questions and verification based on automated reasoning are constructed. It can generate several kinds of exercises such as filling in the blank, judgement, choose, calculation and proof, which can certificate the problem of real-time answers for users. This provides a solution for generating geometry exercises and improves the efficiency for test.Integrating the application of above research results, an automated geometry reasoning prototype system under constrained conditions has been programmed in this paper. The system is concerned with the limits and methods of the scope of geometry knowledge in high school, its main features include:the dynamic geometry construction, automated reasoning and automated generation of geometric exercises. The organic integration of the three main functions could satisfy the classroom teaching by teachers and self-study courses by students.Finally, a question worthy of further study and future prospects for this direction are concluded.更多还原