Deductive Module Extraction for Expressive Description Logics

1 Introduction

Module extraction in description logics (DLs) is to extract some subset of a given ontology, usually for a given signature of names, that preserves certain properties w.r.t. that signature. Originally motivated by ontology reuse, ontology modularity has been widely used in different areas, such as ontology matching [Jim´enez-Ruiz and Grau, 2011] and debugging [Ludwig, 2014], forgetting [Koopmann and Schmidt, 2013], or to improve reasoning [Romero et al., 2012]. In this paper, we focus on applications in ontology analysis and ontology reuse, and consider a module notion called deductive modules [Kontchakov et al., 2010], also investigated under the name of subsumption modules [Chen et al., 2017]: given an ontology and a signature Σ of names, a deductive module is a subset of the ontology that preserves all entailments that can be expressed in the DL under consideration using only names fromΣ.

In ontology analysis, an ontology engineer wants exhibit what an ontology states about some names of interest. For this, seeing as few axioms as possible helps getting the information needed quickly. He might furthermore want to see all axioms that are relevant for entailments in the selected signature. We cover this requirement under the notion of a complete deductive module, which turns out to be a stronger notion than the similarly motivated notion of Σ-essential axioms discussed in [Grau et al., 2008].

Usually, the module will use additional names than the ones specified. The ontology engineer might thus be interested to know why the axioms belong to a module, and how they contribute to entailments in the signature. For standard reasoning services, the necessity of explaining inferences has long been understood and implemented under the service of justification [Baader and Pe˜naloza, 2007; Horridge et al., 2008]. Our approach for computing deductive modules computes a so-called annotated interpolant, which shows the entailments in the selected signature, parts of which are annotated with axioms from the ontology that contribute to these entailments, and can thus be seen as an explanation of that module.

Another application of modules is in ontology reuse [Jim´enez-Ruiz et al., 2008; Grau et al., 2008]. Here the ontology engineer wants to reuse a part of the ontology in another context in which only a subset of the signature is relevant, and thus a module would be sufficient. Here, being complete and explainable might not be as relevant, but robustness properties gain importance: specifically, it is not only important that all entailments in the signature are covered by the module, but also that entailments are preserved when further axioms are added: the module should be replaceable with the original ontology and still preserve the same entailments.

While most module notions investigated in the literature cover the above properties, often they concern much stronger notions of modules, which can make the problem of optimal module extraction hard. For instance, for the notion of semantic modules, already for the light-weight description logic EL it is undecidable whether a given subset is a module for a given signature, [Konev et al., 2013]. As a consequence, existing algorithms for computing minimal semantic modules can only deal with acyclic EL [Konev et al., 2012] and DL-Lite [Kontchakov et al., 2010]. Practical implementations, such as the syntactical locality-based module extraction method implemented in the OWL API [Grau et al., 2008], AMEX [Gatens et al., 2014] and PriM [Romero et al., 2016], usually compute approximations of minimal modules that may contain more axioms than necessary.

For deductive modules, the situation looks different. Deciding deductive modules is ExpTime-complete for ELontologies [Lutz and Wolter, 2007] and 2ExpTime-complete for ALC ontologies [Ghilardi et al., 2006]. For acyclic ELHr -ontologies, it was shown that deductive modules are substantially smaller than other module types [Chen et al., 2018; 2019]. However, we are not aware of any practical method for computing deductive modules in more expressive DLs such as ALC.

In this paper, we present a method for computing deductive modules in ALC and ALCH, which are often substantially smaller than modules computed by existing methods. This method is based on a method for uniform interpolation for expressive DLs presented in [Koopmann and Schmidt, 2013]. Both uniform interpolants and modules preserve entailments in a specified signature. The difference is that, while a module is always a subset of the ontology, and may use more names than specified, a uniform interpolant may only use names from the specified set and will thus usually be of a syntactical different shape. This can lead to uniform interpolants that contain substantially more complex axioms than the input ontology [Lutz and Wolter, 2011], which is why it is often preferable to use modules rather than uniform interpolants.

Uniform interpolants cover exactly the entailments in the given signature. The main idea of our technique is to track these entailments back to axioms in the original ontology. For this, we label each axiom in the input ontology with a fresh concept name, and then compute a uniform interpolant for an extended signature. The result is an annotated interpolant, which links the entailments shown in the uniform interpolant to the axioms in the ontology, and can be used to illustrate how the axioms in the ontology contribute to a module. Using the annotated interpolant, we present methods for computing two types of deductive modules, complete deductive modules and minimised deductive modules, which we define in the corresponding sections 4 and 5. These modules consider the two contradicting requirements a user might have, completeness in terms of covering every axiom relevant to an entailment on the one hand, and minimality on the other hand.

To obtain modules that are robust under replacement, we cannot directly re-use the uniform interpolation method that was presented in [Koopmann and Schmidt, 2013], but have to adapt it to support for universal roles. The adaptation has the nice side-effect that a computationally expensive rule for eliminating role names is replaced by a simpler rule, so that uniform interpolants can be computed in shorter time. The adapted method is presented in Section 3. Since robustness under replacement might not always be a requirement, in Section 6, we show how the methods can be modified to compute potentially smaller ALC modules that do not follow this requirement. Finally, in Section 7, we extend all methods to ALCH, for which, in contrast to the other methods, we cannot use uniform interpolation as a black-box method.

We implemented a prototype of our approach which we evaluate and compare with existing methods, both for computing random modules and atomic decompositions, a structure representing all self-contained modules of an ontology. Since uniform interpolation can be an expensive operation, we may not always be able to compute optimal modules in short time. Furthermore, our algorithmmight require reasoning capabilities that are not supported by state-of-the-art DL

reasoners. For those cases, our implementation allows for a flexible way to approximate modules: the more time given, the smaller the modules, and we know when the module is minimal. Our results indicate that in most cases, an approximation is not necessary, and the modules computed by our method are significantly smaller than those computed with existing tools. For proofs and details omitted due to space limitations, we refer to the extended technical report [Koopmann and Chen, 2020].

2 Description Logics and Deductive Modules

We recall the DLs relevant in this paper [Baader et al., 2007], as well as the notions of deductive modules.

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. A role is an element r ∈ NR ∪{∇}, where ∇ denotes the universal role. Concepts are built according to the syntax rule C ::= A | ¬C | C ⊔ C | ∃r.C, where A ∈ NR and r is a role. Further concepts are introduced as abbreviations: C ⊓ D = ¬(¬C ⊔ ¬D), ∀r.C = ¬∃r.¬C, ⊤ = A ⊔ ¬A and ⊥ = ¬⊤. A concept inclusion (CI) is an expression C ⊑ D, where C, D are concepts. A role inclusion (RI) is an expression r ⊑ s, where r, s are roles. CIs and RIs are collectively called axioms. The DL ALCH∇ uses all constructors introduced so far. Without RIs, we obtain the DL ALC∇, and without the universal role, we obtain the DLs ALCH and ALC respectively. Given a concept/axiom/ontology X, we denote by sig(X) the signature of X, i.e. the concept and role names occurring in X.

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 A ∈ NC to AI ⊆ ∆I , every r ∈ NR to a binary relation rI ⊆ ∆I , that satisfies ∇I = ∆I ×∆I , and is extended to concepts by (¬C)I := ∆I \C I , (C ⊔ D)I := C I ∪ DI , and (∃r.C)I := {x ∈ ∆I | ∃y ∈ C I : (x, y) ∈ rI }. An interpretation I satisfies a CI C ⊑ D iff C I ⊆ DI , and an RI r ⊑ s if rI ⊆ sI . For an axiom α, we write I |= α if I satisfies α. An interpretation I is a model of an ontology O if I |= α for all α ∈ O. An axiom α is entailed by O, written O |= α, if for all models I of O, we have that I |= α.

Definition 1. Let L be a DL, O an ontology and Σ a signature. Then, a subset M ⊆ O is a deductive 〈L,Σ〉-module of O iff for every L-axiom α with sig(α) ⊆ Σ, O |= α iff M |= α.

If the DL L is clear from the context, we may refer to an 〈L,Σ〉-module simply as Σ-module. Note that deductive modules are related to conservative extensions: namely, ifM is a deductive 〈L,Σ〉-module of O, then O is a conservative extension of M.

In this paper, we consider the input ontologies to be expressed in ALC and ALCH. Still, there might be entailments using universal roles that we want to preserve by the module. This is particularly the case for ALC/ALC∇, due to following result from [Konev et al., 2009].

Figure 1: Uniform interpolation calculus.

Theorem 1. Let O be an ALC-ontology, Σ a signature, and M an 〈ALC∇,Σ〉-module of O. Then, for every ALContology O′ with (sig(O′ ) ∩ sig(O)) ⊆ Σ and every ALCaxiom α s.t. sig(α) ⊆ Σ, we have (O ∪ O′ ) |= α iff (M∪O′ ) |= α.

These 〈ALC∇,Σ〉-modules are called robust under replacements, as they can serve as a replacement of the original ontology in a reusing context. Intuitively, if we want to use terms from the signature Σ in a new ontology O′ , we can replace O by its 〈ALC∇, Σ〉-module. We refer to these modules as robust modules in the following.

3 Resolution-Based Uniform Interpolation

Uniform interpolants [Lutz and Wolter, 2011] cover exactly the entailments a deductive module should preserve.

Definition 2. Let L be a DL, O an ontology and Σ a signature. Then, a uniform 〈L,Σ〉-interpolant of O is an ontology OΣ s.t. sig(OΣ) ⊆ Σ and for every L-axiom α with sig(α) ⊆ Σ, OΣ |= α iff O |= α.

Our method for computing deductive modules uses uniform interpolation to track entailments in the target signature back to the axioms in the original ontology. Our arguments are easier to follow in perspective of the resolution-based method for computing uniform interpolants from in [Koopmann and Schmidt, 2013]. To capture entailments of robust modules, we need to compute uniform 〈ALC∇,Σ〉- interpolants. The method in [Koopmann and Schmidt, 2013] only supports ALCH, which is why we adapt the calculus used by the method to support for universal roles. The rest of the method remains the same. Due to space restrictions, we only give a brief overview of the important steps.

The method proceeds in three steps, which we discuss one after the other. Let ND ⊆ NC be a special set of concept names not used in the input.

Step 1 transforms all axioms of the ontology into the following form:

where A ∈ NC, Q ∈ {∀, ∃}, r ∈ NR and D ∈ ND, and at most one literal of the form ¬D, D ∈ ND, occurs in each axiom. Here, we treat disjunctions as sets, that is, duplicates are silently removed and the order is not important. Furthermore, as it is the same for all axioms, we discard the leading ⊤ ⊑, and call the normalised axiom clause.

In Step 2, inferences on the names outside the target signature are performed using the rules shown in Figure 1. Here, D12 refers to a possibly new definer representing D1 ⊓ D2, which we introduce, if such a definer does not exist yet, by adding ¬D12 ⊔D1, ¬D12 ⊔D2 to the current clause set. The difference to the calculus in [Koopmann and Schmidt, 2013] is the R∃-rule: since they compute uniform interpolants for a DL without universal roles, instead a more expensive role resolution rule is used that makes use of an external reasoner, which is not necessary in our case. Still, in order to eliminate a role name r from a clause, we need to consider all inferences of the RQ-rule on that role name before applying the R∃-rule.

Rules are only applied if the result contains at most one literals of the form ¬D, where D ∈ ND. In order to perform all relevant inferences on the names outside the target signature, usually further inferences on names inside the target signature are necessary. This is typically the case for the RQ-rule: this rule might trigger the introduction of a new definer D12 with the clauses ¬D12 ⊔ D1, ¬D12 ⊔ D2. If we have also two clauses ¬D1 ⊔ C ′1 ⊔ A, ¬D2 ⊔ C ′2 ⊔ ¬A, and A is a name we want to perform inferences on, new resolution steps on A become possible only due to the new definers. How to determine which rules have to be used is described in more detail in [Koopmann, 2020]. After all inferences on a name X outside of the signature are performed, we filter out all occurrences of that name.

Finally, in Step 3, the introduced definers are eliminated as follows.

1. For every definer D, the clauses ¬D⊔C1, . . ., ¬D⊔Cn are grouped into a single axiom D ⊑ C1 ⊓ . . . ⊓ Cn.
2. We then repeat following steps as long as as possible:
3. (a) Replace D ⊑ C[D], where C[D] is a concept in which D occurs positively, by D ⊑ νX.C[X], where C[X] is obtained from C[D] by replacing D by X.
4. (b) For every CI D ⊑ C where D ̸∈ sig(C), remove that axiom and replace all occurrences of D by C.
5. νX.C[X] is a special concept constructor called the greatest fixpoint, which corresponds to the limit of the infinite sequence of concepts C[⊤], C[C[⊤]], C[C[C[⊤]], . . .. For the formal semantics, we refer to [Calvanese and De Giacomo, 2003]. There exist inputs for which no uniform interpolant without fixpoint operators exists [Lutz and Wolter, 2011].

Lemma 1. Let O be an ALC-ontology and Σ a signature. The method always terminates and computes a uniform 〈ALC∇, Σ〉-interpolant of O.

4 Complete Robust Deductive Modules

For ontology analysis, it might be desirable to see all axioms in an ontology that contribute to entailments in a signature of interest. "Contributing to an entailment" is formally captured by the notion of justifications [Baader and Pe˜naloza, 2007]: given an ontology O and an axiom α s.t. O |= α, a justification for O |= α is a subset J ⊆ O s.t. J |= α and J is minimal w.r.t. ⊊. If O ̸|= α, there is no justification for O |= α.

Definition 3. Let L be a DL, O an ontology and Σ a signature. An 〈L,Σ〉-moduleMof O is complete iff for every Laxiom α s.t. sig(α) ⊆ Σ and every justification J for O |= α, J ⊆ M.

Complete modules contain all axioms that contribute to entailments in the signature of interest, and are thus useful for ontology analysis tasks. Similarly motivated is the set of Σessential axioms, as defined in [Grau et al., 2008]: Given a signature Σ, the set of Σ-essential axioms in O is the intersection of all subset-minimal Σ-modules in O. However, in the presence of redundancy, Σ-essential axiom sets may "miss" axioms, as already the following simple example illustrates. Take the ontology O = {A ⊑ B ⊓ C, A ⊑ B} and the signature Σ = {A,B,C}. Clearly, both axioms contribute to the entailment A ⊑ B, but only the first axiom occurs in a minimal module for Σ. Thus, A ⊑ B ⊓ C is the only Σessential axiom, while the complete module would also contain A ⊑ B. While this is a very simply example, we note that redundancy is a common phenomenon in real-life ontologies [Grimm and Wissmann, 2011].

To compute complete deductive modules, we track the axioms used during uniform interpolation. For this, we use axiom annotation.

Definition 4. Let O be an ontology. The annotation Oa of O is defined as

where each AC⊑D is fresh.

We call the concept names AC⊑D labels. The following result can be shown using the rule applications used when computing the uniform interpolant as described in Section 3.

Theorem 2. Let O be an ontology, Σ a signature, and Oa the annotation of O. Additionally, let OΣ a be the uniform 〈ALC∇, Σ′ 〉-interpolant of Oa for Σ′ = Σ ∪ {Aα | α ∈ O}. Then, the ontologyM= {α | Aα ∈ sig(OΣ a )}

is a complete deductive 〈ALC∇, Σ〉-module of O for Σ.

In the above definition, we call OΣ a the annotated uniform 〈ALC∇, Σ〉-interpolant of O. In addition in helping us find a complete module, the annotated uniform interpolant provides for a link between the module and the uniform interpolant that allows us to better understand how the axioms contribute to entailments in the target signature.

Example 1. Consider the following ontology O:

The uniform interpolant of O for Σ = {A, r}, consisting of the following axioms, captures all entailments of O over Σ:

To understand which axioms contribute to these entailments, we first annotate O:

Algorithm 1 Computing minimal deductive modules

Input: ontology O, signature Σ, integer n

Output: a minimal deductive module M

• 1: LetM= O, Q= divide(O, n)
• 2: while L ̸= ∅ do
• 3: B := head(Q), Q := tail(Q)
• 4: if (M\ B)Σ |= OΣ then
• 5: M :=M\ B
• 6: else
• 7: L := divideInHalf(B) :: Q
• 8: end if
• 9: end while
• 10: returnM

The annotated uniform interpolant of O for Σ is then the following:

We can directly read off the complete Σ-module for O, which is O itself. We can furthermore understand how the axioms contribute to entailments over Σ: α3 is needed for every nontrivial entailment over Σ, while α2 and α1 each contribute to what is under the different existential role restrictions.

5 Minimised Robust Deductive Modules

Both for ontology reuse or ontology understanding, if we are not interested in completeness, we would prefer a module that does not contain more axioms than necessary.

Definition 5. A deductive 〈L,Σ〉-module Mof an ontology O is minimal if no subset M′ ⊂ M is a deductive 〈L,Σ〉- module of O .

We note that the number of minimal modules can be exponential in the size of the ontology. We aim neither to compute the complete set of minimal modules, nor the module that contains the smallest number of axioms, but just to compute any minimal module. Our method for minimising modules guarantees minimality if the computed uniform interpolants does not contain fixpoints. However, as our evaluation shows, it still often results in modules that are much smaller than the complete module.

Minimal deductive modules can be seen as justifications for the corresponding uniform interpolant. Computing justifications has been studied in the literature under the name of axiom pinpointing [Baader and Pe˜naloza, 2007], and there exist implementations even as part of the OWL API [Horridge et al., 2008]. However, those methods are optimised for justifying smaller axioms, and generally do not perform well for large entailments such as complex uniform interpolants. Our algorithm uses ideas from axiom pinpointing, but is optimised for our particular use-case.

Algorithm 1 computes a minimal deductive module by removing all superfluous axioms from O. Similar algorithms can be found in [Kontchakov et al., 2010; Chen et al., 2018].

Since entailment checks can be expensive, instead of checking axioms one by one, we check entailment of a set of axioms, called bubble, in each step. divide(O, n) partitions the axioms in O into a sequence Q of bubbles of size n plus the remainder, while divideInHalf (B) splits a bubble into two equally sized bubbles to be attached at the beginning of the current sequence Q.

Note that in Line 4, we could also test for M\ B |= OΣ, in which case our algorithm would directly correspond to an algorithm for computing justifications. However, this test can be computationally expensive, because OΣ can be large, or even impossible, if OΣ can contains fixpoints which are not supported by DL reasoners. Note that in most cases, there will be no syntactical overlap between OΣ and M, since OΣ has to be fully in Σ. In contrast, the interpolants (M\ B)Σ and OΣ use the same signature, and thus can overlap syntactically, if computed wisely. As we can decide (M\B)Σ |= OΣ by only testing entailment of the axioms in OΣ \ (M\ B)Σ, those syntactical overlaps can reduce reasoning times significantly, and we may not even have to consider all fixpoint expressions occurring in OΣ for reasoning. If greatest fixpoints occur only in (M\ B)Σ, these can be simulated using auxiliary names [Koopmann and Schmidt, 2013].

To compute interpolants of the different subsets (M\ B) of the ontology fast, we use the following lemma.

Lemma 2. Let O be an ALC-ontology, Σ a signature and OΣ a an annotated uniform 〈ALC∇,Σ〉-interpolant of O. Additionally, let O1 ⊆ O. Then, the ontology

is a uniform 〈ALC∇, Σ〉-interpolant of O1 for Σ.

Thus, before entering Algorithm 1, we compute the annotated uniform interpolant of the input ontology, from which then all other required uniform interpolants are cheaply obtained by replacing the labels with ⊤ and ⊥. We further use some syntactical simplification rules to replace tautological as well as contradictory subconcepts by ⊤ and ⊥, and to remove tautological axioms. The interpolant OΣ is replaced by the logically equivalent MΣ when it turns out to be smaller.

Example 2. Continuing on Example 1, we obtain for {α1, α2} after simplification the uniform interpolant

of which the second axiom would be removed by simplification. For {α2, α3}, we similarly obtain

of which the second axiom would be removed. For {α1, α2} we only obtain tautological axioms. None of these interpolants entails the uniform interpolant of O, which is why O is also a minimal module of itself.

6 Deductive Modules for Pure ALC

The previous sections considered uniform interpolants and deductive modules for ALC∇. For applications in ontology analysis where robustness under replacements is not a requirement, it might be sufficient to preserve entailments in pure ALC, for which the modules can be smaller. Our method for uniform interpolation introduces universal roles only under existential restrictions. This allows for a simple way of generating corresponding uniform interpolants for ALC.

Lemma 3. Let O be an ALC∇ ontology in which the universal role only occurs in concepts of the form ∃∇.C, and where every ∃∇.C occurs only positively. Additionally, let O′ the result of replacing every ∃∇.C in O by ⊥ if O |= C ⊑ ⊥, and otherwise by ⊤. Then, for every ALC-axiom α, O |= α iff O′ |= α.

When we apply this lemma on an annotated uniform interpolant, we lose however all annotations that occur in expressions of the form ∃∇.C. We thus have to extend our mechanism for tracking inferences using annotations. Let O be an ontology, Σ a signature and Oa the annotation of O. Then, the extended annotation of O for Σ is defined as

Correspondingly, we obtain the annotated uniform 〈ALC,Σ〉-interpolant based on this extended annotation, in the same way as we obtain the annotated uniform 〈ALC∇, Σ〉-interpolant from the annotation.

The additional axioms make sure that the label information is preserved when eliminating a role name r. Specifically, they make sure that for every justification J of an entailment O |= C ⊑ D, we also have Oea |= dα∈J Aα ⊓ C ⊑ D. In Oa, there would be a corresponding entailment Oa ⊑ C ′ ⊑ D′ , in which however the labels can occur under role restrictions in C ′ and D′ . Intuitively, the additional axioms in Oea allow to "pull" these labels out of the role restrictions to make sure that Oea |= dα∈J Aα ⊓ C ⊑ D.

With this adaptation, we can use the methods presented in Section 4 and 5 for computing complete deductive modules as well as minimised deductive modules for entailments in ALC, based on the following results.

Theorem 3. Let O be an ontology, Σ a signature, and Oea the extended annotation of O for Σ. Additionally, let OΣ ea be the uniform 〈ALC,Σ′ 〉-interpolant of Oea, where Σ′ = Σ ∪ {Aα | α ∈ O}. Then, M = {α | Aα ∈ sig(OΣ ea )} is a complete deductive 〈ALC, Σ〉-module of O for Σ.

Lemma 4. Let O be an ontology, Σ a signature and OΣ ea an annotated uniform 〈ALC,Σ〉-interpolant of O for Σ. Additionally, let O1 ⊆ O. Then, the ontology

is a uniform 〈ALC, Σ〉-interpolant of O1 for Σ.

7 Handling Role Hierarchies

Though we presented one uniform interpolation method in this paper, in general, all methods presented here can be combined with any uniform interpolation method for the respective DL. This approach fails however for ALCH, because we cannot annotate RIs. Here, we have to modify the uniform interpolation procedure so that it tracks usage of role axioms itself. The rules shown in Figure 2 are based on rules from the original calculus in [Koopmann and Schmidt, 2013], and extend the calculus presented in Section 3 by explicitly tracking used role inclusion axioms. Note that the resulting method is not sound anymore for computing uniform interpolants, and can thus only be used for computing annotated interpolants.

In our implementation, these rules are either used on their own, when the aim is to eliminate a role name r, or in combination with the RQ-rule. In the latter case, we do not perform the individual inferences of these rules explicitly, but determine in one step which additional disjuncts have to be added to the newly derived clause, and which role is used in the role restriction. For instance, if we have the clauses C1 ⊔ ∀r.D1 and C2 ⊔ ∃s.D2 and there exist a justification J for O |= s ⊑ r, we derive

in one step. The resulting method is applied on the (extended) annotation of an ontology as before, resulting in the annotated uniform 〈L,Σ〉-interpolant for respectively L = ALCH∇ and L = ALCH.

Entailments of RIs cannot be handled in this way, but are not hard to obtain from the set of RIs. For a set R of RIs, the uniform Σ-interpolant RΣ = {r ⊑ s | r, s ∈ Σ, O |= r ⊑ s} can be easily computed by following the RIs in R. We thus compute the uniform interpolant of the RIs directly.

Theorem 4. Let L ∈ {ALCH,ALCH∇}, O be an ALCHontology with RIs R, Σ a signature and OΣ a an annotated uniform 〈L,Σ〉-interpolant of O for Σ. Additionally, let RΣ be a uniform Σ-interpolant of R. Then, the ontology

where J(R |= β) is the union of all justifications for R |= β, is a complete deductive 〈L, Σ〉-module of O.

Lemma 5. Let L ∈ {ALCH,ALCH∇}, O be an ALCHontology with RIs R, Σ a signature and OΣ a an annotated uniform 〈L,Σ〉-interpolant of O for Σ. Additionally, let O1 ⊆ O. Then, the ontology

is a uniform 〈L, Σ〉-interpolant of O1.

We use this approach for computing minimised deductive modules with Algorithm 1. For the complete deductive module, we just need to additionally collect the justifications of the entailed RIs.

8 Proof of Concept Evaluation

We implemented our technique for extracting complete and minimal ALCH∇-modules in Java and evaluated it on a varied corpus of ontologies. For this, we implemented the calculus consisting of the rules in Figures 1 and 2, as well as the module extraction techniques, as extension to the uniform interpolation tool LETHE [Koopmann, 2020]. 1 To keep the modules small, we used the redundancy elimination rules presented in [Koopmann and Schmidt, 2013], and applied a set of syntactic, equivalence-preserving simplification rules on the computed uniform interpolants. Uniform interpolation is an expensive operation, which becomes more challenging in the presence of labels. However, we observed that even for the hardest cases, the majority of names could usually be eliminated fast. To acknowledge this, we implemented a timeout within the uniform interpolation procedure: once the timeout is reached, we output and simplify the annotated uniform interpolant computed so far. For checking entailments, we used the reasoner HermiT [Glimm et al., 2014].

We evaluated our method on ontologies in the DL Classification track of the OWL Reasoner Evaluation (ORE) 2015 [Parsia et al., 2017]. This corpus contains a balanced and varied mix of ontologies in expressive DLs, which have been taken from the corpora MOWLCorp, BioPortal and the Oxford Ontology Repository, and thus contains many reallife ontologies. From each ontology, we removed axioms that could not be equivalently expressed in ALCH, and removed from the resulting set ontologies that had less than 100 names or more than 100,000 axioms, resulting in a set of 227 ontologies. The sizes of the ontologies, measured in number of axioms, can be seen in Figure 3. All experiments were performed on an Intel Core i5-4590 CPU with 3.30GHz and 32 GB RAM.

8.1 Complete andMinimised Deductive Modules

To evaluate the performance of our method for small modules, we randomly generated 60 signatures per ontology of 100 names each, including both concept and role names, where each name was selected with a probability proportional to its number of occurrences in the ontology. We used a timeout of 5 minutes for the uniform interpolation procedure, and a timeout of 10 minutes in complete. We compared the results with modules computed by the two other alternatives for computing modules in expressive DLs: ⊤⊥∗ -modules as implemented in the OWL-API [Grau et al., 2008], and AMEX modules [Gatens et al., 2014].

In 90.9% of cases, uniform interpolation did not cause a timeout, and in 96.4% of cases, we could generate a (possibly approximated) module. When the uniform interpolation step was stopped due to the timeout, an average of 2 names was not eliminated. In 83.4% of cases, we were able to also minimise the module within the time limit. As was to be expected, our method was more expensive than the other methods for module extraction. On average, computing the complete and minimised module took respectively 22 and 44 seconds, while each ⊤⊥∗ -module was computed within 5 seconds. Computing the AMEX-module based on the precomputed ⊤⊥∗ -modules always took less than a second.

1 https://lat.inf.tu-dresden.de/∼koopmann/LETHE (version 0.65)

Statistics on the sizes of modules are shown in Table 1. As AMEX only supports acyclic ALC ontologies and cannot handle role hierarchies, 143 ontologies could not be processed by AMEX. Category 1 regards the cases that were supported by AMEX, and Category 2 the remaining cases. As we can see in Table 1, the size of minimised modules is significantly smaller than ⊤⊥∗ -modules and, on average, considerably smaller than AMEX-modules and complete modules.

8.2 Self-ContainedModules and Atomic Decompositions

A self-contained module M for a signature Σ is a module that is also a module for its own signature, i.e. Σ ∪ sig(M). Our method of computing complete modules can be easily extended to compute self-contained modules, where after the computation of the module, we update the signature with the signature of the computed module, and repeat the procedure until the size of modules does not change anymore. While in Section 8.1, we had to use random samples of signatures of a specified size, it is possible to construct a structure that represents all complete self-contained modules, thus allowing for more significant insights on how module sizes behave in general. Specifically, we use the atomic decomposition (AD) [Vescovo et al., 2011], a structure initially developed for locality-based modules such as ⊤⊥∗ -modules, and represents all possible modules. The AD of an ontology partitions the ontology into a set of atoms, so that every module is the union of atoms. Here, an atom a of an ontology O is a set of axioms such that for every module M of O, a ⊆ M or a ∩M = ∅ w.r.t. any signature. Larger atoms can lead to larger modules, as a module with one axiom from an atom always contains all other axioms in that atom. Thus, the smaller the atoms, the more fine-grained is the structure of the atomic decomposition, and the smaller are modules in general.

We computed atomic decompositions for the 171 ontologies in our corpus that contained less than 10,000 axioms, using both ⊤⊥∗ -modules and complete self-contained modules computed by our method, where this time, we used a timeout of 30 seconds for uniform interpolation, so that the AD was approximated in some cases. Our method produced much less large atoms, indicating a finer granularity of self-contained complete axioms compared to ⊤⊥∗ -modules. In the following, we call atoms generated by our method complete-atoms, and atoms generated using ⊤⊥∗ -modules star-atoms. For 70.1% of the ontologies, each complete-atom contained at most 4 axioms, which was only the case for 39.8% of the ontologies regarding star-atoms. The 90% quantile for the maximal atom size per ontology was 9 for complete-atoms, and 118 for star-atoms. This shows that self-contained modules computed by our method can be much smaller than ⊤⊥∗ - modules in general.

9 Conclusion and FutureWork

We presented a practical method for computing deductive modules in ALC and ALCH ontologies based on uniform interpolation. Our evaluation showed that deductive modules are often considerably smaller than other types of modules. In the future, we would like to investigate the impact timeouts in the uniform interpolation method have on the module size, and whether precomputed atomic decompositions can be used to speed up the computation. Furthermore, we want to investigate whether uniform interpolation methods for more expressive DLs, such as the approaches in [Zhao and Schmidt, 2018; Koopmann and Schmidt, 2014], can be used. While for some more expressive DLs, deductive modules are undecidable, it could still be possible that approximations result in smaller modules than for existing module types.

Acknowledgements

Patrick Koopmann is partially supported by the DFG grant 389793660 as part of TRR 248 (see https://www. perspicuous-computing.science). Jieying Chen is supported by the SIRIUS centre, which is funded by the Norwegian Research Council, project number 237898 and is co-funded by its partner companies. We would like to thank Boris Konev for his help with the AMEX system, and Marco Benedetti for providing the solver sKizzo used by AMEX.