When subsumption relationships unexpectedly fail to be detected by a description logic reasoner, the cause for this “non-entailment” need not be evident. In this case, succinct automatically generated explanations would be helpful. Reasoners for the description logic EL compute the canonical model of a TBox in order to perform subsumption tests. We devise parts of such models as relevant parts for explanation and propose an approach based on graph transductions to extract such relevant parts from canonical models.
enjoys the canonical model property, which guarantees the existence of a
particular standardized model with useful properties. Reasoning in EL then amounts
to computing the canonical model. In fact, many EL reasoners implement the
computation of the canonical model [
For explaining positive answers to a subsumption test, early approaches use
justifications as explanations, which are subset-minimal subsets of the TBox
that are “responsible” for the subsumption [
Description logics are a family of decidable knowledge representation formalisms that can model structures over unary and binary predicates. Unary predicates are called concepts and binary predicates are called roles. Concepts for the description logic EL are built inductively from a set of concept names NA and a set of role names NR. Let A 2 NA and r 2 NR, then (complex) EL-concepts are built by the syntactic rule:
C ::= A | C u C | 9 r.C | >.
We assume that the sets of concept names and role names are disjoint. We denote concepts by upper case and roles with lower case letters. For concept names, we usually write A and B, and by C and D we indicate possibly complex concepts. A signature ⌃ is a union of two finite sets ⌃ C ⇢ NA and ⌃ R ⇢ NR.
An interpretation I = ( I , ·I ) over a signature ⌃ consists of a non-empty set I called the interpretation domain and an interpretation function ·I that maps every concept name in ⌃ C to a subset of I and every role name in ⌃ R to a subset of I ⇥ I . The mapping ·I extends to concepts: – (C u D)I = CI \ DI , – (9 r.C)I = {d 2 I | there is an e 2 CI s.t. (d, e) 2 rI }, – and >I = I .
An EL TBox T is a finite set of concept inclusions (CIs), which are formulae of
the form C v D, where C and D are EL concepts. We abbreviate C v D and
D v C by C ⌘ D. An interpretation I satisfies a CI C v D if CI ✓ DI . An
interpretation I is called a model of a TBox T if I satisfies all the CIs in T . For
a TBox, an interpretation or a concept X, we denote its signature by sig(X).
To denote the concept signature of X, we write use sigC(X) = sig(X) \ NC,
and sigR(X) = sig(X) \ NR for the role signature of X. A prominent reasoning
problem for DLs is to decide subsumption. Given two concepts C and D and
a TBox T , subsumption (denoted C vT D) decides whether for each model I
of T , CI ✓ DI holds. Since EL cannot express negation, satisfiability is trivial.
The main method for deciding subsumption is to compute the canonical model
of an EL TBox [
A v B,
A1 u A2 v B, 9 r.A v B, or
A v 9 r.B,
where A, A1, A2, and B are concept names or >, and r is a role name. Every
EL TBox T can be transformed into a TBox T 0 in normal form such that the
size of T 0 is linear in the size of T and every model of T 0 is a model of T [
IT := {A | A 2 NC \ sig(T )} [ {>} , AIT := {B 2
IT | B vT A} for all A 2 ⌃ C, rIT := {(A, B) 2
IT ⇥
IT | A vT 9 r.B} for all r 2 ⌃ R.
For any normalized EL TBox T , its canonical model IT , and for two named
concepts A and B, we have that A vT B if and only if IT |= A v B [
Model transformations is a binary (usually functional) relations on the class
of finite DL interpretations. We mostly use monadic second-order (MSO)
transductions as formalism to describe model transformations. Such transductions are
defined in [
Definition 2 (Monadic Second-Order Definition Scheme). Let ⌃ be a binary signature, and let W be a finite set of parameters. A monadic secondorder definition scheme is a tuple
D = h, ,
(✓ N )N2 ⌃ C , (⌘ r)r2 ⌃ R i, where – 2 M SO(⌃, – 2 M SO(⌃, – ✓ N 2 M SO(⌃, – ⌘ r 2 M SO(⌃,
The di↵erent formulae serve di↵erent purposes. The precondition needs to be satisfied by the input interpretation. This is essentially a test whether the transformation specified by the scheme is applicable to the input. The domain formula defines the interpretation domain of the output interpretation. More precisely, it selects those elements from the input interpretation that satisfy . For these domain elements, the concept formulae ✓ and role formulae ⌘ define the extensions of the named concept and roles for each symbol from the signature. MSO definition schemes are employed to generate transductions on interpretations. For our purpose of extracting relevant parts of models, we can restrict ourselves to the case of non-copying transductions, i.e. to transductions that do not increase the size of the interpretation.
Definition 3 (Transduction Induced by a Definition Scheme). Let I be an interpretation over a binary signature ⌃ , let W be a set of parameters, and let be a W-assignment in I, i.e., : W ! I . A definition scheme D defines the interpretation I0 from (I, ) if – ( , ) |= (W),1
I 0 – I := {a 2 I | (I, ) |= (W, a)}, – AI0 := {a 2 I0 | (I, ) |= ✓ N (W, a)} for all N 2 ⌃ C, – rI0 := {(a, b) 2 ( I0 )2 | (I, ) |= ⌘ r(W, a, b)} for all r 2 ⌃ R, with (I, ) |= (W, a) meaning (I, 0) |= (W, x), where 0 is the assignment extending such that 0 : x 7! a (and accordingly for ✓ and ⌘ ). We denote Db(I, ) = I0. The transduction ⌧ induced by D is defined as ⌧ := {(I, Db(I, )) | is a W-assignment in I with (I, ) |= }, and ⌧ (I) denotes {Db(I, ) | (I, ) |= tions we write ⌧ (I) = I0. for some }. For functional transduc1 We indicate parameters variables from the set W = {z1, . . . , zn} by writting (W, x) instead of (z1, . . . , zn, x). 3
Recall that we want to explain a non-subsumption by showing relevant parts of a counter model. We start from the basic definition of a counter model. We refer to asking for the validity of a subsumption relation in a given TBox as subsumption query. Let T be a TBox and := A v B a subsumption query that uses w.l.o.g. named concepts, s.t. T 6|= . An interpretation I is called a counter model for w.r.t. T i↵ I |= T and I 6|= . Presenting an entire model of the full knowledge base to the user is not ideal because it contains a lot of irrelevant parts. In this section, we provide four di↵erent definitions of what relevant parts of a counter model are. The goal is to reduce the amount of information in the counter model, i.e., reducing the amount of domain elements, concept labels, and role labels in order to provide a concise explanation of the non-subsumption. In case of the DL EL, the canonical model IT is the standard counter model and we describe our methods for this kind of model. We exemplify our approach by a running example.
Example 4. Clinical di↵erentiation between Parkinson’s disease (PD) and
progressive supranuclear palsy (PSP) can be challenging due to overlapping clinical
features [
Tex :=
Our example subsumption query is ex := PD vTex PSP which is not entailed by Tex and for which we want to supply relevant parts from the canonical model of Tex as this is our standard counter model. Figure 1 depicts the canonical model ITex of Tex using the obvious abbreviations for the names. ITex contains element a as the representative for the concept PD and b for the concept PSP.
We want to identify relevant substructures of a counter model by requiring that these substructures to be models of sets of implications that follow from the TBox T , and in that sense preserve parts of the model. Therefore, we define sets of implications w.r.t. a given TBox T . With EL(sig(T )) denoting EL concepts written in the signature of T , we define
SubT (C) := {H | C vT H, H 2 EL(sig(T ))}.
By H[N/M, R/S] we denote the exhaustive syntactic substitution of first, every occurrence of N by M and second, every occurrence of R by S. f h
Protein, AlphaProtein accumulates
Tremor e a s a h
lossOf diagnosedWith Protein
PD, NeuroDisease
Tubuli n c Mobility l d builds lossOf
Protein, TauProtein g s e t a l u m u c c a b diagnosedWith
PSP, NeuroDisease
Speech j impairs
i
NeuroDisease PDPatient
PSPPatient
Definition 5 (Relevant Implication Sets). Let T be a TBox and A, B 2 sig(T ) be concept names. The relevant implication sets of T w.r.t. A and B are:
ST (A) := {A v H | H 2 SubT (A)}, CT (A, B) := {G v H | H 2 SubT (A) \ SubT (B), G 2 {A, B}}, S¯T (A, B) := {B v H | H 2 SubT (B), H[N/>, 9 r.>/>] 2 SubT (A)
for all N 2 sig(H) \ ⌃ C and all r 2 sig(H) \ ⌃ R}.
Intuitively, ST (A) consists of all the CIs that preserve the information on the instances of A w.r.t. T . The set CT (A, B) contains CIs that preserve for A and for B the information on the commonalities of A and B w.r.t. T . The CIs in S¯T (A, B) preserve for B some commonalities of A and B that follow from T . These commonalities are restricted to those subsumers of A that remain subsumers, if all concept names are removed from them and the role-depth of each nested existential restriction is reduced by 1. The idea will become evident with the continuation of the running example.
Definition 6 (Relevant Parts of Counter Models). Let T be a TBox, := A vT B a subsumption query, I a counter model of w.r.t. T . Let a, b 2 I s.t. a 2 AI \ BI , and b 2 BI if BI 6= ; . An interpretation I0 is called {exemplify-A, exemplify-A&B, di↵ , flat-di↵ }-relevant part of I w.r.t. and T i↵ I0 is one of the smallest substructures of I, s.t. I0 6|= , and either – a 2 AI0 and I0 |= ST (A); – a 2 AI0 , b 2 BI0 and I0 |= ST (A) [ ST (B); – a 2 AI0 , b 2 BI0 and I0 |= CT (A, B) [ ST (B); – a 2 AI0 , b 2 BI0 and I0 |= CT (A, B) [ S¯T (A, B,).
(exemplify-A) (exemplify-A&B)
(di↵ ) (flat-di↵ )
substructure I00 of I0 is not a model of for the other relevance notions. and ST (A), we mean that any strict and ST (A) anymore — and likewise f Protein,AlphaProtein Tunbuli buildPsrotein,TgauProtein Speech j accumulates Tremohras elossOf Mobcility lossOf ltscceaauum impairs h a diagnosedWith diagnosedWith b i Protein PD,NeuroDisease l d PSP,NeuroDisease NeuroDisease
PDPatient PSPPatient f Protein,AlphaProtein Tunbuli buildPsrotein,TgauProtein Speech j accumulates Tremohras elossOf Mobcility lossOf ltscceaauum impairs h a diagnosedWith diagnosedWith b i Protein PD,NeuroDisease l d PSP,NeuroDisease NeuroDisease
PDPatient PSPPatient (a) exemplify-A-relevant part (b) exemplify-A&B-relevant part f Protein,AlphaProtein Tunbuli buildPsrotein,TgauProtein Speech j accumulates Tremohras elossOf Mobcility lossOf ltscceaauum impairs h a diagnosedWith diagnosedWith b i Protein PD,NeuroDisease l d PSP,NeuroDisease NeuroDisease
PDPatient PSPPatient f Protein,AlphaProtein Tunbuli buildPsrotein,TgauProtein Speech j accumulates Tremohras elossOf Mobcility lossOf ltscceaauum impairs h a diagnosedWith diagnosedWith b i Protein PD,NeuroDisease l d PSP,NeuroDisease NeuroDisease
PDPatient PSPPatient (c) di↵ -relevant part (d) flat-di↵ -relevant part
We explain the intuition and the purpose of the four relevance parts in reference to Figure 2, where the corresponding parts of the canonical model ITex from our running example are depicted. The exemplify-A-relevant part, depicted in Figure 2a, highlights the information on A w.r.t. T and hence can be used to display a “full” example of an instance of A from the subsumption query that is not subsumed by B. The exemplify-A&B-relevant part, displayed in Figure 2b, follows the same idea but for both concepts A and B. Therefore, the “full” information from both query concepts can be shown to the user. These two kinds of relevant parts give a full descriptions of the involved concepts. Explaining non-entailment can be considered as a kind of abduction problem, which, in our case, is to infer what A lacks compared to B. This consideration motivates the remaining two relevance parts we suggest. The di↵ -relevant part shows the di↵erence of A and B by preserving the information on the commonalities of both concepts at a and gives full information on B at b. It thereby highlights which parts of B are not entailed for A. The di↵ -relevant part is displayed in Figure 2c. The flat-di↵ -relevant part illustrates a flattened form of di↵erence as it preserves only those parts from B up to the smallest depth where a di↵erence to A occurs. The flat-di↵ -relevant part in Figure 2d prunes the relational structure of b in comparison to the di↵ -relevant part. In particular, di↵ shows that PSP accumulates tau proteins and also that they build tubuli, whereas flat-di↵ merely shows that PSP accumulates tau proteins. That is already is a di↵erence to PD, which accumulates alpha protein. The fact that tau protein build tubuli is hidden because it already suces to know that PSP requires the accumulations of tau proteins to explain the di↵erence between PD and PSP. 4
Given a canonical model of a TBox and a subsumption query, one can obtain the
four kinds of counter model parts from Definition 5 by model transformation.
As input for the transformation we consider canonical models of normalized
TBoxes, which are finite for general EL TBoxes and computable in polynomial
time [
Definition 7 (Transduction ⌧ exemplify-A). Let ⌃ be a signature s.t. A, B 2 ⌃ C ⇢ ⌃ , and let W = {u}. The definition scheme Dexemplify-A inducing the transduction ⌧ exemplify-A consists of the formulae:
(W) := A(u) ^ ¬ B(u), (W, x) := reach(u, x), ⌘ r(W, x, y), := r(x, y).
We assume that the parameter u is assigned by (u) to the representative for A as the expected subsumee from the subsumption query in IT . We use this assumption also for the subsequent definition schemes. The preconditions indicate which parameter is mapped to which concept representative. The transduction simply picks the representative of A as the witness for the non-subsumption A vT B from IT and collects all the reachable successors of it to induce a substructure of IT w.r.t. sig(IT ). Since the representative is unique for canonical models, we treat this transduction as functional.
Lemma 8. Let be a set containing only EL CIs of the form A v H, where A is a concept name and H an arbitrary EL concepts. Let I be a model of with a 2 AI. Then, the induced substructure I0 of I w.r.t. sig(I) that contains only the element a and all elements reachable from a, is a model of . Proof. We show (I0, a) |= H for all EL concepts H by induction on the structure of H. For the induction base, we assume H = A0 for A0 2 NC. The claim holds since we have that a 2 I0 and that a 2 CI0 for every concept name C if and only if a 2 CI because I0 is an induced substructure of I, meaning that b get the very same concept labels in I0 as it has in I. This, in particular, holds for C = A0. For the induction step we have two cases. First, H = H0 u H00. Due to (I0, a) |= H0 and (I0, a) |= H00, which is true by hypothesis, we immediately have that (I0, a) |= H0 u H00. Second, H = 9 r.H0 for some role name r. Since we have (I, a) |= 9 r.H0, there is an element a0 with (a, a0) 2 rI and hence, because a0 is reachable from a in I, we have that (a, a0) 2 rI0 , and by induction hypothesis we have that (I0, a0) |= H0, hence we have that (I0, a) |= H. Since ⌧ exemplify-A exactly induces the substructure of a given input model with a and all its reachable elements, we can apply Lemma 8 to ⌧ exemplify-A(IT ) and have that the image is a model of ST (A) because T entails ST (A).
In order to achieve minimality of the resulting structure through the model transformation as required in Definition 6, we compose ⌧ exemplify-A with a transduction ⌧ A-min that takes as an input a finite interpretation and yields a respective minimal part of a counter model. The idea of ⌧ A-min is the following. After the application of ⌧ exemplify-A to the canonical model IT of the TBox T , the obtained substructure of IT satisfies the relevant implication sets, but is not minimal yet. This part we call coarse relevant part of IT w.r.t. the subsumption query and the TBox under consideration.
Transduction ⌧ A-min itself is a composition of two transductions. In the first step, superfluous roles of the coarse relevant part of IT are deleted, s.t. the model property of the coarse relevant part w.r.t. the relevant implication set is preserved. In the second step of ⌧ A-min, the reachable part from the representative of concept A is cut out, for which the concept names and role names are induced much like in ⌧ exemplify-A. This second transformation step of extracting the exemplify-A relevant part of a IT , we name ⌧ A-reach and define it to be ⌧ exemplify-A. For canonical models IT for some EL TBox T , we have that ⌧ A-min(IT ) is unique up to isomorphism. Hence, we write ⌧ A-min(IT ) = IT 0, where IT 0 refers to a random element from the set of isomorphic smallest substructures.
The first step of ⌧ A-min deletes only superfluous roles and there might be several such sets of superfluous roles, which, strictly speaking, yield di↵erent substructures. To be formally accurate, we take into consideration that di↵erent selections of sets of superfluous roles might yield sets of substructures. However, instead of using parameters for the first step in the transduction ⌧ A-min, we introduce sets of superfluous pairs in every role that serve for constructing the definition scheme for ⌧ min. Let I be a finite interpretation and let ⌃ = sig(I). We define Sr(I) as a maximal subset of rI , s.t. (I \ Sr(I), a) |= H , (I, a) |= H for all concepts H 2 EL(⌃ ) (and respectively for b if BI 6= ; ).We remind the reader that we assume a and b to be the representatives of A and B. Furthermore, we call S(I) := S˙r2 ⌃ Sr(I) a set of superfluous roles, which is the disjoint union of the sets Sr indexed by the respective role name, for all role names in ⌃ . We omit writing I in Sr(I) whenever it is clear from the context.
Definition 9 (Transduction ⌧ min). Let I be a finite interpretation over signature ⌃ , let A, B 2 ⌃ C, and let S be a set of superfluous roles. The transduction ⌧ min is the composition of the transductions induced by the definition scheme:
(W, x) := True, ✓ N (W, x) := N (x), ⌘ r(W, x, y) := r(x, y) ^ ¬ Sr(x, y). We define ⌧ A-min to be the composition ⌧ min ⌧ A-reach. Di↵erent possible sets of superfluous roles S yield only isomorphic substructures for canonical models. Therefore, we will not explicitly mention S. Lemma 10. Let T be an EL TBox, let IT be the canonical model of T , and let ⌃ = sig(IT ). Furthermore, let A, B 2 ⌃ C, and let ⌧ exemplify-A(IT ) = I0. Then, ⌧ A-min(I0) is a minimal non-empty substructure of IT , s.t. ⌧ A-min(I0) |= ST (A). Proof. Since ⌧ A-min is model preserving by definition and Lemma 8, we have that I, s.t. a 2 A⌧ A-min(I0) and that ⌧ A-min(I) |= ST (A). Second to show is that ⌧ min(I0) is indeed minimal, i.e., that for every strict substructure I⇤ of ⌧ A-min(I0) we have that I⇤ 6|= ST (A). This, however, is immediately given the definition of S, since it’s components are maximal subsets Sr for each role name in the signature, s.t. (I \ Sr(I), a) |= H , (I, a) |= H. Then, the transduction ⌧ A-min cuts out the reachable part from a 2 AI and induces the substructure w.r.t. ⌃ by the composition with ⌧ reach. Applying Lemma 8 additionally again implies that ⌧ A-min(I0) is a minimal model of ST (A), meaning that one cannot remove another element, role or concept label.
The lemmata from above are used to show soundness of the transformations of canonical models, meaning that the obtained structures are indeed the exemplify-A-relevant part of the respective canonical models w.r.t. the subsumption query and TBox under consideration.
Theorem 11 (Soundness for exemplify-A-Relevance). Let T be an EL TBox, let := A vT B a subsumption query, s.t. T 6|= , and let IT the canonical model of T . Then, we have that ⌧ A-min(⌧ exemplify-A(IT )) is the exemplify-A-relevant part of IT w.r.t. and T .
Proof. The transduction ⌧ exemplify-A is always defined for the canonical model of an EL TBox if T 6|= . Fist, we need an element a 2 ⌧ exemplify-A(I), s.t. a 2 A⌧ exemplify-A(I) and a 62 B⌧ ↵ (I). The precondition ensures that the parameter u is mapped to these conditions accordingly. The transduction then collects all reachable elements from u by . Due to the relation formulae ✓ and ⌘ , ⌧ exemplify-A actually yields an induced substructure of I. By Lemma 8 we have that this substructure is a model of ST (A). Also, ⌧ exemplify-A(I) is not a model of by . By Lemma 10 we have that ⌧ A-min(⌧ exemplify-A(I)) satisfies the minimality condition of Definition 6.
Theorem 11 concludes the work on extracting exemplify-A-relevant parts from canonical models for EL TBoxes. We now move to extracting exemplify-A&Brelevant parts using the very same techniques as for exemplify-A-relevant parts.
Recall that exemplify-A&B-relevant parts of counter models are, in principle, the same as exemplify-A-relevant parts with the di↵erence that the exemplify-A&Brelevant part also features a representative of B with all its properties as formulated in the TBox. Hence, we can easily apply the same techniques and lemmata as in the previous subsection. In order to construct a definition scheme that induces an MSO transduction that yields coarse exemplify-A&B-relevant parts of counter models, we modify the formulae of definition scheme Dexemplify-A. We will also have to adapt the minimality transduction accordingly. Definition 12 (Transduction ⌧ exemplify-A&B). Let ⌃ be a signature s.t. A, B 2 ⌃ C ⇢ ⌃ , and let W = {u, v}. The definition scheme Dexemplify-A&B inducing the transduction ⌧ exemplify-A&B consists of the formulae:
(W) := A(u) ^ ¬ B(u) ^ B(v), (W, x) := reach(u, x) _ reach(v, x),
Similarly to exemplify-A-relevance, we have to compose ⌧ exemplify-A&B with a minimizing transduction that is applied the substructure of the canonical model under consideration. For this purpose, we redefine ⌧ A&B-reach to be ⌧ exemplify-A&B because we now also have to take care of the representative of B and its reachable elements. Now, we define ⌧ A&B-min to be ⌧ min ⌧ A&B-reach.
Theorem 13 (Soundness for exemplify-A&B-Relevance). Let T be an EL TBox, let := A vT B a subsumption query, s.t. T 6|= , and let IT a canonical model of T . Then, we have that ⌧ A&B-min(⌧ exemplify-A&B(IT )) is the exemplify-A&Brelevant part of IT w.r.t. and T .
Proof. The proof follows the same argumentation as in the Theorem 11. The only di↵erence is that there now also is a representative for concept B, which ensured by the precondition . From both the A (and not B) and the B representatives, all reachable elements are being collected and used to produce the induced substructure to satisfy Definition 6 applying Lemma 8 and Lemma 10.
Extracting the di↵ -relevant part of a canonical model is more dicult than the previous two cases. Here it is required that the representative of concept A must not satisfy subsumers of A w.r.t. T that are not subsumers of B w.r.t. T ; whereas the representative of concept B has no such restrictions, and hence must satisfy all subsumers of B w.r.t. T . We make use of additional auxiliary predicates to extract the di↵erence-based relevance parts of counter models. The predicate sam is true for two sets of elements if they constitute paths made of the same roles in I. We denote the occurrence of free second-order variables X in a formula ' by box brackets in '[X].
sam[X, Y, a, b] := 9 h : '[h, X, Y, a, b] ^ [h] := 8 x, y, z, w : h(x, y) ^ h(z, w) ! [h, X, Y, a, b] , where _ r(x, z) ^ r(y, w), and r2 ⌃ R '[h, X, Y, a, b] defines h as a surjective map from Y to X with h(b, a). To express that there is a path from element a to element b over the elements in X using the succ relation, we use an MSO formula path[X, a, b] defined in [7, Proposition 5.11]. We combine these formulae in the predicate sim:
sim(a, b, x, y) := 9 X, Y : sam[Y, X, a, b] ^ path[X, a, x] ^ path[Y, b, y]. Note that sam contains a quantification over a binary relation h and the definition schemes using this formula are not inducing MSO transductions but rather second-order logic transductions. However, since the definition scheme formulae are evaluated on finite interpretations, sam is still decidable and hence the induced transduction computable. Definition 14 (Transduction ⌧ di↵ ). Let ⌃ be a signature s.t. A, B 2 ⌃ C ⇢ ⌃ , and let W = {u, v}. The definition scheme Ddi↵ inducing the transduction ⌧ di↵ consists of the formulae:
(W) := A(u) ^ ¬ B(u) ^ B(v), (W, x) := x = u _ [reach(u, x) ^ 9 y : sim(u, v, x, y)] _ reach(v, x),
Lemma 15. Let I be an interpretation, let A, B 2 sig(I) be two concept names, let a 2 (A \ B)I, and let b 2 BI. Then, for all EL concept descriptions H, with H 6= A, we have that (⌧ di↵ (I), a) |= H implies (⌧ di↵ (I), b) |= H.
Proof. By induction on the length of H. For the induction base, we assume H is a concept name other than A. By , we have a, b 2 ⌧ di↵ (I) and by ✓ H (W, x), we have that [reach(u, x) ^ H(x) ^ 9 y : sim(u, v, x, y) ^ H(y)], and hence, by h(b, a), we have that H(b). Assume the claim holds for |H| = n. For the induction step, we have two cases: (1) H = H1 u H2 and (2) H = 9 r.H1. For (1), the induction hypothesis applies to both H1 and H2, and hence, (⌧ di↵ (I), b) |= H1 and (⌧ di↵ (I), b) |= H2, and thus, (⌧ di↵ (I), b) |= H1 u H2. For (2), the induction hypothesis applies to H1. By (W, x), we have that I |= reach(a, x) ^ 9 y : sim(u, v, x, y). Hence, there are reachable elements y from b and an element z reachable from b with (⌧ di↵ (I), y) |= H1 and r(z, y) and hence (⌧ di↵ (I), b) |= H. As a consequence of Lemma 15 we have the following statement. Corollary 16. Let T be a TBox, let I be a model of T , and let := A vT B be a subsumption query, s.t. I 6|= . Then, for all H 2 SubT (A) \ SubT (B), we have that (⌧ di↵ (I), a) |= H.
Theorem 17 (Soundness for di↵ -Relevance). Let T be an EL TBox, let := A vT B a subsumption query, s.t. T 6|= , and let IT a canonical model of T . Then, ⌧ A&B-min(⌧ di↵ (IT )) is the di↵ -relevant part of IT w.r.t. and T . Proof. As in Theorem 11, the transduction ⌧ di↵ is always defined for the canonical model of an EL TBox if T 6|= . First, having elements a 2 (A \ B)⌧ di↵ (I) and b 2 B⌧ di↵ (I) is ensured by the precondition again. Hence, we also have that ⌧ di↵ (I) 6|= . We need to show that ⌧ di↵ (I) |= CT (A, B)[ ST (B). That means, for all C 2 SubT (H), we have to show (⌧ di↵ (I), b) |= H. This follows directly from Lemma 8, since ⌧ di↵ induces the substructure of b and all its reachable elements. We now have to show that (⌧ di↵ (I), a) |= H for all H 2 SubT (G) \ SubT (H), which follows from Corollary 16. Minimality follows the same argumentation as in Lemma 10. Lastly, we define the transduction ⌧ flat-di↵ and prove its soundness for canonical models in a similar fashion as for the previous relevance parts. Definition 18 (Transduction ⌧ flat-di↵ ). Let ⌃ be a signature s.t. A, B 2 ⌃ C ⇢ ⌃ , and let W = {u, v}. The definition scheme Dflat-di↵ inducing the transduction ⌧ flat-di↵ consists of the formulae:
(W) := A(u) ^ ¬ B(u) ^ B(v), (W, x) := [reach(u, x) ^ 9 y : sim(u, v, x, y)] _ [reach(v, x) ^ 9 y : sim(u, v, x, y)] _ [reach(v, x) ^ 9 z : sim(u, v, x, z) ^ succ(z, x)], ✓ A(W, x) := [reach(u, x) ^ A(x) ^ 9 y : sim(u, v, x, y) ^ A(y)] _ x = u _ Proof. As before, the transduction ⌧ flat-di↵ is defined for I since T 6|= . Also, the precondition ensures together with ✓ A and ✓ B that ⌧ flat-di↵ (I) 6|= . It also contains the A and B representatives by definition. As before, the substructure on the reachable elements from b is induced w.r.t. the signature of I, and the concept and role labels for the by selected reachable elements from a are defined as in ⌧ di↵ . Following the argumentation in Lemma 15 and Corollary 16, we show that ⌧ flat-di↵ (I) |= CT (A, B) [ S¯T (A, B). To ensure (⌧ flat-di↵ (I), b) |= S¯T (A, B) we point to the disjunct [reach(v, x) ^ 9 z : sim(u, v, x, z) ^ succ(z, x)] in . Since the also collects the direct successors of the leaves of the common part of the model starting in b compared to the part starting in a, we have satisfy (exactly) S¯T (A, B). Furthermore, minimality stems from the arguments in Lemma 10.
Throughout the paper, we have assumed that the TBox is given in normal form. In order to get rid of the freshly introduced concept names, one can devise a definition scheme that simply induces the substructure of the model w.r.t. the signature of the not yet normalized TBox. 5
We have introduced and motivated four notions of relevant parts of counter
models for explaining non-subsumptions w.r.t. EL TBoxes, and we have devised
sound means for extracting these parts by model transformation. We are
currently implementing a system for providing explanations of EL non-subsumptions
based on our relevance notions, to be evaluated on ontologies from practical
applications. Possible extensions of this work are to consider DL knowledge bases
that also contain data, as well as elaborating the methods for more expressive
logics that also have the canonical model property, such as Horn DLs. In the
long run, we would also like to consider di↵erent types of reasoning tasks such
as explaining negative query answering results [
Acknowledgements This work was supported by the DFG in grant 389792660 as part of TRR 248 (https://perspicuous-computing.science), and QuantLA, GRK 1763 (https://lat.inf.tu-dresden.de/quantla).