There are various techniques for specifying a module of an ontology that covers all knowledge about a given set of terms. These differ with respect to the size of the module, the complexity of its computation, and certain robustness properties. In this paper, we survey existing logic-based approaches, focus on syntactic approximations, and compare different kinds of modules with respect to their properties. This is intended to give guidelines on how to choose “the right kind of module”.
? This work has been supported in part by the UK EPSRC grant no. EP/E065155/1. 3 Terms are concept (class) names and role (property) names. Σ, we mean that all consequences of O that can be expressed over Σ are also consequences of M. Then O is said to be a conservative extension (CE) of M.
The logic-based view seems theoretically sound and elegant and provides
a desirable guarantee: reusing only terms from Σ, we will not be able to
distinguish between importing M and importing O into our ontology. However,
deciding CEs is computationally expensive in general: the problem of deciding
whether two ontologies entail the same concept inclusions over a given signature
is usually harder than standard reasoning tasks. For DL-Litehorn, for instance,
complexity grows from polynomial-time to coNP-complete, and for DL-Litebool
it grows from NP-complete to Π2p-complete [
This paper surveys existing logic-based approaches, focusing on syntactic approximations. We will compare different kinds of locality-based modules with each other and with CE-based modules. In particular, we will explore nested locality-based modules more in-depth than the existing literature. The comparison of module kinds will be based on examining properties relevant for ontology reuse. It will help learning which modules are best suited for which requirements.
The relevant properties have been identified in [
In the following, we will use L to denote a description logic contained in SHOIQ,
whose standard syntax and semantics are defined in [
Let NC be a set of concept names, and NR a set of role names. A signature Σ is a set of terms, i.e., Σ ⊆ NC ∪ NR. We can think of a signature as specifying a topic of interest. Axioms that only use terms from Σ can be thought of as “on-topic”, and all other axioms as “off-topic”. For instance, if Σ = {Animal, Duck, Grass, eats}, then Duck v ∃eats.Grass is on-topic, while Duck v Bird is off-topic.
Any concept name, role name, TBox, or axiom that uses only terms from Σ is called a Σ-concept, Σ-role, Σ-TBox, or Σ-axiom. Given any such object X, we call the set of terms in X the signature of X and denote it with sig(X) or Xe .
Given an interpretation I, we denote its restriction to the terms in a signature Σ with I|Σ . Two interpretations I and J are said to coincide on a signature Σ, in symbols I|Σ = J |Σ , if ΔI = ΔJ and XI = XJ for all X ∈ Σ. 2.1
There are a number of variants of the notion of conservative extensions, which capture the desired preservation of knowledge to different degrees. We focus on the following basic ones.
Definition 1. Let L be a DL, M ⊆ T be L-TBoxes, and Σ a signature. (1) T is a deductive Σ-conservative extension (Σ-dCE ) of M w.r.t. L if for all
GCI axioms α over L with αe ⊆ Σ, it holds that M |= α if and only if T |= α. (2) T is a model Σ-conservative extension (Σ-mCE ) of M if {I|Σ | I |= M} = {I|Σ | I |= T }. (3) M is a dCE-based (mCE-based ) module for Σ of T if T is a Σ-dCE (Σ-mCE) of M w.r.t. L.
It is clear that T being a Σ-mCE of M implies that T is a Σ-dCE of M.
Due to the computational difficulty to decide both kinds of CEs,
approximations have been introduced [
It has been shown in [
Furthermore, locality can be tested using available DL-reasoners [
Let A⊥, R⊥ ∈/ Σ, C⊥ ∈ Bot(Σ), C(>i) ∈ Top(Σ), n¯ ∈ N \ {0} Bot(Σ) ::= A⊥ | ⊥ | ¬C> | C u C⊥ | C⊥ u C | ∃R.C⊥ | >n¯ R.C⊥ | ∃R⊥.C | >n¯ R⊥.C Top(Σ) ::= > | ¬C⊥ | C1> u C2> | >0 R.C (b) >-Locality
Let A>, R> ∈/ Σ, C⊥ ∈ Bot(Σ), C(>i) ∈ Top(Σ), n¯ ∈ N \ {0} Bot(Σ) ::= ⊥ | ¬C> | C u C⊥ | C⊥ u C | ∃R.C⊥ | >n¯ R.C⊥ Top(Σ) ::= A> | > | ¬C⊥ | C1> u C2> | ∃R>.C> | >n¯ R>.C> | >0 R.C
It has been shown in [
Modules of O for each of the four locality notions are obtained by
starting with an empty set of axioms and subsequently adding axioms from O that
are non-local. In order for this procedure to be correct, the signature against
which locality is checked has to be extended with the terms in the axiom that is
added in each step. Definition 4 (1) introduces locality-based modules, which are
always mCE-based (and therefore dCE-based) modules [
We write M = x-mod(Σ, T ). (2) A TBox M is the yz-module of T w.r.t. Σ, written M = yz-mod(Σ, T ), if
M = y-mod(Σ, z-mod(Σ, T )). (3) Let (Mi)i>0 be a sequence of TBoxes such that M0 = T and Mi+1 = yz-mod(Σ, Mi) for every i > 0. For the smallest n > 0 with Mn = Mn+1, we call Mn the yz∗-module of T w.r.t. Σ, written M = yz∗-mod(Σ, T ).
Input: TBox T , signature Σ, x ∈ {∅, Δ, ⊥, >} Output: x-module M of O w.r.t. Σ M ← ∅; T 0 ← T repeat changed ← false for all α ∈ T 0 do if α not x-local w.r.t. Σ ∪ Mf then
M ← M ∪ {α} T 0 ← T 0 \ {α} changed ← true end if end for until changed = false return M
As for (1), it has been shown in [
Modulo the locality check, Algorithm 1 runs in time cubic in |T | + |Σ| [
The notions of modules defined so far were induced by CEs and different notions of locality. We will now put them into a more general context of modules generated by inseparability relations. For a given logic L, an inseparability relation
S is a family S = {≡Σ | Σ is a signature} of equivalence relations on the set of S L-TBoxes. The intuition behind this notion is as follows: T1 ≡Σ T2 means that T1 and T2 are indistinguishable w.r.t. Σ, i.e., they represent the same knowledge about the topic represented by Σ. The exact meaning of the terms “indistinguishable” and “the same knowledge” depends on the precise definition of the 5 Our algorithm is a special case of the one in [3, Figure 4]. inseparability relation. M being a module for Σ of T should be equivalent to M ⊆ T and M being inseparable w.r.t. Σ from T .
The requirement to preserve entailments or models leads to the following
inseparability relations, which have been examined in [
{I|Σ | I |= T2}. c – T1 and T2 are Σ-concept name inseparable, written T1 ≡Σ T2, if for all Σconcept names C, D, it holds that T1 |= C v D if and only if T2 |= C v D. – T1 and T2 are Σ-subsumption inseparable w.r.t. a logic L, written T1 ≡sΣ T2, if for all terms X and Y that are concept expressions over Σ or role names from Σ, it holds that T1 |= X v Y if and only if T2 |= X v Y . q – T1 and T2 are Σ-query inseparable, written T1≡Σ T2, if for all Σ-ABoxes A, Σqueries q(x) and tuples a of object names from A, it holds that (T1, A) |= q(a) if and only if (T2, A) |= q(a).
– T1 and T2 are Σ-model inseparable, written T1 ≡sΣem T2, if {I|Σ | I |= T1} = We denote the respective sets of inseparability relations with Sc, Ss, and Ssem. It is easy to see that, for each signature Σ, it holds that ≡sΣem ⊆ ≡sΣ ⊆ ≡cΣ .
Inseparability relations induce modules as follows.
Definition 5. Let S be an inseparability relation, T a TBox, M ⊆ T , and Σ a signature. We call M
S (1) an SΣ -module of T if M ≡Σ T ; S (2) a self-contained SΣ -module of T if M ≡Σ∪Mf T ;
S (3) a depleting SΣ -module of T if ∅ ≡Σ∪Mf T \ M.
M is called a minimal (self-contained, depleting) ≡Σ -module of T if M, but no proper subset of M, is a (self-contained, depleting) ≡Σ -module of T .
Due to the shift from Σ to Σ ∪ Mf, it is not necessarily the case that every self-contained (or depleting) SΣ -module of T is an SΣ -module of T . However, under certain robustness properties, this implication holds.
While self-contained and depleting SΣ -modules tend to be bigger than SΣ
modules, they have important applications. One of those is the computation
of all justifications for an entailment η of the ontology T [
Anothereapplication of depleting modules is the import scenario [
Finally, while there can be exponentially many minimal SΣ -modules, minimal depleting modules are uniquely determined—under mild conditions involving inseparability relations.
In order to find natural candidates for inseparability relations for locality-based modules, we proceed by analogy to inseparability relations for conservativity: ontologies T1 and T2 are inseparable if they have the same modules, i.e., if the module extraction algorithm returns the same output for each of them. We have replaced the semantic criterion “the same entailments/models” in conservativitybased inseparability with a syntactic criterion “the same extraction result” simply because locality-based modules are defined algorithmically. Furthermore, we will see that two of the thus obtained inseparability relations have almost all desired properties—which makes them even superior to dCE-based modules.
We consider the following inseparability relations for locality-based modules, where x stands for one of the locality notions ∅, Δ, ⊥, and >, and yz stands for one of the combinations ⊥> and >⊥.
Relation
x ≡Σ
yz ≡Σ
yz∗ ≡Σ
T1 and T2 are in relation if . . . x-mod(Σ, T1) = x-mod(Σ, T2) yz-mod(Σ, T1) = yz-mod(Σ, T2) yz∗-mod(Σ, T1) = yz∗-mod(Σ, T2)
3.1
In the introduction, we have already sketched four important properties of inseparability relations and have seen why they are of interest for applications of modules. We will now define them.
Definition 6. Let L be a DL. The inseparability relation S is called (1) robust under vocabulary restrictions if, for all L-TBoxes T1, T2 and all signaS S tures Σ, Σ0 with Σ ⊆ Σ0, the following holds: if T1 ≡Σ0 T2, then T1 ≡Σ T2. (2) robust under vocabulary extensions if, for all L-TBoxes T1, T2 and all signaS S tures Σ, Σ0 with Σ0 ∩ (Te1 ∪ Te2) ⊆ Σ : if T1 ≡Σ T2, then T1 ≡Σ0 T2. (3) robust under replacement if, for all L-TBoxes T1, T2, all signatures Σ and S every L-TBox T with Te ∩ (Te1 ∪ Te2) ⊆ Σ, the following holds: if T1 ≡Σ
S
T2, then T1 ∪ T ≡Σ T2 ∪ T . (4) robust under joins if, for all L-TBoxes T1, T2 and all signatures Σ with Te1 ∩ Te2 ⊆ Σ and every i = 1, 2, the following holds: if T1 ≡SΣ T2, then Ti ≡SΣ T1 ∪T2.
As mentioned in Section 2.2, some of these robustness properties have an
effect on the relation between the three different kinds of induced SΣ-modules
from Definition 5, see [
Let us now examine the properties of the inseparability relations Ssem, Ss,
Sc, Sx, Syz and Syz∗ , where x ∈ {≡∅Σ,Δ⊆, ⊥≡,>cΣ}fraonmd Syezct∈ion{⊥2>.2,,>t⊥h}e. fFolilroswt,ining
addition to the inclusions ≡sΣem ⊆ s
inclusions hold, see [
Theorem 7. Let Σ be a signature, x ∈ {∅, Δ, ⊥, >} and yz ∈ {>⊥, ⊥>}. Then the following properties hold: ≡xΣ ⊆ ≡sΣem ; ≡yΣz ⊆ ≡sΣem ; ≡yΣz∗ ⊆ ≡sΣem . property corresponding module notion (min.) modules (min.) self-contained mod.s (min.) depleting modules
relation robustness voc. restr. robustness voc. ext. robustness replacement robustness joins
Ssem
Ss mCE dCE 3− 3− 7 7 7 7
Sc — — — —
The properties of the equivalence relations defined in Subsection 2.2 are
summarised in Figure 2. The first four lines give the module notion which is
generalised by this inseparability relation, and indicate whether each such module
for Σ is a (minimal) SΣ -module, or a (minimal) self-contained SΣ -module, or
a (minimal) depleting SΣ -module. For Sc, this question is meaningless because
there is no corresponding standard module notion, apart from redefining Σ-dCEs
to take only Σ-concept inclusions into account. For Ssem and Ss, it is clear that
Definition 1 (3) leads to SΣ -modules, but not to minimal, self-contained, or
depleting ones. This can, however, easily be achieved by adopting stronger module
notions as in [
The remaining four lines indicate whether the respective inseparability
relation satisfies the four robustness properties from Definition 6. The results for
Ssem, Ss and Sc are taken from [
The following theorem states the results in Figure 2 for locality-based
inseparability relations. Their proofs can be found in [
Theorem 8. Let x ∈ {∅, Δ, ⊥, >} and yz ∈ {⊥>, >⊥}. (1) The inseparability relation SΣx is robust under replacement, vocabulary restrictions, vocabulary extensions and joins. (2) The inseparability relation SΣyz is not robust under vocabulary restrictions or extensions, but under replacement and joins. (3) The inseparability relation Syz∗ is robust under replacement, vocabulary reΣ strictions, vocabulary extensions and joins. (4) Let T be a TBox, Σ a signature, and M = x-mod(Σ, T ). Then M is a minimal SΣx -module, a minimal self-contained SΣx -module, and a minimal depleting SΣx -module of T . (5) Let T be a TBox, Σ a signature, and M = yz-mod(Σ, T ). Then M is not generally a minimal SΣyz-module, but it is a minimal self-contained SΣyzmodule and a minimal depleting SΣyz-module of T . (6) Let T be a TBox, Σ a signature, and M = yz∗-mod(Σ, T ). Then M is a minimal Syz∗ -module, a minimal self-contained SΣyz∗ -module, and a minimal Σ depleting SΣyz∗ -module of T . 3.2
Theoretical results. For ALC and ALCQI, the problem of deciding whether two
ontologies entail the same concept inclusions over a given signature Σ is
2ExpTime-complete [
Fortunately, extracting mCE-based modules can be tractable, for instance
for acyclic E L ontologies [
For the DL-Lite family [
Experimental results. Since CE-based modules are so hard to extract, it is difficult to perform experiments comparing modules of different notions extracted from the same ontology for the same signature. However, in two cases this has been possible. We will briefly describe the two cases and show the difference between conservativity-based and locality-based modules.
Snomed CT, the Systematized Nomenclature of Medicine, Clinical Terms,
is an ontology that consists of approximately 360,000 concepts and 1.4 million
relationships, and defines the medical terminology for health care systems in the
US, the UK, and other countries. It is an acyclic E L TBox; therefore extracting
mCE-based modules is tractable: the system MEX [
The version of Snomed CT underlying these figures was dated 9 February 2005. A version of 30 December 2006 led to similar results.
In [
(a) |Σ| = 1 (b) |Σ| = 10 (c) |Σ| = 5 + 5
Core Umbrella Core Umbrella Core Umbrella MCM MQM MDQM >⊥∗-mod
The results show that, on average, locality-based modules can be considerably
bigger than dCE-based modules. On the other hand, since locality-based modules
are always depleting (see Section 3.1), it is only fair to compare them with
MDQM, and in only one of six cases are >⊥∗-modules more than one and a
half times as big as MDQMs on average. In [
Example 9. Let Σ = {A, D} and T = {A v B, C v D}.
Then we have >-mod(Σ, T ) = {C v D} and ⊥-mod(Σ, T ) = {A v B}, but >⊥-mod(Σ, T ) = ⊥>-mod(Σ, T ) = ∅.
There are cases where repeated nesting of >⊥-modules (⊥>-modules) decreases module size even further, see Example 10.
Example 10. Consider Σ = {A} and T = {A v B t C, B v A}. Then we have T ⊃ >⊥-mod(Σ, T ) ⊃ >⊥-mod(Σ, >⊥-mod(Σ, T )) because:
N1 = ⊥-mod(Σ, T )
= {A v B t C, B v A} M1 = >-mod(Σ, N1) = {B v A} N2 = ⊥-mod(Σ, M1) = ∅
M2 = >-mod(Σ, N2) = ∅ An analogous example for ⊥>-modules is Σ = {A}; T = {B v A t ¬C, A v B}.
It therefore makes sense to continue this nesting up to a fixpoint. The
following lemma shows that the number of steps until this fixpoint is reached can be
asymptotically as big as the number of axioms in T . The proof is given in [
We have compared important properties of conservativity-based and localitybased modules via the more general notion of inseparability relations. It has turned out that, while modules based on locality are in general larger than conservativity-based ones, they are very robust. Two out of three versions of locality-based modules enjoy the same robustness properties as mCE-based modules and are therefore more robust than modules based on dCEs. In addition, they are self-contained and depleting. However, their robustness does not simply follow from the fact that they are a special case of mCE-based modules: yz-modules do not “inherit” all robustness properties.
Furthermore, modules based on syntactic locality can be extracted efficiently
for all logics up to SHOIQ. They can thus also serve as an intermediate step
for extracting conservativity-based modules [