Reasoning About Typicality in ALC and E L

Abstract

In this work we summarize our recent results on extending Description Logics for reasoning about prototypical properties and inheritance with exceptions. First, we focus our attention on the logic ALC. We present a nonmonotonic logic ALC + Tmin, which is built upon a monotonic logic ALC + T obtained by adding a typicality operator T to ALC. The operator T is intended to select the “most normal” or “most typical” instances of a concept, so that knowledge bases may contain subsumption relations of the form“T(C) is subsumed by P ”, expressing that typical C-members have the property P . In order to perform nonmonotonic inferences, we define a “minimal model” semantics: the intuition is that preferred, or minimal models are those that maximise typical instances of concepts. By means of ALC + Tmin we are able to infer defeasible properties of (explicit or implicit) individuals. We also show that the satisfiability of an ALC + T-knowledge base is in EXPTIME, whereas deciding query entailment in ALC + Tmin is in co-NExpNP. We apply our approach based on the operator T also to the low complexity Description Logic E L+⊥ . We propose an extension E L+⊥ T and we show that the problem of entailment in E L+⊥ T is in co-NP.

-

Description logics (DLs) represent one of the most important formalisms of knowledge representation. A DL knowledge base (KB) comprises a TBox, containing the definition of concepts (and possibly roles), and a specification of inclusions relations among them, and an ABox containing instances of concepts and roles. Since the very objective of the TBox is to build a taxonomy of concepts, the need of representing prototypical properties and of reasoning about defeasible inheritance of such properties naturally arises.

Several approaches to handle prototypical reasoning and inheritance with exceptions in DL have been proposed in the literature, all of them are based on the integration of DLs with some nonmonotonic reasoning mechanism: either default logic (see [ 4, 19, 5 ]), or autoepistemic logic (see [ 9, 15 ] for some recents developmentes) and circumscription (see [ 7 ] and [ 6 ]). In particular, [ 6 ] analyzes the complexity of reasoning with circumscribed low complexity description logics, such as DL-lite and the E L family. While reasoning with circumscribed ALC knowledge bases is NExpNP-hard [ 7 ], in circumscribed DL-liteR complexity drops to the second level of the polynomial hierarchy. In [ 6 ] is also shown that in EL reasoning over circumscribed knowledge bases remain ExpTime-hard in general. However, by limiting occurrences of existential restrictions, complexity drops to the second level of the polynomial hierarchy.

In this paper, we present an overview of our approach to reasoning about typicality in DLs, which is based on the idea of introducing in the language a typicality operator T. First, we present the monotonic logic ALC + T, obtained by adding the operator T to ALC. Then we introduce a minimal model semantics for it, which allows typical instances of concepts to be maximized. Finally, we present the logic EL+⊥ T, obtained by extending the logic EL+⊥ with T. We analyze and compare the complexity of these logics.

The intended meaning of the operator T, for any concept C, is that T(C) singles out the instances of C that are considered as “typical” or “normal”. Thus assertions as “normally students do not pay taxes” are represented by T(Student) ⊑ ¬TaxPayer . The operator T is characterised by a set of postulates that are essentially a reformulation of KLM [ 16 ] axioms of preferential logic P, namely the assertion T(C) ⊑ P is equivalent to the conditional assertion C |∼ P of P. It turns out that the semantics of the typicality operator can be equivalently specified by a suitable modal logic.

The idea underlying the modal interpretation is that there is a global preference relation (a strict partial order) < on individuals, so that typical instances of a concept C can be defined as the instances of C that are minimal with respect to <. In this modal logic, < works as an accessibility relation R with R(x, y) ≡ y < x, so that we can define T(C) as C ⊓ ¬C. The preference relation < does not have infinite descending chains as we adopt the so-called Smoothness condition or Limit Assumption of conditional logics. As a consequence, the corresponding modal operator has the same properties as in G¨odel-L¨ob modal logic G of arithmetic provability.

In this setting, we assume that a KB comprises, in addition to the standard TBox and ABox, a set of assertions of the type T(C) ⊑ D where D is a concept not mentioning T. For instance, let the KB contain:

T(Student) ⊑ ¬TaxPayer

T(Student ⊓ Worker ) ⊑ TaxPayer

T(Student ⊓ W orker ⊓ ∃HasChild .⊤) ⊑ ¬TaxPayer corresponding to the assertions: normally a student does not pay taxes, normally a working student pays taxes, but normally a working student having children does not pay taxes. Suppose further that the ABox contains alternatively the following facts about john: 1. Student(john); 2. Student(john), Worker (john); 3. Student(john), Worker (john), ∃HasChild .⊤(john). We would like to infer the expected (defeasible) conclusion about john in each case: 1. ¬TaxPayer (john), 2. TaxPayer (john), 3. ¬TaxPayer (john). Furthermore, we would like to infer (defeasible) properties also of individuals implicitly introduced by existential restrictions, for instance, if the ABox further contains ∃HasChild .(Student ⊓ Worker )(jack ) it should derive (defeasibly) the “right” conclusion ∃HasChild .TaxPayer (jack ) in the latter. Finally, adding irrelevant information should not affect the conclusions. Given the KB as above, one should be able to infer as well T(Student ⊓ SportLover ) ⊑ ¬TaxPayer and T(Student ⊓ Worker ⊓ SportLover ) ⊑ TaxPayer , as SportLover is irrelevant with respect to being a TaxPayer or not. For the same reason, the conclusion about john being a TaxPayer or not should not be influenced by adding SportLover (john) to the ABox.

The monotonic logic ALC + T allows some weak forms of inference through cautious monotonicity. For instance, if typical students are young, from the KB above we can derive that typical young students do not pay taxes. Inference in ALC + T is in ExpTime. However, ALC + T is not sufficient to perform the kind of defeasible reasoning illustrated above. Concerning the example, we get for instance that: KB ∪ {Student(john), Worker (john)} 6|= TaxPayer (john); KB 6|= T(Student ⊓ SportLover ) ⊑ ¬TaxPayer . In order to derive the conclusion about john we should know (or assume) that john is a typical working student, but we do not dispose of this information. Similarly, in order to derive that also a typical student who loves sport does not have to pay taxes, we must be able to infer or assume that a “typical student loving sport” is also a “typical student”, since there is no reason why it should not be the case; this cannot be derived by the logic itself given the nonmonotonic nature of T. The basic monotonic logic ALC + T is then too weak to enforce these extra assumptions. In order to perform defeasible inferences, we strenghten the semantics of ALC + T by proposing a minimal model semantics. Intuitively, the idea is to restrict our consideration to models that maximise typical instances of a concept. In order to define the preference relation on models we take advantage of the modal semantics of ALC + T: the preference relation on models (with the same domain) is defined by comparing, for each individual, the set of modal (or more precisely -ed) concepts containing the individual in the two models. Similarly to circumscription, where we must specify a set of minimised predicates, here we must specify a set of concepts LT of which we want to maximise the set of typical instances (it may just be the set of all concepts occurring in the knowledge base). We call the new logic ALC + Tmin and we denote by |=LmTin semantic entailment determined by minimal models. Taking the KB of the examples above we obtain, for instance, KB ∪ {Student(john), Worker (john)} |=LmTin TaxPayer (john); KB ∪ {∃HasChild .(Student ⊓ Worker )(jack)} |=LmTin ∃HasChild .TaxPayer (jack ) and KB |=LmTin T(Student ⊓SportLover ) ⊑ ¬TaxPayer . As the second example shows, we are able to infer the intended conclusion also for the implicit individuals. In [ 11 ] we have provided a decision procedure for checking satisfiability and validity in ALC + Tmin. Our procedure, not presented here, can be used to determine constructively an upper bound of the complexity of ALC + Tmin. Namely we obtain that checking query entailment for ALC + Tmin is in co-NExpNP. +⊥

Finally, we introduce an extension of the logic EL with typicality. The logics of the EL family allow for conjunction (⊓) and existential restriction (∃R.C). Despite their relatively low expressivity, a renewed interest has recently emerged for these logics. Indeed, it has been shown that EL has better algorithmic properties than F L0, which allows for conjunction and value restriction (∀R.C). [ 1, 8 ] show that reasoning in EL and several of its extensions remains tractable (i.e., polynomial-time decidable) in the presence of the TBox, and even of general concept inclusions (GCIs). Furthermore, it has turned out that the logics of the EL family are relevant for several applications, in particular in the bio-medical domain; for instance, medical terminologies, such as the Galen Medical Knowledge Base (GALEN, [ 17 ]), the Systemized Nomenclature of Medicine (SNOMED [18]), and the Gene Ontology [20] used in bioinformatics, can be formalized in small extensions of EL.

We present some preliminary results about the complexity of EL+⊥ T. In particular, we show that a consistent EL+⊥ T knowledge base has a small model whose size is polynomial in the size of the knowledge base. In the paper, we sketch the construction of the model. We show that, as a consequence of this result, the problem of deciding entailment in EL+⊥ T is in co-NP. 2

The logic ALC + T

We consider an alphabet of concept names C, of role names R, and of individuals O. The language L of the logic ALC + T is defined by distinguishing concepts and extended concepts as follows: (Concepts) A ∈ C, ⊤ and ⊥ are concepts of L; if C, D ∈ L and r ∈ R, then C ⊓ D, C ⊔ D, ¬C, ∀r.C, ∃r.C are concepts of L. (Extended concepts) if C is a concept, then C and T(C) are extended concepts, and all the Boolean combinations of extended concepts are extended concepts of L. A knowledge base is a pair (TBox,ABox). TBox is a finite set of GCIs C ⊑ D, where C ∈ L is an extended concept (either C′ or T(C′)), and D ∈ L is a concept. ABox contains expressions of the form C(a) and r(a, b) where C ∈ L is an extended concept, r ∈ R, and a, b ∈ O.

In order to provide a semantics to the operator T, we extend the definition of a model used in “standard” terminological logic ALC: Definition 1 (Semantics of T with selection function). A model is any structure hΔ, I, fTi, where: Δ is the domain; I is the extension function that maps each extended concept C to CI ⊆ Δ, and each role r to a rI ⊆ ΔI × ΔI . I is defined in the usual way (as for ALC) and, in addition, (T(C))I = fT(CI ). fT : P ow(Δ) → P ow(Δ) is a function satisfying the following properties: (fT − 1) fT(S) ⊆ S (fT − 3) if fT(S) ⊆ R, then fT(S) = fT(S ∩ R) (fT − 5) ! fT(Si) ⊆ fT(" Si) (fT − 2) if S "= ∅, then also fT(S) "= ∅ (fT − 4) fT(! Si) ⊆ ! fT(Si) Intuitively, given the extension of some concept C, fT selects the typical instances of C. (fT − 1) requests that typical elements of S belong to S. (fT − 2) requests that if there are elements in S, then there are also typical such elements. The next properties constraint the behavior of fT wrt ∩ and ∪ in such a way that they do not entail monotonicity. According to (fT − 3), if the typical elements of S are in R, then they coincide with the typical elements of S ∩ R, thus expressing a weak form of monotonicity (namely cautious monotonicity). (fT − 4) corresponds to one direction of the equivalence fT(S Si) = S fT(Si), the one that does not entail monotonicity. Similar considerations apply to the equation fT(T Si) = T fT(Si), of which only the inclusion T fT(Si) ⊆ fT(T Si) is derivable. (fT−5) is a further constraint on the behavior of fT wrt arbitrary unions and intersections; it would be derivable if fT were monotonic.

We can give an alternative semantics for T based on a preference relation. The idea is that there is a global preference relation among individuals and that the typical members of a concept C, i.e. selected by fT(CI ), are the minimal elements of C wrt this preference relation. Observe that this notion is global, that is to say, it does not compare individuals wrt a specific concept (something like y is more typical than x wrt concept C). In this framework, an object x ∈ Δ is a typical instance of some concept C, if x ∈ CI and there is no C-element in Δ more typical than x. The typicality preference relation is partial since it is not always possible to establish which object is more typical than which other. The following definition is needed: Definition 2. Given a relation <, which is a strict partial order (i.e. an irreflexive and transitive relation) over a domain Δ, for all S ⊆ Δ, we define M in<(S) = {x : x ∈ S and ∄y ∈ S s.t. y < x}. We say that < satisfies the Smoothness Condition iff for all S ⊆ Δ, for all x ∈ S, either x ∈ M in<(S) or ∃y ∈ M in<(S) such that y < x.

In [ 10 ] it is shown that given a model with a selection function, it is possible to define on the same domain a preference relation < such that, for all S ⊆ Δ, fT(S) = M in<(S). Formally, given any model hΔ, I, fTi, fT satisfies postulates (fT − 1) to (fT − 5) above if and only if it is possible to define on Δ a strict partial order <, satisfying the Smoothness Condition, such that for all S ⊆ Δ, fT(S) = M in<(S). By this result, we can refer to the following semantics for ALC + T: Definition 3 (Semantics of ALC +T). A model M is any structure hΔ, <, Ii, where Δ and I are defined as in Definition 1, and < is a strict partial order over Δ satisfying the Smoothness Condition (see Definition 2 above). As a difference wrt Definition 1, the semantics of the T operator is: (T(C))I = M in<(CI ). For concepts (built from operators of ALC), CI is defined in the usual way. We introduce the following definition: Definition 4 (Model satisfying a Knowledge Base). Consider a model M, as defined in Definition 3. We extend I so that it assigns to each individual a of O an element aI of the domain Δ. Given a KB (TBox,ABox), we say that: – M satisfies TBox if for all inclusions C ⊑ D in TBox, and all elements x ∈ Δ, if x ∈ CI then x ∈ DI . – M satisfies ABox if: (i) for all C(a) in ABox, we have that aI ∈ CI , (ii) for all r(a, b) in ABox, we have that (aI , bI ) ∈ rI .

M satisfies a knowledge base if it satisfies both its TBox and its ABox. Notice that the meaning of T can be split into two parts: for any a of the domain Δ, a ∈ (T(C))I just in case (i) a ∈ CI , and (ii) there is no b ∈ CI such that b < a. In order to isolate the second part of the meaning of T (for the purpose of the calculus that we will present later), we introduce a new modality . The basic idea is simply to interpret the preference relation < as an accessibility relation. By the Smoothness Condition, it turns out that has the properties as in G¨odelLo¨b modal logic of provability G. The Smoothness Condition ensures that typical elements of CI exist whenever CI 6= ∅, by preventing infinitely descending chains of elements. This condition therefore corresponds to the finite-chain condition on the accessibility relation (as in G). The interpretation of in M is as follows: ( C)I = {a ∈ Δ | for every b ∈ Δ, if b < a then b ∈ CI }. Therefore, we have that a is a typical instance of C (a ∈ (T(C))I ) iff a ∈ (C ⊓ ¬C)I . Since we only use to capture the meaning of T, in the following we will always use the modality followed by a negated concept, as in ¬C.

It is possible to prove that the satisfiability of an ALC + T-knowledge base is in EXPTIME. We omit the proof that can be found in section 3.1 of [ 13 ]. Theorem 1 (Complexity of ALC + T). Given an ALC + T-knowledge base (TBox,ABox), the problem of checking whether it is satisfiable can be solved in exponential time. 3

The logic ALC + Tmin

The logic ALC + T allows one to reason about typicality. As a difference with respect to standard ALC, in ALC + T we can consistently express, for instance, the fact that three different concepts, as student, working student and working student with children, have a different status as taxpayers. As we have seen in the introduction, this can be consistently expressed by including in a knowledge base the three formulas: T(Student) ⊑ ¬TaxPayer ; T(Student ⊓Worker ) ⊑ TaxPayer ; T(Student ⊓Worker ⊓∃HasChild .⊤) ⊑ ¬TaxPayer . Assume that john is an instance of the concept Student ⊓Worker ⊓∃HasChild .⊤. What can we conclude about john? If the ABox contains the assertion (∗) T(Student ⊓ Worker ⊓ ∃HasChild .⊤)(john), then, in ALC +T, we can conclude that ¬TaxPayer (john). However, in the absence of (*), we cannot derive ¬TaxPayer (john).

We would like to infer that individuals are typical instances of the concepts they belong to, if consistent with the KB. In order to maximize the typicality of instances, we define a preference relation on models, and we introduce a semantic entailment determined by minimal models. Informally, we prefer a model M to a model N if M contains more typical instances of concepts than N .

Given a KB, we consider a finite set LT of concepts occurring in the KB, the typicality of whose instances we want to maximize. The maximization of the set of typical instances will apply to individuals explicitly occurring in the ABox as well as to implicit individuals. We assume that the set LT contains at least all concepts C such that T(C) occurs in the KB.

We have seen that a is a typical instance of a concept C (a ∈ (T(C))I ) when it is an instance of C and there is not another instance of C preferred to a, i.e. a ∈ (C ⊓ ¬C)I . In the following, in order to maximize the typicality of the instances of C, we minimize the instances of ¬ ¬C. Notice that this is different from maximising the instances of T(C). We have adopted this solution since it allows to maximise the set of typical instances of C without affecting the extension of C (whereas maximising the extension of T(C) would imply maximising also the extension of C).

− We define the set MLT of negated boxed formulas holding in a model, relative − to the concepts in LT . Given a model M = hΔ, <, Ii, let MLT = {(a, ¬ ¬C) | a ∈ (¬ ¬C)I , with a ∈ Δ, C ∈ LT }.

Definition 5 (Preferred and minimal models). Given a model M = hΔM, <M, IMi of KB and a model N = hΔN , <N , IN i of KB, we say that M is preferred to N with respect to LT , and we write M <LT N , if the following − − conditions hold: ΔM = ΔN and MLT ⊂ NLT . A model M is a minimal model for KB (with respect to LT ) if it is a model of KB and there is no a model M′ of KB such that M′ <LT M.

A query α is either a formula of the form C(a) or a subsumption relation C ⊑ D. Definition 6 (Minimal Entailment in ALC +Tmin). A query α is minimally entailed from a knowledge base KB with respect to LT if α holds in all models of KB minimal with respect to LT . We write KB |=LmTin α.

While the original ALC+T is monotonic (see [ 10 ]), ALC+Tmin is nonmonotonic.

In [ 11 ] we have defined a tableaux calculus for ALC + Tmin and we have proved that: Theorem 2 (Complexity of ALC + Tmin). The problem of deciding whether KB |=LmTin α is in co-NExpNP. 4

The logic EL+⊥ T Let us now consider the case of the logic EL+⊥ , namely we apply the above semantics to describe an extension EL+⊥ T of EL+⊥ with the T operator. In EL+⊥ T, concepts are restricted only to the cases of A ∈ C, ⊤, ⊥, C ⊓ D, and ∃r.C, where C, D are concepts of EL+⊥ T and r ∈ R. Concerning extended concepts, if C is a concept, then C and T(C) are extended concepts of EL+⊥ T. A knowledge base is a pair (TBox,ABox). TBox contains (i) a finite set of GCIs C ⊑ D, where C is an extended concept (either C′ or T(C′)), and D is a concept, and (ii) a finite set of role inclusions (RIs) r1 ◦ r2 ◦ · · · ◦ rn ⊑ r. ABox contains expressions of the form C(a) and r(a, b) where C is an extended concept, r ∈ R, and a, b ∈ O.

Notice that an EL+⊥ T TBox can formalize transitive roles, role hierarchies, as well as the so-called right identities on roles (r ◦ s ⊑ s); these constructs are very useful to formalize medical ontologies.

We can show that, given a model M = hΔ, <, Ii of a KB, we can build a small model of KB whose size is polynomial in the size of the KB. As we will see, this will provide a complexity upper bound for the logic EL+⊥ T.

First of all, we must introduce an appropriate normal form for KBs, in particular for TBoxes. Given a KB=(TBox,ABox), we say that it is normal if: – all the inclusion relations in TBox have one of the following forms: C1 ⊑ D; C1 ⊓ C2 ⊑ D; C1 ⊑ ∃r.C2; ∃r.C1 ⊑ D; T(C1) ⊑ C2; T(C1 ⊓ C2) ⊑ D; T(C1) ⊑ ∃r.C2; T(∃r.C1) ⊑ D, where C1, C2 ∈ C ∪ {⊤} and D ∈ C ∪ {⊥}; – all role inclusions in TBox are of the form r ⊑ s or r1 ◦ r2 ⊑ s. By extending the results presented in [ 2 ], we can show that any KB can be turned into a normalized KB’ that is a conservative extension of KB, that is to say every model satisfying KB’ is also a model of KB, whereas every model of KB can be extended to a model of KB’ by appropriately choosing the interpretations of the additional concept and role names introduced by the normalization procedure. Furthermore, it can be shown that the size of KB’ is linear in the size of KB, and that the normalization procedure can be done in linear time. Without loss of generality, from now on we only refer to normalized KBs. Starting from a normalized KB, we can now prove the following theorem: Theorem 3 (Small model theorem). Let KB=(TBox,ABox) be an EL+⊥ T knowledge base. For all models M = hΔ, <, Ii of KB and all x ∈ Δ, there exists a model N = hΔ◦, <◦, I◦i of◦ KB such that (i) x ∈ Δ◦, (ii) for all EL+⊥ T concepts C, x ∈ CI iff x ∈ CI , and (iii) | Δ◦ | is polynomial in the size of KB. We sketch the proof through the following steps. In the first step, we build a model M′ by means of the following algorithm. Intuitively, we keep only those worlds needed to retain the values of formulas in x. Roughly speaking, we reuse the same domain element to make true existential formulas in different domain elements. For technical reasons, we need to add new elements to the domain of the constructed model, in order to keep the same evaluation of existential formulas as in the initial model. For each concept C ∈ C and for each role r ∈ R we let S(C) and R(r) be the mappings computed by the algorithm defined in [ 3 ] to compute subsumption in EL by means of completion rules. As usual, for a given individual a occurring in ABox, we write aI to denote the element of Δ corresponding to the extension of a in M. In the algorithm, we make use of three sets of elements: Δ0 will be part of the domain of the model being constructed, and it contains a portion of the domain Δ of the initial model. All the elements introduced in the domain must be processed in order to satisfy the existential formulas. Unres is used to keep track of the elements not yet processed. Finally, Δ1 is a set of elements that will belong to the domain of the constructed model. Each element of Δ1 is created for one atomic concept C, and is used to satisfy all existential formulas ∃r.C throughout the whole model. The model M′ = hΔ′, <′, I′i is defined as follows: – Δ′ = Δ0 ∪ Δ1 – we extend <′ computed by the algorithm by adding u <′ v if u < v, for each u, v ∈ Δ′; – the extension function I′ is defined as follows: • fo∗∗r affoollrraeetaaoccmhhicuwDc∈on∈Δc0Δe,p1tw,sewClee∈tleu′tC,∈wfDoCrI∈a′lCilfwIu′oi∈rfldCCsI∈i;nSΔ(D′, )w. e define: • for all roles r, we extend rI constructed by the algorithm by means of the following role closure rules: ′ ′ ∗ for all inclusions r ⊑ s ∈ TBox, if (u, v) ∈ rI thenI′ add (u, v) to sI ′; ∗ for all inclusions r1 ◦′r2 ⊑ s ∈ TBox, if (u, v) ∈ r1 and (v, w) ∈ r2I then add (u, w) to sI .

• I′ is extended so that it assigns aI to each individual a in the ABox. It can be shown that M′ is a model of KB. M′ is not guaranteed to have polynomial size in the KB because in line 17 we add an element yi for each yi < y, then the size of Δ0 may be arbitrarily large. For this reason, we refine our construction in order to build a multi-linear model, that we will be able to further refine in order to obtain a model of polynomial size. First of all, we introduce the notion of multi-linear model of a KB. Given a model M = hΔ, <, Ii, we say that it is multi-linear if the following properties hold for every u, v, z ∈ Δ: (i) if u < z and v < z and u 6= v, then u < v or v < u; (ii) if z < u and z < v and u 6= v, then u < v or v < u. The construction of a multi-linear model is similar to the one presented in [ 12 ] and it requires two steps. In the first step, we replicate some domain elements, namely those belonging to more than one descending ch′a′ in of <′. In the second step, we build a multi-linear model M∗ = hΔ′′, <∗, I i. Details can be found in [ 14 ]. The proof is ended by constructing a model N = hΔ◦, <◦, I◦i whose domain has polynomial size in the size of KB. Let the size of the initial KB be n. We know that M∗ contains a polynomial number of linear chains of domain elements related by <∗, each one starting from a domain elements in Δ1 (built by the algorithm above) or from one domain element in {x, a1, . . . , ak}, where a1, . . . , ak are the domain elements corresponding to the individuals in the ABox. We know that there are O(n) +⊥ chains, as Δ1 contains one domain element for each atomic concept in E L and the domain elements a1, . . . , ak are O(n). However, we have no bound on the length of the chains.

We want to show that the linear chains in the model can be reduced to finite chains of polynomial length in the size of the KB. To this purpose, given M∗, we build a new multi-linear model N = hΔ◦, <◦, I◦i whose descending chains have polynomial length.

Let us consider a chain w0, w1, w2, . . . in the model M∗, with w0 in Δ1 or w0 in {x, a1, . . . , ak}. Starting from w1, we consider each element wi in the chain and compare it with its predecessor wi−1: we remove from the chain wi if wi is an instance of exactly the same negated box formulas ¬ ¬C1, . . . , ¬ ¬Ch as its predecessor wi−1. After processing an element of the chain, we consider the next one. We keep on removing domain elements from the chain until, for each element w of the chain, there is at least a box formula ¬C of which w is an instance, while the domain element preceding w in the chain is not an instance of ¬C. As there is only a finite polynomial number of such box formulas, we can only retain a finite polynomial number of worlds in the chain.

The same transformation is applied to all the O(n) chains in the model M∗. The resulting model N = hΔ◦, <◦, I◦i is defined as follows: Δ◦ is the set of all the domain elements in Δ∗ which have not been removed during the chain transformation process; the relation <◦ is defined so that, for all x, y ∈ Δ∗, x <◦ y if and only if x <∗ y; the interpretation of atomic formulas in the domain elements is left unchanged.

It can be shown that N is a multi-linear model of the KB and that the valuation in x is the same in N and in M∗. By construction, the descending chains in N are of polynomial length.

Given the small model theorem above, we can conclude that, when evaluating the entailment, we can restrict our consideration to small models, namely, to polynomial multi-linear models of the KB. As usual, we write KB |= α to say that a query α holds in all the models of the KB. We write KB |=s α to say that α holds in all polynomial multi-linear models of the KB.

Theorem 4. KB |= α if and only if KB |=s α.

Proof. From left to right, the statement is obvious. From right to left: using contraposition, we prove that if KB 6|=s α then KB 6|= α. Let M = hΔ, <, Ii be a model of KB falsifying α, that is, x 6∈ αI , for some domain element x ∈ Δ. By Theorem 3 above, we can construct a polynomial multi-linear model N = hxΔ∈◦,C<I◦◦,.IH◦ienocfeK,xB,∈suαcIh◦ .that x ∈ Δ◦ and, for all E L+⊥ T concepts C, x ∈ CI iff Given the result above, we can prove an upper bound on the complexity of entailment in E L+⊥ T.

Theorem 5 (Complexity entailment in E L whether KB |= α is in co-NP. +⊥

T). The problem of deciding

+⊥ Proof. Let us consider the complementary problem of deciding whether KB 6|= α. This problem can be solved by a nondeterministic polynomial time algorithm which guesses a model N of polynomial size and a domain element x of the model, and then checks in polynomial time that N is a model of the KB and that x falsifies α.

As a consequence, for logic E L T the problems of satisfiability of a knowledge base and of concept satisfiability are in NP. The problems of subsumption and of instance checking are in co-NP. 5

Conclusions and Future Works This work presents our approach to handle prototypical reasoning in DL by means of a typicality operator T, the latter is intended to select the “most normal” instances of a concept. In this work, we have considered the description logics ALC + T and E L+⊥ T. Whereas for ALC + T deciding satisfiability (subsumption) is EXPTIME complete (see [ 13 ]), for E L+⊥ T the complexity is significantly smaller, namely it reduces to NP for satisfiability (and co-NP for subsumption). This result is obtained by a “small” model property that fails for the whole ALC + T as well as for ALC. We believe that this bound is also a lower bound, but we have not proved it yet.

Concerning ALC, we have observed that this logic is not sufficient to perform defeasible reasoning. Therefore, we have also proposed a nonmonotonic extension called ALC + Tmin of ALC. This nonmonotonic extension is based on a (nonmonotonic) entailment relation determined by restricting the entailment of ALC + T to “minimal models”. Intuitively minimal models are those that maximise “typical instances” of a concept. We have proved that deciding ALC +Tmin entailment is in co-NExpNP. We believe that for E L+⊥ Tmin we can obtain a smaller complexity upper bound on the base of the results presented here.

In future work we will deal with the precise relation between our T-DLs with the other nonmonotonic extensions of DLs mentioned above, notably with circumscription. In this setting, a natural question is to compare E L+⊥ Tmin with circumscribed E L and see whether we get the same complexity bounds or not. 18. K.A. Spackman. Managing clinical terminology hierarchies using algorithmic calculation of subsumption: Experience with snomed-rt. J. of the American Medical Informatics Association, Fall Symposium Special Issue, 2000. 19. U. Straccia. Default inheritance reasoning in hybrid kl-one-style logics. In Proc.

of IJCAI, pages 676–681, 1993. 20. The GO Consortium. Gene ontology: Tool for the unification of biology. Nature Genetics, 25, 2000.

References

1. F. Baader . Terminological cycles in a description logic with existential restrictions . In Proc. of IJCAI'03 , pp. 325 - 330 , 2003 .

2. F. Baader , S. Brandt , and C. Lutz . Pushing the E L envelope . In LTCSReport LTCS- 05 -01, Inst. for Theoretical Computer Science, TU Dresden, http://lat.inf.tudresden.de/research/reports.html, 2005 .

3. F. Baader , S. Brandt , and C. Lutz . Pushing the E L envelope . In Proc. of IJCAI'05 , Professional Book Center pp. 364 - 369 , 2005 .

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

5. F. Baader and B. Hollunder. Priorities on defaults with prerequisites, and their application in treating specificity in terminological default logic . J. of Automated Reasoning (JAR) , 15 ( 1 ): 41 - 68 , 1995 .

6. P. Bonatti , M. Faella , and L. Sauro . Defeasible inclusions in low-complexity dls: Preliminary notes . In Proc. IJCAI2009 , to appear.

7. P. A. Bonatti , C. Lutz , and F. Wolter . Description logics with circumscription . In Proc. of KR , pages 400 - 410 , 2006 .

8. S. Brandt . Polynomial time reasoning in a description logic with existential restrictions, gci axioms, andwhat else ? In Proc. of ECAI'04 , pp. 298 - 302 , 2004 .

9. F. M. Donini , D. Nardi , and R. Rosati . Description logics of minimal knowledge and negation as failure . ACM Trans. Comput. Log. , 3 ( 2 ): 177 - 225 , 2002 .

10. L. Giordano , V. Gliozzi , N. Olivetti , and G. L. Pozzato . Preferential Description Logics . In Nachum Dershowitz and Andrei Voronkov, editors, Proceedings of LPAR 2007 ( 14th Conference on Logic for Programming , Artificial Intelligence, and Reasoning) , volume 4790 of LNAI , pages 257 - 272 , Yerevan, Armenia, October 2007 . Springer-Verlag.

11. L. Giordano , V. Gliozzi , N. Olivetti , and G. L. Pozzato . Reasoning About Typicality in Preferential Description Logics . In S. H´olldobler, C. Lutz, and H. Wansing, editors, Proceedings of JELIA 2008 (11th European Conference on Logics in Artificial Intelligence) , volume 5293 of LNAI , pages 192 - 205 , Dresden, Germany, September 2008 . Springer-Verlag.

12. L. Giordano , V. Gliozzi , N. Olivetti , and G. L. Pozzato . Analytic Tableaux Calculi for KLM Logics of Nonmonotonic Reasoning . ACM Transactions on Computational Logic , 10 ( 3 ), 2009 .

13. L. Giordano , V. Gliozzi , N. Olivetti , and G. L. Pozzato . On Extending Description Logics for Reasoning About Typicality: a First Step . In Technical Report 116/09 , Dipartimento di Informatica, Universit´a degli Studi di Torino , Italy, http://www.di.unito.it/∼argo/papers/RT 11609.pdf, 2009 .

14. L. Giordano , V. Gliozzi , N. Olivetti , and G. L. Pozzato . Reasoning About Typicality in Low Complexity Description Logics: Preliminary Results . In Technical Report 150/09 , Dipartimento di Informatica, Universit´a degli Studi di Torino , Italy, http://www.di.unito.it/∼argo/papers/RT 15009.pdf, 2009 .

15. P. Ke and U. Sattler . Next Steps for Description Logics of Minimal Knowledge and Negation as Failure . In DL2008 , 2008 .

16. S. Kraus , D. Lehmann , and M. Magidor . Nonmonotonic reasoning, preferential models and cumulative logics . Artificial Intelligence , 44 ( 1-2 ): 167 - 207 , 1990 .

17. A. Rector and I. Horrocks. Experience building a large, re-usable medical ontology using a description logic with transitivity and concept inclusions . In Proc. Workshop on Ontological Engineering , 1997 .