Study On Formalization Of Plane Geometry Proposition Text

Machine proof of geometric theorem refers to the principle and method of automatically proving a certain type of geometric theorem or even all theorems of a certain kind of geometry by computer.The typical human-like problem solving method is to realize the automatic solving of geometric propositions through the automatic deductive process based on the given given conditions and the knowledge base of known theorems.In order to accomplish this task,the first problem is how to make the computer understand these given conditions.Based on this problem,this paper studies the formal representation of plane geometry proposition text.The task goal is to convert the geometric proposition text into a specific formal representation.The geometric proof machine can understand the meaning of geometric proposition by reading these formal representations containing geometric entities and geometric relations.The main work of this paper is divided into the following three parts:(1)Study on the formal definition of plane geometry propositions.The geometric entity and geometric relation in plane geometry proposition are defined and its formal definition is given.A total of 26 referable geometric entities and 38 referable geometric relations and their formal definitions are provided in this paper.In order to complete the tasks of geometric entity recognition and geometric relation extraction,this paper constructs small corpora for model training respectively,and provides detailed descriptions of corpus preprocessing methods.(2)Formalized transformation of plane geometry proposition geometric entity.Geometric proposition text is a kind of restricted natural language description,that is,it has certain constraint specification.In this paper,two schemes are adopted to realize the formal representation transformation of geometric entities in proposition text,including matching model scheme and deep learning model scheme.The matching model scheme is to define a number of matching rules to scan the text of geometric propositions,extract the geometric entities that have been successfully matched and then carry out formal transformation.Deep learning model scheme is to use the most classic Bi LSTM-CRF model in NER field for geometric entity recognition.By extracting the predictive tag sequence of the model output,the geometric entity list of the text is obtained,and then the geometric entity identified is further formalized and transformed.(3)Formalized transformation of geometric relation of plane geometry propositions.Due to the complex relationship between geometric entities in the geometric proposition text,a single entity may be shared by multiple relationships.After research and exploration,this paper adopts the joint extraction BERT-Cas Rel model based on parameter sharing in the RE task in the NER field to complete the triplet extraction task of geometric relations.The research focus of this model is to solve the problem of entity relationship nesting.It is applicable to the complex relationship between geometric entities.After the triplet list of the geometric relationship is obtained,the formalization transformation process is completed by the algorithm.Through the above work combined with theoretical research and experiments,this paper shows that it is feasible to convert geometric proposition text into formal representation by using NER and RE technology,and the formal conversion of geometric proposition text can effectively solve the problem of geometric theorem proving machine to understand the proposition text,and play an auxiliary role to a certain extent.