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.
|
Print this page
