Exploiting Modularity for Ontology Verification

Within knowledge representation, ontologies are logical theories that support software integration and decision support systems. Ontology verification is concerned with the relationship between the intended structures for an ontology and the models of the axiomatization of the ontology. To verify a particular ontology, we ideally characterize all the models of the ontology up to elementary equivalence and prove that these models are equivalent to the intended structures for the ontology. In this paper, we investigate the use of automated theorem provers and model finders to assist in the interactive verification of first-order ontologies. We identify the reasoning tasks that are associated with different aspects of ontology verification and discuss challenges for the application of automated reasoning systems to support these tasks.