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

Introduction

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.¹

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 competition² (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 Library³ (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).