Andrei Voronkov (University of Manchester and Microsoft Research)

The Horizons of Untruth or
How Seemingly Natural Assertions Turn out to be Inconsistent

The first computer programs that can prove mathematical theorems was implemented in 1951. Since then automated reasoning developed into a mature discipline with applications in mathematics, logic, and computer science.

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 (and in the near future hundreds of millions) axioms.

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. We show that the ontologies contain information of varying quality. Most surprisingly, the ontologies turned out to contain many inconsistencies arising from seemingly natural statements.

We discuss the problem of analysing inconsistencies and repairing ontologies from the viewpoints of automated reasoning, logic and philosophy. Our research reveals interesting problems in studying the evolution and the quality of formal knowledge. These problems will be especially interesting to study in the context of hard-to-formalise irrational areas, such as philosophy and religion.