Making Quantification Relevant Again —the Case of Defeasible EL⊥ Maximilian Pensel and Anni-Yasmin Turhan∗ Institute for Theoretical Computer Science, Technische Universität Dresden first-name.last-name @tu-dresden.de Abstract. Defeasible Description Logics (DDLs) extend Description Log- ics with defeasible concept inclusions. Reasoning in DDLs often employs rational or relevant closure according to the (propositional) KLM pos- tulates. If in DDLs with quantification a defeasible subsumption rela- tionship holds between concepts, this relationship might also hold if these concepts appear in existential restrictions. Such nested defeasi- ble subsumption relationships were not detected by earlier reasoning algorithms—neither for rational nor relevant closure. Recently, we de- vised a new approach for EL⊥ that alleviates this problem for rational closure by the use of typicality models that extend classical canonical models by domain elements that individually satisfy any amount of con- sistent defeasible knowledge. In this paper we lift our approach to rele- vant closure and show that reasoning based on typicality models yields the missing entailments. 1 Introduction Description Logics (DLs) are usually decidable fragments of First Order Logic. In DLs concepts describe groups of objects by means of other concepts (unary FOL predicates) and roles (binary relations). Such concepts can be related to other concepts as sub- and super-concepts in the TBox which is essentially a theory constraining the interpretation of the concepts. One of the main reasoning problems in DLs is to compute subsumption relationships between two given concepts, i.e., decide whether all instances of one concept must be necessarily instances of the other (w.r.t. the TBox). While classical DLs allow only for monotonic reasoning, defeasible DLs ad- mit a form of non-monotonic reasoning and have been intensively studied in the last years [5,6,7,3,4,8]. Most defeasible DLs allow to state relationships between concepts by defeasible concept inclusions (DCIs), which characterise typical in- stances of a concept and can be overwritten by more specific information that would otherwise cause an inconsistency. Often the semantics of defeasible DLs is ∗ This work is supported (in part) by the German Research Foundation (DFG) in the Research Training Group QuantLA (GRK 1763) and within the Collaborative Research Center SFB 912 – HAEC. 2 Maximilian Pensel and Anni-Yasmin Turhan based on a translation of propositional preferential and (the stronger) rational reasoning for conditional knowledge bases introduced by Kraus, Lehmann and Magidor (KLM) in [10] to DLs. Recent studies on DDLs investigate different se- mantics, such as a typicality operator under preferential model semantics in [8], a syntactic materialisation-based approach [5,4], characterised with a different kind of preferential model semantics in [3], and extensions of rational reasoning to the inferentially stronger lexicographic and relevant closure in [4,7]. We consider here an extension of the lightweight DL EL. In this DL complex concepts are built by conjunctions and existential restrictions, which are a form of quantification and clearly not expressible by propositional logic. The DL EL enjoys good computational properties: subsumption can be computed in polyno- mial time [2]. Despite its moderate expressivity, many applications rely on EL, predominantly the bio-medical domain and the web ontology language with the OWL 2 EL profile. In contrast to EL, its extension EL⊥ can express disjointness of concepts and thus inconsistencies. We consider in this paper non-monotonic subsumption under relevant closure in defeasible EL⊥ . In [5] Casini et al. showed that the complexity of non-monotonic subsumption coincides with the complexity of classical reasoning of the underlying DL and devise reasoning algorithms for defeasible subsumption under rational and rele- vant closure. Their algorithm uses a reduction to classical reasoning and thereby allows to employ highly optimised classical DL reasoners for the reasoning task. Their reduction uses materialisation, where the idea is to encode one consistent subset of the defeasible statements as a concept which is then used in the classical subsumption query as an additional constraint for the (potential) sub-concept in the query. Essentially, the algorithms for the two types of closure differ in the subsets of DCIs from the knowledge base they use for reasoning. While rational closure utilises only a single sequence of decreasing subsets of DCIs, the stronger relevant closure admits any such subset during reasoning. Thus relevant rea- soning is done w.r.t. a lattice of DCI sets which include more combinations of DCIs potentially leading to more fine-grained entailments. However, both of the resulting algorithms in [4,5,7] are not complete in the sense that not all expected subsumption relationships are inferred. The reason is, that defeasible knowledge is not propagated to concepts nested in existential restrictions and thus even un-defeated knowledge is omitted during reasoning. The goal of this paper is to devise a reduction algorithm for reasoning under relevant closure for EL⊥ that derives defeasible knowledge for concepts nested in existential restrictions. We have recently devised an approach that achieves this for reasoning under the weaker rational closure by the use of typicality models [11]. These models are an extension of the well-known canonical models for clas- sical DLs of the EL family where the domain consists of elements representing the concepts occurring in the TBox. Now, typicality models have representatives for each pair of a concept occurring in the TBox and a set of defeasible state- ments. Thus, for the case of relevant closure such typicality models are built over a lattice-shaped domain according to the lattice of DCI subsets. For a simple form of these typicality models we show that it results in the same entailments Making Quantification Relevant Again —the Case of Defeasible EL⊥ 3 as the materialisation-based approach [4] for relevant closure. We then extend the simple typicality models to remedy the mentioned shortcoming regarding existential restrictions. The main idea is, to admit in this kind of model differing “amounts” of consistent defeasible information for different occurrences of the same nested concept. This paper is structured as follows: the next section introduces the basic notions of (D)DLs and EL⊥ . Section 3 recalls the materialisation-based approach for rational and relevant closure and investigates their shortcomings. Section 4 introduces minimal typicality models over a lattice domain and shows that the same subsumption relationships under relevant closure can be inferred as by the materialisation-based approach from [4]. In Section 5 we extend these models to maximal typicality models over a lattice domain and show that these allow to obtain the formerly omitted entailments. The paper ends with conclusions and an outlook to future work. 2 Preliminaries We introduce here the basic notions of (defeasible) DLs and their inferences. Starting from the two disjoint sets NC of concept names and NR of role names, complex concepts can be defined inductively. Let C and D be EL-concepts and r ∈ NR , then (complex) EL-concepts are: named concepts (A ∈ NC ), the top- concept >, conjunctions C u D and existential restrictions ∃r.C. The DL EL⊥ extends EL by the bottom-concept ⊥, which can be used in conjunctions and existential restrictions. We will occasionally also use the concepts negation ¬C and disjunction C t D. The semantics of concepts is given by means of inter- pretations. An interpretation I = (∆I , ·I ) consists of an interpretation domain ∆I and a mapping function that assigns subsets of the domain ∆I to concept names and binary relations over ∆I to role names. The top-concept is inter- preted as the whole domain (>I = ∆I ) and the bottom-concept as the empty set (⊥I = ∅). The complex concepts are interpreted as follows: conjunction (C uD)I = C I ∩DI , negation (¬C)I = ∆I \C I , disjunction (C tD)I = C I ∪DI , and existential restriction (∃r.C)I = {d ∈ ∆I | ∃e.(d, e) ∈ rI and e ∈ C I }. If in an interpretation I (d, e) ∈ rI holds, then e is called a role successor of d. DL ontologies can state (monotonous) relationships between concepts. Let C and D be concepts. A general concept inclusion axiom (GCI) is of the form: C v D. A TBox T is a finite set of GCIs. A concept C is satisfied by an interpretation I iff C I 6= ∅. A GCI C v D is satisfied in an interpretation I, iff C I ⊆ DI (written I |= C v D). An interpretation I is a model of a TBox T, iff I satisfies all GCIs in T (written I |= T). Based on the notion of a model, DL reasoning problems are defined. A concept is consistent w.r.t. a TBox T iff some model of T satisfies the concept. A concept C is subsumed by a concept D w.r.t. a TBox T (written C vT D) iff C I ⊆ DI holds in all models I of T. We fix some notation to access parts of knowledge bases or concepts. Let X denote a concept or a TBox, then sig(X) denotes the signature of X. We define sigNC (X) = sig(X) ∩ NC and sigNR (X) = sig(X) ∩ NR . We also define the set 4 Maximilian Pensel and Anni-Yasmin Turhan Qc(X) of quantified concepts in X as F ∈ Qc(X) iff ∃r.F syntactically occurs in X for some r ∈ NR . In extensions of EL that are in the Horn fragment of DLs, canonical models are widely used for reasoning [2]. For an EL⊥ -TBox T, the ca- nonical model IT = (∆, ·IT ) of T with ∆ = {dF | F ∈ Qc(T )} has the mapping function satisfying the conditions dF ∈ AIT iff F vT A and (dF , dG ) ∈ rIT iff F vT ∃r.G. Once the canonical model is computed, subsumption relationships between concepts can be directly read-off from it [2,1]. In defeasible DLs it can be stated that instances of a concept are subsumed by another concept as long as there is no contradicting information. A defea- sible concept inclusion (DCI) is of the form C @ ∼ D and states that C usually entails D. A DBox D is a finite set of DCIs. A defeasible knowledge base (DKB) K = (T, D) consists of a TBox T and a DBox D. The definitions for sig(X), sigNC (X), sigNR (X) and Qc(X) extend to DBoxes or DKBs d in the obvious way. A materialisation of a DBox D is the concept D = E @F ∈D (¬E t F ). The ∼ semantics of DBoxes differ from the ones for TBoxes, since DCIs need not hold at each element in the model whereas GCIs do. The satisfaction of DCIs for d ∈ ∆I is captured by I, d |= D iff ∀G @ I I ∼ H ∈ D.d ∈ G =⇒ d ∈ H . Usually, the semantics of DBoxes is given by means of ranked/ordered interpretations— called preferential model semantics [3][8]. Instead of using these, we define a new kind of model for DKBs (in Sect. 4) that extends canonical models for EL⊥ . The main idea is to use several copies of the representatives, such as dF , for each existentially quantified concept, where each copy satisfies a different set of DCIs from the entire lattice built over (the subsets of) the DBox. We want to develop a decision procedure for (defeasible) subsumption rela- tionships between concepts, say C and D, w.r.t. a given DKB K under relevant closure. For the remainder of the paper we make two simplifying assumptions for the sake of ease of presentation. We assume w.l.o.g. that (1) concepts C and D appear syntactically in Qc(T) which can be achieved by adding ∃r.E v > with E ∈ {C, D} to T and (2) all quantified concepts in K are consistent i.e., ∀F ∈ Qc(K).F 6vT ⊥ and thus ⊥ ∈ / Qc(K). To motivate our approach for reasoning under relevant closure in defeasible EL⊥ , we discuss first earlier approaches for this task and identify their main shortcoming. 3 Minimal Relevant Closure by Materialisation We recall the reduction algorithms for reasoning by Casini et al. from [4]. Ratio- nal entailment in [4] uses materialisation of DCIs to decide defeasible subsump- tions C @ ∼ D w.r.t. a given DKB K = (T, D). Since C might be inconsistent w.r.t. the materialisation of the entire DBox D, the algorithm needs to determine a sub- set D0 ⊆ D whose materialisation is consistent with C and T in order to decide whether D0 uC vT D holds. To obtain D0 , D is iteratively reduced to that subset containing all DCIs whose left-hand side is inconsistent in conjunction with the materialisation of the current DBox: E(D) = {C @ ∼ D ∈ D | T |= DuC v ⊥}. De- fine E 1 (D) = E(D) and E j (D) = E(E j−1 (D)) (for j > 1). Using E(), the DCIs in Making Quantification Relevant Again —the Case of Defeasible EL⊥ 5 D can be ranked according to their level of exceptionality, i.e., rK (G @∼ H) = i−1, i for the smallest i s.t. G @ ∼ H ∈ 6 E (D), or rK (G @ ∼ H) = ∞ if no such i exists. A DKB K = (T, D) is well-separated if no DCI in D has an infi- nite rank of exceptionality [3]. We assume w.l.o.g. that all DKBs are well- separated: any DKB K = (T, D) can be transformed into a well-separated DKB K0 by testing a quadratic number of subsumptions in the size of D: K0 = T ∪ {C v ⊥ | rK (C @  ∼ D) = ∞}, D \ {C @ ∼ D | rK (C @ ∼ D) = ∞} . Based on the level of exceptionality, the algorithm from [4] partitions the DBox D into @ @ Sn(E0 , E1 , . . . , En ) where Ei = {G ∼ H ∈ D | rK (G ∼ H) = i}, i.e. D = i=0 Ei . To find the maximal (w.r.t. cardinality) subset D0 of D, whose materialisation is consistent with C and T the procedure starts with D0 = D. If D0 u C vT ⊥, then Ei is removed from D0 for the smallest not yet used i. This test and removal is done iteratively until a subset of D is reached whose materialisation is consistent with C and T. While rational closure treats inconsistencies with the granularity of the par- titions Ei , relevant closure uses a more fine-grained treatment. To illustrate this, let G @ ∼ H ∈ E0 and assume that C is only consistent with D\E0 (or its subsets). It need not hold, that (¬G t H) u D \ E0 u C vT ⊥, since the inconsistency may be due to other DCIs in E0 . Still G @ ∼ H is never used for reasoning about C. This effect is called inheritance blocking, as it might be possible to include G@ ∼ H for reasoning about C, but other DCIs induce some inconsistency and so block the inheritance of property G @ ∼ H for C. Relevant closure disregards only DCIs that are relevant for the inconsistency of C, thereby averting inheritance blocking. The notion of relevance is introduced in [4] in terms of justification. Definition 1. Let K = (T, D) be a DKB, J ⊆ D and C a concept. J is a C-justification w.r.t. K iff J u C vT ⊥ and J 0 u C 6vT ⊥ for all J 0 ⊂ J . Let justifications(K, C) = (J1 , . . . , Jm ) be the (exponential time [9]) procedure that determines and returns all minimal C-justifications w.r.t. K. To present a simplified (but equivalent) version of the algorithm from [4] for computing minimal relevant closure containment, we need to define the D0 ⊆ D that is consistent with C and ultimately used for deciding D0 u C vT D. Let partition(D) = (E0 , . . . , En ) be a function that computes the above defined partitioning of DBoxes and let J ⊆ D. Then min(partition(D), J ) returns Ei for the smallest i, s.t. J ∩ Ei 6= ∅. Given K = (T, D) and the subsumption query C @ ∼ D, we define the rank-minimal part of all C-justifications w.r.t. K as (M1 , . . . , Mm ) for (J1 , . . . , Jm ) = justifications(K, C), where Mi = Ji ∩ min(partition(D), Ji ), for 1 ≤ i ≤ m. In order to obtain a subset of D that is consistent with C, at least one statement from every justification has to be removed from D. By a preference of exceptionality rank and due to a lack of more refined preference1 , the removed Smstatements shall be the rank-minimal parts of all justifications, i.e. D0 = D \ ( i=1 Mi ). We denote non-monotonic entailments obtained by minimal relevant closure and materialisation as K |=m C @ ∼ D iff 0 0 D u C vT D for K = (T, D) and D as defined above. 1 Such as a quantitative ranking of DCIs. 6 Maximilian Pensel and Anni-Yasmin Turhan The following example illustrates the problem of inheritance blocking caused by rational closure, but not by minimal relevant closure. Example 2. Let Kex1 = (T ex1 , Dex1 ) with: T ex1 = {Boss v W orker, Boss u ∃superior.W orker v ⊥}, Dex1 = {W orker @ ∼ ∃superior.Boss, W orker @∼ P roductive, Boss @ ∼ Responsible}, and partition(Dex1 ) = E0 = {W orker @ ∼ ∃superior.Boss, W orker @ ∼ P roductive},  E1 = {Boss @ ∼ Responsible} . Rational closure recognises the inconsistency Dex1 u Boss vT ex1 ⊥, but it holds that Dex1 \ E0 u Boss 6vT ex1 ⊥. Thus Boss @ ∼ W orker u Responsible is entailed from Kex1 , while Boss @ ∼ P roductive is not, even though the DCI W orker @ ∼ P roductive does not cause the inconsistency of Boss. For minimal rel- evant closure, J1 = {W orker @ ∼ ∃superior.Boss} is the only Boss-justification w.r.t. Kex1 . Therefore, the largest consistent DBox subset of Dex1 for reasoning about the concept Boss is D0 = {W orker @ ∼ P roductive, Boss @ ∼ Responsible}, providing the consequence D0 u Boss vT ex1 P roductive. Example 2 also illustrates the issue caused by employing materialisation that is addressed in this paper. Materialising the DCI W orker @ ∼ P roductive to ¬W orker t P roductive in conjunction with ∃superior.W orker yields a con- cept that is not subsumed by ∃superior.P roductive. The defeasible informa- tion is unjustly disregarded when reasoning about quantified concepts yield- ing uniformly non-typical role successors. Hence, in Example 2, both rational and relevant closure (based on materialisation) are oblivious to the conclusion W orker @∼ ∃superior.Responsible. 4 Typicality Models for Propositional Relevant Entailment In order to achieve relevant entailment also for quantified concepts, DCIs need to hold for concepts in (nested) existential restrictions. A naive idea to ex- tend the materialisation approach is to enrich all concepts in existential restric- tions with materialisations of the DBox. However, for Example 2, enriching the concept ∃superior.Boss with W orker @ ∼ ∃superior.Boss to ∃superior.(Boss u (¬W orker t ∃superior.Boss)) leads to infinitely many such enriching steps (due to Boss v W orker). Instead, our approach is to extend the canonical models for the classical members of the EL-family to DDLs. Our new kind of models captures varying amounts of DCIs from a DKB to be satisfied by role successors. Their domain essentially consist of copies of the domain of a classical canonical model for each set of DCIs. These typicality models were recently introduced by us in [11]. To develop the semantics for reasoning under nested relevant entail- ment and an appropriate reasoning procedure we proceed in two steps: 1. We introduce minimal typicality models with a lattice domain where all do- main elements have non-typical role successors only, i.e., no role successor Making Quantification Relevant Again —the Case of Defeasible EL⊥ 7 needs to satisfy any DCI. We show that these minimal typicality models yield exactly the same subsumption relationships as the materialisation-based rel- evant entailment in [4]. 2. We extend minimal typicality models to maximal typicality models, where each role successor required by K is chosen such that it satisfies a subset of DCIs from D that is of maximal cardinality while not causing an incon- sistency. We define subsumption under nested relevant entailment based on maximal typicality models and show that these models then yield more sub- sumption relationships than the materialisation-based relevant entailment. To devise an algorithm that gives the same entailments as materialisation-based relevant entailment, we use the same subsets of the DBox as Casini et al. in [4] based on justifications. To decide the entailment of C @∼ D w.r.t. K = (T, D), the subset D0 of D is constructed by removing rank-minimal parts of all justifications relevant for the inconsistency of C. Since we need to distinguish the subsets obtained from C-justifications for different concepts C, we denote from now on, D0 as DC (e.g. for DX ⊆ D, use X-justifications w.r.t. K). In order to infer all the undefeated facts for a concept F , the representative domain element of F in a model needs to satisfy the largest subset of D that is still satisfiable together with the TBox. If minimal relevant closure is used, this subset is obviously DF . Now, in EL⊥ -concepts a syntactical sub-concept F can occur in multiple existential restrictions (not top-level), causing several role successors in a model. These in turn might be able to satisfy any subset of DCIs “up to” DF each. To be able to capture elements satisfying any set of DCIs, typicality interpretations (potentially) need a representative domain element for each subset of the given DBox D. The subsets of D form a lattice. Definition  K = (T, D) be a DKB. A complete lattice S 3. Let ∅ domain is defined as ∆K = U ⊆D dU F | F ∈ Qc(K) . A domain ∆ with {dF | F ∈ Qc(K)} ⊆ ∆ ⊆ ∆K is a lattice domain. Typicality interpretations over a lattice domain are the basis for our semantics and we define under which conditions a DKB is satisfied in such interpretations. Definition 4 (model of K). Let K = (T, D) be a DKB. A typicality interpre- tation I = (∆I , ·I ) over a lattice domain ∆I is a model of K (written I |= K) iff 1. I |= T and 2. I, dU F |= U for all U ⊆ D, F ∈ Qc(K). We define when a defeasible subsumption relationship holds in a typicality in- terpretation over a lattice domain. Definition 5. Let I be a typicality interpretation over a lattice domain. Then DC I I satisfies a defeasible subsumption C @ ∼ D (written I |= C @∼ D) iff dC ∈ D . In order to construct a model for K by means of a TBox, we use auxiliary concept names from the set NCaux ⊆ NC \ sig(K) to introduce representatives for all F ∈ Qc(K) for each subset of the given DBox. Given concept F and DBox D, we use FD ∈ NCaux to define the extended TBox of F : T D (F ) = T ∪ {FD v F } ∪ {FD u G v H | G @ ∼ H ∈ D} (1) 8 Maximilian Pensel and Anni-Yasmin Turhan Here {FD v F } ensures that all constraints on F hold for the auxiliary concept as well. The last set of GCIs in Eq. (1) ensures that every element in FDI (for I |= T D (F )) satisfies the DCIs in D. The auxiliary concept F∅ introduced in the extended TBox T ∅ (F ) and the concept F from T have the same subsumers. Proposition 6. Let T be a TBox and F, G be concepts with sig(G) ∩ NCaux = ∅. Then F vT G iff F∅ vT ∅ (F ) G. The proof for this proposition as well as most results of this paper are given in detail in the technical report [12]. To use typicality interpretations for reasoning under materialisation-based relevant entailment, the DCIs from U ⊆ D need to be satisfied at the elements dU F representing F ∈ Qc(K), but not (necessarily) for the role successors of these elements. In fact, it suffices to construct a typicality interpretation of minimally typical role successors (for now), i.e. to use only the TBox for reasoning about role successors induced by existential restrictions. Definition 7. Let K = (T, D) be a DKB and U ⊆ D. The minimal typicality model over a lattice domain LK of K consists of the lattice domain ∆LK = {dU F ∈ ∆K | FU 6vT U (F ) ⊥} and an interpretation mapping that satisfies the following conditions for all dU F ∈∆ LK : – dU F ∈A LK iff FU vT U (F ) A, for A ∈ sigNC (K) and U ∅ – (dF , dG ) ∈ rLK iff FU vT U (F ) ∃r.G, for r ∈ sigNR (K). Typicality models need not use the complete lattice domain of 2|D| ∗ |Qc(K)| elements due to inconsistent combinations of the represented concept F , U and T. Note that LK is well-defined, as the initial assumption that F 6vT ⊥ holds (for all F ∈ Qc(K)) implies that all d∅F exist in ∆LK by Prop. 6. Furthermore, it is not hard to show that Prop. 6 implies that LK , restricted to elements regarding the empty set of DCIs, is the classical canonical model for the EL⊥ TBox T. Example 8 (Minimal typicality model). Consider again the DKB Kex1 from Ex- ample 2 with the consistent subsets of the DBox DW orker = Dex1 , and DBoss = {W orker @ ∼ P roductive, Boss @ ∼ Responsible} w.r.t. W orker and Boss, respec- tively. The subset-lattice of Dex1 and LKex1 are illustrated in Fig. 1 using obvious abbreviations. Note, that the domain elements are grouped in grey boxes accord- ing to the subset-lattice indicating which DBox subsets are satisfied by which do- main elements. According to Definition 5, LKex1 |= W orker @ ∼ ∃superior.Boss, DW orker as well as LKex1 |= Boss @ ∼ Responsible u P roductive, because dW orker and DBoss dBoss satisfy DW orker and DBoss , respectively. Rational closure would select the DBox subset {Boss @ ∼ Responsible} for reasoning about Boss and would therefore not conclude the latter subsumption. For the minimal typicality model LK it can be shown that dD C ∈D C LK (Def. 5) is equivalent to reasoning with the extended TBox, i.e. deciding CDC vT DC (C) D. The following claim can be proved using this equivalence. Lemma 9. Let K = (T, D) be a DKB. Then the minimal typicality model LK over the lattice domain ∆LK is a model of K. Making Quantification Relevant Again —the Case of Defeasible EL⊥ 9 W @ ∼ ∃s.B, W W @ DW ∼ P, B@ ∼R W B W W W @ W @ W @ DB ∼ P, ∼ ∃s.B, ∼ ∃s.B, B@ ∼R B@ ∼R W @ ∼P W B W B W B@ ∼R W @ ∼P W @ ∼ ∃s.B ∅ W B ∅ Fig. 1: a Subset lattice of Dex1 and b LKex1 We want to characterise different entailment relations based on different kinds of typicality models for a given DKB K which vary in the defeasible information admitted for required role successors. We use minimal typicality models over a lattice domain to characterise entailment of propositional nature |=p . Definition 10. Let K be a DKB. K propositionally entails a defeasible sub- ∼ D (written K |=p C @ sumption relationship C @ ∼ D) iff LK |= C @ ∼ D. This form of entailment is called propositional since all role successors are uni- formly non-typical and thus DCIs are neglected for quantified concepts. Next, we investigate the relationship between |=m (Sec. 3) and |=p . Our approach to decide propositional entailments based on the extended TBox for a concept F , coincides with enriching F with the materialisation of the given DBox. Lemma 11. Let T be a TBox T, D a DBox, and C, D be concepts, with sig(X)∩ NCaux = ∅ (for X ∈ {T, D, C, D}). Then D u C vT D iff CD vT D (C) D. Proof (sketch). The lemma is proven by induction on the size of D. The base case is D = ∅ and thereby Prop. 6 holds. For the induction step, let D0 = D∪{G @ ∼ H} and use the hypothesis that the claim holds for D. We do a case distinction for (i) D u C v G and (ii) D u C 6v G. For case (i), it can be shown that reasoning with C u H, yields the same consequences as reasoning with C. All elements in C u H satisfying G, already satisfy H. Thus we can remove the introduced DCI G@ ∼ H without losing any consequences. Hence, G @ ∼ H can be removed from D0 and the induction hypothesis holds. In case (ii) we show that the added DCI has no effect on the reasoning. By the condition of this case, no element in C, satisfying all DCIs in D, satisfies G. Therefore, the presence of the DCI G @ ∼H does not affect the reasoning allowing it to be removed in order to reduce the induction step to the induction hypothesis. In both cases, both sides of the “iff ” in the claim are reduced to their respective sides of the induction hypothesis individually. Since the full proof is fairly long and technical, it is deferred to the technical report [12]. Although the entailment relations |=m as introduced in [4] and |=p are defined in different ways and are based on distinct semantics, they yield the same con- sequences (for subsumption) w.r.t. DKBs. 10 Maximilian Pensel and Anni-Yasmin Turhan Theorem 12. K |=p C @ ∼ D iff K |=m C @ ∼ D. DC LK Proof (sketch). K |=p C @ ∼ D is defined as LK |= C @ ∼ D, i.e. dC ∈ D which is equivalent to CDC vT DC (C) D as shown in the technical report [12]. This subsumption in turn is equivalent to deciding DC u C vT D by Lemma 11, which is precisely the definition of K |=m C @ ∼ D (from Section 3). t u In addition, this result shows that entailments based on minimal typicality mod- els also bear the shortcomings for defeasible reasoning regarding nested existen- tial restrictions—a nuisance which we want to alleviate next. 5 Maximal Typicality Models for Relevant Entailment We illustrate by continuing on Example 8 how defeasible information is disre- garded for nested existential restrictions and our proposed countermeasure. Example 13. Consider again the DKB Kex1 from Example 8, with LKex1 (as depicted in Fig. 1). No defeasible information is used for reasoning over the superior successors of dD @ W orker and thus LK 6|= W orker ∼ ∃superior.Responsible. W orker ∅ However, Boss @ ∼ Responsible remains undefeated for dBoss . Instead of satisfying Boss @∼ Responsible at d∅Boss , we can “upgrade” the existing superior relation- {Boss@ ∼ Responsible} ship, e.g. (dD ∅ DW orker W orker , dBoss ) to (dW orker , dBoss W orker ) —as illustrated in Fig. 2 by the dashed arrows. Note that Figure 2 depicts only an excerpt of LKex1 for comprehensibility. Our method upgrades typicality of role successors as much as possible, as long as it does not result in inconsistencies. Here, this even yields the conclusion W orker @ ∼ ∃superior.P roductive. Upgrading the typicality of a role successor depends on the information W DW present in the model. Different orders of such upgrade steps can yield different models of increased typicality. In order W B W W DB to handle sets of models over the same lattice domain ∆, we need the notions of intersection and inclusion of models. W B W B W Definition 14. For two interpretations I, J over the same domain ∆ we define W B – I ∩ J = (∆, ·I∩J ) with ∅ AI∩J = AI ∩ AJ (for A ∈ NC ) and rI∩J = rI ∩ rJ (for r ∈ NR ) Fig. 2: Increasing typicality of role – I ⊆ J iff ∀A ∈ NC .AI ⊆ AJ and successors ∀r ∈ NR .rI ⊆ rJ. Using this definition we can formalise the notion of “upgrading the typicality” of a typicality interpretation, i.e. introduce copies of role edges that point to ele- ments representing the same concept, but satisfying more defeasible statements. Making Quantification Relevant Again —the Case of Defeasible EL⊥ 11 Definition 15. Let I be a typicality interpretation over a lattice domain for K = (T, D). The set of more typical role edges for a given role r is defined as 0 T RI (r) = {(dX U I I I X U I 0 G , dH ) ∈ ∆ × ∆ \ r | ∃ U ⊆ D.(dG , dH ) ∈ r ∧ U ⊂ U ⊆ DH }. Let I and J be typicality interpretations. J is a typicality extension of I iff 1. ∆J = ∆I , 2. AJ = AI (for A ∈ NC ), 3. rJ = rI ∪ R, where R ⊆ T RI (r) (for r ∈ sigNR (K)), and 4. ∃r ∈ sigNR (K). rI ⊂ rJ . The set of all typicality extensions of a typicality interpretation I is typ(I). With typicality extensions at hand we can transform typicality interpretations into a set of more typical interpretations. Unfortunately, this operation does not preserve the property of being a typicality model. Let us demonstrate this by Ex- ample 13, let Kex2 = (T ex2 , Dex1 ), and T ex2 = T ex1 ∪ {∃superior.Responsible v ∃coworker.W orker}. Since LKex2 coincides with LKex1 , Fig. 2 depicts a typical- ity extension of LKex2 according to Def. 15. However, the extension in Fig. 2 is no longer a model of T ex2 , as the newly introduced GCI is no longer satisfied for dD W orker . It can be extended to a model by introducing a coworker successor for dD W orker that belongs to W orker. In order not to introduce unwanted incon- sistencies, the successor in this new relationship needs to be picked such that it only contains the information strictly required by K, i.e. d∅W orker . We formalise the particular model completions that we are interested in. Definition 16. Let K = (T, D) be a DKB and ∆ a lattice domain. An interpre- tation I = (∆, ·I ) is a model completion of an interpretation J = (∆, ·J ) iff 1. ∅ J ⊆ I, 2. I |= K, and 3. ∀E ∈ Qc(K).dU F ∈ (∃r.E) I =⇒ (dU I F , dE ) ∈ r (for any F ∈ Qc(K) and U ⊆ D). The set of all model completions of J is denoted as mc(J ). An interpretation that is a model completion to itself is called a safe model and obviously satisfies the properties of Def. 16, e.g. for some typicality interpretation J over a lattice domain, all interpretations in mc(J ) are safe models. Since model completions introduce minimal typical role successors they may necessitate further typicality extensions. So, typicality extensions and model completions need to be applied alternatingly until a maximum is reached. Max- imality for typicality extensions is characterised in the following way: a typi- cality interpretation I is typicality extensible iff ∃J ∈ typ(I).mc(J ) 6= ∅. In- tuitively, a typicality interpretation is typicality extensible if it admits to some typicality extension that is, or can be completed to a safe model. Therefore, a typicality interpretation is maximal iff it is not typicality extensible. To for- malise the process of increasing typicality and completing to a model until reaching maximal typicality, we introduce some notation and an upgrade op- erator. Given a lattice domain ∆, define the set of all safe models over ∆ as P (∆) = {J | J = (∆, ·J ) ∧ J ∈ mc(J )}. Definition 17. The typicality upgrade operator T : 2P (∆) → 2P (∆) is defined for S ⊆ P (∆) as: 12 Maximilian Pensel and Anni-Yasmin Turhan S 1. T (S) = S \ {I} ∪ J ∈typ(I) mc(J ), if I ∈ S is typicality extensible, 2. T (S) = S, otherwise. For a given set of model completions S ⊆ P (∆), the fixpoint of T is Tm (S) if Tm (S) = Tm+1 (S) with T0 (S) = S, Ti (S) = T (Ti−1 (S)) (i > 0). The set of maximal typicality extensions of the typicality interpretations in S is typmax (S) = Tm (S). It is clear that neither Definition 15 nor 16 supply unique typicality exten- sions or model completions, respectively. Thus the typicality upgrade operator is defined over sets of typicality interpretations. Applying T to {I} easily leads to an exponential amount of typicality interpretations. The following example illustrates that this typicality extension can quickly lead to multiple different maximal typicality interpretations, starting from a single interpretation. Example 18. We extend the DKB from Example 8 to DKB Kex3 = (T ex3 , Dex1 ) with the TBox T ex3 = T ex1 ∪ {∃superior.∃superior.Responsible v ⊥}. Let the ∅ role edge (dDW orker , dW orker ) ∈ superior LKex3 be upgraded to (dD D W orker , dW orker ) D ∅ LKex3 D DBoss and likewise (dW orker , dBoss ) ∈ superior to (dW orker , dBoss ). If both of these upgrades exist in the same typicality extension J , it does not admit to a model completion, as dD J W orker ∈ (∃superior.∃superior.Responsible) . The typi- {W orker @ P roductive} cality upgrade (dD W orker , dBoss ∼ ), however, is “allowed” to occur in a typicality extension, leading to the entailment of W orker @ ∼ ∃superior.(Bossu P roductive). This shows that inheritance blocking can be remedied even for quantified concepts when upgrading typicality of successors in a lattice domain. It is clear that the above described process leads to a variety of maximal typical- ity models, and there are several ways to use these sets for our new entailment. Since in classical DL reasoning entailment considers all models, we pick seman- tics closely related to cautious reasoning here. To this end we build a single model that is canonical in the sense that it is contained in all maximal typicality models obtained from LK . T Definition 19. The relevant canonical model is RK = I∈typmax ({LK }) I. Note that the intersection over all maximal typicality models is well-defined as typmax ({LK }) is finite and since LK is a safe model (i.e. LK ∈ mc(LK )) it is not empty, as shown in the technical report [12]. Lemma 20. The relevant canonical model RK is a model of the DKB K. The main argument in the proof of Lemma 20 is that the intersection of models in any set S ⊆ P (∆) yields another model in P (∆). This result is ensured by Condition 3 of Definition 16 The relevant canonical model is used to decide nested relevant entailment of the form C @ ∼ K D, which requires to propagate DCIs to concepts occurring in existential restrictions. We capture this stronger and quantifier-aware relevant entailment. Definition 21. Let K be a DKB. A defeasible subsumption relationship C @ ∼D holds under nested relevant entailment (written K |=q C @ ∼ D) iff RK |= C @ ∼ D. Making Quantification Relevant Again —the Case of Defeasible EL⊥ 13 We are ready to state our main result: nested relevant entailment allows for strictly more inferences than the materialisation-based relevant entailment from [4] to compute the relevant closure. Theorem 22. For two EL⊥ concepts C, D and an EL⊥ DKB K 1. K |=m C @ ∼ D =⇒ K |=q C @∼ D, and 2. K |=m C @ ∼ D ⇐= 6 K |= q C @ ∼D The first Claim of Theorem 22 is not too hard to show, as J ∈ typmax ({LK }) implies that LK ⊆ J and thus LK ⊆ RK . Hence by Definition 5, LK |= C @ ∼D implies RK |= C @ ∼ D. The second claim can be supported by Example 13 and is formally shown in the technical report [12]. Extending our work on rational closure [11], the present approach fixes a deficit induced by materialisation and computes strictly more entailments than materialisation-based relevant reasoning. Since relevant closure is stronger than rational closure, the reduction presented here preserves all merits for rational closure from [11] and fixes remaining problems such as inheritance blocking. 6 Conclusions and Future Work In this paper we have extended a new approach for reasoning in DDLs to char- acterise entailment under relevant closure (for deciding subsumption) in the DDL EL⊥ . The new approach is motivated by the observation that earlier rea- soning procedures for this problem do not treat existential restrictions in an adequate way. The key idea is to extend canonical models such that for each concept from the DKB, several copies representing different amounts of defea- sible information are introduced. The new semantics supports the propagation of defeasible information to concepts nested in existential restrictions. It allows for extensions to more expressive approaches, e.g. more expressive DLs. While rational closure needs to consider only one sequence of increasing subsets of the DBox [11], relevant closure needs (potentially) all subsets of the given defea- sible information—forming a lattice. In minimal typical models over a lattice domain the role successors are “a-typical” in the sense that they satisfy only the GCIs from the TBox. Such models can be computed by a reduction to classical TBox reasoning. We showed that the obtained entailments coincide with the ones obtained by earlier materialisation-based algorithms. We extended these models to maximally typical models, which have role successors of “maximal typicality”. Entailment over these models propagates defeasible information to role successors and thus allows for more entailments. There are several paths for future work. Besides the extensions to more ex- pressive DLs, an extension to ABox reasoning, i.e., reasoning about data, would be an interesting topic to investigate. Furthermore, a completion-like algorithm as for classical EL [2,1] would be desirable to effectively compute these mod- els. The current definition of typicality extensions and model completions leaves plenty of room for developing practical algorithms worth implementing. 14 Maximilian Pensel and Anni-Yasmin Turhan References 1. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence IJCAI-05. Edinburgh, UK (2005) 2. Brandt, S.: Polynomial time reasoning in a description logic with existential re- strictions, GCI axioms, and—what else? In: R.L. de Mantáras, L. Saitta (eds.) Proceedings of the 16th European Conference on Artificial Intelligence (ECAI- 2004), pp. 298–302 (2004) 3. Britz, A., Casini, G., Meyer, T., Moodley, K., Varzinczak, I.: Ordered Interpreta- tions and Entailment for Defeasible Description Logics. Tech. rep., CAIR, CSIR Meraka and UKZN, South Africa (2013) 4. Casini, G., Meyer, T., Moodley, K., Nortjé, R.: Relevant closure: A new form of defeasible reasoning for description logics. In: Proceedings of the 14th European Conference on Logics in Artificial Intelligence (JELIA’14), pp. 92–106 (2014) 5. Casini, G., Straccia, U.: Rational closure for defeasible description logics. In: Pro- ceedings of 12th European Conference on Logics in Artificial Intelligence (Jelia’10), pp. 77–90 (2010) 6. Casini, G., Straccia, U.: Defeasible inheritance-based description logics. In: IJ- CAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, pp. 813–818 (2011) 7. Casini, G., Straccia, U.: Lexicographic closure for defeasible description logics. In: Proceedings of the Eighth Australasian Ontology Workshop, pp. 28–39 (2012) 8. Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: Semantic characterization of rational closure: From propositional logic to description logics. Artif. Intell. 226, 1–33 (2015) 9. Horridge, M.: Justification based explanation in ontologies. Ph.D. thesis, University of Manchester (2011) 10. Kraus, S., Lehmann, D.J., Magidor, M.: Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell. 44(1-2), 167–207 (1990) 11. Pensel, M., Turhan, A.Y.: Including quantification in defeasible reasoning for the description logic EL⊥ . In: M. Balduccini, T. Janhunen (eds.) Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reason- ing - LPNMR (2017). To appear. 12. Pensel, M., Turhan, A.Y.: Including quantification in defeasible reasoning for the description logic EL⊥ . LTCS-Report 17-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden (2017). See http://lat.inf.tu-dresden.de/research/reports.html