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.
[sig(M) ;.
a signature. Then M is a depleting
Every depleting module M of T is inseparable from T for its signature and, in
particular, T M. It follows from results in [
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 E L and for acyclic ALC-TBoxes [
Assume that T1 and T2 are TBoxes and a signature. Then T1 and T2 are 1- inseparable, in symbols T1 1 T2, if fIj j ] I = 1 and I j= T1g = fIj j ] I = 1 and I j= T2g: If T1 and T2 are -inseparable, then they are 1- -inseparable. j j r a t S
0% X E M A d ir b y H
50% X E M A
NCI? p e d 1 0 0 2 /iff D r a t S d ir b y H p e d 1 0 0 2 i/ff D r a t S Definition 2. Let M -module of T if T n M 1 [sig(M) ;
.
depleting -module of T is a 1-depleting are a good candidate for approximating depleting modules from below. -module of T , so 1-depleting 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 -modules 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.
T n M should not contain direct indicate a semantic link between two distinct symbols in
Our upper approximation of depleting -modules is also based on
1but 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 fA; X g with A + X , where + is the transitive
T
T
closure of the relation T NC (NC [ NR) defined by setting A T X iff there exists
an axiom of the form A v 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 n M contains
direct [ sig(M)-dependencies (see [
-inseparability [ sig(M).
Theorem 2. Given an acyclic ALCQI TBox T and signature , the unique minimal depleting -module s.t. T n 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.
Experiments and Evaluation To evaluate how close depleting module extraction
algorithms can approximate minimal depleting modules we compared
– our new system AMEX, in which the inseparability check is implemented by
reduction to the validity of QBF and uses the QBF solver sKizzo [
In the full version of the paper [
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.