Research Of Automated Eometry Reasoning And Its Application With Constrained Conditions

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.