Geometry Theorem Proving on Ontology and Prolog

In this paper, we propose a method to solve the problem of geometry theorem proving based on ontology theory. We describe the process of ontology construction, the reasoning based on ontology and prolog rules, and an example of a geometry theorem proving. The result shows that theorem proving based on ontology is efficient. This approach has advantages such as avoiding determining the problem repeatedly, natural language more closely, expressing the domain knowledge and the concepts hierarchy clearly. In addition this method can execute reasoning of complex relationships, and ultimately accomplishes elementary geometry theorem proving on ontology and prolog rules.