Introduction

Finding High-Level Explanations for Subsumption w.r.t. Combinations of CBoxes in E L and E L+

Dennis Peuter

Viorica Sofronie-Stokkermans⋆

0 0 University Koblenz-Landau , Koblenz , Germany

We address the problem of finding high-level explanations for concept subsumption w.r.t. combinations of E L (resp. E L+) CBoxes. Our goal is to find explanations for concept subsumptions in such combinations of CBoxes which contain only symbols (concept names and role names) that are common to the CBoxes. For this, we use the encoding of TBox subsumption as a uniform word problem in classes of semilattices with monotone operators for E L and the ≤-interpolation property in these classes of algebras, as well as extensions to these results in the presence of role inclusions. For computing the ≤-interpolating terms we use a translation to propositional logic and methods for computing Craig interpolants in propositional logic.

Introduction

Description logics are logics for knowledge representation which provide a logical basis for modeling and reasoning about objects, classes of objects (concepts), and relationships between them (roles). They are of particular importance in providing a logical formalism for ontologies. One of the problems arising when creating ontologies is to ensure that they do not contain mistakes that could allow to prove subsumptions between concepts that are not supposed to hold. One situation in which this can happen is when already existing databases (or ontologies) which can be considered trustworthy are extended or when two databases (or ontologies) are put together. Even if the new ontology is still consistent, one needs to make sure that no concept inclusions which are not supposed to be true can be derived. It is therefore important to provide simple explanations for concept subsumptions in such combined ontologies (containing, for instance, only symbols that occur both in the original ontology and in the extension). In this paper we analyze this particular problem for the case in which the two ontologies consist only of TBoxes resp. CBoxes. We restrict the description logics to E L and E L+. We use the encoding of TBox subsumption for E L as a uniform word problem in classes of semilattices with monotone operators and the ≤-interpolation property in these classes of algebras, as well as extensions to these results in ⋆ Copyright c 2020 for this paper by its authors. Use permitted under Creative

Commons License Attribution 4.0 International (CC BY 4.0). the presence of role inclusions. (A subset of the axioms needed for deriving a concept inclusion can be determined using an unsatisfiable core computation.) For computing the ≤-interpolating terms we use a translation to propositional logic and methods for computing Craig interpolants in propositional logic. We regard these ≤-interpolating terms as high-level explanations for the subsumption. If more explanations are needed, they can then be obtained by analyzing the unsatisfiable cores and the resolution derivation of the ≤-interpolating terms. Related work One method for finding justifications in description logics which has been addressed in previous work is the so-called axiom pinpointing. The idea is to find a minimal axiom set, which already has the consequence in question. Similar algorithms for computing minimal axiom sets for ALC-terminologies were given by Baader and Hollunder [ 4 ], and by Schlobach and Cornet [ 18 ]. They are extensions of the tableau-like satisfiability algorithm for ALC and the tableau-like consistency algorithm for ALC, respectively, in which they make use of labels to keep track of the axioms that were used during the execution of the algorithms. In contrast to the algorithm in [ 18 ], the one in [ 4 ] does not compute minimal axiom sets directly, but Boolean formulae from which they can be derived. Possibilities of explaining ALC-subsumption (again based on tableau implementations) are described in [ 9 ]. In [ 17 ], a general approach to produce axiom pinpointing extensions of consequence-based algorithms is proposed. The methods we propose in this paper are based on resolution and hierarchical reasoning and are restricted to E L and E L+.

In [ 7 ] and [ 8 ] Baader et al. give a similar algorithm for axiom pinpointing in the description logics E L and E L+, respectively, in which they modify the subsumption algorithm for E L (respectively E L+). Here again labels are used to keep track of the axioms needed and the output is a Boolean formula, from which the axioms can be derived. They show that computing all possible minimal axiom sets may need exponential time, whereas computing one such set can be done in polynomial time. In [ 8 ] they consider extensions of TBoxes, i.e. unions of a static TBox (with irrefutable axioms) and a refutable TBox. There are also approaches to finding and enumerating justifications in E L-ontologies and extensions thereof using saturation with respect to a consequence-based calculus [ 14 ], using resolution [ 11 ], or using other suitable SAT-tools [ 2 ]. The approach we present could use these methods for axiom pinpointing or justification computation (here we instead use unsatisfiable core computation).

Possibilities of finding small proofs for description logics have been investigated in [ 1 ]. This is not the direct goal of this paper, but might be considered as a further step in an incremental way of generating explanations, after having constructed intermediate terms. In [ 10 ], provenance for variants of the description logic E L is studied; our approach could be extended with such considerations for making the explanations more informative.

Possibilities of detecting differences between ontologies have been studied in [ 12 ]; this could be seen as a first step of obtaining the concept inclusions on which our method could be applied.

A1 : A2 : A3 : A4 : A5 : A6 : A7 : A8 : A9 : A10 : A11 : A12 : B1 : B2 : B3 : B4 : R1 : R2 :

Inflammation ⊓ ∃has-location.Endocardium

⊑

Endocarditis Endocardium

⊑

Tissue Endocardium ⊑ ∃part-of.HeartWall HeartWall ⊑ BodyWall HeartWall ⊑ ∃part-of.LeftVentricle HeartWall ⊑ ∃part-of.RightVentricle LeftVentricle ⊑ RightVentricle ⊑ Ventricle Ventricle Endocarditis ⊑ Inflammation Endocarditis ⊑ ∃has-location.Endocardium Inflammation ⊑ Disease Inflammation ⊑ ∃acts-on.Tissue Ventricle ⊑ ∃part-of.Heart HeartDisease ⊑ Disease HeartDisease ⊑ ∃has-location.Heart Disease ⊓ ∃has-location.Heart ⊑ HeartDisease part-of ◦ part-of ⊑ part-of has-location ◦ part-of ⊑ has-location

We illustrate our ideas on the example CBox in Figure 1. It is based on an example from [ 28 ], which we modified in some points. We changed the CBox in a way that it only contains general concept inclusions and conjunction only appears on the left hand side of an axiom. Furthermore we left out some axioms and concepts, but also added new concepts (LeftVentricle, RightVentricle, Ventricle) and changed some axioms accordingly. (Note that concept names always start with capital letters, whereas role names start with small letters.)

We divided the CBox into three parts: The A-part is our main CBox, which is supposed to be consistent. The B-part is an extension of the main CBox and may introduce some new (and in the worst case even unwanted) consequences. The R-part contains only role axioms RI (we assume that role symbols are always among the shared symbols of the two CBoxes). Thus, the A-part is the CBox TA ∪ RI and the B-part is the CBox TB ∪ RI, where TA and TB are TBoxes. We are interested in finding simple explanations for consequences w.r.t. this extended CBox. One such consequence is Endocarditis ⊑ Heartdisease.

Constructor name Syntax Semantics conjunction C1 ⊓ C2 C1I ∩ C2I existential restriction ∃r.C {x | ∃y((x, y) ∈ rI and y ∈ CI)}

Note that TA ∪ TB ∪ RI |= Endocarditis ⊑ Heartdisease, but TA ∪ RI 2 Endocarditis ⊑ Heartdisease and TB ∪ RI 2 Endocarditis ⊑ Heartdisease, i.e. the consequence comes from the extension of the ontology and is not a consequence of one of the parts alone. Our goal now is to find an explanation of the reason why TA ∪ TB ∪ RI |= Endocarditis ⊑ Heartdisease. Formally this means that we try to find a concept description C which contains only shared symbols of TA and TB such that TA ∪ RI |= Endocarditis ⊑ C and TA ∪ TB ∪ RI |= C ⊑ Heartdisease. The common concepts in this example are Disease and Ventricle. We obtain the concept description C := Disease ⊓ ∃has-location.Ventricle, which can be regarded as a high-level explanation for TA ∪ TB ∪ RI |= Endocarditis ⊑ Heartdisease. The details are presented in Section 4. 2

Preliminaries

The central notions in description logics are concepts and roles. In any description logic a set NC of concept names and a set NR of roles is assumed to be given. Complex concepts are defined starting with the concept names in NC , with the help of a set of concept constructors. The available constructors determine the expressive power of a description logic. The semantics of description logics is defined in terms of interpretations I = (ΔI , ·I ), where ΔI is a non-empty set, and the function ·I maps each concept name C ∈ NC to a set CI ⊆ ΔI and each role name r ∈ NR to a binary relation rI ⊆ ΔI × ΔI .

The description logics E L, E L+ and some extensions. If we only allow intersection and existential restriction as concept constructors, we obtain the description logic E L [ 3 ], a logic used in terminological reasoning in medicine [ 27, 26 ]. Fig. 2 shows the constructor names used in the description logic E L and their semantics. The extension of ·I to concept descriptions is inductively defined using the semantics of the constructors. In [ 6, 5 ], the extension E L+ of E L with role inclusion axioms is studied. Relationships between concepts and roles are described using TBoxes or, more generally, CBoxes.

Definition 1 (TBox, Model, TBox subsumption). A TBox (or terminology) is a finite set consisting of primitive concept definitions of the form C ≡ D, where C is a concept name and D a concept description; and general concept inclusions (GCI) of the form C ⊑ D, where C and D are concept descriptions. – An interpretation I is a model of a TBox T if it satisfies: • all concept definitions in T , i.e., CI =DI for all definitions C≡D ∈ T ; • all general concept inclusions in T , i.e., CI⊆DI for every C⊑D ∈ T . – Let T be a TBox, and C1, C2 two concept descriptions. C1 is subsumed by

C2 w.r.t. T (C1 ⊑T C2) if and only if C1I ⊆ C2I for every model I of T . Since definitions can be expressed as double inclusions, in what follows we will only refer to TBoxes consisting of general concept inclusions (GCI) only. Definition 2 (CBox, Model, CBox subsumption). A CBox consists of a TBox T and a set RI of role inclusions of the form r1 ◦ · · · ◦ rn ⊑ s. Since terminologies can be expressed as sets of general concept inclusions, we will view CBoxes as unions GCI∪RI of a set GCI of general concept inclusions and a set RI of role inclusions of the form r1 ◦ · · · ◦ rn ⊑ s, with n≥1.

– An interpretation I is a model of the CBox C = GCI ∪ RI if it is a model of GCI and satisfies all role inclusions in C, i.e., r1I ◦ · · · ◦ rnI ⊆ sI for all r1 ◦ · · · ◦ rn ⊆ s ∈ RI. – If C is a CBox, and C1, C2 are concept descriptions then C1 ⊑C C2 if and only if C1I ⊆ C2I for every model I of C.

In [ 6 ] it was shown that subsumption w.r.t. CBoxes in EL+ can be reduced in linear time to subsumption w.r.t. normalized CBoxes, in which all GCIs have one of the forms: C ⊑ D, C1 ⊓ C2 ⊑ D, C ⊑ ∃r.D, ∃r.C ⊑ D, where C, C1, C2, D are concept names, and all role inclusions are of the form r ⊑ s or r1 ◦ r2 ⊑ s, where r, s, r1, r2 are role names. Therefore, in what follows, we consider w.l.o.g. that CBoxes only contain role inclusions of the form r ⊑ s and r1 ◦ r2 ⊑ s. Algebraic semantics for EL, EL+ and extensions thereof. In [ 20 ] we studied the link between TBox subsumption in EL and uniform word problems in the corresponding classes of semilattices with monotone functions. In [ 22, 23 ], we showed that these results naturally extend to the description logic EL+. Let SLO(Σ) be the class of all ∧-semilattices with unary operators (S, ∧, {fS}f∈Σ), such that, for every f ∈ Σ, fS : S → S is a monotone function, i.e. f satisfies: Mon(Σ) = ^ ∀x, y x ≤ y → f (x) ≤ f (y) .

f∈Σ When defining the semantics of EL or EL+ with role names NR we use a class of ∧-semilattices with monotone operators of the form SLO∃NR = (S, ∧, {f∃r}r∈NR). Every concept description C can be represented as a term C; the encoding is inductively defined: – Every concept name C ∈ NC is regarded as a variable C = C.

– C1 ⊓ C2 = C1 ∧ C2 and ∃rC = f∃rC.

If RI is a set of role inclusions of the form r ⊑ s and r1 ◦ r2 ⊑ s, let RIa be the set of all axioms of the form ∀x (f∃r(x) ≤ f∃s(x)) for all r ⊑ s ∈ RI ∀x (f∃r1(f∃r2(x)) ≤ f∃s(x)) for all r1 ◦ r2 ⊑ s ∈ RI We will denote by SLO∃NR (RIa) the class of all semilattices with monotone operators in which all axioms in RIa hold. Theorem 3 ([ 23 ]). If the only concept constructors are intersection and existential restriction, then for all concept descriptions D1, D2 and every E L+ CBox C=GCI∪RI – where RI consists of role inclusions of the form r ⊑ s and r1 ◦ r2 ⊑ s – with concept names NC = {C1, . . . , Cn} and set of roles NR the following are equivalent: (1) D1⊑CD2. (2) SLO∃NR (RIa) |= ∀C1 . . . Cn

VC⊑D∈GCI C≤D → D1≤D2 .

In [ 23, 24 ] we showed that the uniform word problem for the class of algebras SLO∃NR (RIa) is decidable in PTIME. For this, we proved that SLONR (RIa) can ∃ be seen as a “local” extension (cf. [ 19 ]) of the theory SLat of semilattices. Theorem 4 ([ 25, 23 ]). Let G be a set of ground clauses. The following are equivalent: (1) SLat ∪ Mon(Σ) ∪ G |=⊥. (2) SLat ∪ Mon(Σ)[G] ∪ G has no partial model A such that its {∧}-reduct is a semilattice, and all Σ-subterms of G are defined.

Here we denoted by Mon(Σ)[G] the set of all instances of axioms of Mon(Σ) containing only (ground) subterms occurring in G.

Let Mon(Σ)[G]0 ∪ G0 ∪ Def be obtained from Mon(Σ)[G] ∪ G by replacing (in a bottom-up manner) every term t = f (c) starting with functions in Σ with a fresh constant ct, and adding t ≈ ct to the set Def.

The following are equivalent (and equivalent to (1) and (2) above): (3) Mon(Σ)[G]0 ∪ G0 ∪ Def has no partial model A such that its {∧}-reduct is a semilattice, and all Σ-subterms of G are defined. (4) Mon(Σ)[G]0 ∪ G0 is unsatisfiable in SLat.

(Note that in the presence of Mon(Σ) the instances Con[G]0 of the congruence axioms for the functions in Σ, Con[G]0 = {g=g′ → cf(g)=cf(g′) | f (g)=cf(g), f (g′)=cf(g′) ∈ Def}, are not necessary.) This equivalence allows us to hierarchically reduce, in polynomial time, proof tasks in SLat ∪ Mon(Σ) to proof tasks in SLat (cf. e.g., [ 25 ]) which can then be solved in polynomial time. In [ 23, 24 ] we proved that similar results hold for the class SLOΣ(RI) of semilattices with monotone operators in a set Σ satisfying a family RIa axioms of the form: resp. their flattened version RIaflat, in which (2) is replaced by (3): ∀x g(x)

≤ h(x) ∀x f (g(x)) ≤ h(x) ∀x y ≤ g(x) → f (y) ≤ h(x) (1) (2) Theorem 5 ([ 24 ]). Let SL be a local axiomatization of the theory of semilattices. The following are equivalent: Let Pred be a set of predicates. We look at a certain kind of interpolation property which we call P -interpolating. In the following we give a definition for P -interpolation and show that the theory of semilattices has this property. Definition 6. T0 is P -interpolating with respect to P ∈ Pred, if for all conjunctions A and B of ground literals, all binary predicates R ∈ P and all terms a and b such that a contains only constants occurring in A and b contains only constants occurring in B (or vice versa), if A ∧ B |=T0 aRb then there exists a term t containing only constants common to A and B with A ∧ B |=T0 aRt ∧ tRb. T0 is strongly P -interpolating, if there exists such a term t with A |=T0 aRt and B |=T0 tRb.1 Proving P -interpolability is sometimes easier for theories which are P -convex. Definition 7. A theory T0 is convex with respect to the set Pred of all predicates (which may include also equality ≈) if for all conjunctions Γ of ground atoms, relations R1, . . . , Rm ∈ Pred and ground tuples of corresponding arity t1, . . . , tn, if Γ |=T0 Wim=1 Ri(ti) then there exists j ∈ {1, . . . , m} such that Γ |=T0 Rj (tj ). We will prove that the theory of semilattices with monotone operators is ≤interpolating. For this we will use the fact that the theory of semilattices is ≤-convex.

Lemma 8. The theory of semilattices is ≤-convex.

Proof: The convexity of the theory of semilattices w.r.t. ≈ follows from the fact that this is an equational class; convexity w.r.t. ≤ follows from the fact that x ≤ y if and only if (x ∧ y) ≈ x.

Lemma 9. The theory SLat of semilattices is ≤-interpolating. 1 This definition is equivalent to the definition, sometimes used in the literature, in which a and b are required to be constants. Proof: This is a constructive proof based on the fact that SLat = ISP (S2) (i.e. every semilattice is isomorphic to a sublattice of a power of S2), where S2 is the 2-element semilattice, or, alternatively, that every semilattice is isomorphic to a semilattice of sets. We prove that the theory of semilattices is ≤-interpolating, i.e. that if A and B are two conjunctions of literals and A ∧ B |=SLat a ≤ b, where a is a term containing only constants which occur in A and b a term containing only constants occurring in B, then there exists a term containing only common constants in A and B such that A |=SLat a ≤ t and A ∧ B |=SLat t ≤ b. We can assume without loss of generality that A and B consist only of atoms (otherwise one moves the negative literals to the right and uses convexity - details are given in Appendix B). A ∧ B |=SLat a ≤ b if and only if the following conjunction of literals in propositional logic is unsatisfiable: We obtain an unsatisfiable set of clauses (NA ∧ Pa) ∧ (NB ∧ ¬Pb) |=⊥, where NA and NB are sets of Horn clauses in which each clause contains a positive literal. We can saturate NA ∪ Pa under ordered resolution, in which all symbols occurring in A but not in B are larger than the common symbols. We show that if A ∧ B |=SLat a ≤ b holds, then for the term

t := V{e | A |=SLat a ≤ e, e common subterm of A and B} the following hold: (i) A |=SLat a ≤ t, and (ii) A ∧ B |=SLat t ≤ b.

This means that for the theory of semilattices we have a property stronger than ≤-interpolability, but not quite as strong as strongly ≤-interpolability.2 Every e ∈ T = {e | A |= a ≤ e, e common subterm of A and B} corresponds to the positive unit clause Pe (where Pe is a propositional variable common to NA and NB) which can be derived from NA using ordered resolution (with the ordering described above).

It is clearly the case that A |=SLat a ≤ t, because NA∧Pa∧¬Pt∧(Pt ↔ Ve∈T Pe) is unsatisfiable. Thus, (i) holds. For proving (ii), observe that by saturating NA ∧Pa under ordered resolution we obtain the following kinds of clauses containing only shared symbols which can possibly lead to ⊥ after inferences with NB ∧¬Pb (and thus to the consequence a ≤ b together with B). (a) Pek positive unit clauses s.t. ek contains symbols common to A and B. (b) Vjn=1 Pcij → Pdi , where cij and di are common symbols, such that for all i, j and k we have cij 6= ek and di 6= ek. 2 This proof fixes a problem with a claim made in the Appendix of [ 21 ] where it is mentioned that the theory of semilattices is strongly ≤-interpolating. Other types of clauses may appear too, but they can not be used to obtain a ≤ b (the details are presented in Appendix B).

For the proof of (ii) one needs to consider separately the case in which none of the clauses of type (b) is needed to derive ⊥ together with NB ∧ ¬Pb (and thus the consequence a ≤ b) and the case when some clauses of type (b) are needed. In the first case, ⊥ is derived already because of a subset {Pei | i ∈ S}. In the second case a careful analysis is needed. The details are presented in Appendix B. ⊓⊔ We show how to compute an intermediate term in the theory of semilattices on an example.

Example 10. Let A = {a1 ≤ c1, c2 ≤ a2, a2 ≤ c3} and B = {c1 ≤ b1, b1 ≤ c2, c3 ≤ b2}. It is easy to see that A ∧ B |= a1 ≤ b2. We can find an intermediate term by using the methods described in the proof: We saturate NA ∧ Pa1 = (Pa1 → Pc1 )∧(Pc2 → Pa2 )∧(Pa2 → Pc3 )∧Pa1 under ordered resolution, in which the symbols Pa1 , Pa2 are larger than Pc1 , Pc2 , Pc3 . This yields the clauses Pc1 and Pc2 → Pc3 containing shared propositional variables. (NA ∧ Pa1 ) ∧ (NB ∧ ¬Pb2 ) is unsatisfiable iff NB ∧ ¬Pb2 ∧ Pc1 ∧ (Pc2 → Pc3 ) is unsatisfiable. Indeed t = c1 is an intermediate term, as A |= a1 ≤ c1 and A ∧ B |= c1 ≤ b2. Note that NB ∧ ¬Pb2 ∧ Pc1 is satisfiable, so B 6|= c1 ≤ b2. Moreover, we only need Pc2 → Pc3 in addition to NB ∪ ¬Pb2 to derive ⊥, thus A ∧ B |= c1 ≤ b2 and the clause Pc2 → Pc3 obtained from NA is really needed for this.

Theorem 11. The theory SLO∃NR (RIa) of semilattices with monotone operators satisfying axioms RIa is ≤-interpolating.

Proof (Sketch): The operators of SLO∃NR (RIa) satisfy the monotonicity condition Mon; the axioms in RIa are in a class we studied in [ 21 ]. Let A and B be two conjunctions of literals (corresponding to two TBoxes), let RI be a set of role axioms and let Mon be the family of all monotonicity axioms for the functions {f∃r | r ∈ NR}. Assume that A ∧ B |=SLO∃NR (RIa) a ≤ b, where a is a term containing only constants and Σ-functions occurring in A and b is a term containing only constants and Σ-functions occurring in B. By Theorem 4, A ∧ B |=SLO∃NR (RIa) a ≤ b if and only if (with the notation used in Theorem 4), A0 ∧B0 ∧Mon[A∧B]0 ∧RIa[A∧B]0 ∧Con0 ∧¬(a ≤ b)0 |=SLat⊥. In the presence of monotonicity, Con is not needed. The set H = Mon[A∧B]0 ∧RIa[A∧B]0 ∧¬(a ≤ b)0 contains mixed clauses. Using a result similar to one used in [ 21 ] (the proof is given in Appendix C, cf. Proposition 13) we can “separate” all clauses in H as well as a ≤ b, i.e. we have A0 ∧ HA ∧ B0 ∧ HB ∧ ¬(a0 ≤ t0 ∧ t0 ≤ b0) |=SLat⊥, where t0 contains only constants common to A0 and B0. After replacing back the new constants with the terms they represent, we obtain: A ∧ B |=SLO∃NR (RIa) (a ≤ t ∧ t ≤ b), where t contains symbols common to A and B.3 ⊓⊔ 3 As in [ 21 ], for function symbols f, g, if f occurs in A and g occurs in B, but they occur together in one of the axioms in RI, they are considered to be shared. ≤-Interpolation for High-Level Explanations In this section we explain our method in detail and illustrate each step of the method on the example from Section 1.1. First we give a formal statement of the problem we are addressing: Let TA and TB be two E L+ TBoxes and RI a set of role inclusions. Let NC be the set of all concept names occurring in TA ∪ TB, NCA and NCB be the set of concept names occurring in TA and TB , respectively, and NCAB = (NCA ∩ NCB) be the common concept names. Let X be a concept description over NCA and Y a concept description over NCB such that they do not contain only shared symbols and such that TA ∪ TB ∪ RI |= X ⊑ Y , but TA ∪ RI 6|= X ⊑ Y and TB ∪ RI 6|= X ⊑ Y . The goal is to find a concept description C, containing only concepts in NCAB (and possibly also only roles common to TA and TB ), such that TA ∪RI |= X ⊑ C and TA ∪TB ∪RI |= C ⊑ Y . The concept description C can then be seen as a “high-level explanation” for X ⊑ Y . Using Theorem 3 and Theorem 11, we can always compute such a concept description. For this we apply the following steps: 1. Translate to the theory of semilattices with monotone operators 2. Flatten, purify and use instantiation 3. Separate all mixed instances of role and monotonicity axioms 4. Compute an intermediate term using P -interpolation Remark 12. We can make the method more efficient especially for large ontologies, by modifying Steps 2 and 3. Usually, if we have very large TBoxes, only some of their axioms are necessary for obtaining a certain consequence. Therefore it is sufficient to apply Step 2 only on the relevant axioms. Similarly, we can speed up our method by applying Step 3 only on the instances relevant for our problem. For determining which axioms/instances are relevant we can compute a minimal axiom set, for example by using unsatisfiable core computation. We therefore modify the method by including a Step 2a (before Step 2) and a Step 3a (before Step 3) in which we compute a minimal axiom or instance set. For the ontology from Section 1 we have the following sets of symbols (we indicate also the abbreviations used in what follows):

NCA =

NCB = NCAB = {Endocardium(Em), Tissue(T), HeartWall(HW),

LeftVentricle(LV), RightVentricle(RV), Ventricle(V) Disease(D), Inflammation(I), Endocarditis(Es)} {Heart(H), HeartDisease(HD), Disease(D), Ventricle(V)} {Disease(D), Ventricle(V)}

Therefore the consequence Endocarditis ⊑ Heartdisease indeed belongs to the problem described above. We show how to apply steps 1 to 4 (including steps 2a and 3a) in detail: Step 1: Figure 3 shows the ontology after the translation to the theory of semilattices (SLat). For this we replace ⊑ by ≤ and ⊓ by ∧, and write the role A1 : A2 : A3 : A4 : A5 : A6 : A7 : A8 : A9 : A10 : A11 : A12 :

Em ≤ T Em ≤ po(HW) HW ≤ BW HW ≤ po(LV) HW ≤ po(RV)

LV ≤ V RV ≤ V Es ≤ I

Es ≤ hl(Em) I ∧ hl(Em) ≤ Es

I ≤ D I ≤ ao(T) B1 : B2 : B3 : B4 : R1 : R2 : M1 : M2 : M3 :

V ≤ po(H) HD ≤ D

HD ≤ hl(H)

D ∧ hl(H) ≤ HD ∀X: po(po(X)) ≤ po(X) ∀X: hl(po(X)) ≤ hl(X) ∀X,Y: X ≤ Y ∀X,Y: X ≤ Y ∀X,Y: X ≤ Y → po(X) ≤ po(Y) → hl(X) ≤ hl(Y) → ao(X) ≤ ao(Y) axioms as universal formulae. Note that we use abbreviations for role names (e.g. hl for has-location, po for part-of, ao for acts-on). Also note that we now state the monotonicity axioms for each role explicitly.

Step 2a: Using unsat core computation we get the minimal axiom set minA = {A2, A4, A6, A8, A9, A11, B1, B4, R2}. This means that for the following instantiation step we only have to consider the role axiom R2 and none of the monotonicity axioms is needed.

Step 2: Let T0 = SLat and T1 = SLat∪R2 be the extension of T0 with axiom R2. We know that it is a local theory extension, so we can use hierarchical reasoning. We first flatten the role axiom R2 in the following way:

R2flat : ∀X, Y: X ≤ po(Y) → hl(X) ≤ hl(Y) We have the following instances of this axiom:

I1 : I2 : I3 : I4 : I5 : I6 : I7 : I8 :

Em ≤ po(HW) Em ≤ po(LV) Em ≤ po(RV) Em ≤ po(H) HW ≤ po(LV) HW ≤ po(RV) HW ≤ po(H) LV ≤ po(HW) → → → → → → → → hl(Em) ≤ hl(HW) hl(Em) ≤ hl(LV) hl(Em) ≤ hl(RV) hl(Em) ≤ hl(H) hl(HW) ≤ hl(LV) hl(HW) ≤ hl(RV) hl(HW) ≤ hl(H) hl(LV) ≤ hl(HW)

I9 : LV ≤ po(RV) I10 : LV ≤ po(H) I11 : RV ≤ po(HW) I12 : RV ≤ po(LV) I13 : RV ≤ po(H) I14 : H ≤ po(HW) I15 : H ≤ po(LV) I16 : H ≤ po(RV) → → → → → → → → hl(LV) ≤ hl(RV) hl(LV) ≤ hl(H) hl(RV) ≤ hl(HW) hl(RV) ≤ hl(LV) hl(RV) ≤ hl(H) hl(H) ≤ hl(HW) hl(H) ≤ hl(LV) hl(H) ≤ hl(RV) We purify all formulae by introducing new constants for the terms starting with a function symbol, i.e. role names. We save the definitions in the following set: Def = {poHW = po(HW), poLV = po(LV), poH = po(H), hlEM = hl(EM), hlHW = hl(HW), hlLV = hl(LV), hlHC = hl(HC), hlH = hl(H)} We then have the set A0 ∧B0∧I0, where A0, B0 and I0 are the purified versions of A = {A2, A4, A6, A8, A9, A11}, B = {B1, B4} and I = {I1, ..., I10}, respectively. Step 3a: Computing an unsatisfiable core yields the following set of axioms: {A2, A4, A6, A8, A9, A11, B1, B4, I1, I5, I10}. So we have H = {I1, I5, I10}. Out of these instances the first two are pure A (meaning the premise contains only symbols in NCA), but I10 is a mixed instance, since LV ∈ NCA\NCB and H ∈ NCB\NCA, so Hmix = {I10}.

Step 3: To separate the mixed instance LV ≤ poH → hlLV ≤ hlH one has to find an intermediate term t in the common signature such that LV ≤ t and t ≤ poH. t = V is such a term. We get Hsep = {I1A0, I1B0} where

I1A0 : I1B0 :

LV ≤ V V ≤ poH → → hlLV ≤ hlV hlV ≤ hlH Note that I1A0 is an instance of the monotonicity axiom for the has-location role and I1B0 is an instance of axiom R2flat.

Step 4: Note that w.r.t. SLat the formula A0 ∧ I1 ∧ I5 ∧ I1A0 is equivalent to: A0 = Em ≤ poHW ∧ HW ≤ poLV ∧ LV ≤ V ∧ Es ≤ I ∧ Es ≤ hlEm ∧ I ≤ D ∧ hlEM ≤ hlHW ∧ hlHW ≤ hlLV ∧ hlLV ≤ hlV To obtain an explanation for TA ∪ TB ∪ RI |= Endocarditis ⊑ HeartDisease we saturate the set A0 ∧ Es under ordered resolution as described in the proof of Theorem 9, where symbols occurring in A and not in B are larger than common symbols. Doing this yields two inferences containing only common symbols: D and hlV. By taking the conjunction of these terms and translating the formula back to description logic, we obtain J = Disease ⊓ ∃has-location.Ventricle. Then TA ∪ RI |= Endocarditis ⊑ J and TA ∪ TB ∪ RI |= J ⊑ HeartDisease. 5

Conclusion

We analyzed a possibility of giving high-level justifications for subsumption in the description logics E L and E L+. For this, we used the encoding of TBox subsumption as a uniform word problem in classes of semilattices with monotone operators for E L and the ≤-interpolation property in these classes of algebras, as well as extensions to these results in the presence of role inclusions. This can be seen as a first step towards providing short, high-level explanations for subsumption. If more explanations are needed, they can then be obtained by pinpointing and analyzing the resolution derivation of the ≤-interpolating terms.

There has been work on other forms of interpolation in the family of E L description logics: a variant of interpolation is proved in [ 16 ], possibilities for uniform interpolation are analyzed in [ 13 ] and [ 15 ] (it is well known that neither ALC nor E L allow uniform interpolation). As a plan for future work we would like to analyze possibilities of symbol elimination and abduction in such logics – which are strongly related to uniform interpolation.

Acknowledgements: We thank the reviewers for their helpful comments.

Example of local reasoning in E L+ We illustrate the ideas on the example from Section 1.1. Consider the CBox C consisting of the following GCI:

A1 − A2 A4 A6 A8 − A9 A11 B1 B2 − B4

Endocardium ⊑ Tissue ⊓ ∃part-of.HeartWall HeartWall ⊑ ∃part-of.LeftVentricle LeftVentricle ⊑ Ventricle Endocarditis ⊑ Inflammation ⊓ ∃has-location.Endocardium Inflammation ⊑ Disease Ventricle ⊑ ∃part-of.Heart Heartdisease = Disease ⊓ ∃has-location.Heart

and the following role inclusions RI:

part-of ◦ part-of ⊑ part-of has-location ◦ part-of ⊑ has-location We want to check whether Endocarditis ⊑C Heartdisease. This is the case iff (with some abbreviations – e.g. hl stands for ∃has-location and po for ∃part-of, HW for

HeartWall, Em for Endocardium, H for Heart, etc.):

Then st(K, G) = {po(HW), po(LV), po(H), hl(Em), hl(H)}. To compute ΨK(G), note that ΨR0 I = st(K, G), ΨR1 I = {po(Em), po(H)}, and ΨR2 I = ΨR1 I .

Thus, ΨK(G) = {po(HW), po(LV), po(Em), po(H), hl(Em), hl(H)}. After computing (RIa ∪ Mon(hl, po) ∪ Con)[Ψ (G)] we obtain the following conjunction of (Horn) ground clauses:

G Em ≤ T ∧ po(HW) HW ≤ po(LV), LV ≤ V V ≤ po(H)

Endocarditis ≤ I ∧ hl(Em)

I ≤ D Heartdisease = D ∧ hl(H)

Endocarditis 6≤ Heartdisease

(RIa ∧ Mon ∧ Con)[Ψ (G)]∧SL[Ψ (G)] y≤po(x) → po(y)≤po(x) for x, y ∈ {HW, LV, Em, H} y≤po(x) → hl(y) ≤ hl(x) for x, y ∈ {Em, H} xRy → po(x)Rpo(y) xRy → hl(x)Rhl(y)

SL[Ψ (G)] for x, y ∈ {HW, LV, Em, H} for x, y ∈ {Em, H} R ∈ {≤, ≥, =}

By Theorem 5, Endocarditis ⊑C Heartdisease iff φ = G ∧ (RIa ∧ Mon ∧ Con)[Ψ (G)] ∧ SL[Ψ (G)] is unsatisfiable. Note that φ is a set of ground clauses in first-order logic with equality, containing all instances of the congruence axioms corresponding to the (ground) terms which occur in φ. A translation to Datalog can easily be obtained by replacing the function symbols with binary predicate symbols. Alternatively, we can process the instances in φ by replacing, in a bottom-up fashion, all the terms starting with function symbols (which are all ground) with new constants (and adding, separately, the corresponding definitions). We obtain the following set of clauses: Def

G0 Lemma 9. The theory SLat of semilattices is P -interpolating for P = {≈, ≤}. Proof: This is a constructive proof based on the fact that SLat = ISP (S2), where S2 is the 2-element semilattice. We prove that the theory of semilattices is ≤-interpolating, i.e. that if A and B are two conjunctions of literals and A ∧ B |=SLat a ≤ b, where a is a term containing only constants which occur in A and b a term containing only constants occurring in B, then there exists a term containing only common constants in A and B such that A |=SLat a ≤ t and A∧B |=SLat t ≤ b. We can assume without loss of generality that A and B consist only of atoms: Indeed, assume that A ∧ B = A1 ∧ · · · ∧ An ∧ ¬A′1 ∧ · · · ∧ ¬A′m, where A1, . . . , An, A′1, . . . , A′m are atoms. Then the following are equivalent: – A ∧ B |=SLat a ≤ b Since the theory of semilattices is convex w.r.t. ≤ and ≈, it follows that if A ∧ B |=SLat a ≤ b then either (a) A1 ∧ · · · ∧ An |=SLat A′j for some j ∈ {1, . . . , m} or (b) A1 ∧ · · · ∧ An |=SLat a ≤ b. It is easy to see that in case (a), A ∧ B |=⊥. Then the conclusion of the theorem follows immediately. We therefore continue the proof for the case when A and B consist only of atoms.

As SLat = ISP (S2), in SLat the same Horn sentences are true as in the 2-element semilattice S2. Thus, A ∧ B |=SLat a ≤ b iff A ∧ B |=S2 a ≤ b, so we can reduce such a test to entailment in propositional logic.

It follows that A ∧ B |=SLat a ≤ b if and only if the following conjunction of literals in propositional logic is unsatisfiable: for all e, e1, e2 subterms in A for all g, g1, g2 subterms in B We obtain an unsatisfiable set of clauses (NA ∧ Pa) ∧ (NB ∧ ¬Pb) |=⊥, where NA and NB are sets of Horn clauses in which each clause contains a positive literal. We can saturate NA ∪ Pa under ordered resolution, in which all symbols occurring in A but not in B are larger than the common symbols. We show that if A ∧ B |=SLat a ≤ b holds, then for the term

t := ^{e | A |=Slat a ≤ e, e common subterm of A and B} the following hold: (i) A |=SLat a ≤ t, and (ii) A ∧ B |=SLat t ≤ b.

This means that for the theory of semilattices we have a property stronger than ≤-interpolability, but not quite as strong as strongly ≤-interpolability. Every e ∈ T = {e | A |=SLat a ≤ e, e common subterm of A and B} corresponds to the positive unit clause Pe (where Pe is a propositional variable common to NA and NB) which can be derived from NA using ordered resolution (with the ordering described above).

It is clearly the case that A |=SLat a ≤ t, because NA ∧Pa ∧¬Pt ∧(Pt ↔ Ve∈T Pe) is unsatisfiable. Thus, (i) holds.

For proving (ii), observe that by saturating NA ∧ Pa under ordered resolution we obtain the following kinds of clauses which can possibly lead to ⊥ after inferences with NB ∧ ¬Pb (and thus to the consequence a ≤ b together with B): (a) Pek positive unit clauses s.t. ek contains symbols common to A and B, for k ∈ {1, . . . , l}. (b) Vjn=i1 Pcij → Pdi, where cij and di are common symbols, such that for all i, j and k we have cij 6= ek and di 6= ek, for i ∈ {1, . . . , p}.

Other types of clauses may appear too, but they can not be used to obtain a ≤ b:

To see that clauses where some cij = ek are not necessary to derive the consequence a ≤ b, note that if Pek is a positive unit literal and we have the clause (Pek ∧ V Pcij ) → Pdi, then by resolution we get as an inference V Pcij → Pdi. It is easy to see that (Pek ∧ V Pcij ) → Pdi is redundant in the presence of V Pcij → Pdi . In the same way, clauses of the form V Pcij → Pek (i.e. clauses of type (b) where di = ek) are redundant in the presence of Pe1 , . . . , Pel . For the proof of (ii) one needs to consider separately the case in which none of the Pdi is needed to derive ⊥ together with NB (and thus the consequence a ≤ b) and the case when some Pdi are needed.

Case 1: None of the Pdi is needed to derive ⊥ together with NB (and thus the l consequence a ≤ b). We know that NA |= Pa → Vk=1 Pek . From this it follows l that A |= a ≤ Vk=1 ek.

l For A ∧ B |= a ≤ b to be true, Vk=1 Pek ∧ NB ∧ ¬Pb must be unsatisfiable, so there has to be a subset S ⊆ {1, ..., l} such that Vk∈S Pek ∧ NB ∧ ¬Pb. This l means that B |= Vs∈S es ≤ b. But then, since Vk=1 ek ≤ Vs∈S es, it follows that l l B |= Vk=1 ek ≤ b, and therefore also A ∧ B |= Vk=1 ek ≤ b.

Case 2: Some Pdi are needed to derive ⊥ from NB ∧ ¬Pb. Again, we know that l l NA |= Pa → Vk=1 Pek (hence A |= a ≤ Vk=1 ek).

For A ∧ B |= a ≤ b to be true, i.e. (NA ∧ Pa) ∧ (NB ∧ ¬Pb) to be unsatisfiable, there have to be subsets S1 ⊆ {1, ..., l} and S2 ⊆ {1, ..., p} such that NB ∧ Vk∈S1 Pek ∧ Vi∈S2((Vj Pcij ) → Pdi ) ∧ ¬Pb is unsatisfiable. Let NAB := NB ∧ Vk∈S1 Pek ∧ Vi∈S2 ((Vj Pcij ) → Pdi ). We know that NB ∧ Vk∈S1 Pek ∧ ¬Pb is satisfiable. Assume that there is no cij such that NB ∧ Vk∈S1 Pek ∧ ¬Pb |= Pcij . Then for every cij, NB ∧ Vk∈S1 Pek ∧ ¬Pb ∧ ¬Pcij is satisfiable. Since all clauses in Nb ∧ Vk∈S1 Pek ∧ ¬Pb are Horn clauses, it follows that NB ∧ Vk∈S1 Pek ∧ ¬Pb ∧ Vi,j ¬Pcij is satisfiable. Every model of NB ∧ Vk∈S1 Pek ∧ ¬Pb ∧ Vi,j ¬Pcij is a model of NAB ∧ ¬Pb. It would therefore follow that NAB ∧ ¬Pb is satisfiable, which is a contradiction. Thus, there exists at least one cij such that NB ∧ Vk∈S1 Pek ∧ ¬Pb |= Pcij . We can add Pcij to this set of clauses and repeat the reasoning for the set of clauses obtained this way as long as we still have one clause of the form ((Vj Pcij ) → Pdi) in NAB such that there exists at least one cij such that Pcij was not added to NAB.

Then there has to be a sequence (di1j)j∈J1 , (di2j)j∈J2 , ..., (dinj)j∈Jn such that: – Pdi1j can be derived from NAB∧ V Pek , for all j ∈ J1, – Pdi2j can be derived from NAB∧ V Pek ∧ Vk∈J1 di1k, for all j ∈ J2, – Pdi3j can be derived from NAB∧ V Pek ∧ Vk∈J1 di1k∧ Vk∈J2 di2k, for all j ∈ J3, . . . – Pdinj can be derived from NAB∧ Vk Pek ∧ Vk∈J1 di1k∧ · · · Vk∈Jn−1 din−1k, for all j ∈ Jn, – Pb can be derived from NAB∧ V Pek ∧ Vk∈J1 di1k∧ . . . ∧ Vk∈Jn dink. But then A ∧ B |= V ek ≤ di1l, for all l ∈ J1, hence A ∧ B |= V ek ≤ Vl∈J1 di1l, hence A ∧ B |= V ek ∧ Vl∈J1 di1l ≈ V ek. Therefore, as A ∧ B |= (V ek ∧ Vl∈J1 di1l) ≤ di2j , for all j ∈ J2, we have A ∧ B |= V ek ≤ Vj di2j . Similarly it can be proved that A ∧ B |= V ek ≤ Vj dinj , and finally that A ∧ B |= V ek ≤ b. ⊓⊔ C

A separation result

Proposition 13. Let T0 be a theory with signature Π0 = (Σ0, Pred). Assume that ≤ ∈ Pred is such that ≤ is a transitive relation in all models of T0 and that T0 is convex with respect to ≤ and ≤-interpolating.

Let A0 and B0 be conjunctions of ground literals in the signature Π0c (the extension of Π0 with a set of constants) such that A0 ∧ B0 ∧ H |=T0 a ≤ b, where a contains only symbols occurring in A0 and b only symbols occurring in B0 and H is a set of Horn clauses of the form c1 ≤ d1 → c ≤ d in the signature Π0c which are instances of flattened and purified clauses of the form Mon[A ∧ B]0 ∧ RIa[A ∧ B]0 as explained in Theorem 11, i.e. of axioms of the following type: x ≤ g(y) → f (x) ≤ h(y) x ≤ y → f (x) ≤ f (y) (4) Then the following hold: (1) There exists a set T of Π0c-terms containing only constants common to A0 and B0 and a term t ∈ T such that

A0 ∧ B0 ∧ (H\Hmix) ∧ Hsep |=T0 a ≤ t ∧ t ≤ b, where Hmix = {a1 ≤ b1 → a2 ≤ b2 ∈ H | a1, a2 constants in A, b1, b2 constants in B}∪ {b1 ≤ a1 → b2 ≤ a2 ∈ H | b1, b2 constants in B, a1, a2 constants in A} Hsep = {(a1 ≤ t1→a2 ≤ cf(t1)) ∧ (t1 ≤ b1→cf(t1) ≤ b2) | a1≤b1→a2≤b2 ∈ Hmix, b1 ≈ g(e1), b2 ≈ h(e1) ∈ DefB, a2 ≈ f (a1) ∈ DefA or vice versa, and t1, f (t1) ∈ T } = HsAep ∧ HsBep where cf(t1) are new constants in Σc (considered to be common) introduced for the corresponding terms f (t1). (2) A0 ∧ B0 ∧ (H\Hmix) ∧ Hsep ∧ ¬(a ≤ t ∧ t ≤ b) is logically equivalent w.r.t.

T0 with the separated conjunction of literals A0 ∧ B0 ∧ ¬(a ≤ t ∧ t ≤ b) = A0 ∧ B0 ∧ V{c ≤ d | Γ →c ≤ d ∈ H\Hmix} ∧ V{c ≤ cf(t) ∧ cf(t) ≤ d | (Γ → c ≤ cf(t)) ∧ (Γ → cf(t) ≤ d) ∈ Hsep} ∧ ¬(a ≤ t ∧ t ≤ b). Proof: We prove (1) and (2) by induction on the number of clauses in H.

If H = ∅ then the initial problem is already separated into an A and a B part so we are done: We have A0 ∧ B0 |=T0 a ≤ b and since we assumed that T0 is ≤-interpolating, there exists a term t containing only constants common to A0 and B0 such that A0 ∧ B0 |=T0 a ≤ t ∧ t ≤ b (we can choose T = {t}).

Assume that H contains at least one clause, and that for every H1 with fewer clauses and every conjunction of literals A′0, B0′ with A′0 ∧ B0′ ∧ H1 |=T0 a ≤ b, (1) and (2) hold.

Let D be the set of all atoms c ≤ d occurring in premises of clauses in H. As every model of A0 ∧ B0 ∧ V(c≤d)∈D ¬(c ≤ d) ∧ ¬(a ≤ b) is also a model for H∧A0 ∧B0 ∧¬(a ≤ b) and H∧A0 ∧B0 ∧¬(a ≤ b) |=T0 ⊥, A0 ∧B0 ∧V(c≤d)∈D ¬(c ≤ d) ∧ ¬(a ≤ b) |=T0 ⊥. Let (A0 ∧ B0)+ be the conjunction of all positive literals in A0 ∧ B0, and (A0 ∧ B0)− be the set of all negative literals in A0 ∧ B0. Then (A0 ∧ B0)+ |=T0

_ (c≤d)∈D (c ≤ d) ∨

_ ¬L∈(A0∧B0)−

L ∨ (a ≤ b).

T0 is convex with respect to ≤ and (A0 ∧B0)+ is a conjunction of positive literals. Therefore, either (i) (A0 ∧ B0)+ |= L for some L ∈ (A0 ∧ B0)− (then A0 ∧ B0 is unsatisfiable and hence entails any atom ci ≤ di), or (ii) (A0 ∧ B0)+ |= a ≤ b, or (iii) there exists (c1 ≤ d1) ∈ D such that A0 ∧ B0 |=T0 c1 ≤ d1.

Case 1: A0 ∧ B0 is unsatisfiable. In this case (1) and (2) hold for T = {t}, where t is an arbitrary term over the common symbols of A0 and B0.

Case 2: A0 ∧ B0 is satisfiable and (A0 ∧ B0)+ |= a ≤ b. Then we can use the fact that T0 is ≤-interpolating and we are done.

Case 3: A0 ∧ B0 is satisfiable and there exists (c1 ≤ d1) ∈ D such that A0 ∧ B0 |=T0 c1 ≤ d1. Then A0 ∧B0 is logically equivalent in T0 with A0 ∧B0 ∧c1 ≤ d1.

Let C = c1 ≤ d1 → c ≤ d ∈ H such that A0 ∧ B0 |= c1 ≤ d1.

Case 3a. Assume that C contains only constants occurring in A or only constants occurring in B. Then A0 ∧ B0 ∧ H is equivalent w.r.t. T0 with A0 ∧ B0 ∧ (H\C) ∧ c ≤ d. By the induction hypothesis for A′0 ∧ B0′ = A0 ∧ B0 ∧ c ≤ d and H1 = H\{C}, we know that there exists T ′ and t ∈ T ′ such that A′0 ∧ B0′ ∧ (H1\H1mix) ∧ H1sep |= a ≤ t ∧ t ≤ b, and (2) holds too.

Then, for T = T ′, A′0 ∧ B0′ ∧ (H1\H1mix) ∧ H1sep ∧ ¬(a ≤ t ∧ t ≤ b) is logically equivalent to A0 ∧B0 ∧(H\Hmix)∧Hsep ∧¬(a ≤ t∧t ≤ b), so A0 ∧B0 ∧(H\Hmix)∧ Hsep |= (a ≤ t ∧ t ≤ b), i.e. (1) holds.

In order to prove (2), note that, by definition, H1mix = Hmix and and H1sep = Hsep. By the induction hypothesis, A′0 ∧B0′ ∧(H1\H1mix)∪H1sep ∧¬(a ≤ t∧t ≤ b) is logically equivalent to a corresponding conjunction A′0 ∧ B′0 ∧ ¬(a ≤ t ∧ t ≤ b) containing as conjuncts all literals in A′0 and B0′ and all conclusions of rules in H1\H1mix and H1sep. On the other hand, A′0 ∧ B0′ ∧ ¬(a ≤ t ∧ t ≤ b) is logically equivalent to A0 ∧ B0 ∧ (c ≤ d) ∧ ¬(a ≤ t ∧ t ≤ b), where (c ≤ d) is the conclusion of the rule C ∈ H\Hmix. This proves (2).

Case 3b. Assume now that C := c1 ≤ d1 → c ≤ d is mixed, for instance that c1, c are constants in A and d1, d are constants in B.

(a) Assume that C is obtained from an instance of a clause of the form x ≤ g(y) → f (x) ≤ h(y). This means that there exist c ≈ f (c1) ∈ DefA and d1 ≈ g(e), d ≈ h(e) ∈ DefB. We know that A0 ∧ B0 |=T0 c1 ≤ d1 and that T0 is ≤-interpolating. Thus, there exists a term t1 containing only constants common to A0 and B0 such that

A0∧B0 |=T0 c1 ≤ t1 ∧ t1 ≤ d1. (5) Let cf(t1) be a new constant, denoting the term f (t1), and let

CA = c1 ≤ t1→c ≤ cf(t1) and

CB = t1 ≤ d1→cf(t1) ≤ d.

By the induction hypothesis for A0∧B0∧c ≤ cf(t1)∧cf(t1) ≤ d and H1 = H\C we know that there exists a set T ′ of terms such that A0 ∧B0 ∧c ≤ cf(t1) ∧cf(t1) ≤ d ∧ (H1\H1mix) ∧ H1sep ∧ ¬(a ≤ t ∧ t ≤ b) |=⊥, and also (2) holds. Then (1) holds for T = T ′∪{f (t1), t1}.

(b) Assume that C corresponds to an instance of a monotonicity axiom x ≤ y → f (x) ≤ f (y). This means that there exist c ≈ f (c1) ∈ DefA and d ≈ f (d1) ∈ DefB. We know that A0 ∧ B0 |=T0 c1 ≤ d1 and that T0 is ≤-interpolating. Thus, there exists a term t1 containing only constants common to A0 and B0 such that A0∧B0 |=T0 c1 ≤ t1 ∧ t1 ≤ d1. (6) Let cf(t1) be a new constant, denoting the term f (t1), and let

CA = c1 ≤ t1→c ≤ cf(t1) and

CB = t1 ≤ d1→cf(t1) ≤ d.

Thus, CA corresponds to the instance c1 ≤ t1→f (c1) ≤ f (t1) of the monotonicity axiom for f , whereas CB corresponds to the instance t1 ≤ d1→f (t1) ≤ f (d1) of the monotonicity axiom for f . The proof can then continue as the proof of case (a); also in this case we can choose T = T ′∪{f (t1), t1}. (2) can be proved similarly using the induction hypothesis. ⊓⊔

[1]

Alrabbaa ,

Baader ,

Borgwardt ,

Koopmann , and

Kovtunova . Finding small proofs for description logic entailments: Theory and practice . In E. Albert and L . Kova´cs, editors, LPAR 2020: 23rd International Conference on Logic for Programming , Artificial Intelligence and Reasoning , EPiC Series in Computing 73 , pages 32 - 67 . EasyChair, 2020 .

[2]

M. F.

Arif , C. Menc´ıa, A . Ignatiev,

Manthey ,

Pen

˜aloza, and

J. MarquesSilva.

BEACON: an efficient sat-based tool for debugging E L+ ontologies . In N. Creignou and D. L . Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Proceedings, LNCS 9710 , pages 521 - 530 . Springer, 2016 .

[3]

Baader . Terminological cycles in a description logic with existential restrictions . In G. Gottlob and T. Walsh, editors, IJCAI-03, Proceedings of the 18th International Joint Conference on Artificial Intelligence , pages 325 - 330 . Morgan Kaufmann, 2003 .

[4]

Baader and

Hollunder . Embedding defaults into terminological knowledge representation formalisms . J. Autom. Reasoning , 14 ( 1 ): 149 - 180 , 1995 .

[5]

Baader ,

Lutz , and

Suntisrivaraporn . Efficient reasoning in E L+ . In B. Parsia,

Sattler , and D. Toman, editors, Proceedings of the 2006 International Workshop on Description Logics (DL2006) , CEUR Workshop Proceedings 189. CEUR-WS.org , 2006 .

[6]

Baader ,

Lutz , and

Suntisrivaraporn . Is tractable reasoning in extensions of the description logic E L useful in practice? Journal of Logic, Language and Information , 2007 . Special issue on Method for Modality (M4M ), 2007 .

[7]

Baader , R. Pen˜aloza, and

Suntisrivaraporn . Pinpointing in the description logic E L . In D. Calvanese,

Franconi ,

Haarslev ,

Lembo ,

Motik ,

Turhan , and S. Tessaris, editors, Proceedings of the 2007 International Workshop on Description Logics (DL2007) , CEUR Workshop Proceedings 250. CEURWS.org , 2007 .

[8]

Baader , R. Pen˜aloza, and

Suntisrivaraporn . Pinpointing in the description logic E L+ . In J. Hertzberg,

Beetz , and R. Englert, editors, KI 2007: Advances in Artificial Intelligence, 30th Annual German Conference on AI, KI 2007 , Proceedings , LNCS 4667 , pages 52 - 67 . Springer, 2007 .

[9]

Borgida , E. Franconi, and I. Horrocks. Explaining ALC subsumption . In W. Horn, editor, ECAI 2000, Proceedings of the 14th European Conference on Artificial Intelligence , pages 209 - 213 . IOS Press, 2000 .

[10]

Bourgaux ,

Ozaki , R. Pen˜aloza, and

Predoiu . Provenance for the description logic E LHr . In C. Bessiere, editor, Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020 , pages 1862 - 1869 . ijcai.org, 2020 .

[11]

Kazakov and

Skocovsky ´. Enumerating justifications using resolution . In D. Galmiche,

Schulz , and R. Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018 , Held as Part of the Federated Logic Conference , FloC 2018 , Proceedings, LNCS 10900 , pages 609 - 626 . Springer, 2018 .

[12]

Konev ,

Ludwig ,

Walther , and

Wolter . The logical difference for the lightweight description logic E L . J. Artif . Intell. Res. , 44 : 633 - 708 , 2012 .

[13]

Konev ,

Walther , and

Wolter . Forgetting and uniform interpolation in large-scale description logic terminologies . In C. Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence , pages 830 - 835 , 2009 .

[14]

Ludwig . Just: a tool for computing justifications w .r.t. E LH ontologies . In S. Bail,

Glimm , E.

Jim´enez-

Ruiz , N.

Matentzoglu , B.

Parsia , and A . Steigmiller, editors, Informal Proceedings of the 3rd International Workshop on OWL Reasoner Evaluation (ORE 2014 ) co-located with the Vienna Summer of Logic (VSL 2014 ), CEUR Workshop Proceedings 1207 , pages 1 - 7 . CEUR-WS.org, 2014 .

[15]

Lutz , I. Seylan , and

Wolter . An automata-theoretic approach to uniform interpolation and approximation in the description logic E L . In G. Brewka,

Eiter , and S. A . McIlraith, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference , KR 2012 . AAAI Press, 2012 .

[16]

Lutz , I. Seylan , and

Wolter . The data complexity of ontology-mediated queries with closed predicates . Log. Methods Comput. Sci. , 15 ( 3 ), 2019 .

[17]

Ozaki and

Pen ˜aloza. Consequence-based axiom pinpointing . In D. Ciucci, G. Pasi, and B. Vantaggi, editors, Scalable Uncertainty Management - 12th International Conference, SUM 2018, Proceedings, LNCS 11142 , pages 181 - 195 . Springer, 2018 .

[18]

Schlobach and

Cornet . Non-standard reasoning services for the debugging of description logic terminologies . In G. Gottlob and T. Walsh, editors, IJCAI-03, Proceedings of the 18th International Joint Conference on Artificial Intelligence , pages 355 - 362 . Morgan Kaufmann, 2003 .

[19]

Sofronie-Stokkermans . Hierarchic reasoning in local theory extensions . In R. Nieuwenhuis, editor, Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Proceedings, LNCS 3632 , pages 219 - 234 . Springer, 2005 .

[20]

Sofronie-Stokkermans . Automated theorem proving by resolution in nonclassical logics . Ann. Math. Artif. Intell., 49 ( 1-4 ): 221 - 252 , 2007 .

[21]

Sofronie-Stokkermans . Interpolation in local theory extensions . Logical Methods in Computer Science , 4 ( 4 ), 2008 .

[22]

Sofronie-Stokkermans . Locality and subsumption testing in E L and some of its extensions . In F. Baader,

Lutz , and B. Motik, editors, Proceedings of the 21st International Workshop on Description Logics (DL2008) , CEUR Workshop Proceedings 353. CEUR-WS.org , 2008 .

[23]

Sofronie-Stokkermans . Locality and subsumption testing in E L and some of its extensions . In C. Areces and R. Goldblatt, editors, Advances in Modal Logic 7 , pages 315 - 339 . College Publications, 2008 .

[24]

Sofronie-Stokkermans . Representation theorems and locality for subsumption testing and interpolation in the description logics E L, E L+ and their extensions with n-ary roles and numerical domains . Fundam . Inform., 156 ( 3-4 ): 361 - 411 , 2017 .

[25]

Sofronie-Stokkermans and

Ihlemann . Automated reasoning in some local extensions of ordered structures . Multiple-Valued Logic and Soft Computing , 13 ( 4- 6 ): 397 - 414 , 2007 .

[26]

K. A.

Spackman . Normal forms for description logic expressions of clinical concepts in SNOMED RT . In AMIA 2001 , American Medical Informatics Association Annual Symposium . AMIA, 2001 .

[27]

K. A.

Spackman , K. E. Campbell, and R. A. Cˆot´e. SNOMED RT: a reference terminology for health care . In AMIA 1997 , American Medical Informatics Association Annual Symposium . AMIA, 1997 .

[28]

Suntisrivaraporn . Polynomial time reasoning support for design and maintenance of large-scale biomedical ontologies . PhD thesis , Dresden University of Technology, Germany, 2009 .

Thus , CA corresponds to the instance c1 ≤ t1→f (c1) ≤ f (t1) of the monotonicity axiom for f , whereas CB corresponds to the rule t1 ≤ g(e)→f (t1) ≤ h(e). As A0 ∧ B0 |= c1 ≤ t1 ∧ t1 ≤ c1 and as ≤ is transitive, by (5):