Based On Ontology And Prolog Rules Of Geometry Theorem Proving

With the development of computer technology, artificial intelligence technologyhas made a breakthrough. ATP(Automated Theorem Proving) is an important researchtopic in the field of artificial intelligence. So far there are several methods to solve thisproblem, such as Algebraic method proposed by Mr.Wu, eliminate point algorithm byZhang Jing-zhong, Rule-based theorem proving, etc. They are different from thetraditional methods of geometry theorem proving. How to solve geometry theoremproving in more humane way becomes an important research topic.At the end of20th century, the development of Semantic Web Ontology theoryprovides a new direction to this study. With the study of ontology theory, we have founda geometry theorem proving method. The method uses the ontology model to describethe knowledge of geometrical propositions, and uses Prolog to discribe the geometricdefinition, theorem and axioms. Finally, we complete the geometry theorem proving inthe Inference engine of Knowledge base. To achieve this goal, there are three aspects.1. The research about how to build the ontology model of plane geometry. Basingon the semactic, we find the method of describing the knowlege of geometricalproposition. We use classes, properties, individuals and the relationship between them todescribe the knowlege of geometrical proposition.In this thesis, we use the ontologylanguage OWL DL because it has the ability of logical reasoning and can implementrule-based reasoning.2. The research about geometry theorem proving based on ontology and ontologyrules. Firstly, we use the above method to build ontology model of plane geometry.Secondly, we use Prolog to discribe the geometric theorem. Lastly, we use rules ofProlog to complete the geometry theorem proving in the ontology model of planegeometry.3. The research of buiding the geometic theorem rules in semi-automatic way. Inthis thesis, we get the method of buiding restriction of the geometic theorem rules byin-depth study on the relations of Prolog rules and ontology model of plane geometry. Itcan improve efficiency by using this method and support sustainable theorem proving. In the end, this thesis has two experiments: one is how to generate the theoremrules in semi-automatic way, and the other is how to prove geometric theorem insemi-automatic way. After this, we expound the feasibility of the above theory in theengineering point of view，then analyse the results. Further more, we verify the abovetheory.