Inconsistencies in ontologies

Traditionally, theorem provers have been used to prove theorems with relatively small axiomatisations. The recent development of large ontologies poses a non-trivial challenge of reasoning with axiomatisations consisting of hundreds of thousands axioms. In the near future much larger ontologies will be available. These ontologies will be created by large groups of people and by computer programs and will contain knowledge of varying quality. In the talk we describe an adaptation of the theorem prover Vampire for reasoning with large ontologies using expressive logics. For our experiments we used SUMO and the terrorism ontology. Based on the analysis of inconsistencies found in these ontologies we analyse the quality of information in them. Our research reveals interesting problems in studying the evolution and the quality of formal knowledge. © Springer-Verlag Berlin Heidelberg 2006.