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 EL and EL + . We use the encoding of TBox subsumption for EL 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 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 EL and EL + . In [7] and [8] Baader et al. give a similar algorithm for axiom pinpointing in the description logics EL and EL + , respectively, in which they modify the subsumption algorithm for EL (respectively EL + ). 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 EL-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 EL 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. 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.)

: part-of • part-of ⊑ part-of R2 : has-location • part-of ⊑ has-location

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 T A ∪ RI and the B-part is the CBox T B ∪ RI, where T A and T B are TBoxes. We are interested in finding simple explanations for consequences w.r.t. this extended CBox. One such consequence is Endocarditis ⊑ Heartdisease. Note that T A ∪ T B ∪ RI |= Endocarditis ⊑ Heartdisease, but T A ∪ RI Endocarditis ⊑ Heartdisease and T B ∪ RI 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 T A ∪ T B ∪ RI |= Endocarditis ⊑ Heartdisease. Formally this means that we try to find a concept description C which contains only shared symbols of T A and

T B such that T A ∪ RI |= Endocarditis ⊑ C and T A ∪ T B ∪ 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 T A ∪ T B ∪ RI |= Endocarditis ⊑ Heartdisease. The details are presented in Section 4.

Preliminaries

The central notions in description logics are concepts and roles. In any description logic a set N C of concept names and a set N R of roles is assumed to be given. Complex concepts are defined starting with the concept names in N C , 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 ∈ N C to a set C I ⊆ ∆ I and each role name r ∈ N R to a binary relation r I ⊆ ∆ I × ∆ I .

The description logics EL, EL + and some extensions. If we only allow intersection and existential restriction as concept constructors, we obtain the description logic EL [3], a logic used in terminological reasoning in medicine [27,26]. Fig. 2 shows the constructor names used in the description logic EL and their semantics. The extension of • I to concept descriptions is inductively defined using the semantics of the constructors. In [6,5], the extension EL + of EL with role inclusion axioms is studied. Relationships between concepts and roles are described using TBoxes or, more generally, CBoxes. 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, ∧, {f S } f ∈Σ ), such that, for every f ∈ Σ, f S : S → S is a monotone function, i.e. f satisfies:

• • • • • r I n ⊆ s I for all r 1 • • • • • r n ⊆ s ∈ RI. -If C is a CBox,Mon(Σ) = f ∈Σ ∀x, y x ≤ y → f (x) ≤ f (y) .

When defining the semantics of EL or EL + with role names N R 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 ∈ N C is regarded as a variable C = C. -C 1 ⊓ C 2 = C 1 ∧ C 2 and ∃rC = f ∃r C.

If RI is a set of role inclusions of the form r ⊑ s and r 1 • r 2 ⊑ s, let RI a 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 r 1 • r 2 ⊑ s ∈ RI

We will denote by SLO ∃ NR (RI a ) the class of all semilattices with monotone operators in which all axioms in RI a hold.

Theorem 3 ([23]

). If the only concept constructors are intersection and existential restriction, then for all concept descriptions D 1 , D 2 and every EL + CBox C=GCI∪RI -where RI consists of role inclusions of the form r ⊑ s and r 1 • r 2 ⊑ s -with concept names N C = {C 1 , . . . , C n } and set of roles N R the following are equivalent:

(1) D 1 ⊑ C D 2 . (2) SLO ∃ NR (RI a ) |= ∀C 1 . . . C n C⊑D∈GCI C≤D → D 1 ≤D 2 .

In [23,24] we showed that the uniform word problem for the class of algebras SLO ∃ NR (RI a ) is decidable in PTIME. For this, we proved that SLO ∃ NR (RI a ) 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 ∪ G 0 ∪ 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 c t , and adding t ≈ c t to the set Def.

The following are equivalent (and equivalent to ( 1) and ( 2) above):

(3) Mon(Σ)[G] 0 ∪ G 0 ∪ Def has no partial model A such that its {∧}-reduct is a semilattice, and all Σ-subterms of G are defined. ( 4)

Mon(Σ)[G] 0 ∪ G 0 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 ′ → c f (g) =c f (g ′ ) | f (g)=c f (g) , f (g ′ )=c f (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 RI a axioms of the form:

∀x g(x) ≤ h(x) (1) ∀x f (g(x)) ≤ h(x)(2)

resp. their flattened version RI flat a , in which ( 2) is replaced by (3):

∀x y ≤ g(x) → f (y) ≤ h(x)(3)

Theorem 5 ([24]). Let SL be a local axiomatization of the theory of semilattices. The following are equivalent:

(1) SL ∪ Mon(Σ) ∪ RI flat a |= ∀x n i=1 s i (x) ≤ s ′ i (x) → s(x) ≤ s ′ (x); (2) SL ∪ Mon(Σ) ∪ RI flat a ∧ G |=⊥, where G = n i=1 s i (c)≤s ′ i (c)∧s(c) ≤s ′ (c); (3) (SL ∪ Mon(Σ) ∪ RI flat a )[Ψ RI (G)] ∧ G |=⊥ where Ψ RI (G) = i≥0 Ψ i RI , with Ψ 0 RI =st(G) and Ψ i+1 RI ={f 2 (d) | f (d) ∈ Ψ i RI , (y≤f 2 (x)→f 1 (y)≤f (x)) ∈ RI flat a }.

An example that illustrates the way the method for hierarchical reasoning can be used in this case is given in Appendix A.

P -Interpolation Property

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. T 0 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. T 0 is strongly P -interpolating, if there exists such a term t with A |= T0 aRt and B |= T0 tRb. 1Proving P -interpolability is sometimes easier for theories which are P -convex. Definition 7. A theory T 0 is convex with respect to the set Pred of all predicates (which may include also equality ≈) if for all conjunctions Γ of ground atoms, relations R 1 , . . . , R m ∈ Pred and ground tuples of corresponding arity t 1 , . . . , t n , if Γ |= T0 m i=1 R i (t i ) then there exists j ∈ {1, . . . , m} such that Γ |= T0 R j (t j ).

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.

Proof: This is a constructive proof based on the fact that SLat = ISP (S 2 ) (i.e. every semilattice is isomorphic to a sublattice of a power of S 2 ), where S 2 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(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. 2Every e ∈ T = {e | A |= a ≤ e, e common subterm of A and B} corresponds to the positive unit clause P e (where P e is a propositional variable common to N A and N B ) which can be derived from N A using ordered resolution (with the ordering described above). It is clearly the case that A |= SLat a ≤ t, because N A ∧P a ∧¬P t ∧(P t ↔ e∈T P e ) is unsatisfiable. Thus, (i) holds. For proving (ii), observe that by saturating N A ∧P a under ordered resolution we obtain the following kinds of clauses containing only shared symbols which can possibly lead to ⊥ after inferences with N B ∧¬P b (and thus to the consequence a ≤ b together with B). 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 N B ∧ ¬P b (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 {P ei | 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 = {a 1 ≤ c 1 , c 2 ≤ a 2 , a 2 ≤ c 3 } and B = {c 1 ≤ b 1 , b 1 ≤ c 2 , c 3 ≤ b 2 }. It is easy to see that A ∧ B |= a 1 ≤ b 2 .

We can find an intermediate term by using the methods described in the proof: We saturate N A ∧ P a1 = (P a1 → P c1 )∧(P c2 → P a2 )∧(P a2 → P c3 )∧P a1 under ordered resolution, in which the symbols P a1 , P a2 are larger than P c1 , P c2 , P c3 . This yields the clauses P c1 and [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

P c2 → P c3 containing shared propositional variables. (N A ∧ P a1 ) ∧ (N B ∧ ¬P b2 ) is unsatisfiable iff N B ∧ ¬P b2 ∧ P c1 ∧ (P c2 → P c3 ) is unsatisfiable. Indeed t = c 1 is an intermediate term, as A |= a 1 ≤ c 1 and A ∧ B |= c 1 ≤ b 2 . Note that N B ∧¬P b2 ∧P c1 is satisfiable, so B |= c 1 ≤ b 2 . Moreover,A 0 ∧ H A ∧ B 0 ∧ H B ∧ ¬(a 0 ≤ t 0 ∧ t 0 ≤ b 0 ) |= SLat ⊥,

where t 0 contains only constants common to A 0 and B 0 . After replacing back the new constants with the terms they represent, we obtain:

A ∧ B |= SLO ∃ N R (RIa) (a ≤ t ∧ t ≤ b)

, where t contains symbols common to A and B. 3⊓ ⊔

≤-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 T A and T B be two EL + TBoxes and RI a set of role inclusions. Let N C be the set of all concept names occurring in T A ∪ T B , N A C and N B C be the set of concept names occurring in T A and T B , respectively, and

N AB C = (N A C ∩ N B C

) be the common concept names. Let X be a concept description over N A C and Y a concept description over N B C such that they do not contain only shared symbols and such that 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:

T A ∪ T B ∪ RI |= X ⊑ Y , but T A ∪ RI |= X ⊑ Y and T B ∪ RI |= X ⊑ Y

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): 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:

N A C = {Endocardium(

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 : Em ≤ T A2 : Em ≤ po(HW) A3 : HW ≤ BW A4 : HW ≤ po(LV) A5 : HW ≤ po(RV) A6 : LV ≤ V A7 : RV ≤ V A8 : Es ≤ I A9 : Es ≤ hl(Em) A10 : I ∧ hl(Em) ≤ Es A11 : I ≤ D A12 : I ≤ ao(T) B1 : V ≤ po(H) B2 : HD ≤ D B3 : HD ≤ hl(H) B4 : D ∧ hl(H) ≤ HD R1 : ∀X: po(po(X)) ≤ po(X) R2 : ∀X: hl(po(X)) ≤ hl(X) M1 : ∀X,Y: X ≤ Y → po(X) ≤ po(Y) M2 : ∀X,Y: X ≤ Y → hl(X) ≤ hl(Y) M3 : ∀X,Y: X ≤ Y → ao(X) ≤ ao(Y)

Fig. 3: Ontology after translation to SLat with monotone operators 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

min A = {A 2 , A 4 , A 6 , A 8 , A 9 , A 11 , B 1 , B 4 , R 2 }.

This means that for the following instantiation step we only have to consider the role axiom R 2 and none of the monotonicity axioms is needed.

Step 2: Let T 0 = SLat and T 1 = SLat∪R 2 be the extension of T 0 with axiom R 2 .

We know that it is a local theory extension, so we can use hierarchical reasoning. We first flatten the role axiom R 2 in the following way:

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

I1 : Em ≤ po(HW) → hl(Em) ≤ hl(HW) I2 : Em ≤ po(LV) → hl(Em) ≤ hl(LV) I3 : Em ≤ po(RV) → hl(Em) ≤ hl(RV) I4 : Em ≤ po(H) → hl(Em) ≤ hl(H) I5 : HW ≤ po(LV) → hl(HW) ≤ hl(LV) I6 : HW ≤ po(RV) → hl(HW) ≤ hl(RV) I7 : HW ≤ po(H) → hl(HW) ≤ hl(H) I8 : LV ≤ po(HW) → hl(LV) ≤ hl(HW) I9 : LV ≤ po(RV) → hl(LV) ≤ hl(RV) I10 : LV ≤ po(H) → hl(LV) ≤ hl(H) I11 : RV ≤ po(HW) → hl(RV) ≤ hl(HW) I12 : RV ≤ po(LV) → hl(RV) ≤ hl(LV) I13 : RV ≤ po(H) → hl(RV) ≤ hl(H) I14 : H ≤ po(HW) → hl(H) ≤ hl(HW) I15 : H ≤ po(LV) → hl(H) ≤ hl(LV) I16 : H ≤ po(RV) → 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: Step 3a: Computing an unsatisfiable core yields the following set of axioms: {A 2 , A

Def = {po HW = po(LV ≤ V → hl LV ≤ hl V I B 10 : V ≤ po H → hl V ≤ hl H

Note that I A 10 is an instance of the monotonicity axiom for the has-location role and I B 10 is an instance of axiom R flat 2 .

Step 4: Note that w.r.t. SLat the formula A 0 ∧ I 1 ∧ I 5 ∧ I A 10 is equivalent to:

A 0 = Em ≤ po HW ∧ HW ≤ po LV ∧ LV ≤ V ∧ Es ≤ I ∧ Es ≤ hl Em ∧ I ≤ D ∧ hl EM ≤ hl HW ∧ hl HW ≤ hl LV ∧ hl LV ≤ hl V

To obtain an explanation for T A ∪ T B ∪ RI |= Endocarditis ⊑ HeartDisease we saturate the set A 0 ∧ 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 hl V . By taking the conjunction of these terms and translating the formula back to description logic, we obtain J = Disease ⊓ ∃has-location.Ventricle. Then T A ∪ RI |= Endocarditis ⊑ J and T A ∪ T B ∪ RI |= J ⊑ HeartDisease.

Conclusion

We analyzed a possibility of giving high-level justifications for subsumption in the description logics EL and EL + . For this, we used the encoding of TBox subsumption as a uniform word problem in classes of semilattices with monotone operators for EL 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 EL 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 EL 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.

A Example of local reasoning in EL +

We illustrate the ideas on the example from Section 1.1. Consider the CBox C consisting of the following GCI:

A 1 − A 2 Endocardium ⊑ Tissue ⊓ ∃part-of.HeartWall A 4 HeartWall ⊑ ∃part-of.LeftVentricle A 6 LeftVentricle ⊑ Ventricle A 8 − A 9

Endocarditis ⊑ Inflammation ⊓ ∃has-location.Endocardium

A 11 Inflammation ⊑ Disease B 1 Ventricle ⊑ ∃part-of.Heart B 2 − B 4

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.):

SL ∪ Mon(hl, po) ∪ {∀x y≤po(x) → po(y)≤po(x), ∀x y≤po(x) → hl(y)≤hl(x)} ∪ {Em ≤ T ∧ po(HW), HW ≤ po(LV), LV ≤ V, V ≤ po(H), I ≤ D, Endocarditis ≤ I ∧ hl(Em), Heartdisease = D ∧ hl(H), Endocarditis ≤ Heartdisease} |= ⊥ .

Then st(K, G) = {po(HW), po(LV), po(H), hl(Em), hl(H)}. To compute Ψ K (G), note that Ψ 0 RI = st(K, G), Ψ 1 RI = {po(Em), po(H)}, and Ψ 2 RI = Ψ 1 RI . Thus, Ψ K (G) = {po(HW), po(LV), po(Em), po(H), hl(Em), hl(H)}. After computing (RI a ∪ Mon(hl, po) ∪ Con)[Ψ (G)] we obtain the following conjunction of (Horn) ground clauses:

G (RIa ∧ Mon ∧ Con)[Ψ (G)]∧SL[Ψ (G)] Em ≤ T ∧ po(HW) y≤po(x) → po(y)≤po(x) for x, y ∈ {HW, LV, Em, H} HW ≤ po(LV), y≤po(x) → hl(y) ≤ hl(x) for x, y ∈ {Em, H} LV ≤ V V ≤ po(H) xRy → po(x)Rpo(y) for x, y ∈ {HW, LV, Em, H} Endocarditis ≤ I ∧ hl(Em) xRy → hl(x)Rhl(y) for x, y ∈ {Em, H} I ≤ D R ∈ {≤, ≥, =} Heartdisease = D ∧ hl(H) Endocarditis ≤ Heartdisease SL[Ψ (G)] By Theorem 5, Endocarditis ⊑ C Heartdisease iff φ = G ∧ (RI a ∧ 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

-|= SLat A ∧ B → a ≤ b -|= SLat ¬A 1 ∨ • • • ∨ ¬A n ∨ A ′ 1 ∨ • • • ∨ A ′ m ∨ a ≤ b -|= SLat (A 1 ∧ • • • ∧ A n ) → A ′ 1 ∨ • • • ∨ A ′ m ∨ a ≤ b -A 1 ∧ • • • ∧ A n |= SLat A ′ 1 ∨ • • • ∨ A ′ m ∨ 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) A 1 ∧ • • • ∧ A n |= SLat A ′ j for some j ∈ {1, . . . , m} or (b) A 1 ∧ • • • ∧ A n |= 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 (S 2 ), in SLat the same Horn sentences are true as in the 2-element semilattice S 2 . Thus,

A ∧ B |= SLat a ≤ b iff A ∧ B |= S2 a ≤ b,↔ P g2 g 1 ≈ g 2 ∈ B P g1 → P g2 g 1 ≤ g 2 ∈ B ¬P b

for all e, e 1 , e 2 subterms in A for all g, g 1 , g 2 subterms in B

We obtain an unsatisfiable set of clauses 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 P e (where P e is a propositional variable common to N A and N B ) which can be derived from N A using ordered resolution (with the ordering described above).

It is clearly the case that A |= SLat a ≤ t, because N A ∧P a ∧¬P t ∧(P t ↔ e∈T P e ) is unsatisfiable. Thus, (i) holds.

For proving (ii), observe that by saturating N A ∧ P a under ordered resolution we obtain the following kinds of clauses which can possibly lead to ⊥ after inferences with N B ∧ ¬P b (and thus to the consequence a ≤ b together with B): Other types of clauses may appear too, but they can not be used to obtain a ≤ b:

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

∧ i,j ¬P cij is satisfiable. Every model of N B ∧ k∈S1 P e k ∧ ¬P b ∧ i,j ¬P cij is a model of N AB ∧ ¬P b .

It would therefore follow that N AB ∧ ¬P b is satisfiable, which is a contradiction. Thus, there exists at least one c ij such that N B ∧ k∈S1 P e k ∧ ¬P b |= P cij . We can add P cij 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 (( j P cij ) → P di ) in N AB such that there exists at least one c ij such that P cij was not added to N AB .

Then there has to be a sequence (d i1j ) j∈J1 , (d i2j ) j∈J2 , ..., (d inj ) j∈Jn such that:

-P di 1 j can be derived from N AB ∧ P e k , for all j ∈ J 1 , -P di 2 j can be derived from N AB ∧ P e k ∧ k∈J1 d i1k , for all j ∈ J 2 , -P di 3 j can be derived from N AB ∧ P e k ∧ k∈J1 d i1k ∧ k∈J2 d i2k , for all j ∈ J 3 , . . .

-P di n j can be derived from

N AB ∧ k P e k ∧ k∈J1 d i1k ∧ • • • k∈Jn−1 d in−1k ,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 Π c 0 -terms containing only constants common to A 0 and B 0 and a term t ∈ T such that

A 0 ∧ B 0 ∧ (H\H mix ) ∧ H sep |= T0 a ≤ t ∧ t ≤ b,

where

H mix = {a 1 ≤ b 1 → a 2 ≤ b 2 ∈ H | a 1 , a 2 constants in A, b 1 , b 2 constants in B}∪ {b 1 ≤ a 1 → b 2 ≤ a 2 ∈ H | b 1 , b 2 constants in B, a 1 , a 2 constants in A} H sep = {(a 1 ≤ t 1 →a 2 ≤ c f (t1) ) ∧ (t 1 ≤ b 1 →c f (t1) ≤ b 2 ) | a 1 ≤b 1 →a 2 ≤b 2 ∈ H mix , b 1 ≈ g(e 1 ), b 2 ≈ h(e 1 ) ∈ Def B , a 2 ≈ f (a 1 ) ∈ Def A or vice versa, and t 1 , f (t 1 ) ∈ T } = H A sep ∧ H B sep

where c f (t1) are new constants in Σ c (considered to be common) introduced for the corresponding terms f (t 1 ).

(

) A 0 ∧ B 0 ∧ (H\H mix ) ∧ H sep ∧ ¬(a ≤ t ∧ t ≤ b) is logically equivalent w.r.t. T 0 with the separated conjunction of literals A 0 ∧ B 0 ∧ ¬(a ≤ t ∧ t ≤ b) = A 0 ∧ B 0 ∧ {c ≤ d | Γ →c ≤ d ∈ H\H mix } ∧ {c ≤ c f (t) ∧ c f (t) ≤ d | (Γ → c ≤ c f (t) ) ∧ (Γ → c f (t) ≤ d) ∈ H sep } ∧ ¬(a ≤ t ∧ t ≤ b).2

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 A 0 ∧ B 0 |= T0 a ≤ b and since we assumed that T 0 is ≤-interpolating, there exists a term t containing only constants common to A 0 and B 0 such that A 0 ∧ B 0 |= T0 a ≤ t ∧ t ≤ b (we can choose T = {t}).

Assume that H contains at least one clause, and that for every H 1 with fewer clauses and every conjunction of literals

A ′ 0 , B ′ 0 with A ′ 0 ∧ B ′ 0 ∧ H 1 |= 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 ofA 0 ∧ B 0 ∧ (c≤d)∈D ¬(c ≤ d) ∧ ¬(a ≤ b) is also a model for H∧A 0 ∧B 0 ∧¬(a ≤ b) and H∧A 0 ∧B 0 ∧¬(a ≤ b) |= T0 ⊥, A 0 ∧B 0 ∧ (c≤d)∈D ¬(c ≤ d) ∧ ¬(a ≤ b) |= T0 ⊥. Let (A 0 ∧ B 0 ) + be

the conjunction of all positive literals in A 0 ∧ B 0 , and (A 0 ∧ B 0 ) − be the set of all negative literals in A 0 ∧ B 0 . Then

(A 0 ∧ B 0 ) + |= T0 (c≤d)∈D (c ≤ d) ∨ ¬L∈(A0∧B0) − L ∨ (a ≤ b).

T 0 is convex with respect to ≤ and (A 0 ∧B 0 ) + is a conjunction of positive literals. Therefore, either

(i) (A 0 ∧ B 0 ) + |= L for some L ∈ (A 0 ∧ B 0 ) − (then A 0 ∧ B 0 is unsatisfiable and hence entails any atom c i ≤ d i ), or (ii) (A 0 ∧ B 0 ) + |= a ≤ b, or (iii) there exists (c 1 ≤ d 1 ) ∈ D such that A 0 ∧ B 0 |= T0 c 1 ≤ d 1 .

Case 1: A 0 ∧ B 0 is unsatisfiable. In this case (1) and (2) hold for T = {t}, where t is an arbitrary term over the common symbols of A 0 and B 0 . (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 (c 1 ) ∈ Def A and d 1 ≈ g(e), d ≈ h(e) ∈ Def B . We know that A 0 ∧ B 0 |= T0 c 1 ≤ d 1 and that T 0 is ≤-interpolating. Thus, there exists a term t 1 containing only constants common to A 0 and B 0 such that

A 0 ∧B 0 |= T0 c 1 ≤ t 1 ∧ t 1 ≤ d 1 .

(

)5

Let c f (t1) be a new constant, denoting the term f (t 1 ), and let

C A = c 1 ≤ t 1 →c ≤ c f (t1) and C B = t 1 ≤ d 1 →c f (t1) ≤ d.

Thus, C A corresponds to the instance c 1 ≤ t 1 →f (c 1 ) ≤ f (t 1 of the monotonicity axiom for f , whereas C B corresponds to the rule t 1 ≤ g(e)→f (t 1 ) ≤ h(e).

As A 0 ∧ B 0 |= c 1 ≤ t 1 ∧ t 1 ≤ c 1 and as ≤ is transitive, by (5): By the induction hypothesis for A 0 ∧B 0 ∧c ≤ c f (t1) ∧c f (t1) ≤ d and H 1 = H\C we know that there exists a set T ′ of terms such that A 0 ∧B 0 ∧c ≤ c f (t1) ∧c f (t1) ≤ d ∧ (H 1 \H 1mix ) ∧ H 1sep ∧ ¬(a ≤ t ∧ t ≤ b) |=⊥, and also (2) holds. Then (1) holds for T = T ′ ∪{f (t 1 ), t 1 }.

A 0 ∧ B 0 ∧ C A ∧ C B |=| T0 A 0 ∧ B 0 ∧ (c 1 ≤ t 1 ∧ C A ) ∧ (t 1 ≤ d 1 ∧ C B ) |=| T0 A 0 ∧ B 0 ∧ c ≤ c f (t1) ∧ c f (t1) ≤ d |= T0 A 0 ∧ B 0 ∧ c ≤ d,

(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 (c 1 ) ∈ Def A and d ≈ f (d 1 ) ∈ Def B . We know that A 0 ∧ B 0 |= T0 c 1 ≤ d 1 and that T 0 is ≤-interpolating. Thus, there exists a term t 1 containing only constants common to A 0 and B 0 such that

A 0 ∧B 0 |= T0 c 1 ≤ t 1 ∧ t 1 ≤ d 1 .(6)

Let c f (t1) be a new constant, denoting the term f (t 1 ), and let

C A = c 1 ≤ t 1 →c ≤ c f (t1) and C B = t 1 ≤ d 1 →c f (t1) ≤ d.

Thus, C A corresponds to the instance c 1 ≤ t 1 →f (c 1 ) ≤ f (t 1 ) of the monotonicity axiom for f , whereas C B corresponds to the instance t 1 ≤ d 1 →f (t 1 ) ≤ f (d 1 ) 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 (t 1 ), t 1 }.

(2) can be proved similarly using the induction hypothesis. ⊓ ⊔