document.142

Abstract This system description paper introduces the OWL 2 reasoner HermiT. The reasoner is fully compliant with the OWL 2 Direct Semantics as standardised by the World Wide Web Consortium (W3C). HermiT is based on the hypertableau calculus, and it supports a wide range of standard and novel optimisations that improve the performance of reasoning on real-world ontologies. Apart from the standard OWL 2 reasoning task of entailment checking, HermiT supports several specialised reasoning services such as class and property classification, as well as a range of features outside the OWL 2 standard such as DL-safe rules, SPARQL queries, and description graphs. We discuss the system’s architecture, and we present an overview of the techniques used to support the mentioned reasoning tasks. We further compare the performance of reasoning in HermiT with that of FaCT++ and Pellet—two other popular and widely used OWL 2 reasoners.
1 Introduction In this system description paper we describe the main features of the HermiT ontology reasoner. HermiT supports all features of the OWL 2 ontology language [4], including all OWL 2 datatypes [26], and it correctly performs both object and data property classification—reasoning tasks that are, to the best of our knowledge, not fully supported by any other OWL reasoner. In addition to these standard reasoning tasks, HermiT also supports SPARQL query answering, and it uses a range of optimisations [21] to ensure efficient processing of real-world ontologies. Furthermore, HermiT supports several features that go beyond existing standards, such as DL-safe SWRL rules [15, 29] and description graphs [24]—an extension of OWL 2 that allows for a faithful modelling of arbitrarily connected structures. A key novel idea in HermiT is the hypertableau calculus [30], which allows the reasoner to avoid some of the nondeterministic behaviour exhibited by the tableau calculus used in Pellet [36] and FaCT++ [39]—two other popular and widely used OWL reasoners. In order to further improve the performance of the calculus, HermiT employs a wide range of standard and novel optimisation techniques, including anywhere blocking [30], blocking signature caching [30], individual reuse [25], and core blocking [7]. HermiT also implements a novel classification algorithm [8] that greatly reduces the number of consistency tests needed to compute the class and property hierarchies. We have compared HermiT’s performance with Pellet [36] and FaCT++ [39] on a set of standard ontologies. Unlike many earlier evaluations, all the ontologies used in our tests are directly accessible via immutable URIs, so our tests are fully repeatable and their results are unambiguous. Our results show that, although HermiT did not outperform the other reasoners on all ontologies, it seemed more robust as it managed to process more ‘hard’ ontologies. The rest of this paper is organised as follows: in Section 2 we introduce HermiT’s system architecture; in Section 3 we present an overview of the hypertableau calculus; in Section 4 we discuss several optimisations of the core calculus; in Section 5 we outline the features that go beyond OWL 2 and discuss their support in the reasoner; and in Section 6 we evaluate HermiT’s performance on a wide range of ontologies and compare it to the performance of Pellet and FaCT++. We assume the reader to be familiar with OWL, description logics [12, 22], and the correspondence between the OWL and the description logic syntax [14]. We take an OWL ontology O to consist of a TBox T and an ABox A, where the former specifies the schema (i.e., the axioms that describe the structure of the domain being modelled) and the latter contains the data (i.e., the assertions describing the objects in a domain of discourse). For brevity we will mainly use the standard description logic syntax; however, as HermiT is an OWL reasoner, we will talk about classes and properties, which are commonly called concepts and roles in the description logic community. 2 System Architecture HermiT consists of several components that together implement a sound and complete OWL reasoning system. Figure 1 shows the most important components (e.g., HermiT: An OWL 2 Reasoner 247 Fig. 1 A diagram showing the components of the HermiT reasoner Loading, Classification, etc.) and their main subcomponents. The system has been implemented in Java for portability and easy integration into applications. Users can interact with the reasoner via three different interfaces: a native Java interface, the OWL API [13], and a command line interface. HermiT’s native interface (the Reasoner component) is a facade that converts typical reasoning tasks into ontology consistency tests—the only reasoning operation supported by the hypertableau calculus. For example, to check whether the currently loaded ontology entails the statement that an object property f is functional, the Reasoner component temporarily extends the ontology’s ABox with two object property assertions relating a fresh individual a via the f property with two fresh individuals b and c, and an assertion specifying that b and c are distinct individuals, and then it checks whether such an extended ontology is consistent using the hypertableau calculus; if that is the case, then a model exists proving f to be not functional. The Reasoner component also implements the OWLReasoner interface from the OWL API. This allows HermiT to be used in any application based on the OWL API, and it also allows the Prot´eg´e editor to use HermiT as a plugin. HermiT does not internally use the OWL API data structures to represent ontologies and axioms, so the Reasoner component converts OWL API data structures into HermiT’s internal data structures and back. The command line interface allows users to invoke basic reasoning tasks from the command line. In order to keep the number of command line options manageable, the interface does not expose all of the inferencing capabilities of the reasoner: only common tasks such as ontology classification are supported. The main benefit of the command line interface is that it allows HermiT to be used without any prior setup (e.g., without writing a Java program that invokes the Reasoner component or the OWLReasoner interface). 248 B. Glimm et al. 2.1 Loading an Ontology HermiT internally represents an ontology as a set of (ground) assertions A and a set of DL-clauses C. A DL-clause is an implication of the form B1 ∧ ... ∧ Bn → H1 ∨ ... ∨ Hm (1) where each Bi and Hi are atoms constructed using the classes and properties from the ontology; see Section 3 for more detail. A DL-clause straightforwardly corresponds to a first-order implication. The Reasoner component is given an OWL ontology, and then the Loading component constructs the set O of all axioms contained in the given and all directly and indirectly imported ontologies,1 and converts O into the sets A and C. Towards this goal, the Normaliser component first simplifies complex axioms (e.g., by removing duplicate or irrelevant conjuncts or disjuncts) and then converts the result into a particular normal form; the normalisation step can be seen as a variant of the well-known structural transformation [31, 32]. For example, the complex superclass in the axiom Person  ∀hasAncestor.(Male  Female) (2) is normalised so that only a fresh class Q occurs inside the quantifier, and the meaning of Q is captured in a separate axiom; more precisely, the above axiom is transformed into the following two axioms: Person  ∀hasAncestor.Q (3) Q  Male  Female (4) ABox assertions are subjected to the same transformation so, after normalisation, the ABox contains only classes and properties, rather than class expressions and property expressions. Moreover, if present in the input ontology, SWRL rules are normalised along the same lines. OWL supports transitive object properties and property chain axioms; however, these features are not handled directly by the hypertableau calculus as this would make it difficult to ensure termination of the calculus. Instead, the Role Chain Encoder component transforms away transitivity and property chain axioms by introducing additional axioms that ensure equisatisfiability between the original and the transformed ontologies; this transformation is realised using an automata-based technique [16, 23]. The Role Chain Encoder component also introduces axioms encoding the semantics of the the universal object property (i.e., owl:topObjectProperty) if needed (i.e., if it occurs in the ontology). The resulting axioms are finally converted directly into DL-clauses. For example, the normalised axioms (3) and (4) are translated into the following DL-clauses: Person(x) ∧ hasAncestor(x,y) → Q(y) (5) Q(x) → Male(x) ∨ Female(x) (6) 1OWL ontologies can include references to other ontologies that are to be ‘imported’ (syntactically added) into the current ontology [28]. HermiT: An OWL 2 Reasoner 249 The ontology expressivity (e.g., whether the ontology contains inverse properties or nominals) is also determined during the loading step, and this information is subsequently used to automatically configure certain options that parameterise the hypertableau calculus. 2.2 Reasoning-Related Components As already mentioned, all reasoning tasks are transformed into one or more ontology consistency tests, whose goal is to determine the consistency of the currently loaded sets of assertions A and DL-clauses C. For certain reasoning tasks (e.g., to determine subsumption between complex class expressions), it might be necessary to extend A and C with temporary assertions and DL-clauses that are needed only for this single reasoning task. The satisfiability of A and C is decided using the hypertableau calculus [30], which tries to construct a pre-model—a finite set of (ground) assertions that describe a (possibly infinite) model satisfying A and C. The Reasoning component implements the hypertableau calculus, and we discuss both the calculus and its implementation in more detail in Section 3. The Classification component uses the Reasoning component to compute class and property hierarchies—that is, to arrange all classes, object properties, and data properties occurring in the ontology into hierarchies that correctly reflect the relevant subsumption relationships. To classify classes, HermiT uses a novel algorithm [8] that extracts information from the constructed pre-models in order to reduce the number of subsumption tests performed. To the best of our knowledge, all reasoners apart from HermiT classify object and data properties by simply computing the reflexive–transitive closure of the asserted property inclusion axioms, which is known to be incomplete (for both object and data properties) even in very simple ontology languages [8]. In contrast, HermiT reduces property classification to class classification [8], and so it is the only reasoner that is guaranteed to be complete for object and data property classification. The Realisation component uses the Reasoning component to compute the set of instances for each class and property in the ontology. Similarly to classification, HermiT optimises this computation by exploiting pre-models constructed during each consistency test. In its default mode, HermiT supports lazy realisation, where known and possible instances of classes are initialised during an initial ontology consistency test, and refined during subsequent query answering. One can, however, also explicitly request a complete computation of the instances of all classes and properties.