Using a Theorem Prover for Reasoning with Large Ontologies

of theorem provers able to reason with full first-order logic and
even its extensions.

So far, theorem provers have extensively been used for running
experiments over TPTP containing mainly problems with relatively
small axiomatisations. A question arises whether such theorem
provers can be used to reason in real time with large axiomatisations
used in expressive ontologies such as SUMO. We answer this question
affirmatively by showing that a carefully engineered theorem prover
can answer queries to ontologies having over 15,000 first-order
axioms with equality. Ontologies used in our experiments are based
on the language KIF, whose expressive power goes far beyond the
description logic based languages currently used in the Semantic Web.

In the second part of my talk I will analyse some common mistakes
found by our theorem prover in large ontologies based on KIF (SUMO:
Standard Upper Merger Ontology and the Terrorism Ontology). This
part of the talk may be called

How one should not develop ontologies

or

How one should not use first-order logic