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.