51 Computing ALCH-Subsumption Modules Using Uniform Interpolation Patrick Koopmann1 and Jieying Chen2 1 Institute of Theoretical Comp. Science, Technische Universität Dresden, Germany patrick.koopmann@tu-dresden.de 2 LRI, Univ. Paris-Sud, CNRS, Université Paris-Saclay, Orsay, France jieying.chen@lri.fr Abstract. We investigate how minimal subsumption modules can be ex- tracted using methods for uniform interpolation and forgetting. Given an ontology and a signature of concept and role names, a subsumption mod- ule is a subset of the ontology that preserves all logical entailments that can be expressed in the description logic of the ontology using only terms in the specified signature. As such, they are useful for ontology reuse and ontology analysis. While there exists a range of methods for computing or approximating minimal modules for a range of module types, we are not aware of a practical, implemented method for computing minimal subsumption modules in description logics beyond ELH. In this paper, we present a method that uses uniform interpolation/forgetting to com- pute subsumption modules in ALCH, and which under certain condi- tions guarantees minimality of the extracted modules. As a side prod- uct, our method computes a so-called LK subsumption module, which over-approximates the union of all minimal subsumption modules, and as such may already have applications of its own. We further present an initial evaluation of this method on a varied corpus of ontologies. 1 Introduction Description Logics [1] (DLs) are a well-investigated family of logics that are commonly used to describe terminological knowledge in form of ontologies. Ap- plications in areas such as medicine, biology and the semantic web have lead to the development of very large ontologies that, with growing size, become harder to understand and maintain. Due to the complexity of existing ontologies, there are areas where it is useful to extract a subset of the ontology, a so-called module, based on a set of terms of interest. For example, when developing a new ontology for a specialised application, one may want to reuse knowledge from an existing ontology. If this ontology covers a large domain of concepts, not all information in it will be relevant for the application at hand, so that it makes sense to first extract a module of the ontology that is sufficient for the application. Secondly, for maintaining an existing ontology it may be important for an ontology engi- neer to understand which axioms in the ontology are responsible for which of its logical entailments. Modules give the engineer an overview on the axioms of Copyright c 2017 by the paper’s authors In: P. Koopmann, S. Rudolph, R. Schmidt, C. Wernhard (eds.): SOQE 2017 – Pro- ceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics, Dresden, Germany, December 6–8, 2017, published at http://ceur-ws.org. 52 the ontology that contribute to any entailment over a selected set of terms. This allows him to browse the ontology in a more directed manner guided by the terms he is interested in. In the mentioned applications, it is usually desirable to extract a module that is optimal in some sense, for example minimal w.r.t. set inclusion. There are a range of different notions and properties for modules that have been defined in the literature, and correspondingly a range of methods for mod- ule extraction have been developed [2,8]. For some of those notions, such as semantic modules, deciding whether a subset of the ontology is a module that is minimal w.r.t. set inclusion is undecidable already for ontologies formulated in the lightweight DL EL [13]. In this paper, however, we consider a notion for which computing a minimal module is decidable. More precisely, we are interested in computing minimal subsumption modules, which are modules that preserve all logical entailments in the form of concept inclusions over the specified signa- ture of terms.While a method for computing minimal subsumption modules in acyclic EL ontologies has been presented in [4], in this paper we focus on the more expressive DL ALCH. Already for ALC ontologies, deciding whether a subset of the ontology is a subsumption module, is known to be 2ExpTime- complete [6], but we are not aware of a practical implementation for extracting minimal subsumption modules in DLs that are more expressive than ELH [3]. The core idea of our method is to use uniform interpolation [22] to compute a finite representation of the entailments the module has to preserve, together with techniques from axiom-pinpointing [28]. The method can compute small subsumption modules of ALCH-ontologies for signatures that contain all role symbols, which under certain conditions guarantees minimality of the computed modules. As a side-product, the method computes a lean kernel (LK) subsump- tion module, an over-approximation of all minimal subsumption modules, which, as our evaluation indicates, is computationally cheaper to compute and usually not much larger than the minimal subsumption module. Moreover, we believe LK subsumption modules may have applications on its own: if subsumption mod- ules are used by ontology engineers to investigate information with respect to certain signatures, it might be useful to have an overview of all the axioms that contribute to this information: this overview is provided, if over-approximated, by the LK subsumption module. Our method only supports signatures that contain all role names, while arbi- trary signatures are left for future work. Modules for this type of signatures have a property that makes them especially useful for ontology reuse. Specifically, as we show, modules for signatures that include all role names provide for a weak form of robustness under replacement [12]. The paper is structured as follows. We first recall related work on module extraction and uniform interpolation in Section 2, and give the preliminaries on ALCH, subsumption modules and uniform interpolation in Section 3. We then describe our core algorithm for computing subsumption modules based on axiom pin-pointing in Section 4. A central idea for reducing the number of entailment checks is to use a technique to quickly compute uniform interpolants for differ- 53 ent subsets of the input ontology, for which we compute an annotated uniform interpolant defined in Section 5. As a by-product, the annotated uniform inter- polant encodes an upper approximation of the minimal subsumption module, which indeed over-approximates all minimal subsumption modules. We call this module lean kernel subsumption module, as they are similar to lean kernels in axiom pinpointing, which we discuss in more detail in Section 6. Finally, we give results from an initial evaluation in Section 7 and conclude with a discussion in Section 8. 2 Related Work There is a range of types and properties of modules that have been investigated in the literature, surveys of which can be found in [12] and [2]. Usually, mod- ules are computed on the basis of an ontology and a signature Σ, i.e. a set of concept and role names, and preserve certain properties of the ontology with re- spect to that signature Σ. Examples include semantic modules, which preserve all models of the ontology when restricted to Σ [13] and subsumption modules, which preserve all logical entailments in the form of concept inclusions over Σ that can be expressed in the description logic under consideration [4,3]. Apart from minimality under set inclusion, additional properties have been considered such as self-containedness (the module is also a module with respect to its own signature) and depletedness (the remaining ontology only entails tautologies in the specified signature, i.e. all relevant information is in the module). Deciding whether a subset of the ontology is a semantic module for a signature is un- decidable already for EL-ontologies [13], and consequently minimal (depleting, self-contained) semantic modules can only be approximated in practice. For EL and ALCI, an exception are modules of acyclic ontologies and for signatures that contain only concept names, for which methods to extract depleting mod- ules have been implemented in the tool MEX [13]. A well-known approximation of semantic modules are locality-based modules, of which syntactical variants, such as >⊥∗-modules, can be computed very cheaply [8,14]. However, locality- based modules may still contain a large portion of the original ontology [27]. A more refined technique for extracting semantic modules is presented in [5], which computes lower and upper approximations of minimal depleting mod- ules in ALCQI using QBF-reasoning. Depending on the application, modules that only preserve entailments in a certain query-language may be sufficient. A method that approximates minimal modules taylored towards specific query languages uses datalog reasoning and has been presented in [26]. For computing minimal subsumption modules of ELH-terminologies, a method has been presented in [3]. An alternative approach is presented in [4], which uses a black-box search algorithm that detects axioms that can be safely removed without causing a logical difference, i.e. a difference in the set of entailed con- cept inclusions over the selected signature. For computing logical differences, the authors use the tool CEX [11], whose latest version supports the computation of logical differences between ELHr -ontologies [21]. However, in principle, the 54 same algorithm could be used for ontologies formulated in any logic for which a tool for computing logical differences exists. We tried this for ALCH ontologies, deploying the tool Lethe [17] that allows for computing logical differences in ALCH for arbitrary signatures, provided a uniform interpolant exists for them. However, we found that this approach is too computationally expensive in prac- tice. A notion strongly related to that of subsumption modules is that of uniform interpolants, which are also computed as part of our method. Both subsumption modules and uniform interpolants preserve all logical entailments in the speci- fied signature that can be expressed in the respective description logic. However, while subsumption modules are subsets of the input ontology, uniform inter- polants are themselves completely formulated in the specified signature, and may therefore contain axioms that do not occur in the original ontology. In fact, in the worst case, already for the description logics EL and ALC, the uniform interpolant may have a size that is triple exponential in the size of the input ontology [23,22]. Despite this discouraging theoretical result, various practical methods for computing uniform interpolants in expressive description logics have been developed [20,16,18,31]. In fact, it turns out that in practice, uniform in- terpolants are often of moderate size. 3 Preliminaries We recall the description logic ALCH [1], as well as the notions of subsumption modules and uniform interpolants. Let Nc and Nr be two disjoint, countably infinite, sets of respectively concept names and role names. A signature Σ ⊆ Nc ∪ Nr is a finite set of concept names and role names. The set of concepts C, D, TBox axioms α and RBox axioms β the set of ALCH-inclusions α are built according to the following grammar rules: C ::= > | ⊥ | A | ¬C | C u C | C t C | ∃r.C | ∀r.C α ::= C v C | C ≡ C β ::= r v s | r ≡ s where A ∈ Nc and r ∈ Nr . A TBox is a finite set of TBox axioms, an RBox a finite set of RBox axioms, and an ontology is the union of a TBox and RBox. The semantics of ALCH is defined using interpretations I = (∆I , ·I ), where the domain ∆I is a non-empty set, and ·I is a function assigning each concept name A to a subset AI of ∆I and every role name r to a binary relation rI over ∆I . Then ·I is inductively extended to complex concepts by: (>)I := ∆I , (⊥)I := ∅, (¬C)I := ∆I \C I , (C u D)I := C I ∩ DI , (C t D)I := C I ∪ DI , (∃r.C)I := {x ∈ ∆I | ∃y ∈ C I : (x, y) ∈ rI }, and (∀r.C)I := {x ∈ ∆I | ∀(x, y) ∈ rI : y ∈ C I }. An interpretation I satisfies a TBox axiom C v D (C ≡ D) iff C I ⊆ DI (C I = DI ). It satisfies an RBox axiom r v s (r v s) iff rI ⊆ sI (rI = sI ). 55 We write I |= α if I satisfies the axiom α. An interpretation I is a model of an ontology O if I satisfies all axioms in O. An axiom α is entailed by O, written O |= α, if for all models I of O, we have that I |= α. A signature is a (countable but possibly infinite) set Σ ⊆ Nr ∪ Nc of concept and role names. Given a concept/axiom/ontology α, we denote by sig(α) the set of concept and role names occuring in α. Definition 1 (Σ-Inseparability, Subsumption Module, Uniform Inter- polant.). Let O1 and O2 be two ALCH-ontologies, and let Σ be a signature. Then O1 and O2 are Σ-inseparable, denoted as O1 ≡Σ O2 , iff for every axiom α s.t. sig(α) ⊆ Σ, we have O1 |= α iff O2 |= α. A Σ-subsumption module of O is an ontology M s.t. O ≡Σ M and M ⊆ O. M is minimal iff there exists no Σ-subsumption module M0 of O s.t. M0 ( M. A uniform interpolant of O for Σ is an ontology OΣ s.t. O ≡Σ OΣ and sig(OΣ ) ⊆ Σ. 4 Minimal Subsumption Modules as Justifications A related problem to minimal subsumption module extraction is that of com- puting justifications [28]. Given an ontology O and an axiom α that is entailed by O, a justification for α in O is a subset J of O s.t. J is minimal w.r.t. ( and J |= α. We can generalise this notion to justifications of ontologies O0 by asking for minimal subsets J ⊆ O s.t. J |= O0 . One easily sees that every min- imal subsumption module is a justification of a uniform interpolant: for a given ontology O and signature Σ, a uniform interpolant OΣ captures all entailments of O that are in Σ, and therefore, any subset of O that entails OΣ entails all axioms that are in Σ. Therefore, one possible approach for computing minimal subsumption modules is to first compute a uniform interpolant, and then com- pute a justification for it using any DL reasoner that supports this. As there are implemented systems for both for uniform interpolation (e.g. [20,17,31]), and for computing justifications (reasoners such as HermiT [7], JFact [30] and Pellet [29] support this directly via the OWL API [9]), it seems that such a method could be implemented without much effort. However, there are two short-comings of this approach. First, it is well-known that uniform interpolants do not always exists for any pair of ontology and sig- nature. For this reason, existing methods for uniform interpolation either only compute approximations of the uniform interpolant, or they compute a uniform interpolant in an extended language that uses greatest fixpoint operators. Un- fortunately, we are not aware of any reasoner that supports fixpoint operators, so that the method can only be applied for ontology-signature pairs for which there exist a uniform interpolant without fixpoint operators. Secondly, in first experiments of this idea we quickly found out that reasoners such as HermiT, Pellet and JFact struggle with the computation of justifications for large en- tailments such as uniform interpolants. While in this paper, we offer no general solution for the case in which there is no uniform interpolant without fixpoints, 56 to overcome the more practical problem of computing justifications for uniform interpolants without fixpoint operators, we developed a more refined approach based on ideas for computing justifications. Given an ontology O1 and a set of entailed axioms O2 , such as a uniform interpolant, we can compute a justification for O2 in O1 using the following algorithm A1. 1. Input: ontology O1 , entailed set of axioms O2 2. For each α ∈ O1 : (a) Set O10 = O1 \ {α} (b) If O10 |= O2 , set O1 = O10 3. Return O1 If in Step 2b), we test entailment of O2 by checking one axiom after the other, this algorithm has to perform a quadratic number of entailment tests, namely one for each pair (α, β) of axioms α ∈ O1 and β ∈ O2 . However, if O1 and O2 overlap syntactically, this number of tests can be reduced, as we do not need to call a reasoner for axioms that are already in O1 . Unfortunately, if O2 is a uniform interpolant of O1 for Σ, it only contains axioms in Σ, and is therefore unlikely to syntactically overlap with O1 , especially if Σ is significantly smaller than the signature of O1 . To overcome this problem, we propose the following algorithm A2, which checks for entailment of the uniform interpolant by another uniform interpolant. 1. Input: Ontology O, signature Σ 2. Initialise Om to the >⊥∗-module of O for Σ 3. Compute the uniform interpolant OΣ of Om for Σ 4. For each β ∈ Om : (a) Compute the uniform interpolant O2Σ of Om \ {β} for Σ (b) Set Od = OΣ \ O2Σ (c) If O2Σ |= Od , set Om = Om \ {β} 5. Return Om Of course, the improvement of this method relies on the shape of the uniform interpolants we compute: in general, OΣ and O2Σ may not overlap at all, so that Od may have the same size as OΣ . However, as our experiments confirmed, if the uniform interpolants are computed wisely, in the algorithm above Od is usually significantly smaller than O2Σ , and in fact often contains only a single axiom. Therefore, the algorithm is expected to require a much smaller number of entailment checks than A1. However, we now need to compute a uniform interpolant in every iteration, which usually is a much more expensive operation than testing for entailment of axioms. Luckily, as it turns out, for signatures Σ s.t. Nr ⊆ Σ, we can compute the required uniform interpolants very efficiently if we compute an annotated uniform interpolant first, from which all required uniform interpolants can then be obtained by simple replacement operations. 57 5 Annotated Uniform Interpolants In the following, for simplicity, let O be the input ontology of our method. Let Na ⊆ Nc be a special set of concept names called annotation concepts, which we assume to be disjoint from the signature of O, and let A : O → Nc be a bijective function that maps each axiom in O to an annotation concept. To improve readability, we write A(α) as Aα . Note that in ALCH, every TBox axiom is equivalent to a set of TBox axioms of the form C v D. Given a TBox axiom α, we denote by gci(α) the set of GCIs that is equivalent to α. Definition 2. Given an axiom α, the annotation αa of α is defined as {C v D t Aα | C v D ∈ gci(α)}. Given an ontology O, the annotation Oa of O is the union of all annotations of axioms in O. Given a signature Σ, a annotated uniform interpolant of O for Σ is a uniform interpolant OaΣ of the annotation of O for the signature Σ ∪ {Aα | α ∈ O}. Note that the annotation Oa of an ontology O is usually not a conservative extension. Specifically, Oa 6|= C v D may not hold even for C v D ∈ O, due to the added disjuncts. Instead, all non-tautological entailments now involve annotation concepts that refer to the axioms that have been used to infer the axiom. The idea of the annotation concepts is to track which axioms contributed to computing a uniform interpolant. This way, we can easily obtain a uniform interpolant of any subset of the original ontology. Specifically, given an anno- tated uniform interpolant of O for Σ, where Nr ⊆ Σ, we can obtain uniform interpolants for Σ of any subset O0 of O as follows: we replace every annotation concept Aα s.t. α ∈ O0 by ⊥, and every remaining annotation concept by >. Example 1. Consider the following ontology O. ∃r.> v A t B A ≡ ∃r.B The following ontology is a uniform interpolant of O for Σ = {A, r}. A v ∃r.> ∃r.(∃r.> u ¬A) v A To track which axioms contributed to the uniform interpolant, we compute the annotated uniform interpolant. For this, we first compute the annotation of O, which is the following. ∃r.> v A t B t A∃r.>vAtB A v ∃r.B t AA≡∃r.B ∃r.B v A t AA≡∃r.B 58 By interpolating the annotation of O, we obtain the following annotated uniform interpolant of O for Σ. A v ∃r.> t AA≡∃r.B ∃r.(∃r.> u ¬A u ¬A∃r.>vAtB ) v A t AA≡∃r.B The annotation concepts mark which parts of the uniform interpolant where influenced by which axiom. If we replace every annotation concept by ⊥, we obtain a uniform interpolant of O again. If instead, we replace AA≡∃r.B by ⊥ and A∃r.>vAtB by >, we obtain the following uniform interpolant of A ≡ ∃r.B: A v ∃r.> t ⊥ ∃r.(∃r.> u ¬A u ¬>) v A t ⊥, which can be simplified to {A v ∃r.>}, as the second axiom is tautological. In a same way, we obtain that a uniform interpolant of ∃r.> v A t B is {⊥ v >}. This technique however only works for signatures that contain all role sym- bols of the original ontology. The following lemma, which can be shown by inspection of the uniform interpolation method presented in [15], provides the central property of uniform interpolants which make our technique possible. Lemma 1. Let O be an ontology and Σ a signature s.t. Nr ⊆ Σ. Let O1 ⊆ O be such that sig(O1 ) = Σ and O1 contains no RBox axioms, and let O2 = O \ O1 . Further, let O2Σ be a uniform interpolant of O2 for Σ. Then, O1 ∪ O2Σ is a uniform interpolant of O for Σ. As a corollary of this lemma, we obtain the robustness property of subsump- tion modules for signatures Σ s.t. Nr ⊆ Σ which was claimed in the introduction, and which can equivalently be proved based on a corresponding result for ALC from [12]. Corollary 1 (Weak robustness under replacement). Let O be an ontology, Σ a signature s.t. Nr ⊆ Σ, and M be a Σ-subsumption module for O. Let O0 be an ontology s.t. sig(O0 )∩sig(O) ⊆ Σ and O0 contains no RBox axioms containing role names from O. Then, for any axiom α s.t. sig(α) ⊆ sig(O0 ) ∪ Σ, we have O ∪ O0 |= α iff M ∪ O0 |= α. We can now show that uniform interpolants of subsets of the original ontol- ogy can indeed be computed using the replacement operations described earlier. (Recall that annotated uniform interpolants are defined as uniform interpolants of the annotated ontology, for the given signature extended by annotation con- cepts.) Theorem 1. Let O be an ontology, Σ a signature s.t. Nr ⊆ Σ, and OaΣ an annotated uniform interpolant of O for Σ. Let O1 ⊆ O. Then, the ontology O1Σ = OaΣ [Aα 7→ ⊥ | α ∈ O1 ][Aα 7→ > | α ∈ O \ O1 ] is a uniform interpolant of O1 for Σ. 59 Proof. Let O, Σ, OaΣ and O1 be as in the lemma. Let Oa be the annotation of O, and extend Oa to following ontology O2 . Oa ∪ {Aα ≡ ⊥ | α ∈ O1 } ∪ {Aα ≡ > | Aα ∈ O \ O1 } By looking at the way axioms are annotated, one easily establishes that the uniform interpolant of O2 for sig(O) is equivalent to O1 . Also, one easily sees that this uniform interpolant is simply obtained by replacing every annotation concept Aα s.t. α ∈ O by ⊥, and every annotation concept Aα s.t. Aα ∈ O \ O1 by >. Since uniform interpolation is commutative, we can obtain a uniform interpolant of O1 for Σ, starting from O2 , in two ways. Either we first compute O1 as uniform interpolant of O2 , and compute then the uniform interpolant of O1 for Σ. Or we first compute the uniform interpolant of O2 for Σ ∪Na , of which we then compute the uniform interpolant for Σ. As observed earlier, this last step is simply performed by replacing annotation concepts by ⊥ respectively >. By Lemma 1, the uniform interpolant of O2 is equivalent to the uniform interpolant of Oa —the annotated uniform interpolant—together with the additional axioms in O2 , which means, these axioms are only involved in computing the second uniform interpolant. Therefore, we obtain the same ontology if we first compute the annotated uniform interpolant of O, and then perform the substitution on the annotated uniform interpolant. t u 6 LK Subsumption Modules Theorem 1 allows us to apply Algorithm A2 without having to use an expensive uniform interpolation method in each step. Another consequence of Theorem 1 is that, if we take the axioms associated with the set of annotation concepts occurring in the annotated uniform interpolant, we obtain a set of axioms that contains all minimal subsumption modules. This module is not necessarily equal to the union of all minimal subsumption modules, since the annotated uniform interpolant may contain tautological axioms, so that it is an over-approximation. We call this module lean kernel subsumption module (LK subsumption module for short), since it contains all axioms that were involved in computing the uniform interpolant, similar to lean kernels in SAT-solving [19]. LK subsumption modules can be computed more cheaply than minimal subsumption modules, as they do not require any further subsumption tests after the annotated uniform interpolant is computed. We believe that they also have a special use in ontology engineering: given a set of concept names, they allow the ontology engineer to quickly examine all the axioms that are involved in inferring any entailments involving no other concept names. Definition 3. Let O be an ontology and Σ a signature. An ontology MΣ lk is a Σ LK subsumption module iff there exists an annotated uniform interpolant OaΣ of O for Σ that is obtained by collecting all axioms that belong to some annotation concepts occurring in OaΣ : MΣ Σ lk = {α | Aα ∈ sig(Oa )}. 60 Corollary 2. Given an ontology O, a signature Σ s.t. Nr ⊆ Σ and a Σ LK subsumption module MΣ Σ lk for O, we have M ⊆ Mlk for every minimal Σ- subsumption module M of O. Since LK subsumption modules can be obtained from the annotated uniform interpolant without additional subsumption tests, they can always be computed even in the case where the annotated uniform interpolant contains fixpoint op- erators. However, different to minimal subsumption modules they do not offer any minimality guarantees: which axioms are contained in the LK subsumption module depends on the uniform interpolation procedure used, and as uniform interpolants may contain redundant and tautological information, it is in general possible that an LK subsumption module contains axioms that are not included in any minimal subsumption module. The requirement that the signature contains all role names is indeed crucial for the correctness of our method, as is exemplified by the following example. Example 2. Take following ontology O: A v ∃r.B AvC B v ⊥, and consider the signature Σ1 = {A, r}. The annotation Oa of O looks as follows. A v ∃r.B t AAv∃r.B A v C t AAvC B v ⊥ t ABv⊥ A uniform interpolant OaΣ for Oa for {A, r, AAv∃r.B , AAvC , ABv⊥ } is A v ∃r.ABv⊥ t AAv∃r.B . Consequently, the Σ1 LK subsumption module contains the first and the last axiom of O. One easily verifies that these two axioms also form the only minimal Σ1 -subsumption module of O. Now consider the signature Σ2 = {A, C}. A close look at the original ontology shows that in fact, the concept A is unsatisfiable, which can be inferred just from the first and the last axiom. This makes the second axiom redundant, and therefore the minimal subsumption module for Σ2 is the same as for Σ1 . However, the uniform interpolant OaΣ2 for Oa for {A, C, AAv∃r.B , AAvC , ABv⊥ } just contains the following axiom. A v C t AAvC That is, the LK subsumption module contains just one axiom, which is exactly the only axiom that does not occur in the minimal subsumption module. The reason that the annotated uniform interpolant does not contain any more axioms is that the axiom A v ∃r.ABv⊥ t AAv∃r.B has no non-tautological ALCH- entailment that does not also make use of the role name r. Finally, for the complete signature Σ3 = {A, r, C}, the Σ3 LK subsumption module contains all axioms. However, as we already observed, the second axiom is redundant, and thus, this subsumption module is not minimal. 61 7 Evaluation To evaluate how our method performs in practice, we implemented a Java pro- totype of our method and did an initial evaluation on a set of 96 ontologies that were taken from the classification track for OWL DL ontologies at the ORE competition 2014 [24]. The prototype was implemented in Java 1.7, using the OWL-API [9] for ontology access, Lethe [17] for computing the annotated uni- form interpolants, and MORe [25] as a reasoner in the minimisation step. MORe is a hybrid reasoner that utilises the OWL DL reasoner HermiT [7] together with the EL reasoner ELK [10]. As it was to be expected that the module as well as the uniform interpolants could often be expressed purely in EL, this reasoner was selected to improve reasoner performance for these cases. In fact, we noticed that the minimalisation step was usually significantly faster when using MORe than when using HermiT. We were particularly interested in the performance for computing small sub- sumption modules. In particular, we were interested in the following questions: 1) how well does the method perform in practice for computing LK subsumption modules and minimal subsumption modules, and 2) can minimal subsumption modules in ALCH be expected to be smaller than modules extracted by al- ternative methods, such as locality-based modules. Since we expected both the computation of the annotated uniform interpolant, as well as the minimisation step afterwards, to be costly in practice, we computed subsumption modules in a relaxed setting. For this, we used a timeout for the uniform interpolation step. Lethe computes uniform interpolants by eliminating names outside of the specified signature one after the other. If it did not succeed in computing the uniform interpolant within the specified timeout, we continued the computation with the uniform interpolant it computed so far, thus obtaining LK subsump- tion modules and minimal subsumption modules for an extended signature. This way, we were able to get an upper bound on the size of the minimal subsumption module even if the annotated uniform interpolant was too difficult to compute. Furthermore, note that the annotated uniform interpolant computed in the first step may contain fixpoint expressions, so that the LK subsumption module can- not be minimised in the second step, as we cannot test for entailment of axioms with fixpoint expressions using MORe. To still get an idea about the minimi- sation potential of our approach, we simply treated entailment of axioms with fixpoint expressions as failure, unless the axiom was syntactically contained in the current module. Note that this may result in a module that is not minimal, similar to when the uniform interpolation procedure created a timeout. The ontologies for our experiments were selected as follows. We selected our ontologies from the track “Classification of OWL DL ontologies” of the OWL Reasoner Evaluation competition 2015, because they provide a small, yet well balanced mix of ontologies with very different properties [24]. As our method only supports ALCH ontologies, we further removed from each ontology the axioms that were not in ALCH, where we kept n-ary equivalence and disjointness axioms, as well as concept inclusions. From this set of 315 ontologies, we selected 62 |Σ ∩ Nc | 10 25 50 Success Rate 92.2% 90.3% 90.6% Minimal 71.2% 70.3% 68.7% Fixpoints 20.8% 19.8% 23.6% UI Timeout 2.0% 2.2% 2.0% Duration (s) 0.4 / 594.0 / 3.7 / 20.6 0.4 / 591.9 / 4.1 / 27.1 0.5 / 592.0 / 6.1 / 32.5 Size >⊥∗-Module 0 / 1021 / 131.0 / 204.4 0 / 1374 / 164.0 / 256.7 0 / 1047 / 204.0 / 260.3 Size LK Module 0 / 723 / 103.5 / 170.1 0 / 1054 / 144.0 / 216.7 0 / 835 / 170.0 / 218.5 Size Min. Module 0 / 723 / 103.0 / 169.8 0 / 1051 / 142.0 / 216.1 0 / 814 / 169.0 / 218.0 Size Original Ontology 186 / 8926 / 1792.0 / 2547.5 Table 1. Results of our evaluation for signatures containing 10/25/50 concept names (minimal/maximal/median/average). |Σ ∩ Nc | 100 150 Success Rate 87.7% 85.7% Minimal 66.5% 66.0% Fixpoints 21.7% 20.6% UI Timeout 2.6% 1.7% Duration (s) 0.9 / 584.5 / 9.1 / 39.1 1.0 / 594.9 / 11.6 / 39.7 Size >⊥∗-Mod 1 / 1374 / 305.0 / 352.2 6 / 1242 / 385.0 / 435.8 Size LK Mod 1 / 1054 / 267.0 / 301.2 6 / 1242 / 342.0 / 382.1 Size Minimised Mod 1 / 1051 / 264.0 / 300.0 6 / 1234 / 336.0 / 379.9 Size Original Ontology 186 / 8926 / 1792.0 / 2547.5 Table 2. Results of our evaluation for signatures containing 100/150 concept names (minimal/maximal/median/average). those that contained less than 10,000 axioms and more than 150 concept names, resulting in a set of 96 ontologies in total. The experiment was performed on a server running Ubuntu 15.10 with In- tel Xeon 2.50GHz cluster Core 4 Duo CPU with 64GiB RAM. We used our prototype to compute subsumption modules for randomly created signatures containing 10, 25, 50, 100 and 150 concept names, were we used 30 samples per signature size. The timeout for the interpolation procedure was set to 5 minutes, while the overall timeout was set to 10 minutes. The results of our experiment are shown in Table 2. The success rate shows the number of runs in which the method succeeded within the timeout. The next rows show the percentage of runs that produced modules which were guaranteed to be minimal (Row 3), that did not guarantee minimality due to fixpoints in the uniform interpolant (Row 4), and that did not guarantee minimality due to a timeout in the inter- polation procedure (Row 5). Note that the latter two cases may overlap. We then list the minimal, maximal, median and average duration of computing the module in the successful runs. We obtained median durations between 4.1 and 11.6 seconds, which might be reasonable for daily applications. However, as to be expected, in general our method is more computationally expensive than other methods for module extraction. The following rows compare the sizes of the TBoxes of the >⊥∗-modules, the LK subsumption modules and the minimised subsumption modules. Note 63 that, because the signatures always contained all role names, the >⊥∗-modules as well as the subsumption modules always had the same RBox as the original ontology. It is for this reason that we focus on the TBoxes of the modules to provide for a more meaningful comparison. The LK subsumption modules were on average 12.3%–16.8% smaller than the >⊥∗-modules, while the minimised variants differed only little in size to the LK subsumption modules. This shows that in practice, LK subsumption modules provide for good approximations of minimal subsumption modules. The last row shows for comparison the minimal, maximal, median and average size of the input ontologies. 8 Conclusion and Future Work We presented a method for extracting subsumption modules in ALCH for signa- tures Σ s.t. Nr ⊆ Σ. The method ensures minimality of the extracted modules provided that a uniform interpolant without fixpoint operators can be computed for the given ontology and signature. In the first step, the method computes an annotated uniform interpolant, from which an approximation of the minimal sub- sumption module, the LK subsumption module can be obtained. This module is then minimised in a subsequent step by comparing entailments of corresponding uniform interpolants. Our evaluation indicates that in most cases, the LK sub- sumption module is already minimal or close-to minimal, so that the second step can be omitted. As for LK subsumption modules, we do not have a restriction for cyclic ontologies, this means that our method provides for good approximations of minimal subsumption modules for ALCH ontologies in general. Our evalua- tion indicates that our method is often able to compute subsumption modules that are smaller than locality-based modules. However, in some cases, the com- putation of these modules was quite time-consuming. Our implementation uses a timeout for the uniform interpolation step, and computes a subsumption module for the signature for which a uniform interpolant could be computed within that timeout. It would be interesting to see the exact effect of this timeout on the computed subsumption modules. For small timeouts, our implementation would compute an LK subsumption module for an extended signature that in addition contains those concept names that are especially hard for Lethe to eliminate, which usually is only a small fraction of complete signature. It is possible that those LK subsumption modules provide for close approximations of the LK sub- sumption modules for the given signature, though computable in much shorter time. There are obvious short-comings of our evaluation that should be addressed in future work. First, the sample size used for the signatures was very small, which is why we are currently running the experiments with a higher num- ber of signatures per ontology. Second, we only compared our method with the syntactical method for computing >⊥∗-modules. An alternative obvious choice for comparison would be AMEX [5], which can approximate depleting semantic modules of ALCQI ontologies. Such a comparison could give insights on whether subsumption modules are in practice smaller than semantic modules, or whether 64 they are mostly similar. Third, it would be interesting to evaluate our method on larger ontologies and not only ontologies with at most 10,000 axioms. Further- more, it would be interesting to test our method with other implementations for uniform interpolation than Lethe, for example the Ackermann-based method presented in [31]. Open problems with our approach are 1) how to obtain an optimal, practical method in the case uniform interpolants contain fixpoints, and 2) how to compute minimal subsumption modules for signatures that do not contain all role names. In order to tackle these, it might be necessary to use the uniform interpolation method not as a black box, but to modify its implementation to track inferences directly. Again, it is possible that techniques from the area of justification and axiom-pinpointing could be used here. References 1. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The description logic handbook: theory, implementation, and applications. Cambridge University Press, New York, NY, USA (2007) 2. Botoeva, E., Konev, B., Lutz, C., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Inseparability and conservative extensions of description logic ontologies: A sur- vey. In: Pan, J.Z., Calvanese, D., Eiter, T., Horrocks, I., Kifer, M., Lin, F., Zhao, Y. (eds.) Reasoning Web: Logical Foundation of Knowledge Graph Construction and Query Answering: 12th International Summer School 2016, Aberdeen, UK, September 5-9, 2016, Tutorial Lectures. pp. 27–89. Springer International Publish- ing, Cham (2017), https://doi.org/10.1007/978-3-319-49493-7_2 3. Chen, J., Ludwig, M., Ma, Y., Walther, D.: Zooming in on ontologies: Minimal modules and best excerpts. In: The Semantic Web - ISWC 2017 - 16th International Semantic Web Conference, Vienna, Austria, October 21-25, 2017, Proceedings, Part I. pp. 173–189 (2017) 4. Chen, J., Ludwig, M., Walther, D.: On computing minimal EL-subsumption mod- ules. In: Proceedings of the Joint Ontology Workshops 2016 Episode 2: The French Summer of Ontology co-located with the 9th International Conference on Formal Ontology in Information Systems (FOIS 2016), Annecy, France, July 6-9, 2016. (2016), http://ceur-ws.org/Vol-1660/womocoe-paper6.pdf 5. Gatens, W., Konev, B., Wolter, F.: Lower and upper approximations for deplet- ing modules of description logic ontologies. In: Proceedings of the Twenty-first European Conference on Artificial Intelligence. pp. 345–350. IOS Press (2014) 6. Ghilardi, S., Lutz, C., Wolter, F.: Did I damage my ontology? A case for conserva- tive extensions in description logics. In: Proceedings, Tenth International Confer- ence on Principles of Knowledge Representation and Reasoning, Lake District of the United Kingdom, June 2-5, 2006. pp. 187–197 (2006), http://www.aaai.org/ Library/KR/2006/kr06-021.php 7. Glimm, B., Horrocks, I., Motik, B., Stoilos, G., Wang, Z.: HermiT: an OWL 2 reasoner. Journal of Automated Reasoning 53(3), 245–269 (2014) 8. Grau, B.C., Horrocks, I., Kazakov, Y., Sattler, U.: Modular reuse of ontologies: Theory and practice. Journal of Artificial Intelligence Research (JAIR) 31(1), 273– 318 (2008) 65 9. Horridge, M., Bechhofer, S.: The OWL API: A Java API for OWL ontologies. Semantic Web 2(1), 11–21 (2011) 10. Kazakov, Y., Krötzsch, M., Simančı́k, F.: The incredible ELK. Journal of Auto- mated Reasoning 53(1), 1–61 (2014) 11. Konev, B., Ludwig, M., Walther, D., Wolter, F.: The logical difference for the lightweight description logic EL. Journal of Artificial Intelligence Research (JAIR) 44, 633–708 (2012) 12. Konev, B., Lutz, C., Walther, D., Wolter, F.: Formal properties of modulari- sation. In: Modular Ontologies: Concepts, Theories and Techniques for Knowl- edge Modularization, pp. 25–66. Springer (2009), https://doi.org/10.1007/ 978-3-642-01907-4_3 13. Konev, B., Lutz, C., Walther, D., Wolter, F.: Model-theoretic inseparability and modularity of description logic ontologies. Artificial Intelligence 203, 66–103 (2013) 14. Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology compari- son and module extraction, with an application to DL-Lite. Artificial Intelligence 174(15), 1093–1141 (2010) 15. Koopmann, P., Schmidt, R.A.: Forgetting concept and role symbols in ALCH- ontologies. In: Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, Decem- ber 14-19, 2013. Proceedings. pp. 552–567 (2013), https://doi.org/10.1007/ 978-3-642-45221-5_37 16. Koopmann, P., Schmidt, R.A.: Count and forget: Uniform interpolation of SHQ- ontologies. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Rea- soning: 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Pro- ceedings. pp. 434–448. Springer International Publishing, Cham (2014), https: //doi.org/10.1007/978-3-319-08587-6_34 17. Koopmann, P., Schmidt, R.A.: Lethe: Saturation-based reasoning for non- standard reasoning tasks. In: Proc. ORE’15. pp. 23–30 (2015) 18. Koopmann, P., Schmidt, R.A.: Uniform interpolation and forgetting for ALC on- tologies with ABoxes. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA. pp. 175–181 (2015), http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9981 19. Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunc- tive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel. In: Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings. pp. 22–35 (2006), https://doi.org/10.1007/11814948_4 20. Ludwig, M., Konev, B.: Practical uniform interpolation and forgetting for ALC TBoxes with applications to logical difference. In: Principles of Knowledge Repre- sentation and Reasoning: Proceedings of the Fourteenth International Conference, KR 2014, Vienna, Austria, July 20-24, 2014 (2014), http://www.aaai.org/ocs/ index.php/KR/KR14/paper/view/7985 21. Ludwig, M., Walther, D.: The logical difference for ELHr -terminologies using hy- pergraphs. In: ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014). pp. 555–560 (2014), https://doi.org/10.3233/ 978-1-61499-419-0-555 22. Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in ex- pressive description logics. In: IJCAI 2011, Proceedings of the 22nd International 66 Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16- 22, 2011. pp. 989–995 (2011), https://doi.org/10.5591/978-1-57735-516-8/ IJCAI11-170 23. Nikitina, N., Rudolph, S.: (Non-)succinctness of uniform interpolants of general terminologies in the description logic EL. Artif. Intell. 215, 120–140 (2014), https: //doi.org/10.1016/j.artint.2014.06.005 24. Parsia, B., Matentzoglu, N., Gonçalves, R.S., Glimm, B., Steigmiller, A.: The OWL reasoner evaluation (ORE) 2015 competition report. Journal of Automated Rea- soning pp. 1–28 (2015) 25. Romero, A.A., Grau, B.C., Horrocks, I.: MORe: Modular combination of owl rea- soners for ontology classification. In: International Semantic Web Conference. pp. 1–16. Springer (2012) 26. Romero, A.A., Kaminski, M., Grau, B.C., Horrocks, I.: Module extraction in ex- pressive ontology languages via datalog reasoning. J. Artif. Intell. Res. 55, 499–564 (2016), https://doi.org/10.1613/jair.4898 27. Sattler, U., Schneider, T., Zakharyaschev, M.: Which kind of module should I extract? In: Proceedings of DL’09. CEUR Workshop Proceedings, vol. 477. CEUR- WS.org (2009) 28. Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: IJCAI-03, Proceedings of the Eighteenth Inter- national Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003. pp. 355–362 (2003), http://ijcai.org/Proceedings/03/Papers/053.pdf 29. Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: A practical OWL- DL reasoner. Web Semantics: science, services and agents on the World Wide Web 5(2), 51–53 (2007) 30. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. Automated reasoning pp. 292–297 (2006) 31. Zhao, ` Y., Schmidt, R.A.: Forgetting concept and role symbols in ALCOIHµ + ( , ∩)-ontologies. In: Proceedings of the Twenty-Fifth International Joint Confer- ence on Artificial Intelligence. pp. 1345–1352. AAAI Press (2016)