Nonmonotonic Extensions of Low Complexity DLs: Complexity Results and Proof Methods

Abstract

In this paper we propose nonmonotonic extensions of low complexity Description Logics E L⊥ and DL-Litecore for reasoning about typicality and defeasible properties. The resulting logics are called E L⊥Tmin and DL-Litec Tmin. We summarize complexity results for such extensions recently studied. Entailment in DL-Litec Tmin is in Π2p, whereas entailment in E L⊥Tmin is EXPTIMEhard. However, considering the known fragment of Left Local E L⊥Tmin, we have that the complexity of entailment drops to Π2p. Furthermore, we present tableau calculi for E L⊥Tmin (focusing on Left Local knowledge bases) and 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. Furthermore, they represent decision procedures for Left Local E L⊥Tmin knowledge bases and DL-LitecTmin knowledge bases, whose complexities match the above mentioned results.

-

Introduction The family of description logics (DLs) is one of the most important formalisms of knowledge representation. They have a well-defined semantics based on first-order logic and offer a good trade-off between expressivity and complexity. DLs have been successfully implemented by a range of systems and they are at the base of languages for the semantic web such as OWL. A DL knowledge base (KB) comprises two components: the TBox, containing the definition of concepts (and possibly roles), and a specification of inclusion relations among them, and the 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.

Nonmonotonic extensions of Description Logics (DLs) have been actively investigated since the early 90s, [ 15, 4, 2, 3, 7, 12, 10, 9, 6 ]. A simple but powerful nonmonotonic extension of DLs is proposed in [ 12, 10, 9 ]: in this approach “typical” or “normal” properties can be directly specified by means of a “typicality” operator T enriching the underlying DL; the typicality operator T is essentially characterised by the core properties of nonmonotonic reasoning axiomatized by preferential logic [ 13 ]. In ALC + T [ 12 ], 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 students having children normally do not: T(Student ) ⊑ ¬TaxPayer ; T(Student ⊓ Worker ) ⊑ TaxPayer ; T(Student ⊓ W orker ⊓ ∃HasChild .⊤) ⊑ ¬TaxPayer . Although the operator T is nonmonotonic in itself, the logic ALC + T, as well as the logic E L+⊥ T [ 10 ] extending E L⊥, is monotonic. As a consequence, unless a KB contains explicit assumptions about typicality of individuals (e.g. that john is a typical student), there is no way of inferring defeasible properties of them (e.g. that john does not pay taxes). In [ 9 ], a non monotonic extension of ALC + T based on a minimal model 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 minimalmodel semantics to a standard DL, such as ALC, leads to a very high complexity (namely query entailment in ALC + Tmin is in CO-NEXPNP [ 9 ]). This fact has motivated the study of nonmonotonic 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 hence 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 [ 9 ]. We summarize complexity upper bounds for the resulting logics E L⊥Tmin and DL-Litec Tmin studied 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 present 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 latter tries to build a model which is “more preferred” than the candidate one: if it fails (being closed) the candidate model is minimal, otherwise it is not. Both tableaux constructions comprise some non-standard rules for existential quantification in order to constrain the domain (and its size) of the model being constructed. The second phase makes use in addition of special closure conditions to prevent the generation of non-preferred models. The calculi are very simple and do not require any blocking machinery in order to achieve termination. It comes as a surprise that the modification of the existential rule is sufficient to match the Π2p complexity. 2

The typicality operator T and the Logic E L⊥Tmin

Formally, the E L Before describing E L⊥Tmin, let us briefly recall the underlying monotonic logic E L+⊥ T [ 10 ], 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). +⊥

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 [ 10 ] 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Δ, <, I 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 ∈ 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 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 ∈ 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. Observe that by the Smoothness Condition, has the properties of Go¨ del-Lo¨ b modal logic of provability G. 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 abbreviation for C ⊓ ¬C.

As mentioned in the Introduction, the main limit of E L 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), what is inferred from an E L+⊥ T KB can still be inferred from any KB’ with KB ⊆ KB’. In order to perform nonmonotonic inferences, as done in [ 9 ], 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 if x ∈ ( ¬C)I . Minimizing the non typical instances of C therefore means to minimize the objects not satisfying ¬C for C ∈ LT. Hence, for a given model M = hΔ, <, Ii, we define:

−

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

Definition 3 (Preferred and minimal models). Given a model M = hΔ <, Ii of a knowledge base KB, and a model M′ = hΔ′, <′, I′i of KB, we say that M is preferred − to M′ with respect to 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 (with respect to 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 }. Then 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 nonmonotonic 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 α is EXPTIME-hard.

In order to lower the complexity of minimal entailment in E L⊥Tmin, we consider a syntactic restriction on the KB called Left Local KBs. This restriction is similar to the one 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 α 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 the resulting logic DL-Litec Tmin. The language of DL-LitecTmin 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-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 E L⊥Tmin, a model M for DL-Litec Tmin 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 α 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 8).

As usual, 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 either a variable or an individual of the ABox, that is to say an element of O ∪ V . These R 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 calculus TABEPLH⊥1T is different in two respects from the calculus ALC + Tmin presented in [ 9 ]. First, the rule (∃+) is split in the following two rules:

When the rule (∃+)1 is applied to a formula u : ∃R.C, it introduces a new label xC only when the set W does not already contain xC . Otherwise, since xC has been

R already introduced in that branch, u −→ xC is added to the conclusion of the rule rather than introducing a new label. As a consequence, in a given branch, (∃+)1 only introduces a 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. As it will become clear in the proof of Theorem 4, this 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: just the leftmost conclusion of (∃+)1 introduces a new label (as R mentioned, the xC such that xC : C and u −→ xC are added to the branch); in all the other branches, each one of the other labels yi occurring in S may be chosen.

Second, in order to build multilinear models of Definition 2, the calculus adopts a strengthened version of the rule ( −) used in TABAmLinC+T [ 9 ]. 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 ( −) is as follows: (!−) !−k !−k !S, y1 : Ck, y1 : !¬Ck, SuM→y1, Su→y1 | U | W " . . . !S, ym : Ck, ym : !¬Ck, SuM→ym, Su→ym | U | W " for all k = 1, 2, . . . , n, where y1, . . . , ym are all the labels occurring in S and x is new.

Rule ( −) contains: n branches, one for each u : ¬ ¬Ck in S; in each branch 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; - other n × m branches, where m is the number of labels occurring in S, one for each label yi and for each u : ¬ ¬Ck 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 (some of) the conclusions. Notice that in order to keep S readable, we have used ⊔. This is the reason why our calculi contain 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 corresponding 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}. Definition 7 (Model satisfying a constraint system). Let M = hΔ, I, <i be a model as in Definition 2. We define a function α which assigns to each variable of V an element of Δ, and assigns every individual a ∈ O to aI ∈ Δ. M satisfies a constraint F under R α, written M |=α F , as follows: (i) M |=α x : C iff α(x) ∈ CI ; (ii) M |=α x −→ y iff (α(x), α(y)) ∈ RI . A constraint system hS | U | W i is satisfiable if there is a model M and a function α such that M satisfies every constraint in S under α and that, for all C ⊑ DL ∈ U and for all x ∈ Δ, we have that if x ∈ CI then x ∈ DI . Given a KB=(TBox,ABox), it 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.

Given a node hS | U | W i, for each subsumption C ⊑ DL ∈ U and for each label x that appears in the tableau, we add to S the constraint x : ¬C ⊔ D: we refer to this mechanism as unfolding. As mentioned above, each formula C ⊑ D is equipped with a list L of labels in which it has been unfolded in the current branch. This is needed to !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 avoid multiple unfolding of the same subsumption by using the same label, generating infinite branches.

Before introducing the rules of T ABEPLH⊥1T we need some more definitions. First, we define an ordering relation ≺ to keep track of the temporal ordering of insertion of labels in the tableau, that is to say if y is introduced in the tableau, then x ≺ y for all labels x that are already in the tableau. Furthermore, if x is the label occurring in the query F , then x ≺ y for all y occurring in the constraint system corresponding to the initial KB. The rules of T ABEPLH⊥1T are presented in Figure 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 the operator, 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 T ABEPLH⊥1T contains either x : ¬C or x : ¬ ¬C for each label x: this is needed

EL⊥T in order to allow T ABP H2 to check the minimality of the model corresponding to the open branch.

The rules of T ABEPLH⊥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; 2. apply dynamic rules only if no static rule is applicable. In [ 8 ] it has been shown that the calculus is sound and complete with respect to the semantics in Definition 7 and it ensures termination: Theorem 4 (Soundness and completeness of TABEPLH⊥1T [ 8 ]). If KB 6|=EL⊥Tmin F , then the tableau for the constraint system corresponding to KB ∪ {¬F } contains an open saturated branch, which is satisfiable (via an injective assignment from labels to domain elements) in a minimal model of KB. Given a constraint system hS | U | W i, if it is unsatisfiable, then it has a closed tableau in TABEPLH⊥1T.

Theorem 5 (Termination of TABEPLH⊥1T [ 8 ]). Any tableau generated by TABEPLH⊥1T for hS | U | ∅i is finite.

Let us conclude this section by estimating the complexity of TABEPLH⊥1T. Let n be the size of the initial KB, i.e. the length of the string representing KB, and let hS | U | ∅i be its corresponding constraint system. We assume that the size of F and LT is O(n). The calculus builds a tableau for hS | U | ∅i whose branches’s size is O(n). This immediately follows from the fact that dynamic rules (∃+)1 and ( −) generate at most O(n) labels in a branch. Indeed, the rule (∃+)1 introduces a new label xC for each concept C occurring in KB, then at most O(n) labels. Concerning ( −), consider a branch generated by its application to a constraint system hS, u : ¬ ¬C1 . . . , u : ¬ ¬Cn | U | W i. In the worst case, a new label x1 is introduced. Suppose also that the branch under consideration is the one containing x1 : C1 and x1 : ¬C1. The ( −) rule can then be applied to formulas u : ¬ ¬Ck, introducing also a further new label x2. However, by the presence of x1 : ¬C1, the rule ( −) can no longer consistently introduce x2 : ¬ ¬C1, since x2 : ¬C1 ∈ SxM1→x2 . Therefore, ( −) is applied to ¬ ¬C1 . . . ¬ ¬Cn in u. This application generates (at most) one new world x1 that labels (at most) n − 1 negated boxed formulas. A further application of ( −) to ¬ ¬C1 . . . ¬ ¬Cn−1 in x1 generates (at most) one new world x2 that labels (at most) n − 2 negated boxed formulas, and so on. Overall, at most O(n) new labels are introduced by ( −) in each branch. For each of these labels, static rules apply at most O(n) times: (Unfold) is applied at most O(n) times for each C ⊑ D ∈ U , one for each label introduced in the branch. The rule (cut) is also applied at most O(n) times for each label, since LT contains at most O(n) formulas. As the number of different concepts in KB is at most O(n), in all steps involving the application of boolean rules, there are at most O(n) applications of these rules. Therefore, the length of the tableau branch built by the strategy is O(n2). Finally, we observe that all the nodes of the tableau contain a number of formulas which is polynomial in n, therefore to test whether a node is an instance of a (Clash) axiom has at most complexity polynomial in n.

Theorem 6 (Complexity of TABEPLH⊥1T). Given a KB and a query F , the problem of checking whether KB ∪ {¬F } in TABEPLH⊥1T is satisfiable is in NP.

4.2 The tableaux calculus TABEPLH⊥2T

EL⊥T which, for each open branch B built by Let us now introduce the calculus TABP H2 TABEPLH⊥1T, verifies whether it represents a minimal model of the KB. Given an open !S, x : ¬⊤ | U | K# (Clash)¬⊤ !S, x : ⊥ | U | K# (Clash)⊥ !S | U | ∅# (Clash)∅ !!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+)

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 (∃+) is applied to a constraint system containing a formula

R x : ∃R.C; it introduces x −→ y and y : C where y ∈ D(B), instead of y being a new label. 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. Even 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. Theorem 7 (Soundness and completeness of TABEPLH⊥2T [ 8 ]). Given a KB and a query F , let hS′ | U | ∅i be the corresponding constraint system of KB, and hS | U | ∅i the corresponding constraint system of KB ∪ {¬F }. An open branch B built by TABEPLH⊥1T for hS | U | ∅i is satisfiable by an injective mapping in a minimal model of KB iff the tableau in TABEPLH⊥2T for hS′ | U | B i is closed. − TABEPLH⊥2T always terminates. Termination 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.

Theorem 8 (Termination of TABEPLH⊥2T). Let hS′ | U | B

i be a constraint system starting from an open branch B built by TABEPLH⊥1T, then any tableau generated by −

TABEPLH⊥2T is finite.

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.

ALC+T is defined as follows:

The overall procedure TABmin Definition 8. 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 a KB by means of the following procedure: (phase 1) the eciatlhceurlu(si)TBAiBs EPcLHlo⊥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 .

Theorem 9 (Soundness and completeness of TABEmLin⊥T [ 8 ]). TABEmLin⊥T is a sound and complete decision procedure for verifying if KB |=LmTin F .

EL⊥T matches the results of Theorem 2. Consider the com

The complexity of TABmin plementary problem: KB 6|=LmTin F . This problem can be solved according to the procedure in Definition 8: by nondeterministically generating an open branch of polynomial length in the size of KB in TABEPLH⊥1T (a model MB of KB ∪ {¬F }), and then by calling an NP oracle which verifies that MB is a minimal model of KB. In fact, the verification that MB is not a minimal model of the KB can be done by an NP algorithm which nondeterministically generates a branch in TA B′EPLH⊥2T of polynomial size in the size of MB (and of KB), representing a model MB of KB preferred to MB. Hence, the problem of verifying that KB 6|=LmTin F is in NPNP, i.e. in Σ2p, and the problem of deciding whether KB |=LmTin F is in CO-NPNP, i.e. in Π2p.

F by means of TABEmLin⊥T is in Π2p.

Theorem 10 (Complexity of TABEmLin⊥T). The problem of deciding whether KB |=LmTin 5

A Tableau Calculus for DL-Litec Tmin

In this section we present a tableau calculus TABLmiitnecT for deciding query entailment in the logic DL-Litec Tmin. The calculus is similar to the one for E L⊥Tmin in the previous section, however it contains a few significant differences. Let us analyze in detail the two components of TABLmiitnecT.

5.1 First Phase: the tableaux calculus TABPLiHte1cT

The calculus TABPLiHte1cT is significantly different in three respects from the calculus for E L⊥Tmin. We try to explain such differences in detail. First of all, given a set of r r constraints S and a role r ∈ R, we define r(S) = {x −→ y | x −→ y ∈ S}. 1. The rule (∃+) is split in the following two rules:

!S, x : ∃r.⊤ | U$ (∃+)r1 !S, x −r→ y | U$ !S, x −r→ y1 | U$. . .!S, x −r→ ym | U$ 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 As in the calculus TABEPLH⊥1T, the split of the (∃+) in the two rules above 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-Litec Tmin 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 (∃+)r1 is applied r to a formula x : ∃r.⊤, it introduces a new label y and the constraint x −→ y only r when there is no other previous constraint u −→ v in S, i.e. r(S) = ∅. Otherwise, rule r (∃+)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.⊤ or ∃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$

if r(S) != ∅ if y1, . . . , ym are all the labels occurring in S (∃+)r2− These rules work similarly to (∃+)r1 and (∃+)r2 in order to build a branch repre− senting a small model: when the rule (∃+)r1 irs applied to a formula x : ∃r−.⊤, it introduces a new label y and the constraint y −→ x only when there is no other conr r straint u −→ v in S. Otherwise, since a constraint y −→ u has been already introduced r in that branch, 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 individuals via the role r, i.e. we need to detect a contradiction if both (i) and, for some r y, x −→ y belong to the same branch, in order to 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, r for some y, 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− The rules of TABPLiHte1cT are presented in Figure 3. The calculus TABPLiHte1cT is sound, complete and terminating.

!S, x : C, x : ¬C | U" (Clash) !S, x −r→ y, x : ¬∃r.⊤ | U& (Clash)r !S, y −r→ x, x : ¬∃r−.⊤ | U& (Clash)r− !S, x −r→ y | U$ !S!,Sx, −xr→:∃yr1.⊤| U|U$.$. .!S, x −r→ ym |(U∃+$)r1 !S, x −r→!Sy,1x| :U∃$r...⊤.!S|U,x$ −r→ ym | U$(∃+)r2 !S,!xS,:xC:, xT:(C!)¬|CU|"U("T+) if r(S) != ∅ if r(Sy) n=ew∅ if y1, . . . , ym are all the labels occurring in S if y1, . . . , ym are all the labels occurring in S !S, x : ¬T(C) | U" (T−) !S, x : ¬C | U" !S, x : ¬!¬C | U"

!S | U" (cut) !S, x : !¬C | U" !S, x : ¬!¬C | U" if x : ¬!¬C !∈ S and x : !¬C !∈ S x occuCrs∈inLST

!S | U, C ⊑ DL# (Unfold) !S, x : ¬C ⊔ D | U, C ⊑ DL,x$ if x occurs in S and x !∈ L

Theorem 11 (Soundness and completeness of TABPLiHte1cT). If KB 6|=DL-LitecTmin F , then the tableau for the constraint system corresponding to KB ∪ {¬F } contains an open saturated branch, which is satisfiable (via an injective assignment from labels to domain elements) in a minimal model of KB. Given a constraint system hS | U i, if it is unsatisfiable, then it has a closed tableau in TABPLiHte1cT.

Theorem 12 (Termination of TABPLiHte1cT). Any tableau generated by TABPLiHte1cT for hS | U i is finite.

Reasoning as we have done for TABEPLH⊥1T, we can show that: !S, x −r→ y, x : ¬∃r.⊤ | U | K& (Clash)r !S, y −r→ x, x : ¬∃r−.⊤ | U | K& (Clash)r− !S | U | ∅#(Clash)∅ !S,!xS,:xC:, xT(:C!)¬|CU||UK|"K" (T+)

Theorem 13 (Complexity of TABPLiHte1cT). Given a KB and a query F , the problem of checking whether KB ∪ {¬F } in TABPLiHte1cT is satisfiable is in NP.

5.2 The tableaux calculus TABPLiHte2cT

Let us now introduce the calculus TABPLiHte2cT. Exactly as for TABEPLH⊥2T, for each open saturated branch B built by TABPLiHte1cT, it verifies whether it represents a minimal model of the KB. The rules of TABPLiHte2cT are shown in Figure 4. The rules (∃+)r and (∃+)r− introduce x −r→ y and y −r→ x, respectively, where y ∈ D(B), instead of y being a new label.

Theorem 14 (Soundness and completeness of TABPLiHte2cT). Given a KB and a query F , let hS′ | U i be the corresponding constraint system of KB, and hS | U i the corresponding constraint system of KB ∪ {¬F }. An open saturated branch B built by TABPLiHte1cT for hS | U i is satisfiable by an injective mapping in a minimal model of KB iff the tableau in TABPLiHte2cT for hS′ | U | B − i is closed.

Theorem 15 (Termination of TABPLiHte2cT). Let hS′ | U | B − i be a constraint system starting from an open saturated branch B built by TABPLiHte1cT, then any tableau generated by TABPLiHte2cT is finite.

By reasoning exactly as done for TABEmLin⊥T, we prove that: Theorem 16 (Complexity of TABLmiitnecT). The problem of deciding whether KB |=LmTin F by means of TABLmiitnecT is in Π2p.

Conclusions We have proposed a nonmonotonic extension of low complexity DLs 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 nonmonotonic extensions of DLs have been proposed in the literature [ 15, 4, 2, 3, 7, 12, 10, 9, 6 ] 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 and proof methods for such a fragment extended with T and possibly the definition of a calculus for it.

References

1. F. Baader , S. Brandt , and C. Lutz . Pushing the E L envelope . In IJCAI , pages 364 - 369 , 2005 .

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

3. P. Bonatti , M. Faella , and L. Sauro . Defeasible inclusions in low-complexity dls: Preliminary notes . In IJCAI , pages 696 - 701 , 2009 .

4. P. A. Bonatti , C. Lutz , and F. Wolter . DLs with circumscription . In KR , p. 400 - 410 , 2006 .

5. D. Calvanese , G. De Giacomo, D. Lembo , M. Lenzerini , and R. Rosati . Tractable Reasoning and Efficient Query Answering in DLs: The DL-Lite Family . JAR, 39 ( 3 ): 385429 , 2007 .

6. G. Casini and U. Straccia . Rational closure for defeasible DLs . In JELIA, p. 77 - 90 , 2010 .

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

8. L. Giordano , V. Gliozzi , N. Olivetti , and G. L. Pozzato . A tableau calculus for a nonmonotonic extension of E L⊥ . In TABLEAUX , pages 164 - 179 , 2011 .

9. L. Giordano , V. Gliozzi , N. Olivetti , and G. L. Pozzato . Reasoning About Typicality in Preferential Description Logics . In JELIA , pages 192 - 205 , 2008 .

10. L. Giordano , V. Gliozzi , N. Olivetti , and G. L. Pozzato . Prototypical reasoning with low complexity Description Logics: Preliminary results . In LPNMR , pages 430 - 436 , 2009 .

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

12. L. Giordano , V. Gliozzi , N. Olivetti , and G.L. Pozzato . ALC+ Tmin: a preferential extension of description logics . Fundamenta Informaticae , 96 : 1 - 32 , 2009 .

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

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

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