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). A large and important subset of SUMO can be expressed in first-order logic with equality. SigmaKEE has integrated different reasoning systems in the past, but they either had to be significantly modified, or integrated in a way that multiple queries to the same theory required expensive full re-processing of the full knowledge base.
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 can be easily upgraded to future versions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Benzmüller, C., Pease, A.: Progress in automating higher-order ontology reasoning. In: Konev, B., Schmidt, R., Schulz, S. (eds.) Workshop on Practical Aspects of Automated Reasoning (PAAR 2010). CEUR Workshop Proceedings, Edinburgh, UK (2010)
Benzmüller, C., Pease, A.: Reasoning with Embedded Formulas and Modalities in SUMO. In: The ECAI 2010 Workshop on Automated Reasoning about Context and Ontology Evolution (August 2010)
Bond, F., Paik, K.: A survey of wordnets and their licenses. In: Proceedings of the 6th Global WordNet Conference (GWC, Matsue, pp, 64–71 (2012)
Fellbaum, C.: WordNet: An Electronic Lexical Database. Language, Speech, and Communication. MIT Press (1998), http://books.google.com.hk/books?id=Rehu8OOzMIMC
Hoder, K., Voronkov, A.: Sine Qua Non for Large Theory Reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 299–314. Springer, Heidelberg (2011)
Niles, I., Pease, A.: Toward a Standard Upper Ontology. In: Welty, C., Smith, B. (eds.) Proceedings of the 2nd International Conference on Formal Ontology in Information Systems, FOIS 2001 (2001)
Pease, A.: Ontology: A Practical Guide. Articulate Software Press, Angwin (2011)
Pease, A., Benzmller, C.: Sigma: An Integrated Development Environment for Logical Theories. AI Comm. 26, 9–97 (2013)
Pease, A., Li, J.: Controlled English to Logic Translation. In: Poli, R., Healy, M., Kameas, A. (eds.) Theory and Applications of Ontology. Springer (2010)
Pease, A., Li, J., Nomorosa, K.: WordNet and SUMO for Sentiment Analysis. In: Proceedings of the 6th International Global Wordnet Conference (GWC 2012), Matsue, Japan (2012)
Pease, A., Rust, G.: Formal Ontology for Media Rights Transactions. In: Garcia, R. (ed.) Semantic Web Methodologies for E-Business Applications. IGI publishing (2008)
Pease, A., Sutcliffe, G.: First Order Reasoning on a Large Ontology. In: Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning on Large Theories, ESARLT (2007)
Pease, A., Sutcliffe, G., Siegel, N., Trac, S.: Large Theory Reasoning with SUMO at CASC. AI Comm. 23(2-3), 137–144 (2010); Special issue on Practical Aspects of Automated Reasoning
Pelletier, F.J., Sutcliffe, G., Suttner, C.: The Development of CASC. AI Communications 15(2), 79–90 (2002)
Riazanov, A., Voronkov, A.: The Design and Implementation of VAMPIRE. Journal of AI Communications 15(2/3), 91–110 (2002)
Schulz, S.: E – A Brainiac Theorem Prover. AI Comm 15(2/3), 111–126 (2002)
Schulz, S.: System Description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013)
Sutcliffe, G., Suttner, C.: The state of CASC. AI Comm 19(1), 35–48 (2006)
Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP Data-Exchange Formats for Automated Theorem Proving Tools. In: Sorge, V., Zhang, W. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems. Frontiers in Artificial Intelligence and Applications, pp. 201–215. IOS Press (2004)
Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP Language for Writing Derivations and Finite Interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 67–81. Springer, Heidelberg (2006)
Sutcliffe, G., Stickel, M., Schulz, S., Urban, J.: Answer Extraction for TPTP, http://www.cs.miami.edu/~tptp/TPTP/Proposals/AnswerExtraction.html (acccessed August 7, 2013)
Trac, S., Sutcliffe, G., Pease, A.: Integration of the TPTPWorld into SigmaKEE. In: Proceedings of IJCAR 2008 Workshop on Practical Aspects of Automated Reasoning (PAAR 2008). CEUR Workshop Proceedings (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Pease, A., Schulz, S. (2014). Knowledge Engineering for Large Ontologies with Sigma KEE 3.0. In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_40
Download citation
DOI: https://doi.org/10.1007/978-3-319-08587-6_40
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08586-9
Online ISBN: 978-3-319-08587-6
eBook Packages: Computer ScienceComputer Science (R0)