Research And Application Of Geometry Automatic Reasoning Based On Semantic WEB

Automated reasoning of geometry refers to the proof of geometrical with the aid of computer simulate human brain. It is an important research topic in the field of artificial intelligence. In the1970s, Mr. Wu Wen_jun proposed the method of Automated Theorem Proving. Then, academician Zhang Jing_zhong proposed Eliminate Point Algorithm on the basis of Area Algorithm. These methods make breakthroughs in the study of automated reasoning. However, judging from the current reasoning software, there are still some problems. For example: they are different from the traditional methods of geometry theorem proving, they will not be use the Problem‐solving skills which grasped by geometrits, such as adding auxiliary line and auxiliary point.How to design the method which not can only guarantee the efficiency but also can solve the above problems becomes an important research topic. In order to realize the automated reasoning, related theory and technology of semantic web is introduced. First, the geometric proof and inference rules are described through the ontology. Then, automated reasoning is implemented through model matching and supplementary information querying. To achieve this goal, there are some major aspects are shown as follow:Plane geometry knowledge representation: first, on the basis of analysis of theproof process, the general models and detailed models are extracted from every causalsegment of the process automatically. The general model reflects abstraction of thesegment, the detailed model reflects Instantiation of the segment. Then, on the basis ofanalysis of the inference rules, the elementary geometry ontology is constructed byProtégé which could deal with the problems of auxiliary line and auxiliary point.Plane geometry knowledge reasoning: for those geometrical proofs which do notneed to add auxiliary line or auxiliary point, in order to improve efficiency, first, thisthesis matches with the general model by backward reasoning. If the solution may exist,then, this thesis matches with the detailed model by forward reasoning. For thosegeometrical proofs which need to add auxiliary line or auxiliary point, this thesis gets the new condition through querying the auxiliary database. This way can help usincrease the success ratio of reasoning. In order to improve efficiency, for auxiliary line,this thesis stores new conditions which come from non-segment. For auxiliary point,this thesis designs the algorithm according to the problem solving experience and usesstrategy which increases while deletes.In the end, this thesis uses some experiments to show the construction of processontology and process ontology firstly. Then, this thesis makes use of those ontology toautomated reasoning examples which need to add auxiliary line or auxiliary point. Theexperimental result has indicated the feasibility of above method.