Reasoning about Typicality in Low Complexity DLs: The Logics EL⊥Tmin and DL-Litec Tmin

1 Introduction

Nonmonotonic extensions of Description Logics (DLs) have been actively investigated since the early 90s, [Straccia, 1993; Bonatti et al., 2006; Baader and Hollunder, 1995; Bonatti et al., 2009; Donini et al., 2002; Giordano et al., 2009b; 2009a; 2008; Casini and Straccia, 2010]. The reason is that DLs are used to represent classes and their properties, so that a nonmonotonic mechanism is wished to express defeasible inheritance of prototypical properties. A simple but powerful nonmonotonic extension of DL is proposed in [Giordano et al., 2009b; 2009a; 2008]: in this approach "typical" or "normal" properties can be directly specified by means of a "typicality" operator T enriching the underlying DL; the tipicality operator T is essentially characterised by the core properties of nonmonotonic reasoning axiomatized by preferential logic [Kraus et al., 1990]. In ALC +T [Giordano et al., 2009b] and EL⊥T [Giordano et al., 2009a], one can consistently express defeasible inclusions and exceptions such as: typical students do not pay taxes, but working students do typically pay taxes, but working student having children normally do not: T(Student ) ⊑ ¬TaxPayer ; T(Student ⊓ Worker ) ⊑ TaxPayer; T(Student ⊓ Worker ⊓ ∃HasChild.⊤) ⊑ ¬TaxPayer (for the formalization in EL⊥T see Example 2.6). Although the operator T is nonmonotonic in itself, the logics ALC + T and EL⊥T are monotonic. As a consequence, unless a KB contains explicit assumptions about typicality of individuals (e.g. that john is a typical student), Nicola Olivetti LSIS-UMR CNRS 6168 Universit´e "P. C´ezanne"

∗We thank the project "MIUR PRIN08 LoDeN: Logiche Descrittive Nonmonotone: Complessit´a e implementazioni".

Aix-Marseille 3, France

nicola.olivetti@univ-cezanne.fr Dip. di Informatica di Torino, Italy pozzato@di.unito.it

there is no way of inferring defeasible properties of them (e.g. that john does not pay taxes). In [Giordano et al., 2008], a non monotonic extension of ALC + T based on a minimal models semantics is proposed. The resulting logic, called ALC +Tmin, supports typicality assumptions, so that if one knows that john is a student, one can nonmonotonically assume that he is also a typical student and therefore that he does not pay taxes. As an example, for a TBox specified by the inclusions above, in ALC + Tmin the following inference holds: TBox ∪ {Student(john)} |=ALC+Tmin ¬TaxPayer (john).

Similarly to other nonmonotonic DLs, adding the typicality operator with its minimal-model semantics to a standard DL, such as ALC, leads to a very high complexity (namely query entailment in the resulting logic is in CO-NEXP NP [Giordano et al., 2008]). This fact may motivate the study of nonmonotonic extensions of low complexity DLs such as DL-Litecore [Calvanese et al., 2007] and EL⊥ of the EL family [Baader et al., 2005] which are nonetheless well-suited for encoding large knowledge bases (KBs). In this paper, we hence consider the extensions of the low complexity logics DL-Litecore and EL⊥ with the typicality operator based on the minimal model semantics introduced in [Giordano et al., 2008]. We study the complexity of the resulting logics EL⊥Tmin and DL-LitecTmin. For EL⊥, it turns out that its extension EL⊥Tmin is unfortunately EXPTIME-hard. This result is analogous to the one for circumscribed EL⊥ KBs [Bonatti et al., 2009]. However, the complexity decreases to Πp2 for the fragment of Left Local EL⊥ KBs, corresponding to the homonymous fragment in [Bonatti et al., 2009]. We obtain the same complexity upper bound for DL-LitecTmin.

2 The typicality operator T and the Logic EL⊥Tmin

Before describing EL⊥Tmin, let us briefly recall the underlying monotonic logic EL⊥T [Giordano et al., 2009a], obtained by adding to EL⊥ the typicality operator T. The intuitive idea is that T(C) selects the typical instances of a concept C. In EL⊥T we can therefore distinguish between the properties that hold for all instances of concept C (C ⊑ D), and those that only hold for the normal or typical instances of C (T(C) ⊑ D).

Gian Luca Pozzato Universit`a degli Studi Formally, the EL⊥T language is defined as follows.

Definition 2.1 We consider an alphabet of concept names C, of role names R, and of individuals O. Given A ∈ C and r ∈ R, we define

A KB is a pair (TBox, ABox). TBox contains a finite set of concept inclusions CL ⊑ CR. ABox contains assertions of the form CL(a) and r(a, b), where a, b ∈ O.

The semantics of EL⊥T [Giordano et al., 2009a] is defined by enriching ordinary models of EL⊥ by a preference relation < on the domain, whose intuitive meaning is to compare the "typicality" of individuals: x < y, means that x is more typical than y. Typical members of a concept C, that is members of T(C), are the members x of C that are minimal with respect to this preference relation.

Definition 2.2 (Semantics of T) A model M is any structure 〈Δ,<, I〉 where Δ is the domain; < is an irreflexive and transitive relation over Δ that satisfies the following Smoothness Condition: for all S ⊆ Δ, for all x ∈ S, either x ∈ Min<(S) or ∃y ∈ Min<(S) such that y < x, where Min<(S) = {u : u ∈ S and ∄z ∈ S s.t. z < u}. Furthermore, < is multilinear: if u < z and v < z, then either u = v or u < v or v < u. I is the extension function that maps each concept C to CI ⊆ Δ, and each role r to rI ⊆ ΔI ×ΔI . For concepts of EL⊥, C I is defined in the usual way. For the T operator: (T(C))I =Min<(C I ).

Definition 2.3 (Model satisfying a Knowledge Base)

Given a model M, I can be extended so that it assigns to each individual a of O a distinct element aI of the domain Δ. Msatisfies a KB (TBox,ABox), if it satisfies both its TBox and its ABox, where:

• M satisfies TBox if for all inclusions C ⊑ D in TBox, for all elements x ∈ Δ, if x ∈ C I , then x ∈ DI .
• Msatisfies ABox if: (i) for all C(a) in ABox, aI ∈ C I , (ii) for all aRb in ABox, (aI , bI ) ∈ rI .

The operator T [Giordano et al., 2009b] is characterized by a set of postulates that are essentially a reformulation of KLM [Kraus et al., 1990] axioms of preferential logic P. Roughly speaking, the assertion T(C) ⊑ D corresponds to the conditional C |∼ D of P. T has therefore all the "core" properties of nonmonotonic reasoning as it is axiomatised by P.

The semantics of the typicality operator can be specified by modal logic. The interpretation of T can be split into two parts: for any x of the domain Δ, x ∈ (T(C))I just in case (i) x ∈ C I , and (ii) there is no y ∈ C I such that y < x. Condition (ii) can be represented by means of an additional modality □, whose semantics is given by the preference relation < interpreted as an accessibility relation. Observe that by the Smoothness Condition, □ has the properties of G¨odelL¨ob modal logic of provability G.

The interpretation of □ in M is as follows:

(□C)I = {x ∈ Δ | for every y ∈ Δ, if y < x then y ∈ C I }.

We immediatly get that x ∈ (T(C))I iff x ∈ (C ⊓□¬C)I . From now on, we consider T(C) as an abbreviation for C ⊓ □¬C. Finally, we recall that the problem of entailment in EL⊥T is in CO-NP (as shown in [Giordano et al., 2009a]).

The main limit of EL⊥T is that it is monotonic. Even if the typicality operator T itself is nonmonotonic (i.e. T(C) ⊑ E does not imply T(C ⊓D) ⊑ E), the logic EL⊥T is monotonic: what is inferred from KB can still be inferred from any KB' with KB ⊆ KB'. In order to perform nonmonotonic inferences, as done in [Giordano et al., 2008], we strengthen the semantics of EL⊥T by restricting entailment to a class of minimal (or preferred) models. We call the new logic EL⊥Tmin. Intuitively, the idea is to restrict our consideration to models that minimize the non typical instances of a concept. The preference relation on models (with the same domain) is defined by comparing individuals in the interpretation of modal (or more precisely □-ed) formulas.

Given a KB, we consider a finite set L□ of concepts: these are the concepts whose non typical instances we want to minimize. We assume that the set L□ contains at least all concepts C such that T(C) occurs in the KB or in the query α. A query α is either an assertion C(a) or an inclusion relation C ⊑ D. We have that x is a typical instance of C if x ∈ (C ⊓□¬C)I . Since we do not want to change the extension of concept C by minimization, we minimize only objects not satisfying □¬C for C ∈ L□. Given a modelM= 〈Δ,<, I〉, we first define: M□- L□ = {(x, ¬□¬C) | x ̸∈ (□¬C)I , with x ∈ Δ, C ∈ L□}.

Definition 2.4 (Preferred and minimal models) Given a model M = 〈Δ <, I〉 of a knowledge base KB, and a model M′ = 〈Δ′ , <′ , I ′ 〉 of KB, we say that M is preferred to M′ with respect to L□, and we write M <L□ M′ , if (i) Δ = Δ′ and (ii) M□- L□ ⊂M′□- L□ . A modelMis a minimal model for KB (with respect to L□) if it is a model of KB and there is no other model M′ of KB such that M′ <L□ M.

We can now define entailment in EL⊥Tmin. Let us first say that a query α holds in a model M = 〈Δ <, I〉 of a KB (Definition 2.3) whenever: (i) α = C ⊑ D, and for all x ∈ Δ, if x ∈ C I , then x ∈ DI , or (ii) α = C(a), and aI ∈ C I .

Definition 2.5 (Minimal Entailment in EL⊥Tmin) A query α is minimally entailed in EL⊥Tmin by a knowledge base KB with respect to L□ if it holds in all models of KB that are minimal with respect to L□. We write KB |=EL⊥Tmin α.

Example 2.6 The KB of the Introduction can be reformulated as follows in EL⊥T: TaxPayer ⊓NotTaxPayer ⊑ ⊥; Parent ⊑ ∃HasChild.⊤; ∃HasChild.⊤ ⊑ Parent; T(Student) ⊑ NotTaxPayer; T(Student ⊓ Worker) ⊑ TaxPayer; T(Student ⊓ Worker ⊓ Parent) ⊑ NotTaxPayer. Let L□ = {Student, Student ⊓ Worker, Student ⊓ Worker ⊓ Parent}. Then TBox ∪ {Student(john)} |=EL⊥Tmin NotTaxPayer (john), since johnI ∈ (Student ⊓ □¬Student)I for all minimal models M = 〈Δ <, I〉 of the KB. Similarly we obtain TBox ∪ {∃HasChild.(Student ⊓Worker)(jack)} |=EL⊥Tmin ∃HasChild.TaxPayer(jack). The latter shows that minimal entailment applies to implict individuals as well, without any ad-hoc mechanism.

Observe that minimal entailment is nonmonotonic, since, for KB ⊂ KB', the minimal models of KB' are not necessarily minimal models of KB.

3 Complexity of EL⊥Tmin

In this section we analyze the complexity of EL⊥Tmin. We consider the complexity of minimal entailment of a query as defined above. First we show that, contrary to the mere addition of the operator T to EL⊥, the adoption of the nonmonotonic semantics drastically worsens the complexity of EL⊥Tmin making it EXPTIME hard. Next we identify a syntactic restriction that allows one to obtain a reasonable complexity (laying in the second level of the polynomial hierarchy), comparable to the one of other nonmonotonic mechanisms for EL⊥, such as circumscription.

3.1 An EXPTIME lower bound for EL⊥Tmin

We prove here that EL⊥Tmin is EXPTIME hard. The proof is based on the reduction of the problem of TBox satisfiability in EL¬A to the complement of EL⊥Tmin subsumption. The logic EL¬A is just EL⊥ extended by the complement of concept names and the satisfiability problem for it is known to be EXPTIME-hard [Baader et al., 2005].

Theorem 3.1 Entailment in EL⊥Tmin is EXPTIME-hard.

Proof. Let T be a TBox in EL¬A. We define a KB=(T ′ ,A′ ) in EL⊥Tmin by introducing, for each concept name A in T , the fresh names: A (for representing the negation of A, ¬A), UA (for representing the fact that A has an undefined truth value), NA (meaning normal A), N¬A (meaning normal ¬A), NUA (meaning normal UA). Also, we introduce the new concept names D (for defining a subset of the domain), E and U and the new concept role R.

We translate each concept C into C∗ as follows: (i) C ∗ = C, if C is a concept name; (ii) C ∗ = A, if C = ¬A; (iii) C ∗ = D ⊓ ∃r.(C ∗ 1 ⊓ D), if C = ∃r.C1 (iv) C ∗ = C ∗ 1 ⊓ C ∗ 2 if C = C1 ⊓ C2. For all the inclusions C1 ⊑ C2 ∈ T the translated TBox T ′ contains the inclusion C ∗ 1 ⊑ C ∗ 2 . The translated TBox T ′ , contains, in addition, the following inclusions (for all concept names A):

A′ contains the assertion D(a), for a new individual name a.

A D element of the domain is a normal A, a normal A and a normal UA element (first line) and it can be (in mutual exclusion) either a typical normal A element or a typical normal A element or a typical normal UA element (second and third line). Thus any D element, provides a truth value (true, false or undefined) to each concept name A. The last line says that each D is an E and the typical E are in the relation R with D element for which UA is true. Observe that, if there is a D ⊓ UA element in the domain, there is no reason why a D element should not be assumed to be a typical E element (and in the preferred models, that D element would be in the relation R with a D ⊓ UA element, unless there are no D ⊓ UA elements in the model). Last subsumption says that U must hold for those D elements which make some concept name A undefined. Finally, the assertion D(a) guarantees the existence of at least a D element in the models of KB. Any preferred model of EL⊥Tmin, in which there are no D elements with undefined concept names ((D ⊓ UA)I = ∅), can be mapped to a model in EL¬A, by removing all the relation < and by restricting the domain of the model to the set of elements in which D holds. If the resulting model does not contain any undefined element (i.e. any element in which UA holds for some A), then that model is a (two valued) model of T. Hence, we can verify that T is satisfiable in EL¬A, by verifying that KB has a minimal model M in EL⊥Tmin that does not contain D ⊓ UA elements. This is true if there is a minimal model that does not contain U elements, which can be tested by verifying that KB ̸|=EL⊥Tmin D ⊑ ∃R.U, with L□ = {NA,NA,NUA ,E}. This condition holds whenever there is a model M = 〈Δ, <, I〉 of KB in EL⊥Tmin and an element y in its domain such that: y ∈ DI and y ̸∈ (∃R.U)I . This means that there is no D ⊓ UA element in the model M. Then, we can conclude that entailment in EL⊥Tmin is EXPTIME-hard. ■

The previous result corresponds to an analogous result for circumscribed KBs [Bonatti et al., 2009]. In order to lower the complexity of minimal entailment in EL⊥Tmin, we put the following syntactic restrictions on the KB.

3.2 Left Local Knowledge Bases

In this section, we consider a syntactical restriction on knowledge bases called Left Local KBs. This restriction is similar to the one introduced in [Bonatti et al., 2009].

Definition 3.2 (Left Local knowledge base) A Left Local KB only contains subsumptions C LL L ⊑ CR, where C and CR are as in Definition 2.1 and:

There is no restriction on the ABox.

Observe that the KB in the Example 2.6 is Left Local.

We provide an upper bound for the complexity of Left Local KBs by a small model theorem. Intuitively, what allows us to keep the size of the small model polynomial is that we reuse the same world to verify the same existential concept throughout the model.

We write KB |=small EL⊥Tmin α to say that α holds in all minimal models of the KB whose size is polynomially bounded by the size of KB.

Let KB=(TBox,ABox) be a Left Local KB, and suppose KB ̸|=EL⊥Tmin α. We want to show that KB ̸|=small EL⊥Tmin α (this is one half of Theorem 3.11).

Let M = 〈Δ, <, I〉 be a minimal model of KB in which α does not hold. Let x ∈ Δ be an element falsifying α. Since α can be an existential formula, x is the only world for which we have to preserve the truth value of all existential formulas (also negative) in the small model. For this reason we consider x first. The small modelM′ is built as follows.

1. Δ0 := Unres := {x} ∪ {aI ∈ Δ | a occurs in ABox }
2. for each ∃r.C occurring in KB s.t. x ∈ (∃r.C)I do

3. choose w ∈ Δ s.t. (x, w) ∈ rI and w ∈ C I 4. Δ0 :=Δ0 ∪ {w} 5. add (x,w) to rI ′ 6. while Unres ̸= ∅ do 7. extract one y from Unres 8. for each ∃r.C in KB s.t. y ∈ (∃r.C)I , y ̸= x do 9. if ∃w ∈Δ0 s.t. w ∈ C I ′ then 10. add (y,w) to rI ′ 11. else 12. choose w ∈ Δ s.t. (y, w) ∈ rI and w ∈ C I 13. Δ0 :=Δ0 ∪ {w} 14 add (y,w) to rI ′ 15. Unres:=Unres ∪ {w} 16. for each yi ∈ Δ such that yi < y do 17. Δ0 :=Δ0 ∪ {yi} 18. Unres:=Unres ∪ {yi}

We then defineM′ in the following way.

Definition 3.3 The model M′ = 〈Δ′ , <′ , I ′ 〉 is as follows: (i) Δ′ = Δ0; (ii) we define <′ by adding u <′ v if u < v, for each u, v ∈ Δ′ ; (iii) the extension function I ′ is defined as follows: - for all atomic concepts C ∈ C, for all elements in Δ′ , we define u ∈ C I ′ if u ∈ C I ; - for all roles r ∈ R, rI ′ is as computed by the above algorithm; (iv) I ′ is extended so that it assigns aI to each individual a in the ABox .

Lemma 3.4 The relation <′ is irreflexive, transitive, multilinear and satisfies the Smoothness Condition.

Proof. This is so because these properties hold inM for all descending chains of <. Here, we have imported some of the chains and we have added no new relations to <′ not belonging to <. ■

Lemma 3.5 Given a concept C with form C LL L of Definition 3.2, for all y ∈ Δ′ , y ∈ C I ′ iff y ∈ C I .

Proof. By induction on the complexity of C. To save space, we only present the two most interesting cases. Let C be ∃r.⊤. If y ∈ (∃r.⊤)I , then at step 5 or 10 or 14 (y, z) has been inserted to rI ′ , and y ∈ (∃r.⊤)I ′ . For the other direction, if (y ∈ ∃r.⊤)I ′ , then there must be z such that (y, z) has been added to rI ′ in step 5 or 10 or 14 for a given y ∈ (∃r.C)I . Hence y ∈ (∃r.⊤)I also inM.

Let C be T(C1), and y ∈ (T(C1))I . Then y ∈ C I 1 and for all z < y, z ̸∈ C I 1 , i.e. y ∈ (□¬C1)I . By inductive hypothesis, y ∈ C I ′ 1 . Furthermore, by definition of <′ , for all z ∈ Δ′ , if z <′ y, then z < y, and by inductive hypothesis, z ̸∈ C I ′ 1 , hence y ∈ (□¬C1)I ′ . Hence, y ∈ (T(C1))I ′ . On the other hand, if y ∈ (T(C))I ′ , we can reason analogously: from y ∈ C I ′ 1 we conclude that y ∈ C I 1 , and from y ∈ (□¬C1)I ′ , we conclude that y ∈ (□¬C1)I , i.e., for all z < y, z ̸∈ C I 1 (since for all z < y, z ∈ Δ0 and z <′ y). Hence, y ∈ (T(C1))I . ■

Lemma 3.6 Given a concept C with form CR, for all y ∈ Δ′ , if y ∈ C I then y ∈ C I ′ .

Proof. Let C be ∃r.C1. If y ∈ (∃r.C1)I , by construction, (y,w) ∈ rI ′ for some w ∈ C I 1 . By Lemma 3.5, w ∈ C I ′ 1 . It follows that y ∈ (∃r.C1)I ′ . ■

Lemma 3.7 Given any concept C, x ∈ C I ′ iff x ∈ C I .

Proof. With respect to Lemma 3.5 we also consider here existential concepts, for which we can prove the converse of Lemma 3.6, namely that if x ∈ (∃r.C1)I ′ , then x ∈ (∃r.C1)I . This follows from the fact that for the starting individual x, for all w such that (x, w) ∈ rI ′ , (x, w) ∈ rI , and by Lemma 3.5, if w ∈ C1 I ′ , then w ∈ C1 I . ■

Lemma 3.8 M′ is a model of KB. Furthermore, α does not hold inM′ .

Proof. Assertions in the ABox hold in M′ by Lemma 3.5 or Lemma 3.6. Concerning the TBox, consider C ⊑ D. By definition of Left Local, for C Lemma 3.5 holds. Hence, if y ∈ C I ′ , also y ∈ C I , hence y ∈ DI (since M is a model of KB) and, by Lemma 3.6, y ∈ DI ′ . Last, by hypothesis x falsifies α in M, i.e., if α = C ⊑ D, then x ∈ C I and x ̸∈ DI ; if α = C(a), x = aI and x ̸∈ C I . From Lemma 3.7 inM′ , x ∈ C I ′ but x ̸∈ DI ′ , in the first case, and x ̸∈ CI ′ , in the second case. In both cases, α does not hold inM′ . ■

Lemma 3.9 M′ has a polynomial size in the size of KB.

Proof. First of all, since M is minimal, each descending <- chain must be polynomial in size. Indeed, for each w′ < w in the chain there must be a concept C (occurring in KB) such that w ̸∈ (□¬C)I and w′ ∈ (□¬C)I (it can be shown that if it was not so, we could build a model preferred toM, which, hence, would not be minimal; this model would be obtained by eliminating w from the <-chain and by putting w in the extension of the same concepts to which belongs a given individual with no preferred element, w.r.t. <). Since the number of concepts occurring in KB is polynomial, each chain is polynomial in size. By construction, this also holds in M′ . Furthermore, inM′ the number of chains inserted corresponds to the number of distinct existential concepts occurring in KB, whose number is polynomial. Hence the overall size ofM′ is polynomial in the size of KB. ■

Lemma 3.10 M′ is a minimal model for KB.

Proof. We have already shown in Lemma 3.5, when considering the case of T(C1), that for all w in Δ′ , w ̸∈ (□¬C1)I ′ iff w ̸∈ (□¬C1)I . Hence, M′□- L□ ⊆ M□- L□ (we use ⊆ instead of = because the domain of M′ is smaller than the domain of M). Suppose nowM′ was not minimal. There would be an M′′ whose domain is the same than M′ 's and M′′□- L□ ⊂ M′□- L□ . However, in this case we can build an M′′′ with the same domain as M such that M′′′□- L□ ⊂M□- L□ , thus proving that M is not minimal, against the hypothesis. M′′′ can be built fromM′′ by reintroducing the domain elements of M that do not belong to M′′ . We chose an element y in M′′ with no y1 <′′ y (by the Smoothness Condition this element exists) and we let I ′′′ be the extension of I ′′ that handles the added elements by putting them in the extension of exactly the same concepts to which y belongs in M′′ . Since y satisfies all positive boxed formulas in M′′ , M′′′□- L□ = M′′□- L□ ⊂ M′□- L□ . However, as stated above, M′□- L□ ⊆ M□- L□ , hence we conclude that M′′′□- L□ ⊂ M□- L□ , andMwould not be minimal, contradiction. ■

Theorem 3.11 (Small model theorem) KB |=EL⊥Tmin α if and only if KB |=small EL⊥Tmin α.

Proof. If KB ̸|=EL⊥Tmin α, by the lemmas above we can build a small minimal model of KB that does not satisfy α, hence KB ̸|=small EL⊥Tmin α. On the other hand, if KB |=EL⊥Tmin α in all minimal models of KB, this also holds for small minimal models, hence KB |=small EL⊥Tmin α. ■

Given Theorem 3.11 above, we can conclude that, when evaluating entailment, we can restrict our consideration to small models, namely, to polynomial multilinear models of the KB. This provides an upper bound on the complexity of determining if KB |=EL⊥Tmin α. Indeed, by Theorem 3.11, this amounts to considering whether KB |=small EL⊥Tmin α. We consider the complementary problem of KB ̸|=small EL⊥Tmin α. This problem can be solved by nondeterministically generating a model Mwhose size is polynomial in the size of KB (NP), and then by calling an NP oracle which verifies that M is a minimal model of KB that does not satisfy α. To see this, the verification that M is not a minimal model of the KB can be done by an NP algorithm which nondeterministically generates a new model M′ of KB (whose size is polynomial in the size ofM) and checks whether it is preferred toM (this can be checked in polynomial time in the size of M). Hence, the problem of verifying that KB ̸|=EL⊥Tmin α is in Σp2 , and that of verifying KB |=EL⊥Tmin α is in Πp2 . We can therefore conclude that:

Theorem 3.12 (Complexity for EL⊥Tmin Left Local KBs) If KB is Left Local, the problem of deciding whether KB |=EL⊥Tmin α is in Πp2 .

In [Giordano et al., 2011] we have introduced a tableau calculus for deciding whether a query α is minimally entailed from a Left Local KB in the logic EL⊥Tmin. The calculus is a variant of the calculus TABALC+T min [Giordano et al., 2008] for ALC+Tmin, and it is essentially obtained by: (i) modifying the application of the rule (∃+) in a way such that, when applied to a formula u : ∃R.C, it introduces a new label only when a label xC for C does not belong to the current branch.

Otherwise, if xC has been already introduced, then u R -→ xC is added to the conclusion of the rule. In this way, in a given branch, the rule (∃+) only introduces a new label xC for each concept C occurring in the inital KB in some ∃R.C; (ii) modifying the rule for negated boxed formulas ¬□¬C according to the multilinear models semantics of EL⊥Tmin.

The calculus performs a two-phase computation in order to build an open branch representing a minimal model satisfying KB ∪ {¬α}. In the first phase, the tableau calculus simply verifies whether KB ∪ {¬α} is satisfiable by an EL⊥T model, building candidate models. In the second phase the calculus checks whether the candidate models found in the first phase are minimal models of KB, i.e. for each open branch of the first phase, the second phase tries to build a "smaller" model, i.e. a model whose individuals satisfy less formulas ¬□¬C than the corresponding candidate model.

The resulting calculus is sound, complete, terminating, and its complexity matches the results of Theorem 3.12.

4 The Logic DL-LitecTmin

In this section we present the extension of the low complexity description logic DL-Litecore [Calvanese et al., 2007] with the T operator. We call DL-LitecTmin the resulting logic.

The language of DL-LitecTmin is defined as follows.

Definition 4.1 We consider an alphabet of concept names C, of role names R, and of individuals O. Given A ∈ C and r ∈ R, we define

A DL-LitecTmin KB is a pair (TBox, ABox). TBox contains a finite set of concept inclusions of the form CL ⊑ CR. ABox contains assertions of the form C(a) and r(a, b), where C is a concept CL or CR, r ∈ R, and a, b ∈ O.

As for EL⊥Tmin, a model M for DL-LitecTmin is any structure 〈Δ,<, I〉, defined as in Definition 2.2, where I is extended to take care of inverse roles: given r ∈ R, (r-)I = {(a, b) | (b, a) ∈ rI }.

For DL-LitecTmin KBs we can make a small model construction that is similar to that one for Left Local KBs. As a difference, in this case, we exploit the fact the, for each atomic role r, the same element of the domain can be used to satisfy all occurrences of the existential ∃r.⊤. Also, the same element of the domain can be used to satisfy all occurrences of the existential ∃r-.⊤. This will guarantee that existential concepts (as well as all other concepts) have the same valuation inM′ and inMon the common part of the domain. In the construction, we consider the two cases for ∃r.⊤ and for ∃r-.⊤ separately.

Let M = 〈Δ, <, I〉 be a minimal model of KB in which α does not hold, and let x be the element of the domain falsifying α. The small modelM′ is built as follows:

1. Δ0 := Unres := {x} ∪ {aI ∈ Δ | a occurs in ABox } 2. while Unres ̸= ∅ do 3. extract one y from Unres 4. for each ∃r.⊤ occurring in KB s.t. y ∈ (∃r.⊤)I do 5. if ∃z,w ∈Δ0 s.t. (z,w) ∈ rI ′ then 6. add (y,w) to rI ′ 7. else 8. choose w ∈ Δ s.t. (y, w) ∈ rI 9. Δ0 :=Δ0 ∪ {w} 10 add (y,w) to rI ′ 11. Unres:=Unres ∪ {w} 12. for each ∃r-.⊤ in KB s.t. y ∈ (∃r-.⊤)I do 13. if ∃z,w ∈Δ0 s.t. (w, z) ∈ rI ′ then 14. add (w, y) to rI ′ 15. else 16. choose w ∈ Δ s.t. (w, y) ∈ rI 17. Δ0 :=Δ0 ∪ {w} 18 add (w, y) to rI ′ 19. Unres:=Unres ∪ {w} 20. for each yi ∈ Δ such that yi < y do 21. Δ0 :=Δ0 ∪ {yi} 22. Unres:=Unres ∪ {yi}

We defineM′ in the same way as in Definition 3.3. By reasoning similarly to what done for Left Local KBs, we can now show the following lemmas.

Lemma 4.2 The relation <′ is irreflexive, transitive, multilinear and satisfies the Smoothness Condition.

Lemma 4.3 For all DL-LitecT concepts C occurring in the KB (or in the query), for all y ∈ Δ′ , y ∈ C I ′ iff y ∈ C I .

Proof. By induction on the structure of C. If C is a concept name or a boolean combination of concept names, the proof follows straightforwardly from the definition of I ′ .

Let us consider the case for C is ∃R.⊤. We use the following facts concerning the construction of model M′ : (1) when (y,w) is added to rI ′ in steps 6 and 10, it must be the case that (z, w) ∈ rI , for some z ∈ Δ, i.e. that w ∈ (∃r-.⊤)I . (2) when (w, y) is added to rI ′ in steps 14 and 18, it must be the case that (w, z) ∈ rI , for some z ∈ Δ, i.e. that w ∈ (∃r.⊤)I .

Let y ∈ (∃r.⊤)I . As y ∈ Δ′ , y must have been selected at step 3. Then, in steps 6 or 10, (y,w) is added to rI ′ for some w in Δ0. Hence, y ∈ (∃r.⊤)I ′ . Let y ∈ (∃r.⊤)I ′ . Then there is a w ∈ Δ′ such that (y, w) ∈ rI ′ . There are two cases. In the first one, (y,w) has been added to rI ′ in steps 6 or 10, since the condition of the for loop in step 4 holds. In this case, y ∈ (∃r.⊤)I . In the second case, (y,w) has been added to rI ′ in steps 14 or 18. By fact (2) above, there must be some z ∈ Δ such that (y, z) ∈ rI . Hence, y ∈ (∃r.⊤)I .

Let y ∈ (∃r-.⊤)I . As y ∈ Δ′ , y must have been selected at step 3. Then, in steps 14 or 18, (w, y) is added to rI ′ for some w in Δ0. Hence, y ∈ (∃r-.⊤)I ′ . Let y ∈ (∃r-.⊤)I ′ . Then there is a w ∈ Δ′ such that (w, y) ∈ rI ′ . There are two cases. In the first one, (w, y) has been added to rI ′ in steps 14 or 18, since the condition of the for loop in step 12 holds. In this case, y ∈ (∃r-.⊤)I . In the second case, (w, y) has been added to rI ′ in steps 6 or 10. By fact (1) above, there must be some z ∈ Δ such that (z, y) ∈ rI . Hence, y ∈ (∃r-.⊤)I . ■

Notice that, due to the differences in the treatment of existential concepts here and in the case of Left Local KBs, Lemma 4.3 is stronger than Lemmas 3.5, 3.6, and 3.7.

By Lemma 4.3, and by reasoning as for Left Local KBs, we can prove the following lemma and theorem:

Lemma 4.4 M′ is a minimal model of KB whose size is polynomial in the size of KB.

Theorem 4.5 (Small model theorem) KB |=DL-LitecTmin α if and only if KB |=small DL-LitecTmin α.

By the same argument used for Left Local KBs, we can prove:

Theorem 4.6 (Complexity for DL-LitecTmin) The problem of deciding whether KB |=DL-LitecTmin α is in Πp2 .

5 Conclusions

We have proposed a nonmonotonic extension of low complexity DLs EL⊥ and DL-Litecore for reasoning about typicality and defeasible properties. We have shown that entailment is EXPTIME-hard for EL⊥Tmin, whereas it drops to

Πp2 when considering the Left Local Fragment of EL⊥Tmin. The same complexity has been found for DL-LitecTmin. These results match the complexity upper bounds of the same fragments in circumscribed KBs [Bonatti et al., 2009]. In [Bonatti et al., 2010] a fragment of EL⊥ has been identified for which the complexity of circumscribed KBs is polynomial. In future work we shall investigate the complexity of minimal entailment for such fragment extended with T.