Sigma knowledge engineering environment

Repository	github.com/ontologyportal/sigmakee
Written in	Java
License	GPL-3.0 license
Website	www.ontologyportal.org

In the computer science fields of knowledge engineering and ontology, the Sigma knowledge engineering environment (SigmaKEE) is an open source computer program for the development of formal ontologies. It is designed for use with the Suggested Upper Merged Ontology. It originally included only the Vampire theorem prover as its core deductive inference engine,^[1] but now allows use of many other provers that have participated in the CASC/CADE competitions.^[2]

SigmaKEE is viewed as an integrated development environment for ontologies. The user's typical workflow consists of writing the theory content in a text editor and then debugging it using the SigmaKEE's tools.^[2]

It is written in Java and uses JSP for its web-based user interface. The interface allows the user to make queries and statements in SUO-KIF format and shows proof results with hyperlinks. For each step in the proof, SigmaKEE either points out that it is an assertion in the knowledge base or shows how the step follows from the previous steps using the rules of inference. The interface allows to browse the theory content with hyperlinks and presents hierarchies in a tree-like structure. It also allows to browse WordNet and Open Multilingual WordNet.^[2]

SigmaKEE supports THF, TPTP, SUO-KIF, OWL and Prolog formats and is able to translate theories between these formats. The theorem prover E, which supports TPTP standards for input and output, is integrated into SigmaKEE. It provides the e_ltb_runner control program which runs in an interactive mode. This program receives queries and applies relevance filters. It then runs multiple instances of E which search for an answer to the queries. If one of the instances finds the proof, all other instances are stopped and e_ltb_runner returns the answer to the SigmaKEE's backend.^[2]

• Sigma web site
• TPTP/CADE