Computing Minimal Projection Modules for Conjunctive Queries? Jieying Chen1 , Michel Ludwig2 , Yue Ma1 , and Dirk Walther3 1 Laboratoire de Recherche en Informatique, Université Paris-Sud, France {jieying.chen,yue.ma}@lri.fr 2 Luxembourg, michel.ludwig@gmail.com 3 Fraunhofer IVI, Dresden, Germany dirk.walther@ivi.fraunhofer.de Abstract. We consider the problem of extracting modules of an ontol- ogy that contains the knowledge as represented by a second ontology. The knowledge to be preserved is specified using entailment of conjunc- tive queries over a given vocabulary. We propose a novel module no- tion called projection module that preserves the answers to conjunctive queries as they follow from a reference ontology. We present an algo- rithm for computing minimal projection modules for conjunctive queries. As target and reference ontology we take ELHr -terminologies. The al- gorithm is based on simulation notions developed for detecting logical differences between ELHr -terminologies. 1 Introduction Ontology comparison can help understanding the overlap and differences 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 fine-grained ontology comparison measurement between two ontologies. Various approaches to comparing ontologies have been suggested, including ontology mapping or alignment [12], and logical difference [19–21, 23]. Ontol- ogy matching is the process of determining correspondences, in particular, the subsumption, equivalence, or disjointness relations between two concept or role names from different ontologies. A good concept similarity [1,22] is often helpful for ontology matching. In contrast, logical difference focuses on the compari- son of entailed logical consequences from each ontology and returns difference witnesses if differences are present. When an ontology has no logical difference compared to another one, our approach further extracts sub-ontologies of the first 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 = {A1 v A2 , A2 v A3 }, T2 = {A1 v A3 u B1 , B1 v ∃r.A3 }, and Σ = {A1 , A3 , r}. 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 sufficient to capture all the information of T1 about Σ. Moreover, T2 entails the consequence A1 v ∃r.A3 , which is not the case for T1 . Intuitively, T2 is richer in information about Σ than T1 . Ontology modularity [9, 16, 19, 21, 24, 25] is about the extraction of sub- ontologies that preserve all logical consequences over a given signature. In con- trast, the proposed projection module is different from modules of a single on- tology. For the example above, the basic minimal module [9], ⊥>? -module, and MEX-module [18] of T2 w.r.t. Σ are all T2 itself. The extra axiom in T2 com- pared to its projection module with respect to T1 confirms that T1 conveys less information about Σ than T2 , which gives a way to compare these two ontolo- gies. For latest results on logical inseparability (in particular, inseparability w.r.t. conjunctive queries), see [7,8,13], and for a survey on query inseparability, see [6]. To compute projection modules, in this paper, we generalize the notion of justification to the notion of subsumption justification as a minimal set of axioms that maintains a consequence. Our algorithm employs the classical notion of justification to compute subsumption justification. Currently, the approaches for computing all the justifications of an ontology w.r.t. a consequence can be classified into two categories: “glass-box” [2,5,14,15] and “black-box” [10,14,26]. We proceed as follows. Section 2 gives a brief review of Description Logic EL and its extensions as well as logical difference. In Section 3, we introduce the notion of project module. In Section 4, the notion and the computation of role subsumption justifications are presented, which are employed in Section 5 to compute project modules. Finally, Section 6 concludes the paper. 2 Preliminaries We start by briefly reviewing the description logic EL and several of its exten- sion 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 [3, 4]. Let NC and NR be sets of concept names and role names. We assume these sets to be mutually disjoint and countably infinite. The sets of EL-concepts C, ELran - concepts D, ELu -concepts E, and ELu,u -concepts F , and the sets of ELHr - inclusions α and ELran,u,u -inclusions β are built according to the grammar rules: C ::= A | C u C | ∃r.C | dom(r) D ::= A | D u D | ∃r.D | dom(r) | ran(r) E ::= A | E u E | ∃R.E F ::= A | F u F | ∃R.F | ∃u.F α ::= C v C | ran(r) v C | ran(r) u C v C | C ≡ C | r v s β ::= D v F | r v s where A ∈ NC , r, s ∈ NR , u is a fresh logical symbol (the universal role) and R = r1 u . . . u rn with r1 , ..., rn ∈ NR , for n ≥ 1. We refer to inclusions also as axioms. A Γ -TBox is a finite set of Γ -inclusions, where Γ ranges over the sets of ELHr - and ELran,u,u -inclusions. The semantics is defined 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 defined as usual. We skip a detailed introduction here. A signature is a finite 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 ELHr -terminology T is an ELHr -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 EL-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 iff there is an axiom of the form A v C or A ≡ C in T such that B ∈ sig(C). A terminology T is acyclic if the transitive closure ≺+T of ≺T is irreflexive; otherwise T is cyclic. A concept name A is said to be conjunctive in T iff there exist concept names B1 , . . . , Bn , n > 0, such that A ≡ B1 u . . . u Bn ∈ T ; otherwise A is said to be non-conjunctive in T . An ELHr -terminology T is normalised iff it only contains axioms of the forms ϕ v B1 u . . . u Bn , A v ∃r.B, A v dom(r), r v s, and A ≡ B1 u . . . u Bm , A ≡ ∃r.B, where ϕ ∈ {A, dom(s), ran(s)}, n ≥ 1, m ≥ 2, A, B, Bi ∈ NC , r, s ∈ NR , and each conjunct Bi is non-conjunctive in T . Every ELHr -terminology T can be normalised in polynomial time such that the resulting terminology is a conservative extension of T [17]. A subset M ⊆ T is called a justification for an ELH-concept inclusion α from T iff M |= α and M 0 6|= α for every M 0 ( M . We denote the set of all justifications for an ELH-concept inclusion α from an ELH-terminology T with JustT (α). The latter may contain exponentially many justifications in the number of axioms in T . We now recall the notion of logical difference for concept subsumption queries, instance queries and conjunctive queries from [17, 20]. Definition 1 (Logical Difference). The ELran,u,u -subsumption query and con- junctive query difference between T1 and T2 wrt. Σ are the sets cDiff Σ (T1 , T2 ) and qDiff Σ (T1 , T2 ), where – ϕ ∈ cDiff Σ (T1 , T2 ) iff ϕ is an ELran,u,u Σ -inclusion and T1 |= ϕ and T2 6|= ϕ; – (A, q(a)) ∈ qDiff Σ (T1 , T2 ) iff A is a Σ-ABox and q(a) a Σ-conjunctive query such that (T1 , A) |= q(a) and (T2 , A) 6|= q(a). 1 A concept equation A ≡ C stands for the inclusions A v C and C v A. The following theorem states that ELran,u,u -subsumption queries are suffi- cient to detect the absence of conj. query differences (Lemmas 62 and 63 in [17]). Theorem 1. cDiff Σ (T1 , T2 ) = ∅ iff qDiff Σ (T1 , T2 ) = ∅. If the set cDiff Σ (T1 , T2 ) is not empty, then it typically contains infinitely many concept inclusion. We make use of the primitive witnesses theorems from [17], which state that if there is a concept inclusion difference in cDiff Σ (T1 , T2 ), then there exists an inclusion in cDiff Σ (T1 , T2 ) of one of the following three types δ1 , δ2 , δ3 , which are built according to the grammar rules below: δ1 ::= r v s δ2 ::= D v A δ3 ::= A v E | dom(r) v E | ran(r) v E where δ1 ranges over role inclusions, δ2 is an ELran -inclusion, and δ3 is an ELran,u,u -inclusion. Note that each of these inclusions has either a simple left- hand or a simple right-hand side. The set of all ELran,u,u -subsumption difference witnesses is defined 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 cDiff Σ (T1 , T2 ), and the sets lhsWtnΣ (T1 , T2 ) ⊆ (Σ ∩ NC ) ∪ { dom(r) | r ∈ Σ } ∪ { ran(r) | r ∈ Σ } and rhsWtnΣ (T1 , T2 ) ⊆ NC ∩ Σ of left-hand and right-hand subsumption query difference witnesses consist of the left-hand sides of the type-δ3 inclusions in cDiff Σ (T1 , T2 ) and the right-hand sides of type-δ2 inclusions in cDiff Σ (T1 , T2 ), respectively. Consequently, the set WtnΣ (T1 , T2 ) can be seen as a finite repre- sentation of the set cDiff Σ (T1 , T2 ) [17], which is typically infinite. As a corollary of the primitive witness theorems in [17], we have that the representation is com- plete in the following sense: cDiff Σ (T1 , T2 ) = ∅ iff WtnΣ (T1 , T2 ) = (∅, ∅, ∅). Thus, deciding the existence of concept inclusion differences is equivalent to deciding non-emptiness of the three witness sets. 3 Projection Modules 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, ELran,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 finite representation of Φ with axioms from T1 into a finite 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 verification 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. Definition 2 (Projection Module). Let ρ = hT1 , Σ, T2 i be a projection set- ting. A set M ⊆ T2 is a conjunctive query projection module under ρ iff for every Σ-ABox A and every Σ-conjunctive query q(a): (T1 , A) |= q(a) implies (M, A) |= q(a). There may exist several (even exponentially many) minimal projection modules. Example 1. Let T1 = {A1 v A4 }, T2 = {A1 ≡ A2 u A3 , A2 v A4 , A3 v A4 } and Σ = {A1 , A4 }. Then the conjunctive query projection module under ρ = hT1 , Σ, T2 i is T2 . The notion of projection module is not symmetric, i.e., a projection mod- ule under hT1 , Σ, T2 i is not necessarily the same as a projection module un- der hT2 , Σ, T1 i. When the reference terminology equals the terminology from which axioms are to be extracted, a reflexive projection setting of the form ρ = hT , Σ, T i is used. We call a projection module under ρ also an automor- phic 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 = {Ai v Ai+1 | 1 ≤ i ≤ n}, T2 = {A1 v An , B1 v B2 }, Σ = {A1 , An , B1 , B2 }. Intuitively, T1 contains less information about Σ than T2 . The minimal projection module under ρ = hT1 , Σ, T2 i is M = {A1 v An }. By using |M|/|T2 | = 1/2 as a measure, we see that only half of T2 is about the information of T1 w.r.t. Σ. 4 Representing Projection Modules using Justifications In this section, we introduce justification notions for sets of inclusions and we show how they can be combined to obtain minimal projection modules. We start with defining the notion of role subsumption justifications for a set of ELran,u,u - inclusions of the form r v s, where r, s ∈ Σ (cf. Section 2). Definition 3 (Role Subsumption Justification). Let ρ = hT1 , Σ, T2 i. A set M is called a role subsumption module under ρ iff M ⊆ T2 and for every r, s ∈ NR ∩ Σ, T1 |= r v s implies M |= r v s. A role subsumption justification under ρ is the role subsumption module under ρ that is minimal w.r.t. (. We denote the set of all role subsumption justifications under ρ as JρR . Lemma 1. Let J ∈ JρR . Then roleWtnΣ (T1 , J) = ∅. We continue with defining the notion of subsumption justifications for in- clusions of ELran,u,u that are of the form D v F , where D ranges over ELran - concepts and F over ELu,u -concepts. Definition 4 (Subsumption Justification). A subsumption setting is a tuple χ = hT1 , X1 , Σ, T2 , X2 i, where T1 and T2 are normalised ELHr -terminologies, Σ is a signature, X1 , X2 ∈ NC ∪ { dom(r), ran(r) | r ∈ NR }. A set M is called a subsumer module under χ iff M ⊆ T2 and for every ran,u,u C ∈ ELΣ , T1 |= X1 v C implies M |= X2 v C. M is called a subsumee module under χ iff M ⊆ T2 and for every C ∈ ELran,u,u Σ , T1 |= C v X1 implies M |= C v X2 . M is called a subsumption module under χ iff M is a subsumer module, a subsumee module under χ and role subsumption module under hT1 , Σ, T2 i. A subsumee (resp. subsumer, subsumption) justification 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) justifica- tions under χ as Jχ← (resp. Jχ→ , Jχ ), where χ = hT1 , X1 , Σ, T2 , X2 i. Using Definition 1 and 4, we obtain the following proposition stating the ab- sence of certain concept names, and domain and range restrictions of role names as left-hand and right-hand difference witnesses between a reference terminol- ogy T1 and a subsumer and subsumee justification of a second terminology T2 . For a signature Σ, let Σ dom = { dom(t) | t ∈ NR ∩ Σ } and Σ ran = { ran(t) | t ∈ NR ∩ Σ } be the sets consisting of concepts of the form dom(t) and ran(t) for every role name t in Σ, respectively. Furthermore, let Σ ζ = Σ ∪ Σ dom ∪ Σ ran for ζ ∈ CΣ . Lemma 2. Let ϕ ∈ (Σ ∩ NC ) ∪ Σ dom ∪ Σ ran and let A ∈ Σ ∩ NC . Additionally, let χ = hT1 , ϕ, Σ, T2 , ϕi and χ0 = hT1 , A, Σ, T2 , Ai. Then: – ϕ 6∈ lhsWtnΣ (T1 , Jχ ) for every Jχ ∈ Jχ→ ; – A 6∈ rhsWtnΣ (T1 , Jχ0 ) for every Jχ0 ∈ Jχ←0 . To obtain subsumption modules we can use an operator ⊗ to combine sets of role, subsumer and subsumee justifications, one justification for each potential difference witness that needs to be prevented; cf. Lemmas 1 and 2. Given a set S and S1 , S2 ⊆ 2S , S1 ⊗ S2 := { S1 ∪ S2 | S1 ∈ S1 , S2 ∈ S2 }. For instance, if S1 = {{α1 , α2 }, {α3 }} and S2 = {{α1 , α3 }, {α4 , α5 }}, then S1 ⊗ S2 = {{α1 , α2 , α3 }, {α1 , α2 , α4 , α5 }, {α3 , α4 , α5 }, {α1 , α3 }}. For a set M of sets, we define a function Minimise⊆ (M) as follows: M ∈ Minimise⊆ (M) iff M ∈ M and there does not exist a set M0 ∈ M such that M0 ( M. Continuing the previous example, Minimise⊆ (S1 ⊗ S2 ) = {{α2 , α3 }, {α1 , α2 , α4 , α5 }, {α3 , α4 , α5 }}. We now use ⊗ and Minimise⊆ (·) to combine sets of role, subsumer and sub- sumee justifications to obtain the set of all minimal projection modules. Theorem 2. Let Mρ be the set of all projection modules under ρ = hT1 , Σ, T2 i that are minimal w.r.t. (. Then the following holds, where χ(ψ) = hT1 , ψ, Σ, T2 , ψi: O O → ← Mρ = M inimize⊆ JρR ⊗  Jχ(ϕ) ⊗ Jχ(A) ϕ∈(Σ∩NC )∪Σ dom ∪Σ ran A∈Σ∩NC 5 Computing Projection Modules In this section, we present algorithms for computing role, subsumer and sub- sumee justifications. The algorithms use the following notion of a cover of a set of sets. For a finite set S and a set T ⊆ 2S , we say that a set M ⊆ 2S is a cover of T iff M ⊆ T and for every M ∈ T, there exists M0 ∈ 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 justifications. We will use covers to characterise the output of our algorithms to ensure that all justifications have been computed. Algorithm 7 shows how to collect relevant Σ-role inclusions for role subsump- tion justifications (cf. Def. 3). The following proposition states its correctness. Proposition 1. JρR = CoverR (T1 , Σ, T2 ), where ρ = hT1 , Σ, T2 i. 5.1 Computing Subsumer Justifications We now present our algorithm for computing subsumer justifications. The al- gorithm relies on the notion of a subsumer simulation between terminologies from [11, 23]. For defining the simulation notion, we need a specific notion of reachability. For ϕ ∈ NC ∪ { dom(r), ran(r) | r ∈ NR } and a normalised ELHr - terminology T , let FT (ϕ) be the smallest set closed under the following three con- ditions: ϕ ∈ FT (ϕ); Y ∈ FT (ϕ) if X ∈ FT (ϕ), T |= X v X 0 and X 0 ./ ∃r.Y ∈ T ; and dom(r) ∈ FT (ϕ) if ran(r) ∈ FT (ϕ). Definition 5 (Subsumer Simulation). A relation S ⊆ N (T1 , Σ) × N (T2 , Σ), where N (T , Σ) = { X, dom(r), ran(r) | X, r ∈ (sig(T ) ∪ Σ), X ∈ NC , r ∈ NR }, is a Σ-subsumer simulation from T1 to T2 iff the following conditions are satisfied: (SN→C ) if (X1 , X2 ) ∈ S, then for every ϕ ∈ Σ ∪ Σ dom with T1 |= X1 v ϕ, it holds that T2 |= X2 v ϕ; (S∃→ ) if (X1 , X2 ) ∈ S and X10 ./1 ∃r.Y1 ∈ T1 with ./1 ∈ {v, ≡} such that T1 |= X1 v X10 and T1 |= r v s for some s ∈ Σ, there exists X20 ./2 ∃r0 .Y2 ∈ T2 with ./2 ∈ {v, ≡} such that T2 |= X2 v X20 and for every s ∈ Σ with T1 |= r v s, it holds that T2 |= r0 v s and (Y1 , Y2 ) ∈ S. We write T1 ∼→ Σ T2 iff there exists a Σ-subsumer simulation S from T1 to T2 such that for every ϕ ∈ (Σ ∩ NC ) ∪ Σ dom ∪ Σ ran : (ϕ, ϕ) ∈ S, and for every ψ1 ∈ FT1 (ϕ), there exists a ψ2 ∈ FT2 (ϕ) such that (ψ1 , ψ2 ) ∈ S. For X1 , X2 ∈ NC , we write hT1 , X1 i ∼→ Σ hT2 , X2 i iff there exists a Σ- subsumer simulation S from T1 to T2 with (X1 , X2 ) ∈ 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 formu- lated in the signature Σ. Formally, we obtain the following theorems from [23]. Theorem 3. It holds that T1 ∼→ Σ T2 iff lhsWtnΣ (T1 , T2 ) = ∅. ran,u,u Theorem 4. Let hT1 , X1 i ∼→ Σ hT2 , X2 i. Then for every D ∈ ELΣ : T1 |= X1 v D implies T2 |= X2 v D. Algorithm 2 collects all the axioms necessary to satisfy the conditions of Def- inition 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 justifications. Theorem 5. Let χ = hT1 , X1 , Σ, T2 , X2 i and M := Covercq→ (T1 , X1 , Σ, T2 , X2 ). If T1 ∼→ Σ T2 , then M is a cover of the set of subsumer justifications under χ. 5.2 Computing Subsumee Justifications Next we present the algorithm for computing subsumee justifications 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 define for each concept name X a so-called definitorial forest consisting of sets of axioms of the form Y ≡ Y1 u . . . u Yn which can be thought of as forming trees. Any subsumee justification under hT1 , X1 , Σ, T2 , X2 i 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 define a set of a DefForestTu (X) ⊆ 2T to be the smallest set closed under the following conditions: ∅ ∈ DefForestTu (X); {α} ∈ DefForestTu (X) for α = X ≡ X1 u . . . u Xn ∈ T ; and Γ ∪ {α} ∈ DefForestTu (X) for Γ ∈ DefForestTu (X) with Z ≡ Z1 u. . .uZk ∈ Γ and α = Zi ≡ Zi1 u. . .uZin ∈ T . Given Γ ∈ DefForestTu (X), we set leaves(Γ ) := sig(Γ ) \ { X ∈ sig(C) | X ≡ C ∈ Γ } if Γ 6= ∅; and {X} 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 = {α1 , α2 , α3 }, where α1 := X ≡ Y uZ, α2 := Y ≡ Y1 uY2 , and α3 := Z ≡ Z1 u Z2 . Then DefForestTu (X) = {∅, {α1 }, {α1 , α2 }, {α1 , α3 }, {α1 , α2 , α3 }}. We have that leaves({α1 , α3 }) = {Y, Z1 , Z2 }, max-treeTu (X) = {α1 , α2 , α3 }, and non-conjT (X) = {Y1 , Y2 , Z1 , Z2 }. We say that a concept name A is Σ-entailed w.r.t. T iff there is an ELran Σ - concept C such that T |= C v A; and we say that a role name s is Σ-entailed in T iff there exists s0 ∈ NR ∩ Σ such that T |= s0 v s. We now define the notion of a subsumee simulation from T1 to T2 as a subset of sigNC (T1 ) × sigNC (T2 ) × CTΣ1 , where CTΣ1 := {} ∪ (NR ∩ (Σ ∪ sig(T1 ))) is the range of role contexts. Definition 6 (Subsumee Simulation). A relation S ⊆ sigNC (T1 )×sigNC (T2 )× CTΣ1 is a Σ-subsumee simulation from T1 to T2 iff the following conditions hold: (SN←C ) if (X1 , X2 , ζ) ∈ S, then for every ϕ ∈ Σ ζ and for every X20 ∈ non-conjT2 (X2 ) with T2 6|= ran(ζ) v X20 , T1 |= ϕ v X1 implies T2 |= ϕ v X20 ; (S∃← ) if (X1 , X2 , ζ) ∈ S and X1 ≡ ∃r.Y1 ∈ T1 such that T1 |= s v r for s ∈ Σ and Y1 is Σ-entailed w.r.t. T1 , then for every X20 ∈ non-conjT2 (X2 ) not entailed by dom(s) or ran(ζ) w.r.t. T2 , there exists X20 ≡ ∃r0 .Y2 ∈ T2 such that T2 |= s v r0 and (Y1 , Y2 , s) ∈ S; (Su← ) if (X1 , X2 , ζ) ∈ S and X1 ≡ Y1 u . . . u Yn ∈ T1 , then for every Y2 ∈ non-conjT2 (X2 ) not entailed by ran(ζ) in T2 , there exists Y1 ∈ non-conjT1 (X1 ) not entailed by ran(ζ) w.r.t. T2 such that (Y1 , Y2 , ) ∈ S. We write T1 ∼← Σ T2 iff there is a Σ-subsumer simulation S from T1 to T2 such that for every A ∈ Σ ∩ NC : (A, A, ) ∈ S. For ζ ∈ Σ ∩ NR , we write hT1 , X1 i ∼←Σ,ζ hT2 , X2 i iff there is a Σ-subsumer simulation S from T1 to T2 with (X1 , X2 , ζ) ∈ 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. Theorem 6. T1 ∼← Σ T2 iff rhsWtnΣ (T1 , T2 ) = ∅. ran Theorem 7. Let hT1 , X1 i ∼← Σ,ζ hT2 , X2 i. Then for every C ∈ ELΣ : T1 |= C v X1 implies that T2 |= C v X2 . Before introducing the algorithms, we first extend the notion of Σ-entailment. We say that a concept name X is complex Σ-entailed w.r.t. T iff for every Y ∈ non-conjT (X) one of the following conditions holds: – there exists B ∈ Σ such that T |= B v Y and T 6|= B v X; or – there exists Y ≡ ∃r.Z ∈ T and r, Z are Σ-entailed in T . Otherwise, X is said to be simply Σ-entailed. For example, let T = {X ≡ X1 u X2 , B1 v X1 , X2 ≡ ∃r.Z, B2 v Z, s v r}. We have that non-conjT (X) = {X1 , X2 }, then r is Σ-entailed w.r.t. T ; X is complex Σ-entailed w.r.t. T for Σ = {B1 , B2 , s}; but X is not complex Σ 0 -entailed w.r.t. T , where Σ 0 ranges over {B1 , B2 }, {B1 , s}, {B2 , s}. Additionally, X is not complex Σ-entailed w.r.t. T ∪ {B1 v X}. Algorithm 3 is responsible for computing a cover of all subsumee justifica- tions. It orchestrates three further algorithms in order to collect the axioms nec- essary to satisfy the three conditions of Definition 6: Algorithm 4 for Case (SN←C ), Algorithm 5 for Case (S∃← ) and Algorithm 6 for Case (Su← ). While Algorithm 4 can readily be understood, we provide some additional explanation for the re- maining algorithms. Algorithm 1: Computing a Cover of all Sub- Algorithm 4: Computing a Cover of all Sub- sumer Justifications for Conjunctive Queries sumee Projection Justifications (SN←C ) 1 function Covercq → (T1 , X1 , Σ, T2 , X2 ) 1 function CoverN ← (T1 , X1 , Σ, T2 , X2 , ζ) C 2 M→(X1 ,X2 ) := {∅} 2 M←(X1 ,X2 ) := {∅} 3 for every ψ1 ∈ FT1 (X1 ) do 3 for every B ∈ Σ ζ such that T1 |= B v X1 do M→ 4 for every X2 ∈ non-conjT2 (X1 ) such that 4 ψ1 := {∅} 5 for every ψ2 ∈ FT2 (X2 ) such that ζ = ε or T2 |= ran(ζ) v X2 do 5 M← ← (X1 ,X2 ) := M(X1 ,X2 ) ⊗ JustT2 (B v X2 ) hT1 , ψ1 i ∼→Σ hT2 , ψ2 i do 6 return M← 6 M→ ψ1 ,ψ2 := Cover→ (T1 , ψ1 , Σ, T2 , ψ2 ) (X1 ,X2 ) 7 M→ → → ψ1 := Mψ1 ∪ Mψ1 ,ψ2 Algorithm 5: Computing a Cover of all Sub- 8 M→ → → (X1 ,X2 ) = M(X1 ,X2 ) ⊗ Mψ1 sumee Projection Justifications (S∃← ) 9 return Minimise⊆ (M→ (X1 ,X2 ) ) 1 function Cover∃← (T1 , X1 , Σ, T2 , X2 , ζ) 2 let αX1 := X1 ≡ ∃r.Y1 ∈ T1 Algorithm 2: Computing a Cover of all Sub- M← u 3 (X1 ,X2 ) := {max-treeT2 (X2 )} sumer Justifications (Recursive) 4 for every s ∈ Σ ∩ NR such that T1 |= s v r 1 function Cover→ (T1 , X1 , Σ, T2 , X2 ) do M→ 5 for every X20 ∈ non-conjT2 (X2 ) such that 2 (X1 ,X2 ) := {∅} ζ 6= ε implies T2 6|= ran(ζ) v X20 and 3 for every B ∈ (Σ ∩ NC ) ∪ { dom(r) | r ∈ Σ } T2 6|= dom(s) v X20 do such that T1 |= X1 v B do 6 let αX20 := X20 ≡ ∃r0 .Y20 ∈ T2 4 M→ → (X1 ,X2 ) := M(X1 ,X2 ) ⊗ JustT2 (X2 v B) M← cq 0 Y20 := Cover← (T1 , Y1 , Σ, T2 , Y2 , s) 5 for every Y ./1 ∃r.Z ∈ T1 (./1 ∈ {v, ≡}) ← M(X1 ,X2 ) := ← M(X1 ,X2 ) with T1 |= X1 v Y , T1 |= r v s for some ⊗ {{αX20 }} ⊗ JustT2 (s v r) ⊗ M←  Y0 2 s ∈ Σ ∩ NR do 7 return M← (X1 ,X2 ) 6 M→∃r.Z := {∅} 7 for every Y 0 ./2 ∃r0 .Z 0 ∈ T2 (./2 ∈ {v, ≡}) Algorithm 6: Computing a Cover of all Sub- with T2 |= X2 v Y 0 and T2 |= r0 v s for sumee Justifications (Su← ) every s ∈ { s0 ∈ Σ ∩ NR | T1 |= r v s0 } function Coveru 1 ← (T1 , X1 , Σ, T2 , X2 , ζ) and hT1 , Zi ∼→ 0 Σ hT2 , Z i do 2 let αX1 := X1 ≡ Y1 u . . . u Ym ∈ T1 8 M→ r 0 := {∅} M← 3 (X1 ,X2 ) := ∅ 9 for every s ∈ Σ ∩ NR with T1 |= r v s 4 for every Γ ∈ DefForestTu2 (X2 ) do do 5 let δΓ := { defTu2 (X 0 ) | X 0 ∈ 10 M→ → 0 r 0 := Mr 0 ⊗ JustT2 (r v s) leaves(Γ ) ∩ defTu2 } 11 MZ 0 := Cover→ (T1 , Z, Σ, T2 , Z 0 ) → 6 M← Γ := {Γ } 12 M→ → ∃r.Z := M∃r.Z ∪ JustT2 (X2 v Y ) 0 7 for every X20 ∈ leaves(Γ ) such that ζ = ε ⊗ {{Y 0 ./2 ∃r0 .Z 0 }} ⊗ M→ →  r 0 ⊗ M Z 0 or T2 6|= ran(ζ) v X20 do → → → 13 M(X1 ,X2 ) := M(X1 ,X2 ) ⊗ M∃r.Z 8 M← X 0 := ∅ 2 14 return M→ (X1 ,X2 ) 9 for every X10 ∈ non-conjT1 (X1 ) such that ζ = ε or T2 6|= ran(ζ) v X10 do Algorithm 3: Computing a Cover of all Sub- 10 if hT1 , X10 i ∼← 0 Σ,ζ hT2 \ δΓ , X2 i then sumee Justifications 11 M←X20 := M ← X20 ∪ cq 0 0 1 function Cover← (T1 , X1 , Σ, T2 , X2 , ζ) Covercq ← (T1 , X1 , Σ, T2 \ δΓ , X2 , ) 2 if X1 is not Σ-entailed w.r.t. T1 then 12 MΓ := MΓ ⊗ M← ← ← X0 2 3 return {∅} M← ← ← 13 (X1 ,X2 ) := M(X1 ,X2 ) ∪ MΓ 4 M← NC (X1 ,X2 ) := Cover← (T1 , X1 , Σ, T2 , X2 , ζ) 14 return M← (X1 ,X2 ) 5 if X1 is not complex Σ-entailed in T1 then 6 return M← (X1 ,X2 ) Algorithm 7: Computing a Cover of all Sub- 7 if X1 ≡ ∃r.Y ∈ T1 , and r, Y are Σ-entailed sumption Justifications for Role Inclusions w.r.t. T1 then M← 1 function CoverR (T1 , Σ, T2 ) 8 (X1 ,X2 ) := M← ∃ 2 M = {∅} (X1 ,X2 ) ⊗ Cover← (T1 , X1 , Σ, T2 , X2 , ζ) 9 else if X1 ≡ Y1 u . . . u Ym ∈ T1 then 3 for every r, s ∈ Σ ∩ NR such that 10 M←(X1 ,X2 ) := T1 |= r v s do M← u (X1 ,X2 ) ⊗ Cover← (T1 , X1 , Σ, T2 , X2 , ζ) 4 M := M ⊗ JustT2 (r v s) 11 return Minimise⊆ (M← (X1 ,X2 ) ) 5 return Minimise⊆ (M) Fig. 1. Algorithms of computing all subsumer and subsumee justifications The existence of axiom αX1 := X1 ≡ ∃r.Y1 ∈ T1 in Line 2 of Algorithm 5 is guaranteed by Line 7 of Algorithm 3. The axiom αX20 := X20 ≡ ∃r0 .Y20 ∈ 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 ∈ T1 and at most one αX20 ∈ T2 as T1 and T2 are terminologies. The concept name X2 may be defined as a conjunction in T2 whose conjuncts in turn may also be defined as a conjunction in T2 and so forth. In Line 3 all axioms forming the maximal resulting definitorial conjunctive tree are collected. For the next algorithm, we define defTu := { X ∈ sigNC (T ) | X ≡ Y1 u. . .uYn ∈ T } to be the set of concept names that are conjunctively defined in T . For every X ∈ defTu , we set defTu (X) := α, where α = X ≡ Y1 u . . . u Yn ∈ T . The axiom αX1 := X1 ≡ Y1 u . . . u Ym ∈ T1 in Line 2 of Algorithm 6 is guaranteed by Line 9 of Algorithm 3. In case X2 is defined as a conjunc- tion in T2 , the pair consisting of T2 containing only a partial conjunctive tree rooted at X2 and X2 needs to be considered to be sufficient to “subsumee simu- late” 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 justification is guaranteed to be among the computed sets of axioms. Theorem 8. Let χ = hT1 , ϕ1 , Σ, T2 , ϕ2 i and ϕ1 , ϕ2 ∈ (Σ ∩ NC ) ∪ Σ dom ∪ Σ ran . Additionally, let M := Covercq ← ← (T1 , ϕ1 , Σ, T2 , ϕ2 , ). If T1 ∼Σ T2 , then M is the set of all subsumee justifications under χ. The number of (minimal) projection justifications depends on T1 , T2 and Σ. In general, this number is bounded by an exponential in the size of the termi- nologies. The simulation checks can be performed in polynomial time [11, 23]. Our algorithm for computing projection justifications, therefore, runs in time exponential in the size of the input. 6 Conclusion We introduce the notion of projection module for conjunctive queries as a subset of an ontology capturing the knowledge about a given signature as specified 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 fine-grained fashion compared to merely extracting modules. Projection modules enable us to check how knowledge is implemented in terms of axioms in different ontologies. In particular, we can verify that and how specifications as defined in reference ontologies have been realised. We have presented algo- rithms for computing projection modules of acyclic ELHr -terminologies w.r.t. conjunctive queries. Similar algorithms can be used to deal with projection mod- ules for concept subsumption queries and instance queries. We expect that the algorithms can be extended to deal with cyclic terminologies and even general ELHr -TBoxes. References 1. Alsubait, T., Parsia, B., Sattler, U.: Measuring similarity in ontologies: A new family of measures. In: Proceedings of EKAW’14: the 19th International Conference on Knowledge Engineering and Knowledge Management. pp. 13–25 (2014) 2. Arif, M.F., Mencı́a, C., Ignatiev, A., Manthey, N., Peñaloza, R., Marques-Silva, J.: BEACON: An efficient SAT-based tool for debugging EL+ -ontologies. In: Proceed- ings of SAT’16: the 19th International Conference on the Theory and Applications of Satisfiability Testing. pp. 521–530 (2016) 3. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The description logic handbook: theory, implementation, and applications. Cambridge University Press, 2 edn. (June 2010) 4. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017) 5. Baader, F., Peñaloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic EL. In: Proceedings of DL’07: the 20th International Workshop on Description Logics (2007) 6. Botoeva, E., Konev, B., Lutz, C., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Inseparability and conservative extensions of description logic ontologies: A survey. In: Reasoning Web Summer School 2016, LNCS, vol. 9885, pp. 27–89. Springer International Publishing (2017) 7. Botoeva, E., Kontchakov, R., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Games for query inseparability of description logic knowledge bases. Artificial Intelligence 234, 78 – 119 (2016) 8. Botoeva, E., Lutz, C., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Query-based entailment and inseparability for alc ontologies. In: Proceedings of IJCAI’16: the 25th International Joint Conference on Artificial Intelligence. pp. 1001–1007. AAAI Press (2016) 9. Chen, J., Ludwig, M., Ma, Y., Walther, D.: Zooming in on ontologies: Minimal modules and best excerpts. In: Proceedings Part I of ISWC’17: the 16th Interna- tional Semantic Web Conference. pp. 173–189 (2017) 10. Domingue, J., Anutariya, C. (eds.): Proceedings of ASWC’08: the 3rd Asian Se- mantic Web Conference on The Semantic Web, Lecture Notes in Computer Science, vol. 5367. Springer (2008) 11. Ecke, A., Ludwig, M., Walther, D.: The concept difference for EL-terminologies using hypergraphs. In: Proceedings of DChanges’13 (2013) 12. Euzenat, J., Shvaiko, P.: Ontology Matching, Second Edition. Springer (2013) 13. Jung, J.C., Lutz, C., Martel, M., Schneider, T.: Query conservative extensions in horn description logics with inverse roles. In: Proceedings of IJCAI’17: the 26th In- ternational Joint Conference on Artificial Intelligence. pp. 1116–1122. AAAI Press (2017) 14. Kalyanpur, A., Parsia, B., Sirin, E., Hendler, J.A.: Debugging unsatisfiable classes in OWL ontologies. Journal of Web Semantics 3(4), 268–293 (2005) 15. Kazakov, Y., Skocovsky, P.: Enumerating justifications using resolution. In: Pro- ceedings of DL’17: the 30th International Workshop on Description Logics (2017) 16. Konev, B., Kontchakov, R., Ludwig, M., Schneider, T., Wolter, F., Zakharyaschev, M.: Conjunctive query inseparability of OWL 2 QL TBoxes. In: Proceedings of AAAI’11: the 25th Conference on Artificial Intelligence. AAAI Press (2011) 17. Konev, B., Ludwig, M., Walther, D., Wolter, F.: The logical difference for the lightweight description logic EL. Journal of Artificial Intelligence Research 44, 633–708 (2012) 18. Konev, B., Lutz, C., Walther, D., Wolter, F.: Semantic modularity and module extraction in description logics. In: Proceedings of ECAI’08: the 18th European Conference on Artificial Intelligence. pp. 55–59. IOS Press (2008) 19. Konev, B., Lutz, C., Walther, D., Wolter, F.: Model-theoretic inseparability and modularity of description logic ontologies. Artificial Intelligence 203, 66–103 (2013) 20. Konev, B., Walther, D., Wolter, F.: The logical difference problem for description logic terminologies. In: Proceedings of IJCAR’08. pp. 259–274 (2008) 21. Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology compari- son and module extraction, with an application to DL-Lite. Artificial Intelligence 174(15), 1093–1141 (2010) 22. Lehmann, K., Turhan, A.: A framework for semantic-based similarity measures for ELH-concepts. In: Proceedings of JELIA’12: the 13th European Conference Logics in Artificial Intelligence. Lecture Notes in Computer Science, vol. 7519, pp. 307–319. Springer (2012) 23. Ludwig, M., Walther, D.: The logical difference for ELHr-terminologies using hy- pergraphs. In: Proceedings of ECAI’14: the 21st European Conference on Artificial Intelligence. pp. 555–560 (2014) 24. Romero, A.A., Kaminski, M., Grau, B.C., Horrocks, I.: Module extraction in ex- pressive ontology languages via datalog reasoning. Journal of Artificial Intelligence Research 55, 499–564 (2016) 25. Sattler, U., Schneider, T., Zakharyaschev, M.: Which kind of module should I extract? In: Proceedings of DL’09. CEUR Workshop Proceedings, vol. 477. CEUR- WS.org (2009) 26. Zhou, Z., Qi, G., Suntisrivaraporn, B.: A new method of finding all justifications in OWL 2 EL. In: Proceedings of WI’13: IEEE/WIC/ACM International Conferences on Web Intelligence. pp. 213–220 (2013)