Minimal Module Extraction from DL-Lite Ontologies Using QBF Solvers

1 Introduction

In computer science, ontologies are used to provide a common vocabulary (used here synonymously with 'signature') for a domain of interest, together with a description of the relationships between terms built from the vocabulary. Module extraction-the problem of finding a (minimal) subset of a given ontology that provides the same description of the relationships between terms over a given sub-vocabulary as the whole ontology-has recently become an active research topic in various ontology-related areas such as the semantic web and description logic; see, e.g., the recent volume on ontology modularisation [Parent et al., 2009] and the WoMO workshop series devoted to this problem [Haase et al., 2006; Cuenca-Grau et al., 2007]. The reasons for this are manifold, with one of the most important being ontology re-use. It is often impossible and not even desirable to develop an entirely new ontology for every new application; a better methodology is to re-use appropriate existing ontologies. However, typically only a relatively small part of the vocabulary of a possibly large ontology is required, that is, one only needs a subset, or module, of the ontology that gives the same description of this sub-vocabulary. Extracting such a module is the problem we are concerned with in this paper.

The phrase 'gives the same description of the vocabulary' (formalised below as a family of equivalence relations, one for each signature, and called an inseparability relation) is rather vague and has been interpreted in a variety of different ways, ranging from structural approaches [Noy and Musen, 2004; Seidenberg and Rector, 2006] to logic-based approaches [Cuenca-Grau et al., 2006; 2008; Konev et al., 2008]. While structural approaches use, and depend on, the syntax of the axioms of ontologies and mostly only take into account the induced is-a hierarchy, logic-based approaches consider the consequences of ontologies and require these to be the same for the relevant vocabulary. Although theoretically attractive and elegant, the logic-based approaches suffer from the high computational complexity of the problems to be solved: even checking whether two ontologies imply the same concept inclusions over a given signature is typically one exponential harder than standard reasoning problems (e.g., for ALC ontologies this problem is 2EXPTIME-complete [Ghilardi et al., 2006]). In [CuencaGrau et al., 2008], this difficulty has been addressed by developing a tractable (even for SHIQ) syntactic locality-based module extraction algorithm, the only disadvantage of which is that the extracted modules are typically not minimal. The only existing practical (and tractable) logic-based algorithm capable of extracting minimal modules was developed for acyclic EL-ontologies [Konev et al., 2008].

The main goal of this paper is to introduce a framework for module extraction based on the notion of inseparability between ontologies and to demonstrate that a purely logicbased approach to minimal module extraction is feasible in practice for large-scale DL-Lite ontologies.

The DL-Lite family of description logics [Calvanese et al., 2005; 2006] has been originally designed with the aim of providing query access to large amounts of data via a high level conceptual (ontological) interface. Thus, the DL-Lite logics resulted from various compromises between the necessity of keeping the complexity of query answering low and the desire of having the expressive means for representing various constraints of data modelling formalisms such as the ER model and UML class diagrams [Artale et al., 2007b]. For example, the logic DL-LiteNbool [Artale et al., 2007a; 2009] (containing many other DL-Lite logics) can express is-a hierarchies of concepts; disjointness and covering constraints for concepts; domain, range and cardinality constraints for roles; and multiplicity constraints for attributes. Therefore, standard reasoning in DL-LiteNbool (say, testing concept satisfiability) is NP-complete and, similarly to ALC, the main reasoning tasks required for module extraction are even harder: deciding whether two DL-LiteNbool ontologies imply the same concept inclusions over a given signature or whether they give the same answers to conjunctive queries for arbitrary ABoxes over this signature is Πp2 -complete [Kontchakov et al., 2008].

The contribution of this paper is as follows. We present generic algorithms extracting minimal logic-based modules from DL-LiteNbool ontologies which call (quadratically often, in the worst case) an oracle deciding whether an appropriate inseparability relation holds between DL-LiteNbool ontologies. In our experiments with two large-scale DL-LiteNbool ontologies, the oracle is realised using encodings into quantified Boolean formulas (QBFs) and solving these with the selfadaptive multi-engine QBF solver AQME [Pulina and Tacchella, 2009]. A significant speed-up is achieved by first extracting the (typically non-minimal) locality-based module and then applying to it the above mentioned algorithms. Finally, we provide a comparison of the sizes of the modules extracted for various logic-based notions of modules as well as existing structure-based notions of modules.

2 Inseparability modules

We begin by introducing an abstract notion of inseparability between ontologies w.r.t. a given signature and by investigating corresponding minimal module extraction algorithms. This notion, as well as the algorithms, do not depend on the underlying ontology language. However, to be precise, we introduce it for ontologies given as DL-LiteNbool TBoxes only. The language of DL-LiteNbool TBoxes is based on concept names A1, A2, . . . and role names P1, P2, . . . , with complex roles R and concepts C defined as follows:

where q ≥ 1. (Other concept constructs like ∃R, ≤ qR and C1 ⊔ C2 will be used as standard abbreviations.) As usual, a concept inclusion is of the form C1 ⊑ C2, where C1 and C2 are concepts, and a DL-LiteNbool TBox is a finite set of concept inclusions. A signature is a finite set of concept and role names. Given a concept, role, concept inclusion or TBox E, we denote by sig(E) the signature of E, that is, the set of concept and role names that occur in E.

An inseparability relation S = {≡SΣ| Σ a signature} is a family of equivalence relations ≡SΣ on the set of DL-LiteNbool TBoxes. Intuitively, T1 ≡SΣ T2 means that T1 and T2 are indistinguishable w.r.t. (or give the same description of) the signature Σ. We call an inseparability relation S monotone if it satisfies the following conditions, for all TBoxes T1, T2, signatures Σ and ≡SΣ in S:

Condition (Msig) formalises the intuition that if two TBoxes are indistinguishable w.r.t. a certain signature, then they are indistinguishable w.r.t. any smaller signature; (MT) demands that any TBox sandwiched between two indistinguishable TBoxes should be indistinguishable from either of them.

We now introduce three distinct notions of modules induced by an inseparability relation.

Definition 1 Let S be an inseparability relation, T a TBox, M ⊆ T , and Σ a signature. We say that M is

• an SΣ-module of T ifM≡SΣ T ;
• a self-contained SΣ-module of T ifM≡SΣ∪sig(M) T ;
• a depleting SΣ-module of T if ∅ ≡SΣ∪sig(M) T \M.

M is a minimal (self-contained, depleting) SΣ-module of T if M is a (self-contained, depleting) SΣ-module of T , but no proper subset of M is such an SΣ-module of T .

If S satisfies (Msig) then every self-contained SΣ-module is an SΣ-module; see below for examples showing that no other inclusion between these different types of modules holds in general. We start our investigation by considering minimal SΣ-modules. The following theorem presents a straightforward algorithm extracting one minimal SΣ-module from a given TBox, using an oracle deciding SΣ-inseparability.

input T ,Σ M := T for each α ∈M do if M \ {α} ≡SΣ M then M := M \ {α} end for output M

Proof The algorithm computes an SΣ-moduleMof T such that M\ {α} is not an SΣ-module of T , for any α ∈ M. By (MT), no proper subset of M is an SΣ-module. ❑

Note that the minimal SΣ-module extracted by this algorithm depends on the order of picking the axioms α. There exist natural inseparability relations (see below) for which there are exponentially many distinct minimal SΣ-modules. Consider, e.g., an ontology {α1, β1, . . . , αn, βn}, where αi and βi are syntactically different but SΣ-inseparable axioms.

Denote by |T | the size of T , that is, the number of occurrences of symbols in it. Then the algorithm runs in linear time in |T | calling an oracle deciding ≡SΣ at most |T | times.

Self-contained SΣ-modules are indistinguishable from the original TBox not only w.r.t. Σ but also w.r.t. their own signature. To discuss depleting SΣ-modules, we require two additional conditions on inseparability relations.

Definition 3 We say that an inseparability relation S is

• robust under replacement if, for all TBoxes T , T1, T2 and signatures Σ, we have T1 ∪ T ≡SΣ T2 ∪ T whenever T1 ≡SΣ T2 and sig(T ) ∩ sig(T1 ∪ T2) ⊆ Σ;
• robust under vocabulary extensions if, for all TBoxes T1, T2 and signatures Σ ⊆ Σ′ such that sig(T1∪T2)∩Σ′ ⊆ Σ we have T1 ≡SΣ′ T2 whenever T1 ≡SΣ T2.

Robustness is fundamental for ontology re-use. Suppose an ontology developer imports an SΣ-module M of a TBox T into her own ontology O because she is interested in the relations between terms over Σ defined by T . Then, if S is robust under replacement and vocabulary extensions, we have O ∪ T ≡SΣ′ O ∪M for every signature Σ′ such that Σ′ ∩sig(T ) ⊆ Σ and sig(T )∩sig(O) ⊆ Σ′ . Thus, these properties ensure that it does not make any difference whether she imports T or some SΣ-moduleMof T into O, and this does not depend on O.

Proposition 4 If S is an inseparability relation that is robust under replacement, then every depleting SΣ-module is a selfcontained SΣ-module.

Proof If T \M≡SΣ∪sig(M) ∅, robustness under replacement implies T = (T \M) ∪M≡SΣ∪sig(M) ∅ ∪M=M. ❑

We will consider depleting SΣ-modules only if S is robust under replacement and, therefore, only if they are selfcontained modules as well.

Theorem 5 Let S be a monotone inseparability relation that is robust under replacement, T a TBox, and Σ a signature. Then there is a unique minimal depleting SΣ-module of T , which is computed by the following algorithm:

input T ,Σ T ′ := T ; Γ := Σ; W := ∅ while T ′ \W ̸= ∅ do choose α ∈ T ′ \W W := W ∪ {α} if W ̸≡SΓ ∅ then T ′ := T ′ \ {α}; W := ∅; Γ := Γ ∪ sig(α) endif end while output T \ T ′

Proof Let Mbe a minimal depleting SΣ-module of T . The crucial observation for proving correctness of the algorithm and uniqueness of M is that, if T0 ⊆ T is minimal with T0 ̸≡SΣ ∅, then T0 ⊆ M. Suppose this claim does not hold, i.e., X ≡SΣ ∅, where X = M∩ T0. By robustness under replacement, (T \M) ∪ X ≡Ssig(M)∪Σ X. By (MT), ∅ ⊆ T0 ⊆ (T \M) ∪ X implies T0 ≡Ssig(M)∪Σ X, and so, by (Msig), T0 ≡SΣ ∅, which is a contradiction. ❑

The algorithm above computes the minimal depleting SΣmodule in quadratic time by calling the oracle deciding ≡SΣinseparability at most |T |2 times.

By the result above, minimal depleting modules have the advantage of being uniquely determined (under mild conditions), which sharply contrasts with the behaviour of the other types of modules. Another advantage is that depleting modules support modular ontology development in the following sense. SupposeMis a depleting SΣ-module of T and S is robust under replacement and vocabulary extensions. Then one can import into the ontology T \Many moduleM′ such that sig(M′ )∩sig(T ) ⊆ Σ∪sig(M) and be sure that T \Mdoes not interfere with M′ ; i.e., (T \M) ∪M′ ≡SΣ′ M′ whenever Σ′ ∩ sig(T \M) ⊆ Σ∪ sig(M). The importance of this property was first pointed out in [Cuenca-Grau et al., 2008] in the context of conservative extensions and modularity.

3 Two inseparability relations in DL-LiteNbool

The framework and algorithms presented above can be instantiated with ontologies in any standard DL and with numerous different choices for inseparability relations. Here we consider two inseparability relations between DL-LiteNbool ontologies which have both been introduced and investigated in [Kontchakov et al., 2008]. To give precise definitions of these relations, we require some notation. A DL-LiteNbool ABox A is a set of assertions of the form C(ai), R(ai, aj), where C is a concept, R a role, and ai, aj are object names from an infinite list of object names a1, a2, . . . . A DL-LiteNbool knowledge base (KB, for short) is a pair K = (T ,A) with a TBox T and an ABox A. The semantic notions of an interpretation, I, a concept inclusion C1 ⊑ C2 being satisfied in I, and of I being a model of a TBox, ABox and KB are standard and can be found in [Kontchakov et al., 2008]. A concept inclusion C1 ⊑ C2 follows from T , T |= C1 ⊑ C2 in symbols, if every model of T satisfies C1 ⊑ C2. An essentially positive existential query (simply a query) is a first-order formula

where ϕ is constructed from atoms of the form C(t) and R(t1, t2), with C being an DL-LiteNbool -concept, R a role, and ti being either an object name or a variable from the list x1, . . . , xn, y1, . . . , ym, using only ∧ and ∨. Given a KB K and a query q(x), x = x1, . . . , xn, we say that an n-tuple a of object names is an answer to q(x) w.r.t. K and write K |= q(a) if, for every model I of K, we have I |= q(a).

Given an ABox or query E, we denote by sig(E) the signature of E, that is, the set of concept and role names that occur in E. A concept (role, concept inclusion, TBox, ABox, query) E is called a Σ-concept (role, concept inclusion, TBox, ABox, query, respectively) if sig(E) ⊆ Σ.

Definition 6 Let T1 and T2 be DL-LiteNbool TBoxes and Σ a signature. We say that T1 and T2 are Σ-concept inseparable and write T1 ≡cΣ T2 if, for all Σ-concept inclusions C ⊑ D in DL-LiteNbool , we have T2 |= C ⊑ D iff T1 |= C ⊑ D. The corresponding inseparability relation will be denoted by Sc .

T1 and T2 are said to be Σ-query inseparable (T1 ≡qΣ T2, in symbols) if, for all Σ-ABoxes A, Σ-queries q(x) and tuples a of object names from A, we have (T1,A) |= q(a) iff (T2,A) |= q(a). The corresponding inseparability relation will be denoted by Sq .

We believe that Sq , the inseparability relation which regards ontologies as indistinguishable w.r.t. Σ if they give the same answers to Σ-queries for any Σ-ABox A, is the most appropriate inseparability relation for typical applications of DL-LiteNbool ontologies: recall that the design goal of DLLite was to provide a conceptual interface for querying instance data. As the data is usually not known in advance and may change, it is unrealistic to assume that the ABox is fixed when extracting a module: that is why in our approach we regard ABoxes as 'black boxes.' One could argue that instead of existential queries one should consider the smaller class of conjunctive queries when defining inseparability (and thus obtain smaller minimal modules). However, as shown in [Kontchakov et al., 2008], when considering conjunctive

1. Publisher ⊑ ∃pubHasDistrib
2. Publisher ⊑ ∃pubAdmedBy
3. User ⊑ ¬Publisher
4. ∃pubHasDistrib- ⊑ Distributor (9) ∃pubAdmedBy- ⊑ AdmUser ⊔BookUser (16) Role ⊑ ¬User
5. Publisher ⊑ ¬Distributor
6. AdmUser ⊑ User
7. User ⊑ ∃userAdmedBy

(4) ∃pubHasDistrib ⊑ Publisher

1. BookUser ⊑ User
2. ∃userAdmedBy- ⊑ AdmUser
3. Publisher ⊑ ≤ 1pubHasDistrib (12) User ⊑ ∃hasRole
4. ∃userAdmedBy ⊑ User
5. Role ⊑ ¬Distributor
6. ∃hasRole- ⊑ Role
7. ∃pubAdmedBy ⊑ Publisher
8. User ⊑ ¬Distributor
9. Role ⊑ ¬Publisher

Figure 1: 'Publisher' ontology T .

queries instead of existential ones, one loses the robustness properties of the corresponding inseparability relation. The next theorem follows from [Kontchakov et al., 2008].

Theorem 7 Sc and Sq are monotone and robust under vocabulary extensions; Sq is robust under replacement, Sc is not.

It follows from Proposition 4 that depleting Sq -modules are self-contained Sq -modules. This implication fails for Sc : Example 8 Let T = {A ⊑ ∃R, ∃R- ⊑ B, B ⊑ ⊥}, Σ = {A,B} and M = {B ⊑ ⊥}. Then M is a depleting ScΣmodule of T (because {A ⊑ ∃R, ∃R- ⊑ B} ≡cΣ ∅), but it is not a self-contained ScΣ-module of T (because T |= A ⊑ ⊥). For this reason we will not consider depleting Sc -modules in what follows. Note also that minimal depleting SqΣ-modules are in general larger than self-contained SqΣ-modules. Take, e.g., T = {A ⊑ B,A ⊑ B ⊓ B} and Σ = {A,B}. Then M1 = {A ⊑ B} and M2 = {A ⊑ B⊓B} are self-contained SqΣ-modules, but T itself is the only depleting SqΣ-module.

Example 9 Consider the DL-LiteNbool TBox T shown in Fig. 1 (it is part of the larger Core ontology to be discussed in the next section), and let Σ = {Publisher}. First observe that the minimal ScΣ-module of T is empty, which is typical for singleton signatures and Sc , as no interesting concept inclusions over a singleton signature exist. In contrast, there are three different minimal SqΣ-modules of T :

• MD containing axioms (1)-(3),
• MR containing axioms (8)-(14), and
• MU with axioms (8)-(11) and (15).

First, they are indeed SqΣ-modules of T , i.e., Σ-query inseparable from T . This can be verified via the semantic criterion [Kontchakov et al., 2008, Lemma A.4]. Second, they are minimal: consider the ABox A = {Publisher(a)} and the query q = ∃x¬Publisher(x). Clearly, we have (T ,A) |= q, while (T ′ ,A) ̸|= q, for any proper subset T ′ of MD, MR or MU. In contrast to this finding, the minimal depleting SqΣ-module of T is T itself. Consider now Σ′ = {Publisher, pubHasDistrib}. Then the only minimal ScΣ′ -module of T consists of axioms (1)-(5) and there are two minimal SqΣ′ -modules: M+R = MD ∪ MR ∪ {(4), (5), (6)} and M+U = MD ∪ MU ∪ {(4), (5), (7)}.

4 Practical Minimal Module Extraction

We have conducted experiments with three types of minimal module extraction: for a DL-LiteNbool TBox T and a signature Σ, extract some minimal ScΣ-module (MCM) of T , some minimal SqΣ-module (MQM), and the minimal depleting SqΣmodule (MDQM) of T . In principle, these extraction problems can be solved using the algorithms presented in Theorems 2 and 5 together with the 'oracles' from [Kontchakov et al., 2008] capable of deciding the (Πp2 -complete) problems 'T1 ≡cΣ T2' and 'T1 ≡qΣ T2.' The oracles were realised by encoding these two problems as satisfiability problems for certain (∀∃) quantified Boolean formulas, and first experimental results indicated that standard off-the-shelf QBF solvers such as SKIZZO [Benedetti, 2005], 2CLSQ [Samulowitz and Bacchus, 2006] and QUBE [Giunchiglia et al., 2006] can be successfully used to check satisfiability of the resulting QBFs.

Unfortunately, a na¨ıve implementation of this approach turns out to be hopelessly inefficient. In a nutshell, the main reasons are as follows. First, to extract a minimal module from an ontology with 1K axioms, even for 'typical' realworld examples the algorithm would call the oracle about 500K times. Second, as was discovered in [Kontchakov et al., 2008], no existing QBF solver could cope alone with all the inseparability tests and, even when the solver is successful, the runtime is quite unpredictable and can range from a few seconds to a few hours. The good news, however, is that all the three solvers we used did solve about 99% of tests. (Note that the QBF encodings of our tests below contain up to 232,600 clauses, 710,000 literals and 23,300 variables.) To deal with these problems we have implemented three ideas:

1. To reduce the number of oracle calls, we optimised the algorithms by checking a group of axioms rather than a single axiom at a time (in practice, this reduced the number of calls to 1-3K for a 1K ontology).
2. To select 'the best' QBF solver for a given instance, we used the self-adaptive multi-engine QBF solver AQME [Pulina and Tacchella, 2009], a tool capable of choosing a QBF engine with 'more chances' to solve a given input and learning its engine-selection strategies.
3. To reduce the size of the original ontology, we 'preprocessed' it by means of a tractable syntactic locality-based algorithm from [Cuenca-Grau et al., 2008] extracting the ⊤⊥- module (⊤⊥M), which contains all the minimal modules we are interested in. In fact, we have the following inclusions

where the first one should be read as 'every MQM contains some MCM,' the second as 'every MQM is contained in the MDQM,' and the third as 'the MDQM is contained in the ⊤⊥M.' Thus we can use these inclusions by computing modules from right to left.

Ontologies. Our test ontologies are DL-LiteNbool encodings of two real-world commercial software applications called 'Core' and 'Umbrella.' The Core ontology is based on a supply-chain management system used by the bookstore chain Ottakar's, now rebranded as Waterstone's. It contains 1283 axioms, 83 concept and 77 role names, and features numerous functionality, covering and disjointness constraints, and quite a few concepts of the form ≤ q R with q > 2. The Umbrella ontology is based on a specialised research data validation and processing system used by the Intensive Care National Audit and Research Centre (http://www.icnarc.org). It contains 1247 axioms, 79 concept and 60 role names. Both ontologies are representations of the relevant data structures and were constructed by analysing the data model, database schema and application-level business logic. The Publisher ontology in Fig. 1 is part of Core; full Core and Umbrella are available at http://ijcai09.tripod.com/.

Using AQME. An important property of AQME is that it can update its learned policies when the usage scenario changes substantially, by using an adaptation schema called retraining. Prior to module extraction, AQME computes a selection of syntactic features (characterising this particular problem) from a pool of suitable QBF instances. In view of the findings of [Kontchakov et al., 2008], we used only 3 engines out of the usual 8: 2CLSQ, QUBE and SKIZZO. A typical run of AQME is as follows. First, it leverages its inductive model (built using 1-nearest-neighbour) to predict the best engine for the given input QBF. If the engine solves the QBF, AQME terminates and returns the answer. Otherwise, AQME starts its self-adaptive mechanism. It calls a different engine to solve the input formula. If it is successful, the retraining procedure is called and the inductive model is updated. Which engine is called for retraining and how much CPU time is granted to each engine are critical points for AQME's performance. Our solver selection strategy, ALG, relies on the engine type, which can be search-based, like QUBE or 2CLSQ, or Skolemisation-based, like SKIZZO: the failed solver is replaced by a solver of a different type. Our CPU time strategy is as follows: a fixed amount of CPU time is granted to the predicted solver; if it fails, another engine is called, using the ALG strategy, with a granted amount of CPU time that increases in each iteration, until the solver solves the input formula. In fact, this approach combines the TPE and ITR techniques from [Pulina and Tacchella, 2009]. An important difference from the original version of AQME is the new data management at the retraining phase. As AQME had to deal with a huge number of instances, which could all be used for training and therefore cause a substantial slowdown, we bounded the number of entries in the training set: when the bound is reached, the older entry is replaced by the newer one.

Modules for |Σ| = 1. Our first experiment was to extract the modules of all three types, for all singleton signatures, from the full Core and Umbrella ontologies and from the corresponding pre-computed ⊤⊥Ms. For instance, the extracted MCM, MQM, and MDQM of Core for Σ = {Publisher} are given in Example 9 and contain 0, 3, and 20 axioms, respectively, whereas the corresponding ⊤⊥M has 228 axioms.

The following table summarises the results of the experiments (on average per module) in terms of module sizes and other relevant parameters, where the italicised numbers refer to extraction from the full ontologies. It also contains the average sizes of the segments extracted using the approaches described in [Seidenberg and Rector, 2006] (SR), [Noy and Musen, 2004] (Prompt), and [Cuenca-Grau et al., 2006] (Econn). Since these approaches do not support role names in the initial signature, we have only extracted modules for concept names in these cases. Furthermore, SR and Prompt are not logic-based and do not, in general, preserve entailments. (The Publisher-segments for SR, Prompt, and E-conn contain 19, 189, and 349 axioms, respectively.)

The distribution of calls to the QBF engines changes notably if MDQMs are extracted from the whole ontology rather than from the ⊤⊥Ms: in the former case, the majority of calls is issued to SKIZZO, while QUBE handles most of the calls in the latter case. This complies with the observation that, in general, QUBE tends to solve easy instances more quickly, and SKIZZO performs more successfully on harder instances.

Modules for |Σ| = 10. For each of our ontologies, we randomly generated 30 signatures of 10 concept names each and extracted all possible modules; their average sizes are shown in Fig. 2. MCMs and MQMs were extracted from MDQMs, which in turn were extracted from ⊤⊥Ms. Again, in most of the AQME calls (1302/1694 for MDQMs and 152/181 for MCMs, on average) QUBE was invoked. The average runtime for MDQMs (MCMs) was around 30 (1.5) minutes.

It is to be noted that we have only been able to extract 17 MQMs for Umbrella and 8 MQMs for Core because the runtime for certain instances increases to a couple of days. One of the reasons is the growth of the QBF instances generated whenever the algorithm needs to test inseparability between module candidates and the original ontology. In the case of MDQMs, a candidate's complement needs to be compared with the empty TBox, which can be done rather efficiently. The case of MCMs and MQMs involves many comparisons of two very similar TBoxes, which, for MQMs, leads to the generation of QBF instances that are quadratic in the number of roles involved (as opposed to linear for MCMs).

Modules for |Σ| = 5 + 5. A similar experiment was conducted with 30 random signatures consisting of 5 concept names and 5 role names. The results are summarised in Fig.3. Due to performance issues, we have no MQMs available at all here. For reasons mentioned above, we did not extract module for SR, Prompt, and E-conn either.

5 Conclusion

The main novel contributions of this paper are as follows:

(1) The definition of modules and reconstruction of their properties based on an abstract notion of inseparability formalising the intuitive notion that 'two ontologies give the same description of a vocabulary.' We believe that inseparability can be used to systematise the huge variety of distinct notions of modules in the literature.

(2) Experimental results demonstrating that, for DL-LiteNbool ontologies (and so many other logics in the DL-Lite family), minimal logic-based modules (in particular MDQMs and MCMs) can be extracted in practice using the multi-engine QBF solver AQME and locality-based module extraction. The experiments also show that QBF solvers can be used to solve complex real-world problems, though they are not as stable and scalable yet as the existing SAT solvers.

Many open problems remain. For example, for MQMs the performance of the tested extraction algorithms is rather unsatisfactory and further optimisations are required. Second, it is straightforward to extend the framework and algorithms to the case where modules are extracted for a given signature and a seed set M of axioms to be included in the module. One can thus combine different methodologies and, say, compute the logically correct closure of non-logic based modules M. It is of interest to evaluate this approach in practice.