Research On Plane Geometry Automatic Reasoning System And Auxiliary Point Addition

Machine proof of geometric theorems is a mechanized method to complete the proof of mathematical geometric propositions by using computers.In 1977,the mathematical mechanization method(Wu's method)established by Wu Wenjun greatly promoted the research of machine proof of geometric theorems,and after 40 years of development,the readable machine proof of geometric theorems has made great progress,such as the readable machine proof of geometric theorems established by Zhang Jingzhong et al.Adding the auxiliary point has always been a difficult point in plane geometry solution,which often requires rich mathematical intuition and experience and is difficult to regularize,so there is still no widespread and effective automatic method for adding auxiliary quantities,which seriously limits the computer's ability to solve problems.How to make the computer add an auxiliary point to solve problems according to experience has become one of the important topics in the research of automatic reasoning in plane geometry.This paper implements an automatic reasoning system for plane geometry that supports adding an auxiliary point,aiming to solve more complex geometric problems to improve the solution success rate and reasoning efficiency of the system.The main contents include: 1)Exploring the basic concepts of plane geometry as well as related classical problem types and common methods of adding auxiliary points,and determining the representation of predicates and rules of the inference system;2)The system is developed using the forward projection method.In order to avoid the system's knowledge base from depositing duplicate knowledge,this paper uses a hashing algorithm for knowledge comparison to achieve a efficient and visual plane geometry automatic reasoning system;3)Firstly,this paper constructs a dataset containing 1000 plane geometry problems that need to be solved by adding auxiliary points.Secondly,this papers preprocess the data for the problem information,and then selects different classification models to train the dataset.Finally,this paper compares the classification effects of different models and selects the Fast Text model to obtain the recommended auxiliary point types.This paper uses the implemented automatic reasoning system for plane geometry to validate the recommended auxiliary point.The experimental results show that the planar geometry reasoning system supporting the addition of the auxiliary point implemented in this paper solves 70 selected planar geometry problems,and the comprehensive solution rate increases from 11.4% to 51.4%,which improves the success rate of solving complex planar geometry problems that require the addition of the auxiliary point.