It is known that no algorithm can extract the minimal depleting Σ-module from ontologies in expressive description logics (DLs). Thus research has focused on algorithms that approximate minimal depleting modules 'from above' by computing a depleting module that is not necessarily minimal. The first contribution of this paper is an implementation (AMEX) of such a depleting module extraction algorithm for expressive acyclic DL ontologies that uses a QBF solver for checking conservative extensions relativised to singleton interpretations. To evaluate AMEX and other module extraction algorithms we propose an algorithm approximating minimal depleting modules 'from below' (which also uses a QBF solver). We present experiments based on NCI (the National Cancer Institute Thesaurus) that indicate that our lower approximation often coincides with (or is very close to) the upper approximation computed by AMEX, thus proving for the first time that an approximation algorithm for minimal depleting modules can be almost optimal on a large ontology in a non-tractable DL.

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 N C of concept names and N R of role names using the concept constructors defined by the DL. A signature Σ is a finite subset of N C ∪N R . The Σ-reduct I| Σ of an interpretation I is obtained from I by setting ∆ I| Σ = ∆ I , and X I| Σ = X I for all X ∈ Σ, and X I| Σ = ∅ for all X ∈ Σ. Let T 1 and T 2 be TBoxes and Σ a signature. Then T 1 and T 2 are Σ-inseparable, in symbols

Every depleting module M of T is inseparable from T for its signature and, in particular, T ≡ Σ M. It follows from results in [10] that T |= ϕ iff M |= ϕ holds for any second-order sentence ϕ using symbols from Σ only. Thus, a TBox and its depleting Σ-module can be equivalently replaced by each not only in applications using entailed CIs between Σ-concepts but also in data access applications with data given in Σ. For further discussion of the properties of depleting modules see [3,10].

Approximating Depleting Modules While the inseparability-based notion of a module has its theoretic appeal, 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 EL and for acyclic ALC-TBoxes [10,13]. Therefore, we introduce lower and upper approximations of depleting Σ-modules.

Assume that T 1 and T 2 are TBoxes and Σ a signature. Then T 1 and

In contrast to Σ-inseparability which is undecidable, 1-Σ-inseparability can be decided by reduction to the validity of quantified Boolean formulas (QBF). By definition, every depleting Σ-module of T is a 1-depleting Σ-module of T , so 1-depleting Σ-modules are a good candidate for approximating depleting modules from below.

Theorem 1. Given an ALCQI-TBox T and signature Σ, the unique minimal 1-depleting Σ-module of T can be computed in polynomial time with each call to a QBF solver treated as a constant time oracle call.

Our upper approximation of depleting Σ-modules is also based on 1-Σ-inseparability but uses an additional syntactic dependency check to ensure that a depleting module is extracted. Let T be an acyclic TBox and Σ a signature. We say that T has a direct Σ-dependency if there exists {A, X} ⊆ Σ with A ≺ + T X, where ≺ + T is the transitive closure of the relation ≺ T ⊆ N C ×(N C ∪N R ) defined by setting A ≺ T X iff there exists an axiom of the form A C or A ≡ C in T such that X occurs in C. Although one can construct TBoxes T and depleting Σ-modules M of T such that T \ M contains direct Σ ∪sig(M)-dependencies (see [10]), for typical depleting Σ-modules M, the set T \ M should not contain direct Σ ∪ sig(M)-dependencies because such dependencies indicate a semantic link between two distinct symbols in Σ ∪ sig(M).

Theorem 2. Given an acyclic ALCQI TBox T and signature Σ, the unique minimal depleting Σ-module s.t. T \ M contains no direct Σ ∪ sig(M)-dependencies can be computed in polynomial time with each call to the QBF solver being treated as a constant time oracle call.

our new system AMEX, in which the inseparability check is implemented by reduction to the validity of QBF and uses the QBF solver sKizzo [2]; -⊥ * locality-based module extraction [3,15] as implemented in the OWL-API library version 3.2.4.1806 (called STAR-modules for ease of pronunciation); a hybrid approach in which one iterates AMEX and STAR-module extraction. This results in a depleting module contained in both the AMEX and the STAR-module; the algorithm computing the minimal 1-depleting module. The inseparability check was again implemented using the reduction to the validity of QBF and uses sKizzo. We used fragments of the NCI Thesaurus version 08.09d taken from the Bioportal [20]. The results given in Table 1 show the average sizes of the modules extracted by the four algorithms from the set of CIs NCI ( ), the set of CEs NCI (≡) and the union of both NCI over 200 random signatures for each signature size combination of 100 to 1000 concept names and 0%, 50%, and 100% of role names. In addition, in each case we give the number of signatures (out of 200) in which there is a difference between the hybrid module and the minimal 1-depleting module. It can be seen that in NCI and NCI ( ) the hybrid module almost always coincides with the minimal 1-depleting module (and therefore with the minimal depleting module). in NCI (≡), in 50% of all cases the hybrid module coincides with the minimal 1-depleting module. On average the minimal 1-depleting module is less than 0.3% smaller than the hybrid module. in all three TBoxes, hybrid modules are only slightly smaller than AMEX-modules.

in NCI (≡), AMEX-modules are significantly smaller than STAR-modules.

in NCI ( ), STAR-modules are slightly smaller than AMEX modules.

in NCI , AMEX-modules are still significantly smaller than STAR-modules, but less so than in NCI (≡). In the full version of the paper [5] we also apply the hybrid approach and the lower approximation to the full NCI Thesaurus version 08.09d, which additionally contains role inclusions, domain and range restrictions, and disjointness axioms. The results are very similar to the results for NCI : hybrid modules are on average significantly smaller than STAR modules and are often identical to the minimal 1-depleting module.

We have shown that for the NCI Thesaurus one can compute efficiently depleting modules that are consistently very close to the minimal depleting modules and often coincide with the latter. The experiments also show that for TBoxes with many axioms of the form A ≡ C, AMEX-modules can be significantly smaller than STAR-modules and that a hybrid approach can lead to significantly smaller modules than 'pure' STAR-modules. This is only the first step towards a novel systematic evaluation of the quality of upper approximations of modules using lower approximations. It would be of great interest to compute lower approximations for a more comprehensive set of cyclic ontologies and compare them with the upper approximations given by STAR-modules and by the hybrid approach. It is also interesting to investigate n-depleting modules (based on inseparability for interpretations of size at most n) with n > 1. These modules can still be extracted by using QBF solvers and the same algorithm; the cost is much higher, though, since the length of the encoding into a QBF is exponential in n.