We consider the problem of extracting modules of an ontology that contains the knowledge as represented by a second ontology. The knowledge to be preserved is speci ed using entailment of conjunctive queries over a given vocabulary. We propose a novel module notion called projection module that preserves the answers to conjunctive queries as they follow from a reference ontology. We present an algorithm for computing minimal projection modules for conjunctive queries. As target and reference ontology we take ELHr-terminologies. The algorithm is based on simulation notions developed for detecting logical di erences between ELHr-terminologies.
Ontology comparison can help understanding the overlap and di erences among ontologies which is often desired while a user manipulates multiple knowledge sources. In this paper, we propose the notion of projection module which allows to compare the entailment capacities of two ontologies about a given vocabulary. A projection module characterizes the relative knowledge of one ontology by taking another one as a reference. This can thus lead to a ne-grained ontology comparison measurement between two ontologies.
Various approaches to comparing ontologies have been suggested, including
ontology mapping or alignment [
When an ontology has no logical di erence compared to another one, our approach further extracts sub-ontologies of the rst ontology that contain the ? This work is partially funded by the ANR project GoAsQ (ANR-15-CE23-0022). knowledge as represented by the second ontology. For example, suppose T1 = fA1 v A2; A2 v A3g, T2 = fA1 v A3 u B1; B1 v 9r:A3g, and = fA1; A3; rg. Then T2 entails all queries about that follow from T1. However, the projection module of T2 with respect to T1 and consists of A1 v A3 u B1. This means that a strict sub-ontology of T2 is su cient to capture all the information of T1 about . Moreover, T2 entails the consequence A1 v 9r:A3, which is not the case for T1. Intuitively, T2 is richer in information about than T1.
Ontology modularity [
To compute projection modules, in this paper, we generalize the notion of
justi cation to the notion of subsumption justi cation as a minimal set of axioms
that maintains a consequence. Our algorithm employs the classical notion of
justi cation to compute subsumption justi cation. Currently, the approaches
for computing all the justi cations of an ontology w.r.t. a consequence can be
classi ed into two categories: \glass-box" [
We proceed as follows. Section 2 gives a brief review of Description Logic E L and its extensions as well as logical di erence. In Section 3, we introduce the notion of project module. In Section 4, the notion and the computation of role subsumption justi cations are presented, which are employed in Section 5 to compute project modules. Finally, Section 6 concludes the paper. 2
We start by brie y reviewing the description logic E L and several of its
extension with range restrictions and conjunction of roles and the universal role as
well as concept subsumptions based on these extensions. For a more detailed
introduction to description logics, we refer to [
Let NC and NR be sets of concept names and role names. We assume these sets ranto be mutually disjoint and countably in nite. The sets of E L-concepts C, E L r concepts D, E Lu-concepts E, and E Lu;u-concepts F , and the sets of E LH inclusions and E Lran;u;u-inclusions are built according to the grammar rules: C ::= A j C u C j 9r:C j dom(r) D ::= A j D u D j 9r:D j dom(r) j ran(r) E ::= A j E u E j 9R:E F ::= A j F u F j 9R:F j 9u:F ::= C v C j ran(r) v C j ran(r) u C v C j C ::= D v F j r v s C j r v s where A 2 NC, r; s 2 NR, u is a fresh logical symbol (the universal role) and R = r1 u : : : u rn with r1; :::; rn 2 NR, for n 1. We refer to inclusions also as axioms. A -TBox is a nite set of -inclusions, where ranges over the sets of E LHr- and E Lran;u;u-inclusions.
The semantics is de ned as usual in terms of interpretations, which interpret concept and role names and are inductively extended to complex concepts. The notions of satisfaction of a concept, axiom and TBox as well as the notions of a model and the logical consequence relation are de ned as usual. We skip a detailed introduction here.
A signature is a nite set of symbols from NC and NR. We write sigNC ( ) and sig( ) for the set of concept names and the set of concept and role names occurring in a syntactic object . The symbol is used as a subscript to a set of concepts or inclusions to denote that the elements only use symbols from .
An E LHr-terminology T is an E LHr-TBox consisting of axioms of the form A v C, A C, r v s, ran(r) v C or dom(r) v C, where A is a concept name, C an E L-concept and no concept name occurs more than once on the left-hand side of an axiom.1 To simplify the presentation we assume that terminologies do not contain axioms of the form A B or A > (after removing multiple >-conjuncts) for concept names A and B. For a terminology T , let T be a binary relation over NC such that A T B i there is an axiom of the form A v C or A C in T such that B 2 sig(C). A terminology T is acyclic if the transitive closure T+ of T is irre exive; otherwise T is cyclic. A concept name A is said to be conjunctive in T i there exist concept names B1; : : : ; Bn, n > 0, such that A B1 u : : : u Bn 2 T ; otherwise A is said to be non-conjunctive in T .
An E LHr-terminology T is normalised i it only contains axioms of the
forms ' v B1 u : : : u Bn, A v 9r:B, A v dom(r), r v s, and A B1 u : : : u Bm,
A 9r:B, where ' 2 fA; dom(s); ran(s)g, n 1, m 2, A; B; Bi 2 NC, r; s 2
NR, and each conjunct Bi is non-conjunctive in T . Every E LHr-terminology T
can be normalised in polynomial time such that the resulting terminology is a
conservative extension of T [
We now recall the notion of logical di erence for concept subsumption queries,
instance queries and conjunctive queries from [
De nition 1 (Logical Di erence). The E Lran;u;u-subsumption query and conjunctive query di erence between T1 and T2 wrt. are the sets cDi (T1; T2) and qDi (T1; T2), where { ' 2 cDi (T1; T2) i ' is an E Lran;u;u-inclusion and T1 j= ' and T2 6j= '; { (A; q(a)) 2 qDi (T1; T2) i A is a -ABox and q(a) a -conjunctive query such that (T1; A) j= q(a) and (T2; A) 6j= q(a). 1 A concept equation A
C stands for the inclusions A v C and C v A.
The following theorem states that E Lran;u;u-subsumption queries are su
cient to detect the absence of conj. query di erences (Lemmas 62 and 63 in [
(T1; T2) = ; i qDi
(T1; T2) = ;.
If the set cDi (T1; T2) is not empty, then it typically contains in nitely many
concept inclusion. We make use of the primitive witnesses theorems from [
The set of all E Lran;u;u-subsumption di erence witnesses is de ned as
Wtn (T1; T2) := (roleWtn (T1; T2); lhsWtn (T1; T2); rhsWtn (T1; T2));
where the set roleWtn (T1; T2) consists of all type- 1 inclusions in cDi (T1; T2),
and the sets lhsWtn (T1; T2) ( \ NC) [ f dom(r) j r 2 g [ f ran(r) j r 2 g
and rhsWtn (T1; T2) NC \ of left-hand and right-hand subsumption query
di erence witnesses consist of the left-hand sides of the type- 3 inclusions in
cDi (T1; T2) and the right-hand sides of type- 2 inclusions in cDi (T1; T2),
respectively. Consequently, the set Wtn (T1; T2) can be seen as a nite
representation of the set cDi (T1; T2) [
A terminology T1 together with a signature and a query language Q determine a set of queries from Q formulated using only symbols from that follow from T1. Intuitively, captures the Q-knowledge of T1 about . In this paper, we consider conjunctive queries or, equivalently, E Lran;u;u-subsumption queries as a query language. A projection module for of another terminology T2 is a subset of T2 that entails the queries in . The Q-knowledge in of T1 about is captured by the projection module of T2 and it is represented using axioms from T2. The projection can be seen as transforming the nite representation of with axioms from T1 into a nite representation of with axioms from T2. As an application, the projection of onto T2 allows us to determine the axioms that implement in T2. For instance, projection modules enable the veri cation of compliance to certain modelling guidelines and standards by the axioms of T2 that implement . In particular, projection modules that are minimal w.r.t. set inclusion are relevant for this task. Note that existing module notions suggest to compute a module of T2 for the given signature, , to obtain the Q-knowledge of T2 about , whereas we are only interested in , i.e. the Q-knowledge of T1 about . Consequently, extracting modules of T2 for will yield modules that generally contain irrelevant axioms and that are, therefore, likely too large for manual inspection.
De nition 2 (Projection Module). Let = hT1; ; T2i be a projection setting. A set M T2 is a conjunctive query projection module under i for every -ABox A and every -conjunctive query q(a): (T1; A) j= q(a) implies (M; A) j= q(a).
There may exist several (even exponentially many) minimal projection modules. hT1; ; T2i is T2.
Example 1. Let T1 = fA1 v A4g, T2 = fA1 A2 u A3; A2 v A4; A3 v A4g and = fA1; A4g. Then the conjunctive query projection module under =
The notion of projection module is not symmetric, i.e., a projection module under hT1; ; T2i is not necessarily the same as a projection module under hT2; ; T1i. When the reference terminology equals the terminology from which axioms are to be extracted, a re exive projection setting of the form = hT ; ; T i is used. We call a projection module under also an automorphic projection module.
An interesting application of the projection module is to compare entailment capacities of two terminologies, as shown in the following example. Example 2. Let T1 = fAi v Ai+1 j 1 i ng, T2 = fA1 v An; B1 v B2g; = fA1; An; B1; B2g. Intuitively, T1 contains less information about than T2. The minimal projection module under = hT1; ; T2i is M = fA1 v Ang. By using jMj=jT2j = 1=2 as a measure, we see that only half of T2 is about the information of T1 w.r.t. . 4
In this section, we introduce justi cation notions for sets of inclusions and we show how they can be combined to obtain minimal projection modules. We start with de ning the notion of role subsumption justi cations for a set of E Lran;u;uinclusions of the form r v s, where r; s 2 (cf. Section 2).
De nition 3 (Role Subsumption Justi cation). Let = hT1; ; T2i. A set M is called a role subsumption module under i M T2 and for every r; s 2 NR \ , T1 j= r v s implies M j= r v s. A role subsumption justi cation under is the role subsumption module under that is minimal w.r.t. (.
We denote the set of all role subsumption justi cations under
Lemma 1. Let J 2 J R. Then roleWtn (T1; J ) = ;.
We continue with de ning the notion of subsumption justi cations for inclusions of E Lran;u;u that are of the form D v F , where D ranges over E Lranconcepts and F over E Lu;u-concepts.
= hT1; X1; ; T2; X2i, where T1 and T2 are normalised E LHr-terminologies, is a signature, X1; X2 2 NC [ f dom(r); ran(r) j r 2 NR g.
A set M is called a subsumer module under i M T2 and for every C 2 E Lran;u;u, T1 j= X1 v C implies M j= X2 vraCn;.u;Mu, Tis1 jc=alCledvaXs1ubi msupmlieees module under i M T2 and for every C 2 E L M j= C v X2.
M is called a subsumption module under i M is a subsumer module, a subsumee module under and role subsumption module under hT1; ; T2i. A subsumee (resp. subsumer, subsumption) justi cation under is a subsumee (resp. subsumer, subsumption) module under that is minimal w.r.t. (.
We denote the set of all subsumee (resp. subsumer, subsumption) justi cations under as J (resp. J !, J ), where = hT1; X1; ; T2; X2i.
Using De nition 1 and 4, we obtain the following proposition stating the absence of certain concept names, and domain and range restrictions of role names as left-hand and right-hand di erence witnesses between a reference terminology T1 and a subsumer and subsumee justi cation of a second terminology T2.
For a signature , let dom = f dom(t) j t 2 NR \ g and ran = f ran(t) j tev2erNyRr\ole ngambee tthienset,s rceosnpseicsttiivneglyo.fFcuorntcheeprtms oorfet,hleetform=dom[(t) adonmd[ran(ratn) ffoorr 2 C .
Lemma 2. Let ' 2 ( \ NC) [ dom [ ran and let A 2 let = hT1; '; ; T2; 'i and 0 = hT1; A; ; T2; Ai. Then: { ' 62 lhsWtn (T1; J ) for every J 2 J !; { A 62 rhsWtn (T1; J 0 ) for every J 0 2 J 0 . \ NC. Additionally,
To obtain subsumption modules we can use an operator to combine sets of role, subsumer and subsumee justi cations, one justi cation for each potential di erence witness that needs to be prevented; cf. Lemmas 1 and 2. Given a set S and S1; S2 2S , S1 S2 := f S1 [ S2 j S1 2 S1; S2 2 S2 g. For instance, if S1 = ff 1; 2g; f 3gg and S2 = ff 1; 3g; f 4; 5gg, then S1 S2 = ff 1; 2; 3g; f 1; 2; 4; 5g; f 3; 4; 5g; f 1; 3gg. For a set M of sets, we de ne a function Minimise (M) as follows: M 2 Minimise (M) i M 2 M and there does not exist a set M0 2 M such that M0 ( M. Continuing the previous example, Minimise (S1 S2) = ff 2; 3g; f 1; 2; 4; 5g; f 3; 4; 5gg.
We now use and Minimise ( ) to combine sets of role, subsumer and subsumee justi cations to obtain the set of all minimal projection modules. Theorem 2. Let M be the set of all projection modules under = hT1; ; T2i that are minimal w.r.t. (. Then the following holds, where ( ) = hT1; ; ; T2; i: M = M inimize
J
R
O
J !(') '2( \NC)[ dom[ ran
O A2 \NC
J (A) 5
In this section, we present algorithms for computing role, subsumer and subsumee justi cations. The algorithms use the following notion of a cover of a set of sets. For a nite set S and a set T 2S , we say that a set M 2S is a cover of T i M T and for every M 2 T, there exists M0 2 M such that M0 M. In other words, a cover is a subset of T containing all sets from T that are minimal w.r.t. (. Therefore, a cover of the set of all subsumption modules also contains all subsumption justi cations. We will use covers to characterise the output of our algorithms to ensure that all justi cations have been computed.
Algorithm 7 shows how to collect relevant -role inclusions for role subsumption justi cations (cf. Def. 3). The following proposition states its correctness. Proposition 1. J R = CoverR(T1; ; T2), where = hT1; ; T2i. 5.1
We now present our algorithm for computing subsumer justi cations. The
algorithm relies on the notion of a subsumer simulation between terminologies
from [
where N (T ; ) = f X; dom(r); ran(r) j X; r 2 (sig(T ) [ ); X 2 NC; r 2 NR g, is a -subsumer simulation from T1 to T2 i the following conditions are satis ed: (SN!C) if (X1; X2) 2 S, then for every ' 2 [ dom with T1 j= X1 v ', it holds that T2 j= X2 v '; (S9!) if (X1; X2) 2 S and X10 ./1 9r:Y1 2 T1 with ./1 2 fv; g such that T1 j= X1 v X10 and T1 j= r v s for some s 2 , there exists X20 ./2 9r0:Y2 2 T2 with ./2 2 fv; g such that T2 j= X2 v X20 and for every s 2 with T1 j= r v s, it holds that T2 j= r0 v s and (Y1; Y2) 2 S.
We write T1 ! T2 i there exists a -subsumer simulation S from T1 to T2 such that for every ' 2 ( \ NC) [ dom [ ran: ('; ') 2 S, and for every 1 2 FT1 ('), there exists a 2 2 FT2 (') such that ( 1; 2) 2 S.
For X1; X2 2 NC, we write hT1; X1i ! hT2; X2i i there exists a subsumer simulation S from T1 to T2 with (X1; X2) 2 S for which T1 ! T2.
A subsumer simulation conveniently captures the set of subsumers in the
following sense: If a -subsumer simulation from T1 to T2 contains the pair
(X1; X2), then X2 entails w.r.t. T2 all subsumers of X1 w.r.t. T1 that are
formulated in the signature . Formally, we obtain the following theorems from [
! T2 i lhsWtn (T1; T2) = ;.
Theorem 4. Let hT1; X1i ! hT2; X2i. Then for every D 2 E Lran;u;u: T1 j= X1 v D implies T2 j= X2 v D.
Algorithm 2 collects all the axioms necessary to satisfy the conditions of Definition 5. Observe that Cover!(T1; X1; ; T2; X2) may be called several times during the execution of the algorithm. A possible optimisation is to store return values in memory in order to retrieve them more quickly for subsequent calls.
The following theorem shows that Algorithm 2 indeed computes the set of subsumer modules, thus producing a cover of subsumer justi cations. Theorem 5. Let = hT1; X1; ; T2; X2i and M := Coverc!q (T1; X1; ; T2; X2). If T1 ! T2, then M is a cover of the set of subsumer justi cations under . 5.2
Next we present the algorithm for computing subsumee justi cations based on a notion of a subsumee simulation. The basic idea of the algorithm is to collect as few axioms from T2 as possible to maintain the subsumee simulation between -concept names.
First we present some auxiliary notions for handling conjunctions on the left-hand side of subsumptions. We de ne for each concept name X a so-called de nitorial forest consisting of sets of axioms of the form Y Y1 u : : : u Yn which can be thought of as forming trees. Any subsumee justi cation under hT1; X1; ; T2; X2i contains the axioms of a selection of these trees, i.e., one tree for every conjunction formulated over that entails X1 w.r.t. T1. Formally, we de ne a set of a DefForestTu(X) 2T to be the smallest set closed under the following conditions: ; 2 DefForestTu(X); f g 2 DefForestTu(X) for = X X1 u : : : u Xn 2 T ; and [ f g 2 DefForestTu(X) for 2 DefForestTu(X) with Z Z1u: : :uZk 2 and = Zi Zi1u: : :uZin 2 T . Given 2 DefForestTu(X), we set leaves( ) := sig( ) n f X 2 sig(C) j X C 2 g if 6= ;; and fXg otherwise. We denote the maximal element of DefForestTu(X) w.r.t. with max-treeTu(X). Finally, we set non-conjT (X) := leaves(max-treeTu(X)).
For example, let T = f 1; 2; 3g, where 1 := X Y uZ, 2 := Y Y1uY2, and 3 := Z Z1 u Z2. Then DefForestTu(X) = f;; f 1g; f 1; 2g; f 1; 3g, f 1; 2; 3gg. We have that leaves(f 1; 3g) = fY; Z1; Z2g, max-treeTu(X) = f 1W;e2;say3gt,haantdancoonn-ccoepntjTn(aXm)e=AfYis1; Y-2e;nZt1a;ilZed2gw..r.t. T i there is an E Lranconcept C such that T j= C v A; and we say that a role name s is -entailed in T i there exists s0 2 NR \ such that T j= s0 v s.
We now de ne the notion of a subsumee simulation from T1 to T2 as a subset of sigNC (T1) sigNC (T2) CT1 , where CT1 := f g [ (NR \ ( [ sig(T1))) is the range of role contexts.
De nition 6 (Subsumee Simulation). A relation S sigNC (T1) sigNC (T2) CT1 is a -subsumee simulation from T1 to T2 i the following conditions hold: (SNC) if (X1; X2; ) 2 S, then for every ' 2 and for every X20 2 non-conjT2 (X2) with T2 6j= ran( ) v X20, T1 j= ' v X1 implies T2 j= ' v X20; (S9 ) if (X1; X2; ) 2 S and X1 9r:Y1 2 T1 such that T1 j= s v r for s 2 and Y1 is -entailed w.r.t. T1, then for every X20 2 non-conjT2 (X2) not entailed by dom(s) or ran( ) w.r.t. T2, there exists X20 9r0:Y2 2 T2 such that T2 j= s v r0 and (Y1; Y2; s) 2 S; (Su ) if (X1; X2; ) 2 S and X1 Y1 u : : : u Yn 2 T1, then for every Y2 2 non-conjT2 (X2) not entailed by ran( ) in T2, there exists Y1 2 non-conjT1 (X1) not entailed by ran( ) w.r.t. T2 such that (Y1; Y2; ) 2 S.
We write T1 T2 i there is a -subsumer simulation S from T1 to T2 such that for every A 2 \ NC: (A; A; ) 2 S.
For 2 \ NR, we write hT1; X1i ; hT2; X2i i there is a -subsumer simulation S from T1 to T2 with (X1; X2; ) 2 S for which T1 T2.
Analogously to subsumer simulations, a subsumee simulation captures the set of subsumees as it is made precise in the following theorems.
T2 i rhsWtn (T1; T2) = ;.
X1 implies that T2 j= C v X2.
; hT2; X2i. Then for every C 2 E Lran: T1 j= C v
Before introducing the algorithms, we rst extend the notion of -entailment. We say that a concept name X is complex -entailed w.r.t. T i for every Y 2 non-conjT (X) one of the following conditions holds: { there exists B 2 { there exists Y
such that T j= B v Y and T 6j= B v X; or 9r:Z 2 T and r, Z are -entailed in T .
Otherwise, X is said to be simply -entailed. For example, let T = fX X1 u X2; B1 v X1; X2 9r:Z; B2 v Z; s v rg. We have that non-conjT (X) = fX1; X2g, then r is -entailed w.r.t. T ; X is complex -entailed w.r.t. T for = fB1; B2; sg; but X is not complex 0-entailed w.r.t. T , where 0 ranges over fB1; B2g, fB1; sg, fB2; sg. Additionally, X is not complex -entailed w.r.t. T [ fB1 v Xg.
Algorithm 3 is responsible for computing a cover of all subsumee justi cations. It orchestrates three further algorithms in order to collect the axioms necessary to satisfy the three conditions of De nition 6: Algorithm 4 for Case (SNC ), Algorithm 5 for Case (S9 ) and Algorithm 6 for Case (Su ). While Algorithm 4 can readily be understood, we provide some additional explanation for the remaining algorithms.
Algorithm 1: Computing a Cover of all Subsumer Justi cations for Conjunctive Queries 1 function Coverc!q (T1; X1; ; T2; X2)
M(!X1;X2) := f;g for every 1 2 FT1 (X1) do
M!1 := f;g for every 2 2 FT2 (X2) such that hT1; 1i ! hT2; 2i do M!1; 2 := Cover!(T1; 1; ; T2; 2)
M!1 := M!1 [ M!1; 2
M(!X1;X2) = M(!X1;X2) return Minimise (M(!X1;X2))
M!1 Algorithm 2: Computing a Cover of all Subsumer Justi cations (Recursive) 1 function Cover! (T1; X1; ; T2; X2) 2 3
M(!X1;X2) := f;g for every B 2 ( \ NC) [ f dom(r) j r 2 g such that T1 j= X1 v B do
M(!X1;X2) := M(!X1;X2) JustT2 (X2 v B) for every Y ./1 9r:Z 2 T1 (./12 fv; g) with T1 j= X1 v Y , T1 j= r v s for some s 2 \ NR do M9!r:Z := f;g for every Y 0 ./2 9r0:Z0 2 T2 (./22 fv; g) with T2 j= X2 v Y 0 and T2 j= r0 v s for every s 2 f s0 2 \ NR j T1 j= r v s0 g and hT1; Zi ! hT2; Z0i do Mr!0 := f;g for every s 2 \ NR with T1 j= r v s do
Mr!0 := Mr!0 JustT2 (r0 v s) MZ!0 := Cover!(T1; Z; ; T2; Z0) M9!r:Z := M9!r:Z [ JustT2 (X2 v Y 0)
ffY 0 ./2 9r0:Z0gg Mr!0 MZ!0
M(!X1;X2) := M(!X1;X2) return M(!X1;X2)
M9!r:Z Algorithm 3: Computing a Cover of all Subsumee Justi cations 1 function Covercq (T1; X1; ; T2; X2; ) 2 if X1 is not -entailed w.r.t. T1 then 3 return f;g 4 M(X1;X2) := CoverNC (T1; X1; ; T2; X2; ) 5 if X1 is not complex -entailed in T1 then 6 return M(X1;X2) 7 if X1 9r:Y 2 T1, and r; Y are -entailed w.r.t. T1 then M(X1;X2) :=
M(X1;X2) else if X1
Cover9 (T1; X1; ; T2; X2; )
Y1 u : : : u Ym 2 T1 then M(X1;X2) :=
M(X1;X2) Coveru (T1; X1; ; T2; X2; ) return Minimise (M(X1;X2)) 7 8 9
Fig. 1. Algorithms of computing all subsumer and subsumee justi cations Algorithm 4: Computing a Cover of all Subsumee Projection Justi cations (SNC )
The existence of axiom X1 := X1 9r:Y1 2 T1 in Line 2 of Algorithm 5 is guaranteed by Line 7 of Algorithm 3. The axiom X20 := X20 9r0:Y20 2 T2 in Line 6 of Algorithm 5 exists as we assume that X2 in T2 \subsumee-simulates" X1 in T1. Moreover, there is at most one axiom X1 2 T1 and at most one X20 2 T2 as T1 and T2 are terminologies. The concept name X2 may be de ned as a conjunction in T2 whose conjuncts in turn may also be de ned as a conjunction in T2 and so forth. In Line 3 all axioms forming the maximal resulting de nitorial conjunctive tree are collected.
For the next algorithm, we de ne defTu := f X 2 sigNC (T ) j X Y1u: : :uYn 2 T g to be the set of concept names that are conjunctively de ned in T . For every X 2 defTu, we set defTu(X) := , where = X Y1 u : : : u Yn 2 T .
The axiom X1 := X1 Y1 u : : : u Ym 2 T1 in Line 2 of Algorithm 6 is guaranteed by Line 9 of Algorithm 3. In case X2 is de ned as a conjunction in T2, the pair consisting of T2 containing only a partial conjunctive tree rooted at X2 and X2 needs to be considered to be su cient to \subsumee simulate" X1 in T1. Therefore Algorithm 3 considers every partial conjunctive tree from DefForestTu2 (X2) in Line 4 and removes the axioms in connecting the leaves of with the remaining conjunctive tree from T2 in lines 10 and 11.
The following theorem shows that Algorithm 3 indeed computes a cover of the set of subsumee modules. Thus every subsumee justi cation is guaranteed to be among the computed sets of axioms.
Theorem 8. Let = hT1; '1; ; T2; '2i and '1; '2 2 ( Additionally, let M := Covercq (T1; '1; ; T2; '2; ). If T1 set of all subsumee justi cations under . \ NC) [ dom [ ran.
T2, then M is the
The number of (minimal) projection justi cations depends on T1, T2 and .
In general, this number is bounded by an exponential in the size of the
terminologies. The simulation checks can be performed in polynomial time [
We introduce the notion of projection module for conjunctive queries as a subset of an ontology capturing the knowledge about a given signature as speci ed in a reference ontology. Here knowledge about a signature means the set of entailed conjunctive queries about the signature. This allows comparing ontologies in a more ne-grained fashion compared to merely extracting modules. Projection modules enable us to check how knowledge is implemented in terms of axioms in di erent ontologies. In particular, we can verify that and how speci cations as de ned in reference ontologies have been realised. We have presented algorithms for computing projection modules of acyclic E LHr-terminologies w.r.t. conjunctive queries. Similar algorithms can be used to deal with projection modules for concept subsumption queries and instance queries. We expect that the algorithms can be extended to deal with cyclic terminologies and even general E LHr-TBoxes.