Knowledge Engineering for Large Ontologies with Sigma KEE 3.0

ABSTRACT. The Suggested Upper Merged Ontology (SUMO) is a large, comprehensive ontology stated in higher-order logic. It has co-evolved with a development environment called the Sigma Knowledge Engineering Environment (SigmaKEE). SUMO has been applied to commercial applications in concept extraction and metadata verification. A large and important subset of SUMO can be expressed in first-order logic with equality. To support the knowledge engineer, SigmaKEE has, over time integrated different reasoning systems, either via special modifications to the reasoner or in an ad-hoc manner that requires full re-processing of the full knowledge base for even trivial queries.

To overcome this problem, to create a simpler system configuration that is easier for users to install and manage, and to integrate a state-of-the-art theorem prover we have now integrated Sigma with the E theorem prover. The E distribution includes a simple server version that loads and indexes the full knowledge base, and supports interactive queries via a simple interface based on text streams. No special modifications to E were necessary for the integration, so SigmaKEE have an easy upgrade path to future versions.