We investigate how minimal subsumption modules can be extracted using methods for uniform interpolation and forgetting. Given an ontology and a signature of concept and role names, a subsumption module 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 compute subsumption modules in ALCH, and which under certain conditions guarantees minimality of the extracted modules. As a side product, 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.
Description Logics [
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
module extraction have been developed [
The core idea of our method is to use uniform interpolation [
Our method only supports signatures that contain all role names, while
arbitrary 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 [
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 different subsets of the input ontology, for which we compute an annotated uniform interpolant defined in Section 5. As a by-product, the annotated uniform interpolant 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
There is a range of types and properties of modules that have been investigated
in the literature, surveys of which can be found in [
For computing minimal subsumption modules of E LH-terminologies, a method
has been presented in [
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
specified signature that can be expressed in the respective description logic. However,
while subsumption modules are subsets of the input ontology, uniform
interpolants 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 E L and ALC, the uniform
interpolant may have a size that is triple exponential in the size of the input
ontology [
We recall the description logic ALCH [
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 \CI , (C u D)I := CI ∩ DI , (C t D)I := CI ∪ DI , (∃r.C)I := {x ∈ ΔI | ∃y ∈ CI : (x, y) ∈ rI }, and (∀r.C)I := {x ∈ ΔI | ∀(x, y) ∈ rI : y ∈ CI }.
An interpretation I satisfies a TBox axiom C v D (C ≡ D) iff CI ⊆ DI (CI = DI ). It satisfies an RBox axiom r v s (r v s) iff rI ⊆ sI (rI = sI ). 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 Interpolant.). 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
A related problem to minimal subsumption module extraction is that of
computing justifications [
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 signature. 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. Unfortunately, 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 entailments 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, 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.
0 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.
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 annotated 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 >.
The following ontology is a uniform interpolant of O for Σ = {A, r}. ∃r.> v A t B
A ≡ ∃r.B
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 By interpolating the annotation of O, we obtain the following annotated uniform interpolant of O for Σ.
∃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 AA≡∃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
symbols of the original ontology. The following lemma, which can be shown by
inspection of the uniform interpolation method presented in [
As a corollary of this lemma, we obtain the robustness property of
subsumption 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 [
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 ontology 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 concepts.) 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 Σ.
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.
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 [
Definition 3. Let O be an ontology and Σ a signature. An ontology MlΣk 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Σ :
MlΣk = {α | Aα ∈ sig(OaΣ )}. Corollary 2. Given an ontology O, a signature Σ s.t. Nr ⊆ Σ and a Σ LK subsumption module MlΣk for O, we have M ⊆ MlΣk 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 operators. 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.
A v ∃r.B
A v C
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
B v ⊥ t ABv⊥
A v ∃r.ABv⊥ t AAv∃r.B.
A uniform interpolant OaΣ for Oa for {A, r, AAv∃r.B, AAvC , ABv⊥} is 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.
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 ALCHentailment 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.
To evaluate how our method performs in practice, we implemented a Java
prototype 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 [
We were particularly interested in the performance for computing small subsumption 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 alternative 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 subsumption 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 cannot 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 minimisation 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 [
The experiment was performed on a server running Ubuntu 15.10 with Intel 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 interpolation 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 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
We presented a method for extracting subsumption modules in ALCH for signatures Σ 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 subsumption 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 subsumption 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 evaluation indicates that our method is often able to compute subsumption modules that are smaller than locality-based modules. However, in some cases, the computation 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 subsumption 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
number 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 [
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.