Preferential Low Complexity Description Logics: Complexity Results and Proof Methods

Abstract

In this paper we describe an approach for reasoning about typicality and defeasible properties in low complexity preferential Description Logics. We describe the non-monotonic extension of the low complexity DLs E L⊥ and DL-Litecore based on a typicality operator T, which enjoys a preferential semantics. We summarize complexity results for such extensions, called E L⊥Tmin and DL-Litec Tmin. Entailment in DL-LitecTmin is in Π2p, whereas entailment in E L⊥Tmin is EXPTIME-hard. However, for the Left Local fragment of E L⊥Tmin the complexity of entailment drops to Π2p. We present tableau calculi for Left Local E L⊥Tmin and for DL-Litec Tmin. The calculi perform a two-phase computation in order to check whether a query is minimally entailed from the initial knowledge base. The calculi are sound, complete and terminating, and provide decision procedures for verifying entailment in the two logics, whose complexities match the above mentioned complexity results.

-

has motivated the study of non-monotonic extensions of low complexity DLs such as DL-Litecore [ 5 ] and E L⊥ of the E L family [ 1 ] which are nonetheless well-suited for encoding large knowledge bases (KBs).

In this paper, we consider the extensions of the low complexity logics DL-Litecore and E L⊥ with the typicality operator based on the minimal model semantics introduced in [ 8 ]. We summarize complexity upper bounds for the resulting logics E L⊥Tmin and DL-Litec Tmin given in [ 11 ]. For E L⊥, it turns out that its extension E L⊥Tmin is unfortunately EXPTIME-hard. This result is analogous to the one for circumscribed E L⊥ KBs [ 3 ]. However, the complexity decreases to Π2p for the fragment of Left Local E L⊥ KBs, corresponding to the homonymous fragment in [ 3 ]. The same complexity upper bound is obtained for DL-LitecTmin.

We also describe the tableau calculi for DL-Litec Tmin as well as for the Left Local fragment of E L⊥Tmin for deciding minimal entailment in Π2p. Our calculi perform a two-phase computation: in the first phase, candidate models (complete open branches) falsifying the given query are generated, in the second phase the minimality of candidate models is checked by means of an auxiliary tableau construction. The calculi do not require any blocking machinery in order to achieve termination. A reformulation of existential rules, together with the idea of constructing multilinear models, is sufficient to match the Π2p complexity. 2

The Typicality Operator T and the Logic E L⊥Tmin Before describing E L⊥Tmin , let us briefly recall the underlying monotonic logic E L+⊥ T, obtained by adding to E L⊥ the typicality operator T. The intuitive idea is that T(C) selects the typical instances of a concept C. In E L+⊥ 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).

Formally, the E L+⊥ T language is defined as follows.

Definition 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 C := A | ⊤ | ⊥ | C ⊓ C

CR := C | CR ⊓ CR | ∃R.C

CL := CR | T(C) A KB is a pair (TBox, ABox). TBox contains a finite set of general concept inclusions (or subsumptions) CL ⊑ CR. ABox contains assertions of the form CL(a) and R(a, b), where a, b ∈ O.

The semantics of E L+⊥ T is defined by enriching ordinary models of E L⊥ 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 (Semantics of T). A model M is any structure hΔ, <, Ii 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 ∈ M in<(S) or ∃y ∈ M in<(S) such that y < x, where M in<(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 E L⊥, CI is defined in the usual way. For the T operator: (T(C))I = M in<(CI ).

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 Δ. We say that M satisfies an inclusion C ⊑ D if CI ⊆ DI , and that M satisfies C(a) if aI ∈ CI and aRb if (aI , bI ) ∈ RI . Moreover, M satisfies TBox if it satisfies all its inclusions, and M satisfies ABox if it satisfies all its formulas. M satisfies a KB (TBox,ABox), if it satisfies both its TBox and its ABox.

The operator T [ 12 ] is characterized by a set of postulates that are essentially a reformulation of the KLM [ 13 ] axioms of preferential logic P. T has therefore all the “core” properties of non-monotonic reasoning as it is axiomatized 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 ∈ CI , and (ii) there is no y ∈ CI 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. The interpretation of in M is as follows: ( C)I = {x ∈ Δ | for every y ∈ Δ, if y < x then y ∈ CI }. We immediately get that x ∈ (T(C))I if and only if x ∈ (C ⊓ ¬C)I . From now on, we consider T(C) as an abbrAevsimateionntiofonredCin⊓the¬ICnt.roduction, the main limit of E L+⊥ T is that it is monotonic. Even if the typicality operator T itself is non-monotonic (i.e. T(C) ⊑ E does not imply T(C ⊓ D) ⊑ E), what is inferred from an E L+⊥ T KB can still be inferred from any KB’ with KB ⊆ KB’. In order to perform non-monotonic inferences, as done in [ 8 ], we strengthen the semantics of E L+⊥ T by restricting entailment to a class of minimal (or preferred) models. We call the new logic E L⊥Tmin . Intuitively, the idea is to restrict our consideration to models that minimize the non typical instances of a concept.

Given a KB, we consider a finite set LT of concepts: these are the concepts whose non typical instances we want to minimize. We assume that the set LT contains at least all concepts C such that T(C) occurs in the KB or in the query F , where a query F is either an assertion C(a) or an inclusion relation C ⊑ D. As we have just said, x ∈ CI is typical for C if x ∈ ( ¬C)I . Minimizing the non typical instances of C therefore means to minimize the objects falsifying ¬C for C ∈ LT. Hence, for a given model M = hΔ, <, I i, we define:

−

MLT = {(x, ¬ ¬C) | x 6∈ ( ¬C)I , with x ∈ Δ, C ∈ LT}.

Definition 3 (Preferred and minimal models). Given a model M = hΔ <, I i of a knowledge base KB, and a model M′ = hΔ′, <′, I ′i of KB, we say that M is preferred − − to M′ w.r.t. LT, and we write M <LT M′, if (i) Δ = Δ′, (ii) MLT ⊂ M′LT , (iii) aI = aI′ for all a ∈ O. M is a minimal model for KB (w.r.t. LT) if it is a model of KB and there is no other model M′ of KB such that M′ <LT M.

Definition 4 (Minimal Entailment in E L⊥Tmin ). A query F is minimally entailed in E L⊥Tmin by KB with respect to LT if F is satisfied in all models of KB that are minimal with respect to LT. We write KB |=EL⊥Tmin F .

Example 1. The KB of the Introduction can be reformulated as follows in E L+⊥ T: TaxPayer ⊓ NotTaxPayer ⊑ ⊥; Parent ⊑ ∃HasChild .⊤; ∃HasChild .⊤ ⊑ Parent ; T(Student ) ⊑ NotTaxPayer ; T(Student ⊓ Worker ) ⊑ TaxPayer ; T(Student ⊓ Worker ⊓ Parent ) ⊑ NotTaxPayer . Let LT = {Student, Student ⊓ Worker , Student ⊓ Worker ⊓ Parent }. We have that TBox ∪ {Student(john)} |=EL⊥Tmin NotTaxPayer (john), since johnI ∈ (Student ⊓ ¬Student )I for all minimal models M = hΔ <, Ii of the KB. In contrast, by the non-monotonic character of minimal entailment, TBox ∪ {Student(john), Worker (john)} |=EL⊥Tmin TaxPayer (john). Last, notice that TBox ∪ {∃HasChild .(Student ⊓ Worker )(jack)} |=EL⊥Tmin ∃HasChild .TaxPayer (jack ). The latter shows that minimal consequence applies to implicit individuals as well, without any ad-hoc mechanism.

Theorem 1 (Complexity for E L⊥Tmin KBs (Theorem 3.1 in [ 11 ])). The problem of deciding whether KB |=EL⊥Tmin F is EXPTIME-hard.

To lower the complexity of minimal entailment in E L⊥Tmin , we consider Left Local KBs, a restriction similar to that introduced in [ 3 ] for circumscribed E L⊥ KBs. Definition 5 (Left Local knowledge base). A Left Local KB only contains subsumptions CLLL ⊑ CR, where C and CR are as in Definition 1 and:

CLLL := C | CLLL ⊓ CLLL | ∃R.⊤ | T(C) There is no restriction on the ABox.

Observe that the KB in the Example 1 is Left Local, as no concept of the form ∃R.C with C 6= ⊤ occurs on the left hand side of inclusions. In [ 11 ] an upper bound for the complexity of E L⊥Tmin Left Local KBs is provided 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. This allows us to conclude that: Theorem 2 (Complexity for E L⊥Tmin Left Local KBs (Theorem 3.12 in [ 11 ])). If KB is Left Local, the problem of deciding whether KB |=EL⊥Tmin F is in Π2p. 3

The Logic DL-Litec Tmin

In this section, we present the extension of the logic DL-Litecore [ 5 ] with the T operator. We call it DL-LitecTmin. The language of DL-Litec Tmin is defined as follows. Definition 6. We consider an alphabet of concept names C, of role names R, and of individuals O. Given A ∈ C and r ∈ R, we define

CL := A | ∃R.⊤ | T(A)

R := r | r−

CR := A | ¬A | ∃R.⊤ | ¬∃R.⊤ A DL-Litec Tmin 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 E L⊥Tmin , a model M for DL-LitecTmin is any structure hΔ, <, Ii, defined as in Definition 2, where I is extended to take care of inverse roles: given r ∈ R, (r−)I = {(a, b) | (b, a) ∈ rI }.

In [ 11 ] it has been shown that a small model construction similar to the one for Left Local E L⊥Tmin KBs can be made also for DL-Litec Tmin. As a difference, in this case, we exploit the fact that, 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−.⊤. Theorem 3 (Complexity for DL-Litec Tmin KBs (Theorem 4.6 in [ 11 ])). The problem of deciding whether KB |=DL-LitecTmin F is in Π2p. 4

The Tableau Calculus for Left Local E L⊥Tmin

In this section we present a tableau calculus TABEmLin⊥T for deciding whether a query F is minimally entailed from a Left Local knowledge base in the logic E L⊥Tmin . It performs a two-phase computation: in the first phase, a tableau calculus, called TABEPLH⊥1T, simply verifies whether KB ∪ {¬F } is satisfiable in an E L⊥T model, building candidate models; in the second phase another tableau calculus, called TABEPLH⊥2T, 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, TABEPLH⊥2T tries to build a model of KB which is preferred to the candidate model w.r.t. Definition 3. The whole procedure TABEmLin⊥T is formally defined at the end of this section (Definition 7).

The calculus TABEmLin⊥T tries to build an open branch representing a minimal model satisfying KB ∪ {¬F }. The negation of a query ¬F is defined as follows: if F ≡ C(a), then ¬F ≡ (¬C)(a); if F ≡ C ⊑ D, then ¬F ≡ (C ⊓ ¬D)(x), where x does not occur in KB. Notice that we introduce the connective ¬ in a very “localized” way. This is very different from introducing the negation all over the knowledge base, and indeed it does not imply that we jump out of the language of E L⊥Tmin .

TABEmLin⊥T makes use of labels, which are denoted with x, y, z, . . .. Labels represent individuals either named in the ABox or implicitly expressed by existential restrictions. R These labels occur in constraints (or labelled formulas), that can have the form x −→ y or x : C, where x, y are labels, R is a role and C is either a concept or the negation of a concept of E L⊥Tmin or has the form ¬D or ¬ ¬D, where D is a concept.

Let us now analyze the two components of TABEmLin⊥T, starting with TABEPLH⊥1T. A tableau of TABEPLH⊥1T is a tree whose nodes are tuples hS | U | W i. S is a set of constraints, whereas U contains formulas of the form C ⊑ DL, representing subsumption relations C ⊑ D of the TBox. L is a list of labels, used in order to ensure the termination of the tableau calculus. W is a set of labels xC used in order to build a “small” model, matching the construction of Theorem 3.11 in [ 11 ]. A branch is a sequence of nodes hS1 | U1 | W1i, hS2 | U2 | W2i, . . . , hSn | Un | Wni . . ., where each node hSi | Ui | Wii is obtained from its immediate predecessor hSi−1 | Ui−1 | Wi−1i by applying a rule of TABEPLH⊥1T, having hSi−1 | Ui−1 | Wi−1i as the premise and hSi | Ui | Wii as one of its conclusions. A branch is closed if one of its nodes is an instance of a (Clash) axiom, otherwise it is open. A tableau is closed if all its branches are closed. The rules of TABEPLH⊥1T are presented in Fig. 1. Rules (∃1+) and ( −) are called dynamic since they can introduce a new variable in their conclusions. The other rules are called static. We do not need any extra rule for the positive occurrences of , since these are taken into account by the computation of SxM→y of ( −). The (cut) rule ensures that, given any concept C ∈ LT, an open branch built by TABEPLH⊥1T contTaAinBsEPeLiHt⊥h2eTr txo c:heck the minimality of the model corresponding to the open branch. As ¬C or x : ¬ ¬C for each label x: this is needed in order to allow mentioned above, given a node hS | U | W i, each formula C ⊑ D in U is equipped with the list L of labels to which unfolding of the subsumption has already been applied. This avoids multiple unfolding of the same subsumption with the same label. specTtsh.eFciarlsct,ultuhse TruAleB(EP∃LH+⊥1)Tis split in the two rules (∃+)1 and (∃+)2. When the rule is different from the calculus ALC + Tmin [ 8 ] in two re(∃+)1 is applied to a formula u : ∃R.C, it introduces a new label xC only when the set R W does not already contain xC . Otherwise, xC is already on the branch and u −→ xC is simply added to the conclusion of the rule. As a consequence, in a given branch, (∃+)1 introduces a unique new label xC for each concept C occurring in the initial KB in some ∃R.C, and no blocking machinery is needed to ensure termination. This simplification is possible since we are considering Left Local KBs, which have small models; in these models all existentials ∃R.C occurring in KB are made true by reusing a single witness xC (Theorem 3.12 in [ 11 ]). Notice also that the rules (∃+)1 and (∃+)2 introduce a branching on the choice of the label used to realize the existential restriction u : ∃R.C. However, just the leftmost conclusion of (∃+)1 introduces a new label xC ; in all the other branches, a label yi occurring in S is chosen.

Second, in order to build multilinear models of Definition 2, the calculus adopts a strengthened version of the rule ( −) used in TABAmLinC+T [ 8 ]. We write S as an abbreviation for S, u : ¬ ¬C1, . . . , u : ¬ ¬Cn. Moreover, we define SuM→−ky = {y : ¬D, y : ¬D | u : ¬D ∈ S} and, for k = 1, 2, . . . , n, we define Su→y = {y : ¬ ¬Cj ⊔ Cj | u : ¬ ¬Cj ∈ S ∧ j 6= k}. The strengthened rule ( −) contains: (i) n branches, one for each u : ¬ ¬Ck in S, in which a new typical Ck individual x is introduced (i.e. x : Ck and x : ¬Ck are added), and for all other u : ¬ ¬Cj , either x : Cj holds or the formula x : ¬ ¬Cj is recorded; (ii) other n × m branches, one for each label yi and for each u : ¬ ¬Ck in S (m is the number of labels occurring in S): in these branches, a given yi is chosen as a typical instance of Ck, that is to say yi : Ck and yi : ¬Ck are added, and for all other u : ¬ ¬Cj , either yi : Cj holds or the formula yi : ¬ ¬Cj is recorded. This rule is sound with respect to multilinear models. The advantage of this rule over the ( −) rule in the calculus TABAmLinC+T is that all the negated box formulas labelled by u are treated in one step, introducing only a new label x in one of the conclusions. To keep S readable, we have used ⊔. Hence, our calculus requires the rule for ⊔, even if this constructor does not belong to E L⊥Tmin .

In order to check the satisfiability of a KB, we build its corresponding constraint system hS | U | ∅i, and we check its satisfiability. Given KB=(TBox,ABox), its corre!S, x : C, x : ¬C | U | W" (Clash) !S, x : ¬⊤ | U | W# (Clash)¬⊤ !S, x : ⊥ | U | W# (Clash)⊥ !S, x : C ⊓ D | U | W# (⊓+) !S, x : C, x : D | U | W"

!S, x : ¬(C ⊓ D) | U | W# (⊓−) !S, x : ¬C | U | W" !S, x : ¬D | U | W"

!S, x : C ⊔ D | U | W# (⊔+) !S, x : C | U | W" !S, x : D | U | W" !S, x : T(C) | U | W" (T+) !S, x : C, x : !¬C | U | W"

!S, x : ¬T(C) | U | W" (T−) !S | U, C ⊑ DL | W# (Unfold) !S, x : ¬C | U | W" !S, x : ¬!¬C | U | W" !S, x : ¬C ⊔ D | U, C ⊑ DL,x | W$ if x occurs in S and x !∈ L !S, u −R→ xC, xC : C | U | W ∪ {xC}% !S!S, ,uu: −∃R→R.Cy1|, yU1 |: WC#| U | W$ . . . !S, u −R→ ym, ym : C | U | W$(∃+)1

if xC !∈ W and y1, . . . , ym are all the labels occurring in S !S, u −R→ xC | U | W$ !S, u −!SR→, uy:1,∃yR1.:CC| |UU| |WW# $ . . .!S, u −R→ ym, ym : C | U | W$(∃+)2

if xC ∈ W and y1, . . . , ym are all the labels occurring in S !S, x : ¬∃R.C, x −R→ y | U | W% (∃−) !S, x : ¬∃R.C, x −R→ y, y : ¬C | U | W% if y : ¬C !∈ S !S, x : ¬!¬C | U!|SW| U" | W!S",x : !¬C | U | W" (cut) if x : ¬!¬C !∈ S and x : !¬C !∈ S x occurs in S C ∈ LT !S!,−uk: ¬!¬C1, u : ¬!¬C2, . . . , u : ¬!¬Cn | U | W" (!−) !S, x : Ck, x : !¬Ck, SuM→x, Su→x | U | W" !−k !S, y1 : Ck, y1 : !¬Ck, SuM→y1, Su!→−yk1 | U | W" . . . !S, ym : Ck, ym : !¬Ck, SuM→ym, Su→ym | U | W" x new if y1, . . . , ym are all the labels occurring in S, y1 != u, . . . , ym != u

k = 1, 2, . . . , n

Fig. 1. The calculus TABEPLH⊥1T. sponding constraint system hS | U | ∅i is defined as follows: S = {a : C | C(a) ∈

R ABox} ∪ {a −→ b | R(a, b) ∈ ABox}; U = {C ⊑ D∅ | C ⊑ D ∈ T Box}. KB is satisfiable if and only if its corresponding constraint system hS | U | ∅i is satisfiable. In order to verify the satisfiability of KB ∪ {¬F }, we use TABEPLH⊥1T to check the satisfiability of the constraint system hS | U | ∅i obtained by adding the constraint corresponding to ¬F to S′, where hS′ | U | ∅i is the corresponding constraint system of KB. To this purpose, the rules of the calculus TABEPLH⊥1T are applied until either a contradiction is generated (Clash) or a model satisfying hS | U | ∅i can be obtained from the resulting constraint system.

The rules of TABEPLH⊥1T are applied with the following standard strategy: 1. apply a rule to a label x only if no rule is applicable to a label y such that y ≺ x (where y ≺ x says that label x has been introduced in the tableaux later than y); 2. apply dynamic rules only if no static rule is applicable. In [ 9 ] it has been shown that the calculus is sound and complete and terminating. In particular, any tableau generated by TABEPLH⊥1T for hS | U | ∅i is finite, and the length of the tableau branches built by the strategy is O(n2). This follows from the fact that dynamic rules (∃+)1 and ( −) generate at most O(n) labels in a branch, and that, for each label, static rules are applied at most O(n) times. Hence, given a KB and a query F , the problem of checking whether KB ∪ {¬F } in TABEPLH⊥1T is satisfiable is in NP.

!S, x : C, x : ¬C | U | K" (Clash) !S, x : ¬⊤ | U | K# (Clash)¬⊤ !S, x : ⊥ | U | K# (Clash)⊥ !S | U | ∅#(Clash)∅ !S, x : ¬!¬C | U | K" (Clash)!− if x : ¬!¬C !∈ K

!S | U, C ⊑ DL | K# !S, x : ¬C ⊔ D | U, C ⊑ DL,x | K$ (Unfold) x ∈ D(B) and x !∈ L !!SS,,xx::CC, x⊓:DD||UU||KK#" (⊓+)

!S, x : ¬(C ⊓ D) | U | K# !S, x : T(C) | U | K" !S, x : ¬C | U | K" !S, x : ¬D | U | K" (⊓−) !S, x : C, x : !¬C | U | K" (T+) !S, x : ¬T(C) | U | K" !S, x : ¬C | U | K" !S, x : ¬!¬C | U | K" (T−)

!S, u : ∃R.C | U | K# !S, u −R→ y1, y1 : C | U | K$ . . . !S, u −R→ ym, ym : C | U | K$ (∃+) if D(B) = {y1, . . . , ym}

!S | U | K" !S, x : !¬C | U | K" !S, x : ¬!¬C | U | K" (cut) if x : ¬!¬C !∈ S and x : !¬C !∈ S x ∈ D(B) C ∈ LT !S, u : ¬!¬C1, . . . , u : ¬!¬Cn | U | K, u : ¬!¬C1, . . . , u : ¬!¬Cn" !S, y1 : Ck, y1 : !¬Ck, SuM→y1, Su→y1 | U | K" . . . !S, ym : Ck, ym : !¬Ck, SuM→ym, Su→ym | U | K" (!−) !−k !−k

if D(B) = {y1, . . . , ym} and y1 != u, . . . , ym != u

Fig. 2. The calculus TABEPLH⊥2T. To save space, we omit the rule (⊔+). Let us now introduce the calculus TABEPLH⊥2T which, for each open branch B built by TABEPLH⊥1T, verifies whether it represents a minimal model of the KB. Given an open branch B of a tableau built from TABEPLH⊥1T, let D(B) be the set of labels occurring on − B. M−oreover, let B be the set of formulas x : ¬ ¬C occurring in B, that is to say B = {x : ¬ ¬C | x : ¬ ¬C occurs in B}.

A tableau of TABEPLH⊥2T is a tree whose nodes are tuples of the form hS | U | Ki, where S and U are defined as in a constraint system, whereas K contains formulas of the form x : ¬ ¬C, with C ∈ LT. The basic idea of TABEPLH⊥2T is as follows. Given an open branch B built by TABEPLH⊥1T and corresponding to a model MB of KB ∪ {¬F }, TABEPLH⊥2T checks whether MB is a minimal model of KB by trying to build a model of KB which is preferred to MB. To this purpose, it keeps track (in K) − of the negated box used in B (B ) in order to check whether it is possible to build a model of KB containing less negated box formulas. The tableau built by TABEPLH⊥2T closes if it is not possible to build a model smaller than MB, it remains open otherwise. Since by Definition 3 two models can be compared only if they have the same domain, TABEPLH⊥2T tries to build an open branch containing all the labels appearing on B, i.e. those in D(B). To this aim, the dynamic rules use labels in D(B) instead of introducing new ones in their conclusions. The rules of TABEPLH⊥2T are shown in Fig. 2.

More in detail, the rule (∃+), when applied to a formula x : ∃R.C, introduces,

R for each label y ∈ D(B), x −→ y and y : C. The choice of the label y introduces a branching in the tableau construction. The rule (Unfold) is applied to all the labels of D(B) (and not only to those appearing in the branch). The rule ( −) is applied to a node hS, u : ¬ ¬C1, . . . , u : ¬ ¬Cn | U | Ki, when {u : ¬ ¬C1, . . . , u : ¬ ¬Cn} ⊆ K, i.e. when the negated box formulas u : ¬ ¬Ci also belong to the open branch B. Also in this case, the rule introduces a branch on the choice of the individual yi ∈ D(B) to be used in the conclusion. In case a tableau node has the form hS, x : ¬ ¬C | U | Ki, and x : ¬ ¬C 6∈ K, then TABEPLH⊥2T detects a clash, called (Clash) − : this corresponds to the situation where x : ¬ ¬C does not belong to B, while the model corresponding to the branch being built contains x : ¬ ¬C, and hence is not preferred to the model represented by B.

The calculus TABEPLH⊥2T also contains the clash condition (Clash)∅. Since each application of ( −) removes the negated box formulas x : ¬ ¬Ci from the set K, when K is empty all the negated boxed formulas occurring in B also belong to the current branch. In this case, the model built by TABEPLH⊥2T satisfies the same set of x : ¬ ¬Ci (for all individuals) as B and, thus, it is not preferred to the one represented by B.

Let KB be a knowledge base whose corresponding constraint system is hS | U | ∅i. Let F be a query and let S′ be the set of constraints obtained by adding to S the constraint corresponding to ¬F . TABEEPLLH⊥⊥2TT is sound and complete in the following smeondsee:l aonf KopBe niffbrthanecthabBlebauuiilntbTyATBAEPBLH⊥P2TH1 for hS′ | U | ∅i is satisfiable in a minimal − for hS | U | B i is closed.

Termination of the calculus TABEPLH⊥2T is ensured by the fact that dynamic rules make use of labels belonging to D(B), which is finite, rather than introducing “new” labels in the tableau. Also, it is possible to show that the problem of verifying that a branch B represents a minimal model for KB in TABEPLH⊥2T is in NP in the size of B.

The overall procedure TABAmLinC+T is defined as follows: Definition 7. Let KB be a knowledge base whose corresponding constraint system is hS | U | ∅i. Let F be a query and let S′ be the set of constraints obtained by adding to S the constraint corresponding to ¬F . The calculus TABEmLin⊥T checks whether a query F is minimally entailed from KB by means of the following procedure: (phase 1) the eciatlhceurlu(si)TBAiBs EPcLlHo⊥1sTedisoarp(piil)ie(dphtoasheS′2)| Uthe| t∅aib;liefa,fuorbueialtchbybrtahnecchaBlcubuluilst TbyATBAEPLBH⊥P2TH1for, EL⊥T hS | U | B −

i is open, then KB |=LmTin F , otherwise KB 6|=LmTin F . |=EL⊥Tmin F by means of TABEmLin⊥T is in Π2p.

In [ 9 ] it has been shown that TABEmLin⊥T is a sound and complete decision procedure for verifying if KB |=EL⊥Tmin F . Furthermore, the problem of deciding whether KB 5

A Tableau Calculus for DL-Litec Tmin

differs from TABEPLH⊥1T in the following points: In this section we shortly describe a tableau calculus TABLmiitnecT for deciding query entailment in the logic DL-LitecTmin. The calculus is similar to the one introduced for E L⊥Tmin in the previous section, however it is significantly different from it in the definition of some of the rules. Given a set of constraints S and a role r ∈ R, let r(S) = {x −r→ y | x −r→ y ∈ S}. The calculus TABPLiHte1cT used in the first phase 1. As in the calculus TABEPLH⊥1T, the split of the (∃+) in the two rules: !S, x −r→ y | U$ !!SS,,xx −:r→∃r.y⊤1 || UU$$. . .!S, x −r→ ym | U$ (∃+)r1 if r(S) = ∅

y new if y1, . . . , ym are all the labels occurring in S !S, x : ∃r.⊤ | U$ (∃+)r2 !S, x −r→ y1 | U$ . . . !S, x −r→ ym | U$

if r(S) != ∅ if y1, . . . , ym are all the labels occurring in S reflects the main idea of the construction of a small model at the base of Theorem 4.5 in [ 11 ]. Such small model theorem essentially shows that DL-LitecTmin KBs can have small models in which all existentials ∃R.⊤ occurring in KB are made true in the model by reusing a single witness y. In the calculus we use the same idea: when the rule (∃+)r r 1 is applied to a formula x : ∃r.⊤, it introduces a new label y and the constraint x −→ y r only when there is no other previous constraint u −→ v in S, i.e. r(S) = ∅. Otherwise, r rule (∃+)r2 is applied and it introduces x −→ y. As a consequence, (∃+)r2 does not introduce any new label in the branch whereas (∃+)r1 only introduces a new label y for each role r occurring in the initial KB in some ∃r.⊤ and no blocking machinery is needed to ensure termination.

2. In order to keep into account inverse roles, two further rules for existential formulas are introduced:

!S, x : ∃r−.⊤ | U$ (∃+)r1− !S, y −r→ x | U$ !S, y1 −r→ x | U$ . . . !S, ym −r→ x | U$ if r(S) = ∅

y new if y1, . . . , ym are all the labels occurring in S !S, x : ∃r−.⊤ | U$ !S, y1 −r→ x | U$ . . . !S, ym −r→ x | U$ (∃+)r2−

if r(S) != ∅ if y1, . . . , ym are all the labels occurring in S These rules work similarly to (∃+)r1 and (∃+)r2 in order to build a branch representing − a small model: when the rule (∃+)r1 is applied to a formula x : ∃r−.⊤, it introduces a r r new label y and the constraint y −→ x only when there is no other constraint u −→ v r in S. Otherwise, since a constraint y −→ u has been already introduced in that branch, r y −→ x is added to the conclusion of the rule.

3. Negated existential formulas can occur in a branch, but only having the form (i) x : ¬∃r.⊤ or (ii) x : ¬∃r−.⊤. (i) means that x has no relationships with other individr uals via the role r, i.e. we need to detect a contradiction if both (i) and x −→ y belong to the same branch (for some y), and mark the branch as closed. The clash condition (Clash)r is added to the calculus TABPLiHte1cT in order to detect such a situation. Analogously, (ii) means that there is no y such that y is related to x by means of r, then (Clash)r− is introduced in order to close a branch containing both (ii) and, for some y, r a constraint y −→ x. These clash conditions are as follows: !S, x −r→ y, x : ¬∃r.⊤ | U& (Clash)r !S, y −r→ x, x : ¬∃r−.⊤ | U& (Clash)r− of TABLmiitnecT is in Π2p.

Apart from the differences above, the rules of TABPLiHte1cT are the same as those of TABEPLH⊥1T. Similarly for the calculus TABPLiHte2cT used in the second phase. In [ 10 ] it has been shown that both TABPLiHte1cT and TABPLiHte2cT are sound, complete and terminating. Furthermore, the problem of deciding whether KB |=DL-LitecTmin F by means 6 Conclusions We have proposed a non-monotonic extension of low complexity Description Logics E L⊥ and DL-Litecore for reasoning about typicality and defeasible properties. We have summarized complexity results recently studied for such extensions [ 11 ], namely that entailment is EXPTIME-hard for E L⊥Tmin , whereas it drops to Π2p when considering the Left Local Fragment of E L⊥Tmin . The same Π2p complexity has been found for DL-Litec Tmin. These results match the complexity upper bounds of the same fragments in circumscribed KBs [ 3 ]. We have also provided tableau calculi for checking minimal entailment in the Left Local fragment of E L⊥Tmin as well as in DL-Litec Tmin. The proposed calculi match the complexity results above. Of course, many optimizations are possible and we intend to study them in future work.

As mentioned in the Introduction, several non-monotonic extensions of DLs have been proposed in the literature and we refer to [ 12 ] for a survey. Concerning nonmonotonic extensions of low complexity DLs, the complexity of circumscribed fragments of the E L⊥ and DL-Lite families have been studied in [ 3 ]. Recently, a fragment of E L⊥ for which the complexity of circumscribed KBs is polynomial has been identified in [ 14 ]. In future work, we shall investigate complexity of minimal entailment for such a fragment extended with T and possibly the definition of a calculus for it.

References

1. Baader , F. , Brandt , S. , Lutz , C. : Pushing the E L envelope . In: IJCAI. pp. 364 - 369 ( 2005 )

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

3. Bonatti , P.A. , Faella , M. , Sauro , L. : Defeasible inclusions in low-complexity DLs . J. Artif. Intell. Res. (JAIR) 42 , 719 - 764 ( 2011 )

4. Bonatti , P.A. , Lutz , C. , Wolter , F. : The complexity of circumscription in DLs . J. Artif. Intell. Res. (JAIR) 35 , 717 - 773 ( 2009 )

5. Calvanese , D. , Giacomo , G.D. , Lembo , D. , Lenzerini , M. , Rosati , R. : Tractable reasoning and efficient query answering in Description Logics: the DL-Lite family . J. Autom. Reasoning (JAR) 39(3) , 385 - 429 ( 2007 )

6. Casini , G. , Straccia , U. : Rational closure for defeasible DLs . In: JELIA. pp. 77 - 90 ( 2010 )

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

8. Giordano , L. , Gliozzi , V. , Olivetti , N. , Pozzato , G.L. : Reasoning about typicality in preferential Description Logics . In: JELIA. pp. 192 - 205 ( 2008 )

9. Giordano , L. , Gliozzi , V. , Olivetti , N. , Pozzato , G.L.: A tableau calculus for a nonmonotonic extension of E L⊥ . In: TABLEAUX. pp. 180 - 195 ( 2011 )

10. Giordano , L. , Gliozzi , V. , Olivetti , N. , Pozzato , G.L.: A tableau calculus for a nonmonotonic extension of the Description Logic DL-Litecore . In: AI*IA. pp. 164 - 176 ( 2011 )

11. Giordano , L. , Gliozzi , V. , Olivetti , N. , Pozzato , G.L. : Reasoning about typicality in low complexity DLs: the logics E L⊥Tmin and DL-litecTmin . In: IJCAI . pp. 894 - 899 ( 2011 )

12. Giordano , L. , Gliozzi , V. , Olivetti , N. , Pozzato , G.: ALC + Tmin: a preferential extension of Description Logics . Fundamenta Informaticae 96 , 1 - 32 ( 2009 )

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

14. Bonatti , P.A. , Faella , M. , Sauro , L.: E L with default attributes and overriding . In: ISWC . pp. 64 - 79 ( 2010 )

15. Straccia , U. : Default inheritance reasoning in hybrid kl-one-style logics . In: IJCAI . pp. 676 - 681 ( 1993 )