=Paper=
{{Paper
|id=None
|storemode=property
|title=Preferential Low Complexity Description Logics: Complexity Results and Proof Methods
|pdfUrl=https://ceur-ws.org/Vol-846/paper_11.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/GiordanoGOP12
}}
==Preferential Low Complexity Description Logics: Complexity Results and Proof Methods==
<pdf width="1500px">https://ceur-ws.org/Vol-846/paper_11.pdf</pdf>
<pre>
          Preferential Low Complexity Description Logics:
               Complexity Results and Proof Methods

   Laura Giordano1, Valentina Gliozzi2 , Nicola Olivetti3 , and Gian Luca Pozzato2
  1
    Dip. di Informatica - U. Piemonte O. - Alessandria - Italy - laura@mfn.unipmn.it
      2
      Dip. Informatica - Univ. di Torino - Italy {gliozzi,pozzato}@di.unito.it
3
  LSIS-UMR CNRS 6168 - Marseille - France - nicola.olivetti@univ-cezanne.fr
      Abstract. In this paper we describe an approach for reasoning about typical-
      ity and defeasible properties in low complexity preferential Description Logics.
      We describe the non-monotonic extension of the low complexity DLs EL⊥ and
      DL-Litecore based on a typicality operator T, which enjoys a preferential seman-
      tics. We summarize complexity results for such extensions, called EL⊥ Tmin and
      DL-Litec Tmin . Entailment in DL-Litec Tmin is in Π2p , whereas entailment in
      EL⊥ Tmin is E XP T IME -hard. However, for the Left Local fragment of EL⊥ Tmin
      the complexity of entailment drops to Π2p . We present tableau calculi for Left
      Local EL⊥ Tmin and for DL-Litec Tmin . The calculi perform a two-phase com-
      putation 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 complexi-
      ties match the above mentioned complexity results.

1 Introduction
Nonmonotonic extensions of Description Logics (DLs) have been actively investigated
since the early 90s [15, 4, 2, 3, 7, 12, 8, 6]. A simple but powerful non-monotonic exten-
sion of DLs is proposed in [12, 8]: 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 non-
monotonic 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 hav-
ing children normally do not: T(Student ) ⊑ ¬TaxPayer ; T(Student ⊓ Worker ) ⊑
TaxPayer ; T(Student ⊓ W orker ⊓ ∃HasChild .⊤) ⊑ ¬TaxPayer . Although the
operator T is non-monotonic in itself, the logic ALC + T is monotonic. As a con-
sequence, 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 proper-
ties of them (e.g. that john does not pay taxes). In [8], 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 stu-
dent, one can non-monotonically 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 non-monotonic DLs, adding the typicality operator with its min-
imal model semantics to a standard DL, such as ALC, leads to a very high com-
plexity (namely, query entailment in ALC + Tmin is in CO -N EXP NP [8]). This fact
has motivated the study of non-monotonic extensions of low complexity DLs such as
DL-Litecore [5] and EL⊥ of the EL 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 EL⊥ with the typicality operator based on the minimal model semantics introduced
in [8]. We summarize complexity upper bounds for the resulting logics EL⊥ Tmin and
DL-Litec Tmin given in [11]. For EL⊥ , it turns out that its extension EL⊥ Tmin is un-
fortunately E XP T IME-hard. This result is analogous to the one for circumscribed EL⊥
KBs [3]. However, the complexity decreases to Π2p for the fragment of Left Local EL⊥
KBs, corresponding to the homonymous fragment in [3]. The same complexity upper
bound is obtained for DL-Litec Tmin .
    We also describe the tableau calculi for DL-Litec Tmin as well as for the Left Local
fragment of EL⊥ 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 EL⊥Tmin
Before describing EL⊥ Tmin , let us briefly recall the underlying monotonic logic
     ⊥
EL+ T, 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).
                       ⊥
    Formally, the EL+ 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 EL+ T is defined by enriching ordinary models of EL⊥ by a prefer-
ence 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 con-
cept 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 C I ⊆ ∆, 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 = M in< (C I ).

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
C I ⊆ DI , and that M satisfies C(a) if aI ∈ C I 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 ∈ 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. The interpretation of  in M is as follows:
(C)I = {x ∈ ∆ | for every y ∈ ∆, if y < x then y ∈ C I }. 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 EL+ 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 EL+ 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 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.
     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 ∈ C I
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∆, <, Ii, we define:
                 −
            M                           I
             LT = {(x, ¬¬C) | x 6∈ (¬C) , 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′ w.r.t. LT , and we write M <LT M′ , if (i) ∆ = ∆′ , (ii) M   LT ⊂ MLT , (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 EL⊥ Tmin ). A query F is minimally entailed
in EL⊥ 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 EL+ 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 EL⊥ Tmin KBs (Theorem 3.1 in [11])). The problem of
deciding whether KB |=EL⊥ Tmin F is E XP T IME-hard.

To lower the complexity of minimal entailment in EL⊥ Tmin , we consider Left Local
KBs, a restriction similar to that introduced in [3] for circumscribed EL⊥ KBs.

Definition 5 (Left Local knowledge base). A Left Local KB only contains subsump-
tions 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 EL⊥ 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 EL⊥ 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-Litec Tmin . 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 EL⊥ 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 EL⊥ 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 prob-
lem of deciding whether KB |=DL-Litec Tmin F is in Π2p .


4 The Tableau Calculus for Left Local EL⊥Tmin
                                                       ⊥
                                                     EL T
In this section we present a tableau calculus TAB min     for deciding whether a query F
is minimally entailed from a Left Local knowledge base in the logic EL⊥ Tmin . It per-
                                                                                       EL⊥ T
forms a two-phase computation: in the first phase, a tableau calculus, called TAB P      H1 ,
simply verifies whether KB ∪ {¬F } is satisfiable in an EL⊥ T model, building candi-
                                                                               EL⊥ T
date models; in the second phase another tableau calculus, called TAB P         H2 , checks
whether the candidate models found in the first phase are minimal models of KB, i.e.
                                                 EL⊥ T
for each open branch of the first phase, TAB P    H2 tries to build a model of KB which
                                                                                        EL⊥ T
is preferred to the candidate model w.r.t. Definition 3. The whole procedure TAB min
is formally defined at the end of this section (Definition 7).
                       EL⊥ T
     The calculus TAB min     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 EL⊥ Tmin .
          EL⊥ T
     TABmin      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 EL⊥ Tmin or has the form ¬D or ¬¬D, where D is a concept.
                                                       EL⊥ T                        EL⊥ T
     Let us now analyze the two components of TAB min        , starting with TAB P    H1 .

                                          ⊥
                              EL T
4.1 The Tableaux Calculus TAB P H1
                      ⊥
                   EL T
A tableau of TAB P  H1 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 subsump-
tion 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 se-
quence of nodes hS1 | U1 | W1 i, hS2 | U2 | W2 i, . . . , hSn | Un | Wn i . . ., where each
node hSi | Ui | Wi i is obtained from its immediate predecessor hSi−1 | Ui−1 | Wi−1 i
                                 ⊥
                             EL T
by applying a rule of TAB P   H1 , having hSi−1 | Ui−1 | Wi−1 i as the premise and
hSi | Ui | Wi i 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
                               EL⊥ T                                    +           −
are closed. The rules of TAB P   H1 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 Sx→yM
                                                                     of (− ). The (cut)
                                                                                      ⊥
                                                                                 EL T
rule ensures that, given any concept C ∈ LT , an open branch built by TAB P        H1 con-
tains either  x : ¬C   or x  : ¬¬C     for each label x: this is needed  in order to allow
      EL⊥ T
TAB P   H2 to check the minimality of the model corresponding to the open branch. As
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 ap-
plied. This avoids multiple unfolding of the same subsumption with the same label.
                        EL⊥ T
    The calculus TAB P    H1 is different from the calculus ALC + Tmin [8] in two re-
spects. First, the rule (∃+ ) is split in the two rules (∃+ )1 and (∃+ )2 . When the rule
(∃+ )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 TAB ALC+T  min      [8]. We write S as an
                                                                                M
abbreviation for S, u : ¬¬C1 , . . . , u : ¬¬Cn . Moreover, we define Su→y         = {y :
                                                                                −k
¬D, y : ¬D | u : ¬D ∈ S} and, for k = 1, 2, . . . , n, we define S u→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 TAB ALC+T
                                                                     min       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 EL⊥ 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 ⊓ D) | U | W #                    !S, x : C ⊔ D | U | W #
                                (⊓+ )                                        (⊓− )                                    (⊔+ )
      !S, x : C, x : D | U | W "      !S, x : ¬C | U | W " !S, x : ¬D | U | W "    !S, x : C | U | W " !S, x : D | U | W "

                                                                                                                        L
          !S, x : T(C) | U | W "                  !S, x : ¬T(C) | U | W "                !S | U, C ⊑ D | W # (Unfold)
                                  (T+ )                                         (T− )
       !S, x : C, x : !¬C | U | W "     !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.C | U | W #
             R                                       R                                   R                       (∃+ )1
      !S, u −→ xC , xC : C | U | W ∪ {xC }% !S, u −→ y1 , y1 : C | U | W $ . . . !S, u −→ ym , ym : C | U | W $
                                                      if xC !∈ W and y1 , . . . , ym are all the labels occurring in S

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

                              R
           !S, x : ¬∃R.C, x −→ y | U | W %                                                   !S | U | W "
                         R
                                                (∃− )                                                                     (cut)
       !S, x : ¬∃R.C, x −→ y, y : ¬C | U | W %                               !S, x : ¬!¬C | U | W " !S, x : !¬C | U | W "
                                       if y : ¬C !∈ S                                         if x : ¬!¬C !∈ S and x : !¬C !∈ S
                                                                                               x occurs in S            C ∈ LT

                                      !S, u : ¬!¬C1 , u : ¬!¬C2 , . . . , u : ¬!¬Cn | U | W "
                                                                                                                                    (!− )
                                M       !−k
       !S, x : Ck , x : !¬Ck , Su→x , S u→x | U | W "
                                                           !−k                                                           !−k
                                                M
                     !S, y1 : Ck , y1 : !¬Ck , Su→y 1
                                                      , S u→y1 | U | W " . . . !S, ym : Ck , ym : !¬Ck , Su→yM
                                                                                                                  m
                                                                                                                    , S u→ym | U | W "
                                                                                                                                   x new
                                                           if y1 , . . . , ym are all the labels occurring in S, y1 != u, . . . , ym != u
                                                                                                                       k = 1, 2, . . . , n

                                                                                           ⊥
                                                                       EL T
                                              Fig. 1. The calculus TAB P H1 .



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 satisfi-
                                                                         EL⊥ T
able. In order to verify the satisfiability of KB ∪ {¬F }, we use TAB P    H1 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
                                                          EL⊥ T
of KB. To this purpose, the rules of the calculus TAB P    H1 are applied until either a
contradiction is generated (Clash) or a model satisfying hS | U | ∅i can be obtained
from the resulting constraint system.
                                    ⊥
                       EL T
    The rules of TAB P   H1 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
                                                                                  EL⊥ T
and complete and terminating. In particular, any tableau generated by TAB P        H1 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 }
         EL⊥ T
in TAB P   H1 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, C ⊑ DL | K#
      !S | U | ∅# (Clash)∅                !S, x : ¬!¬C | U | K" (Clash)!−                                              (Unfold)
                                                         if x : ¬!¬C !∈ K            !S, x : ¬C ⊔ D | U, C ⊑ DL,x | K$
                                                                                                           x ∈ D(B) and x !∈ L


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


                   !S, x : ¬T(C) | U | K"                                                    !S | U | K"
                                                         (T− )                                                              (cut)
       !S, x : ¬C | U | K"    !S, x : ¬!¬C | U | K"                        !S, x : !¬C | U | K"       !S, x : ¬!¬C | U | K"
                                                                                              if x : ¬!¬C !∈ S and x : !¬C !∈ S
                                                                                                              x ∈ D(B) C ∈ LT
                              !S, u : ∃R.C | U | K#
              R                                   R
                                                                           (∃+ )
       !S, u −→ y1 , y1 : C | U | K$ . . . !S, u −→ ym , ym : C | U | K$
                                                     if D(B) = {y1 , . . . , ym }

                        !S, u : ¬!¬C1 , . . . , u : ¬!¬Cn | U | K, u : ¬!¬C1 , . . . , u : ¬!¬Cn "
                                              !−k                                                       !−k             (!− )
                                  M                                                        M
       !S, y1 : Ck , y1 : !¬Ck , Su→y 1
                                        , S u→y1 | U | K" . . . !S, ym : Ck , ym : !¬Ck , Su→y m
                                                                                                 , S u→ym | U | K"
                                                                      if D(B) = {y1 , . . . , ym } and y1 != u, . . . , ym != u

                                                           ⊥
                                       EL T                                     +
              Fig. 2. The calculus TAB P H2 . To save space, we omit the rule (⊔ ).

                                                                 ⊥
                              EL T
4.2 The Tableaux Calculus TAB P H2
                                                                     ⊥
                                            EL T
Let us now introduce the calculus TABP        H2 which, for each open branch B built by
     EL⊥ T
TAB P H1 , verifies whether it represents a minimal model of the KB. Given an open
                                          EL⊥ T
branch B of a tableau built from TABP      H1 , let D(B) be the set of labels occurring on
                       −
B. Moreover, let B be the set of formulas x : ¬¬C occurring in B, that is to say
   −
B = {x : ¬¬C | x : ¬¬C occurs in B}.
                         EL⊥ T
    A tableau of TAB P     H2 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
                                                                      EL⊥ T
of the form x : ¬¬C, with C ∈ LT . The basic idea of TAB P             H2 is as follows.
                                               ⊥
                                            EL T
Given an open branch B built by TAB P         H1   and  corresponding to a model MB of
                         ⊥
                      EL T                       B
KB ∪ {¬F }, TAB P       H2 checks whether M 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
                                                                                     EL⊥ T
a model of KB containing less negated box formulas. The tableau built by TAB P        H2
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,
     EL⊥ T
TAB P  H2 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
                                                    EL⊥ T
new ones in their conclusions. The rules of TAB P      H2 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
                                                                       EL⊥ T
hS, x : ¬¬C | U | Ki, and x : ¬¬C 6∈ K, then TAB P                     H2 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.
                         EL⊥ T
    The calculus TAB P    H2 also contains the clash condition (Clash)∅ . Since each ap-
plication 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
                                                  EL⊥ T
branch. In this case, the model built by TAB P     H2 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
                                            EL⊥ T
constraint corresponding to ¬F . TAB P        H2 is sound and complete in the following
                                           EL⊥ T
sense: an open branch B built by TABP H1 for hS ′ | U | ∅i is satisfiable in a minimal
                                       EL⊥ T                  −
model of KB iff the tableau in TAB P     H2 for hS | U | B       i is closed.
                                             ⊥
                                          EL T
    Termination of the calculus TAB P H2 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
                                                           EL⊥ T
branch B represents a minimal model for KB in TABP          H2 is in NP in the size of B.
    The overall procedure TAB ALC+T
                                  min       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
                                                            EL⊥ T
S the constraint corresponding to ¬F . The calculus TAB min        checks whether a query
F is minimally entailed from KB by means of the following procedure: (phase 1) the
                EL⊥ T                 ′                                            EL⊥ T
calculus TAB P   H1 is applied to hS | U | ∅i; if, for each branch B built by TAB P H1 ,
                                                                                EL⊥ T
either (i) B is closed or (ii) (phase 2) the tableau built by the calculus TAB P H2 for
              −                      LT                        LT
            
hS | U | B i is open, then KB |=min F , otherwise KB 6|=min F .
                                        ⊥
                                   EL T
In [9] it has been shown that TABmin     is a sound and complete decision procedure
for verifying if KB |=EL⊥ Tmin F . Furthermore, the problem of deciding whether KB
                                    ⊥
                             EL T
|=EL⊥ Tmin F by means of TAB min  is in Π2p .


5 A Tableau Calculus for DL-Litec Tmin
In this section we shortly describe a tableau calculus TABLite
                                                             min
                                                                 cT
                                                                    for deciding query
entailment in the logic DL-Litec Tmin . The calculus is similar to the one introduced
for EL⊥ 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 −→ y | x −→ y ∈ S}. The calculus TAB Lite
               r         r                                    cT
                                                          P H1   used in the first phase
                     ⊥
                   EL T
differs from TABP   H1  in the following points:
                                                          ⊥
                              EL T                      +
    1. As in the calculus TAB P H1 , the split of the (∃ ) in the two rules:
                       !S, x : ∃r.⊤ | U $                                                          !S, x : ∃r.⊤ | U $
                                                       r
                                                                   (∃+ )r1                                                         (∃+ )r2
                      !S, x −→ y1 | U $ . . . !S, x −→ ym | U $
         r                         r                                                                                    r
  !S, x −→ y | U $                                                                          r
                                                                                    !S, x −→ y1 | U $ . . . !S, x −→ ym | U $
                                                            if r(S) = ∅                                                      if r(S) != ∅
                                                                  y new
                  if y1 , . . . , ym are all the labels occurring in 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-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
                                                                                    r
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 for-
mulas are introduced:
                  !S, x : ∃r− .⊤ | U $                                                               !S, x : ∃r− .⊤ | U $
                                                                (∃+ )r1
                                                                       −
                                                                                                                                   (∃+ )r2
                                                                                                                                          −

         r                     r                       r
  !S, y −→ x | U $ !S, y1 −→ x | U $ . . . !S, ym −→ x | U $                                    r                         r
                                                                                    !S, y1 −→ x | U $ . . . !S, ym −→ x | U $
                                                           if r(S) = ∅                                                       if r(S) != ∅
                                                                 y new              if y1 , . . . , ym are all the labels occurring in 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 individ-
                                                                               r
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 TAB Lite
                                         P H1
                                              cT
                                                 in order to detect such a situation. Anal-
ogously, (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:
                                                                                                      r
         r
  !S, x −→ y, x : ¬∃r.⊤ | U & (Clash)r                                                          !S, y −→ x, x : ¬∃r− .⊤ | U & (Clash)r−



Apart from the differences above, the rules of TAB Lite
                                                    P H1
                                                        cT
                                                           are the same as those of
     EL⊥ T                                Lite T
TAB P H1 . Similarly for the calculus TAB P H2c used in the second phase. In [10] it
has been shown that both TAB Litec T and TAB Litec T are sound, complete and termi-
                                                        P H1                 P H2
nating. Furthermore, the problem of deciding whether KB |=DL-Litec Tmin F by means
of TAB Litec T is in Π p .
             min                      2
6 Conclusions
We have proposed a non-monotonic extension of low complexity Description Log-
ics EL⊥ 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 E XP T IME-hard for EL⊥ Tmin , whereas it drops to Π2p when con-
sidering the Left Local Fragment of EL⊥ 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 EL⊥ 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 non-
monotonic extensions of low complexity DLs, the complexity of circumscribed frag-
ments of the EL⊥ and DL-Lite families have been studied in [3]. Recently, a fragment
of EL⊥ for which the complexity of circumscribed KBs is polynomial has been identi-
fied 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 EL 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. Reason-
    ing (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 prefer-
    ential 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 EL⊥ . 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 com-
    plexity DLs: the logics EL⊥ Tmin and DL-litec Tmin . 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.: EL 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)

</pre>