We present an implementation (AMEX) of a module extraction algorithm for acyclic description logic ontologies. The implementation uses a QBF solver (sKizzo) to check whether one ontology is a conservative extension of another ontology relativised to interpretations of cardinality one. We evaluate AMEX by applying it to NCI (the National Cancer Institute Thesaurus) and by comparing the extracted AMEX-modules with locality-based modules. We also present experiments for a hybrid approach in which AMEX and locality-based module extraction are applied iteratively to NCI.
Introduction the main research problem is to minimise the size of the module (or, equivalently, to approximate minimal modules). Currently, the most popular and successful approximation algorithm is based on locality and computes so-called >? -modules [4]. The size of >? -modules and the performance of algorithms extracting >? -modules has been analysed systematically and in great detail [4]. However, since no alternative logically sound and implemented module extraction algorithms are available for expressive DLs, it remained open how large and significant the difference between >? -modules and minimal modules is and in how far it is possible to improve upon the approximation obtained by >? -modules.2
The contribution of this paper is as follows. 1. We extend the module extraction algorithm introduced in [8] from acyclic ALCITBoxes to acyclic ALCQI-TBoxes with repeated concept inclusions and present a number of optimisations of the algorithm given in [8]. We note that our extraction algorithm is polynomial time except that it uses a QBF-solver as an oracle. 2. We describe our implementation, called AMEX, of this module extraction algorithm. AMEX is available from http://www.csc.liv.ac.uk/~wgatens/ software/amex.html. 3. We evaluate its efficiency in experiments with NCI and compare the size of the computed AMEX-modules with the size of >? -modules. 4. We introduce a hybrid approach to module extraction in which >? -module extraction and AMEX-module extraction are applied iteratively. Unlike AMEX on its own, this hybrid approach is applicable to arbitrary description logic TBoxes. We demonstrate that on some inputs both AMEX and the hybrid approach lead to significant reductions in the size of modules. 2
Preliminaries We use standard notation from logic and description logic (DL), details can be found in [1]. In a DL, concepts are constructed from countably infinite sets NC of concept names and NR of role names using the concept constructors defined by the DL. For example, ALCQI-concepts are built according to the rule
C ::= A j > j :C j n r:C j n r :C j
C u D; where A 2 NC, n is a natural number, and r 2 NR. As usual, we use the following abbreviations: ? denotes :>, 9r:C denotes 1 r:C, 8r:C denotes :9 r::C, C t D denotes :(:C u :D), n r:C denotes :( (n + 1) r:C), and (= n r:C) for (( n r:C) u ( n r:C)).
A general TBox T is a finite set of axioms, where an axiom can be either a concept inclusion (CI) C v D or a concept equality (CE) C D, where C and D are concepts. A general TBox T is acyclic if all its axioms are of the form A v C or A C, where 2 An implementation of semantic locality-based ; -modules and a comparison between >? and ; -modules have been presented in [4]; however, the authors found no significant difference between the two approaches. A promising approach to refine >? -module extraction has recently been presented in [12], but an implemented system is not yet publicly available. A 2 NC, no concept name occurs more than once on the left-hand side and A 6 T+ A, for adneyfinAed2bNyCse,twtihnegreA T+TisXtheifftrtahnesrietivexeicstlsosaunreaxoifotmheorfeltahteiofnormTA vNCC or(ANC [CNRin) T with X 2 sig(C).
The semantics of DLs is given by interpretations I = ( I ; I ), where the domain I is a non-empty set and I is an interpretation function that maps each A 2 NC to a subset AI of I and each r 2 NR to a binary relation rI I I . The function I is inductively expanded to complex concepts C in the standard way [1]. An interpretation I satisfies a CI C v D (written I j= C v D) if CI DI , it satisfies a CE C D (written I j= C D) if CI = DI . I is a model of T if it satisfies all axioms in T . 3
Module Extraction In this section we define depleting modules and give an algorithm computing depleting modules of acyclic ALCQI-TBoxes using a QBF solver. To cover the NCI Thesaurus, we also extend our extraction algorithm to TBoxes that are acyclic except that they contain repeated concept inclusions. The results presented in this section are extensions of the results presented in [8] for acyclic ALCI-TBoxes to acyclic ALCQI-TBoxes with repeated concept inclusions.
A signature is a finite subset of NC [ NR. The signature sig(C) (sig( ), sig(T )) of a concept C (axiom , TBox T , resp.) is the set of concept and role names that occur in C ( ; T , resp.). If a sig(C) we call C a -concept. The -reduct Ij of an interpretation I is obtained from I by setting Ij = I , and XIj = XI for all X 2 , and XIj = ; for all X 62 . Let T1 and T2 be TBoxes and a signature. Then T1 and T2 are -inseparable, in symbols T1 T2, if
fIj j I j= T1g = fIj j I j= T2g: It is proved in [8] that TBoxes T1 and T2 are -inseparable if, and only if, T1 j= ' iff T2 j= ' holds for any second-order sentence ' using symbols for only. Thus, -inseparable TBoxes cannot be distinguished by their second-order consequences formulated in . We use -inseparability to define modules.
Definition 1. Let M module of T if T n M
T be TBoxes and [sig(M) ;.
a signature. Then M is a depleting Every depleting module M of T is inseparable from the T for its signature [8], that is, if M is a depleting -module of T then T [sig(M) M, and, in particular, T M. Thus, a TBox and its depleting -module can be equivalently replaced by each other in applications which concern only. Unfortunately, checking if a subset M of T is a depleting -module of T for some given signature is undecidable already for general TBoxes formulated in E L and for acyclic ALC-TBoxes [8, 11].
We therefore consider syntactic restrictions that ensure that depleting modules become decidable. We say that an acyclic TBox T has a direct -dependency, for some signature , if there exists fA; Xg with A T+ X; otherwise we say that T has no direct -dependencies. Although one can construct TBoxes T and depleting -modules M of T such that T n M contains direct [ sig(M)-dependencies (see [8]), for typical depleting -modules M, the set T n M should not contain direct [ sig(M)-dependencies because such dependencies indicate a semantic link between two distinct symbols in [sig(M). The main advantage of making the assumption that T n M has no direct [ sig(M)-dependencies is that it becomes decidable whether T n M [sig(M) ; [8]. The following lemma directly implies this decidability result. For an acyclic TBox T and a signature let
Lhs (T ) = fA ./ C 2 T j A 2 or 9X 2 (X T+ A)g: The following is proved in [8] for acyclic ALCI-TBoxes. The generalization to ALCQI is straightforward and omitted.
Ij [sig(M) = J j [sig(M).
Lemma 1. Let T be an acyclic ALCQI-TBox. If T n M has no direct dependencies then the following conditions are equivalent for every W [ sig(M)T n M: (a) W [sig(M) ;; (b) for every I with j I j = 1 there exists a model J of Lhs [sig(M)(W) such that Since the condition (b) of Lemma 1 refers to interpretations with a singleton domain, it can be checked by reduction to validity of a quantified Boolean formula: take a propositional variable pA for each name A 2 [sig(M) and a (distinct) propositional variable qX for each symbol X 2 sig(T ) n ( [ sig(M)). Translate concepts D in the signature sig(T ) into propositional formulas Dy by setting
Ay = pA Ay = qA for all A 2 [ sig(M) for all A 2 sig(T ) n ( [ sig(M)) (D1 u D2)y = D1y ^ D2y
(:D)y = :Dy 1 r :D)y = qr ^ Dy for all r 2 sig(T ) n r :D)y = ? for all n > 1 and r 2 sig(T ) ( ( 1 r:D)y = ( n r:D)y = ( Now let
T y =
^ CvD2T nM
Cy ! Dy ^
^ C D2T nM
Cy $ Dy and let p denote the sequence of variables pA, A 2 [ sig(M), and q denote the sequence of variables qX , X 2 sig(T ) n ( [ sig(M)). One can show that condition (b) of Lemma 1 holds if, and only if, the QBF 'T := 8p9qT y is valid. Thus, for TBoxes with no direct [ sig(M)-dependencies the separability check can be implemented using a QBF solver.
Lemma 1 can be used directly for a naïve module extraction algorithm which goes through all subsets of T to identify a smallest possible M such that T n M has no direct [ sig(M)-dependencies and T n M [sig(M) ;. Instead, we consider a refined goal-oriented approched based on the notion of a separability causing axiom. Let M T and a signature be such that T n M has no direct [ sig(M)-dependencies. We call an axiom A ./ C 2 T n M, where ./2 fv; g, separability causing if there exists a W T n M such that
A ./ C 2 W; (W n fA ./ Cg) [sig(M) ;; Clearly, if T n M 6 [sig(M) ; then T n M contains a separability causing axiom.
The algorithm computing a depleting -module of acyclic ALCQI -TBoxes is now given in Figure 1. In the algorithm, the extraction of depleting -modules is broken into the rules R1 and R2. The rule R1 checks for direct [ sig(M)-dependencies. The rule R2 implements an inseparability check. Notice that R2 only applies when R1 is not applicable, that is only if T n M contains no direct [ sig(M)-dependencies. Notice that applications of the R1 rule can lead to axioms unnecessarily being included into the module; but such is the price we pay for regaining the decidability of the inseparability check.
To reduce the number of calls to the QBF solver, rule R2 is implemented as binary search. We first consider T nM itself as W . If T nM [sig(M) ; then T nM contains no separability causing axioms. Otherwise, we consider W to be equal to the top half of T n M (we treat T n M as an ordered set). We then check if W [sig(M) ; and, if this is the case, we grow W from the bottom and if not, we half it again as shown in Theorem 1. Given an acyclic ALCQI TBox T and signature the algorithm in Figure 1 computes the unique minimal depleting -module s.t. T n M contains no direct [ sig(M)-dependencies.
T nM00 [sig(M00) ;, M 6 dependencies.
Note that the minimality condition in the theorem means that for any M0 that T n M0 has no direct [ sig(M0)-dependencies and T n M0 we have M M0. It is, however, still possible that there exists a M00 M00 and such that T nM00 has some direct
T such [sig(M0) ;
T with [sig(M00)Example 1. We apply the algorithm in Figure 1 to the following acyclic TBox T inspired by the NCI Thesaurus (we have simplified some axioms and abbreviated ‘kidney’ with K, ‘ureter’ with U and ‘tract’ with T)
Renal Pelvis and U v 9partOf:K and U (
The algorithm in Figure 2 splits Lhs (T ) into two parts, lastAdded = f(
It can be seen that neither R1 nor R2 applies to T nM = f(4)g and the computation
concludes with M = f(
It is often the case (e.g., for the NCI Thesaurus) that a real-world ontology satisfies all conditions for acyclic TBoxes with the exception that it contains multiple concept inclusions of the form A v C1; : : : ; A v Cn. We call such TBoxes acyclic with repeated concept inclusions. Clearly, one can convert such a TBox into an equivalent acyclic TBox by replacing all repeated concept inclusions of the form A v C1,. . . , A v Cn with A v C1 u: : :uCn. However, such an explicit conversion is an unattractive solution for module extraction because if such an axiom is added to a -module the signature of the module now contains every symbol in the definition of every repeated name increasing the size of the resulting module considerably. The approach we take to handle acyclic TBoxes with repeated concept inclusions is to introduce fresh concept names for different repeated occurrences of a concept name in the left-hand side of concept inclusions, extract modules from the resulting acyclic TBox and then substitute away the added names as follows.
Theorem 2. Let T be an acyclic TBox with repeated concept inclusions and a signature. Let T 0 consist of all A ./ C 2 T which are not repeated in T and all A01 v C1; : : : ; A0n v Cn; A v A01 u : : : u A0n, where A v C1,. . . , A v Cn are all concept inclusions in T with A on the left hand side, n > 1, and A01; : : : ; A0n are fresh concept names.
Let M0 be a depleting -module of T 0 and let M be obtained from M0 by dropping the added axioms of the form A v A01 u : : : u A0n and by replacing every occurrence of the introduced symbols A01; : : : ; A0n with A. Then M is a depleting -module of T . 4
Experiments and Evaluation We implemented the algorithm presented in Figure 1 and the refinement for acyclic TBoxes with repeated concept inclusions in the AMEX system which is written in Java aided by the OWL-API library [5] for ontology manipulation. The inseparability check was implemented using the reduction to the validity of Quantified Boolean Formulae (QBF) and uses the QBF solver sKizzo [2].
To evaluate the efficiency of AMEX and the size of the modules computed by AMEX we compare it to >? locality-based module extraction [3, 13] as implemented in the OWL-API library version 3.2.4.1806 (called STAR-modules for ease of pronunciation).
To evaluate the performance of both approaches we consider random and axiom signatures. To generate a random signature size n given a TBox T we take the set of all concepts in T , i.e. sig(T ) \ NC and select at random n symbols from this set. For each concept signature size we also include a percentage of role names randomly selected from sig(T ), varying between 0% which equates to just using a concept signature to 100% which would be equal to [(sig(T )\NR). For experiments on axiom signatures, for a given number m, we select at random m axioms from T and then extract a module for each of the signatures of selected axioms.
In our experiments we used the NCI Thesaurus version 08.09d taken from the Bioportal [15] repository. This version of NCI contains 116 515 logical axioms among which 87 934 are concept inclusions of the form A v C and 10 366 are concept equations of the form A C. In what follows, NCI?(v) denotes the TBox consisting of all such inclusions, NCI?( ) denotes the TBox consisting of all such equations, and NCI? denotes the union of both. All three TBoxes are acyclic (with repeated concept inclusions), so AMEX can be applied to them. NCI? together with the rest of the ontology 25%
100% iff D % (18 215 axioms) is called NCI and contains, in addition, role inclusions, domain and range restrictions, disjointness axioms, data properties, and 17 763 ABox assertions.
The majority of NCI? (all but 4 588 axioms) are E L-inclusions. The non-E L inclusions contain 7 806 occurrences of value restrictions. The signature of NCI? contains 68 862 concept and 88 role names.
Experiments with NCI and its Fragments The results given in Figure 3 show the average sizes (over 1 000 random signatures for each signature size and role percentage combination) of the modules computed by the two approaches for random signatures. It can be seen that – in NCI?(
), AMEX-modules are significantly smaller than STAR-modules (between 270% and 780%); – in NCI?(v), STAR-modules are, on average, slightly smaller than AMEX modules; – in NCI?, AMEX-modules are still significantly smaller than STAR-modules, but less so than in NCI?( ).
The huge difference between modules in NCI?(v) and NCI?( ) can be explained as follows: it is shown in [8] that for acyclic E L-TBoxes without concept equations, AMEX-modules and STAR-modules coincide. This is not the case for acyclic ALCQI TBoxes (there can be axioms in STAR-modules that are not AMEX-modules and vice versa), but since the vast majority of axioms in NCI?(v) are E L-inclusions one should not expect any significant difference between the two types of modules. Thus, it is exactly those acyclic TBoxes that contain many concept equations for which AMEXmodules are significantly smaller than STAR-modules (see Example 1 for an illustration). 2400 2200 2000 1800 y1600 c n1400 e u1200 q re1000 F800 600 400 200 0 00 00 0 0 0 0 0 0 0 0 0 0 0 0 0 00 00 20− 4200− 06400− 08600− 010080− M1020001−odu0410021−le s6100014−ize (1800061−#Ax0200018−iom0220002−s) 4020022− 2600042− 8020026− 0300028− 320030− 430032− 00 00 0 0 0 0 0 0 0 0 0 0 0 0 0 00 00 10− 2100− 03020− 04030− 05040− 06050− 07060− 00807− 00098− 000109− 1100001− 0120011− 1300021− 1400031− 0150041− 160015− 170016−
Module size (#Axioms)
Experiments with full NCI Although AMEX-modules are significantly smaller than STAR-modules for acyclic TBoxes containing many concept equations, the applications of AMEX alone are very limited since most ontologies contain additional axioms such as disjointness axioms, role inclusions, and domain and range restrictions. To tackle this problem we first observe that, in principle, AMEX can be applied to any general TBoxes: given such a TBox T , one can split T into two parts T1 and T2, where T1 is an acyclic ALCQI-TBox (and as large as possible) and T2 := T n T1. Then for any signature it follows from the robustness properties [7] of the inseparability relation that if M is a depleting [ sig(T2)-module of T1 (note that M can be computed by AMEX), then M [ T2 is a depleting -module of T as well. Such a direct application of AMEX to general TBoxes is unlikely to compute small modules when T2 is large. However, our first experimental results suggest that this approach is beneficial when iterated with STAR-module extraction. The following result provides the theoretical underpinning for our experiments.
Theorem 3. Let M M0 T be TBoxes and a signature such that M0 is a depleting -module of T and M is a depleting -module of M0. Then M is a depleting -module of T .
Since both AMEX and STAR compute depleting -modules, given a signature and ontology T one can extract an AMEX module from the STAR module (and vice versa) and have the guarantee the resulting module is still a depleting -module of T . In this way, one can repeatedly extract from the output of one extraction approach again a module using the other approach until the sequence of modules becomes stable.
The following experiments are based on a naïve implementation of this hybrid approach and extract modules from the full version of NCI. Again we consider random concept signatures with varying amount of role names. The experiments shown in Figure 5 are based on 200 signatures for each concept signature size/role percentage combination and compare the average size of modules extracted using the hybrid approach and using STAR extraction only.
Role% 0% 25% 50% 75% 100% j j traS ttIreaed iffD% traS ttIreaed iffD% traS ttIreaed iffD% traS ttIreaed iffD% traS ttIreaed iffD% 100 5385.7 1949.5 176% 9569.8 6177.7 55% 13733.8 10339.0 33% 19486.4 16089.1 21% 23196.6 19810.2 17% 250 7298.6 3268.7 123% 11959.8 7963.9 50% 16072.1 12069.6 33% 20974.9 16978.8 24% 25141.0 21134.7 19% 500 9445.0 4827.6 96% 13165.1 8533.4 54% 16406.7 11767.0 39% 23046.8 18418.3 25% 27331.2 22691.9 20% 750 11070.2 6058.6 74% 15268.3 10235.9 49% 19696.2 14683.3 34% 23705.7 18689.6 27% 28917.3 23903.4 21% 1000 12370.7 7108.5 74% 16434.7 11174.0 47% 21978.6 16737.6 31% 25529.0 20286.5 26% 30218.5 24965.4 21%
For all signatures we found a reduction in the size of the module when iterated with the STAR module on its own being between 17% and 176% larger than the hybrid module.
In Figure 6, we show the results of our experiments for axioms signatures. They are based on 20 000 randomly selected axioms from the full NCI Thesaurus. 13% of such signatures showed a difference from the STAR module. The frequency of module sizes for the cases when the modules differ is given in Figure 6. The average difference in size, for the cases when there is a difference, is 295.2 axioms.
All individual extractions using the hybrid approach saw exactly 2 alternations of the STAR module extraction whereas the AMEX extraction varied between 1 and 2 times. The cases in which the AMEX extraction alternated just once happened much more often as the signature sizes grew and the difference between the respective module sizes became smaller. The additional time taken to extract the hybrid module compared to the STAR extraction alone was at most only 2.2 seconds.
y c n e u q e r F We have presented a new system, AMEX, for depleting module extraction from acyclic ALCQI-TBoxes. Using the NCI Thesaurus, we have compared the size of AMEXmodules with the size of >? -modules computed by the OWL-API library implementation (referred as STAR-modules) and we have presented a hybrid approach in which STAR and AMEX-module extraction are used iteratively. The results show that for TBoxes with many axioms of the form A C, AMEX-modules can be significantly smaller than STAR-modules and that an iterative approach can lead to significantly smaller modules than ‘pure’ STAR-modules. In contrast to [4], where a large number of ontologies are used to compare STAR-modules and MEX-modules we consider NCI only. The reason is that the majority of ontologies considered in [4] contain no (or only a very small set) of axioms of the form A C that form an acyclic subset of the ontology. For such ontologies it follows both from theoretical results in [8] and experimental results in [4] that there is no significant difference between AMEX and STAR-modules. Instead, we focus on a high quality ontology with a reasonable number of concept equations and where theory predicts that minimal depleting modules can be much smaller than STAR-modules. Many research questions remain to be explored. In particular, to apply AMEX to a larger class of ontologies in an iterative approach, one has to generalise the notion of acyclic TBoxes in such a way that the underpinning methodology of AMEX can still be generalised. 2. M. Benedetti. sKizzo: a QBF decision procedure based on propositional skolemization and symbolic reasoning. Technical Report 04-11-03, ITC-irst, 2004. 3. B. Cuenca Grau, I. Horrocks, Y. Kazakov, and U. Sattler. Modular reuse of ontologies: theory and practice. Journal of Artificial Intelligence Research (JAIR), 31:273–318, 2008. 4. C. Del Vescovo, P. Klinov, B. Parsia, U. Sattler, T. Schneider, and D. Tsarkov. Empirical study of logic-based modules: Cheap is cheerful. Technical report, University of Manchester, 2013. 5. M. Horridge and S. Bechhofer. The OWL API: A Java API for OWL ontologies. Semantic
Web, 2(
Musen. Bioportal: enhanced functionality via new web services from the national center for biomedical ontology to access and use ontologies in software applications. Nucleic Acids Research, 39(Web-Server-Issue):541–545, 2011.