Coupling Ontology with Rule-Based Theorem Proving for Knowledge Representation and Reasoning

Theorem proving is an important topic in artificial intelligence. Several methods have already been proposed in this field, especially in geometry theorem proving. Since they belong to algebraic elimination method or artificial intelligence method, it is difficult to use them to express domain knowledge clearly or represent hierarchy of systems. Therefore, we build a loosely coupled system to combine ontology and rule-based reasoning. Firstly, we construct elementary geometry ontology with OWL DL by creating classes, properties and constraints for searching or reasoning in domains. Then we design bidirectional reasoning based on rules and reasoning strategies such as all-connection method, numerical test method, rule classification methods and so on for complex reasoning. The system greatly improves sharing and reusability of domain knowledge and simultaneously implements readable proofs for geometry theorem proving efficiently.