Adimen-SUMO: Reengineering an Ontology for First-Order Reasoning

Adimen-SUMO: Reengineering an Ontology for First-Order Reasoning

Javier Àlvez (Department of Languages and Information Systems, University of the Basque Country, Donostia, Gipuzkoa, Spain), Paqui Lucio (Department of Languages and Information Systems, University of the Basque Country, Donostia, Gipuzkoa, Spain) and German Rigau (Department of Languages and Information Systems, University of the Basque Country, Donostia, Gipuzkoa, Spain)
Copyright: © 2012 |Pages: 37
DOI: 10.4018/jswis.2012100105
OnDemand PDF Download:
No Current Special Offers


In this paper, the authors present Adimen-SUMO, an operational ontology to be used by first-order theorem provers in intelligent systems that require sophisticated reasoning capabilities (e.g. Natural Language Processing, Knowledge Engineering, Semantic Web infrastructure, etc.). Adimen-SUMO has been obtained by automatically translating around 88% of the original axioms of SUMO (Suggested Upper Merged Ontology). Their main interest is to present in a practical way the advantages of using first-order theorem provers during the design and development of first-order ontologies. First-order theorem provers are applied as inference engines for reengineering a large and complex ontology in order to allow for formal reasoning. In particular, the authors’ study focuses on providing first-order reasoning support to SUMO. During the process, they detect, explain and repair several important design flaws and problems of the SUMO axiomatization. As a by-product, they also provide general design decisions and good practices for creating operational first-order ontologies of any kind.
Article Preview


Recently, the Semantic Web community has become very interested in having practical inference engines for ontological reasoning (Chandrasekaran, Josephson, & Benjamins, 1999, Noy & McGuinness, 2001, Staab & Studer, 2009, d’Aquin & Noy, 2012). A well-known necessary condition for enabling the automated treatment of knowledge – in particular, automated reasoning with ontologies – is that ontologies must be written in a formal language whose syntax and semantics are both formally defined. Automated reasoning uses mechanical procedures to obtain a large body of deducible knowledge that can be inferred from a compact modelling.1

A significant feature of interest for formal ontologies is expressiveness. Since an ontology is a conceptualization of a certain domain of interest, the language should allow to express the properties that characterize that domain (Gruber, 2009). It is also well-known that the expressive power of the underlying logic jeopardizes the computational tractability and the inherent complexity of logical reasoning. Indeed, very expressive logics are undecidable or semi-decidable with high worst-case complexity. Beyond undecidability, a highly expressive logic language may be incomplete, i.e. there is no finite proof system that will prove all entailed sentences in the logic. As a consequence, the trade-off between expressiveness and reasoning efficiency (even decidability) is a key point for the design of formal ontologies.

Today, the family of Web Ontology Languages, including OWL-DL (Horrocks & Patel-Schneider, 2004), is the most common formal knowledge representation formalism, being accepted and standardized by the W3C (World Wide Web Consortium). OWL-DL is a powerful knowledge representation formalism with high computational efficiency and theoretically founded in description logics (DL), which can be embedded into fragments of first-order logic. Additionally, pure DLs are subsets of the guarded fragment (GF) of first-order logic, defined through the relativisation of quantifiers by atomic formulas. The guarded fragment was introduced in Andréka, Németi, and van Benthem (1998), where the authors prove that the satisfiability problem for GF is decidable. Indeed, OWL-DL reasoners, such as Pellet (Sirin, Parsia, Grau, Kalyanpur, & Katz, 2007) or Fact++ (Tsarkov & Horrocks, 2006), implement very efficient decision algorithms for OWL-DL theories (Motik, Shearer, & Horrocks, 2009). However, OWL-DL decidability is achieved at the price of losing expressiveness. Thus, state-of-the-art OWL-DL reasoners are unable to cope with more expressive ontologies such as Cyc (Matuszek, Cabral, Witbrock, & DeOliveira, 2006), DOLCE (Gangemi, Guarino, Masolo, Oltramari, & Schneider, 2002) or SUMO (Niles & Pease, 2001b).

Likewise, first-order logic (FOL) is a very well-known and expressive formalism, although reasoning in FOL is undecidable. Lately, impressive progress has been made in first-order (FO) automated reasoning. Every year, the CASC competition2 (Pelletier, Sutcliffe, & Suttner, 2002, Sutcliffe & Suttner, 2006) evaluates the performance of sound, fully automatic, classical FO automated theorem provers (ATP) on a bounded number of eligible problems, chosen from the TPTP Problem Library3 (Sutcliffe, 2009). As a result, there exists an important collection of FO theorem provers, such as Vampire (Riazanov & Voronkov, 2002) and E-Prover (Schulz, 2002).

Complete Article List

Search this Journal:
Open Access Articles
Volume 18: 4 Issues (2022): Forthcoming, Available for Pre-Order
Volume 17: 4 Issues (2021): 2 Released, 2 Forthcoming
Volume 16: 4 Issues (2020)
Volume 15: 4 Issues (2019)
Volume 14: 4 Issues (2018)
Volume 13: 4 Issues (2017)
Volume 12: 4 Issues (2016)
Volume 11: 4 Issues (2015)
Volume 10: 4 Issues (2014)
Volume 9: 4 Issues (2013)
Volume 8: 4 Issues (2012)
Volume 7: 4 Issues (2011)
Volume 6: 4 Issues (2010)
Volume 5: 4 Issues (2009)
Volume 4: 4 Issues (2008)
Volume 3: 4 Issues (2007)
Volume 2: 4 Issues (2006)
Volume 1: 4 Issues (2005)
View Complete Journal Contents Listing