=Paper=
{{Paper
|id=Vol-477/paper-27
|storemode=property
|title=Reasoning About Typicality in ALC and EL
|pdfUrl=https://ceur-ws.org/Vol-477/paper_15.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/GiordanoGOP09
}}
==Reasoning About Typicality in ALC and EL==
<pdf width="1500px">https://ceur-ws.org/Vol-477/paper_15.pdf</pdf>
<pre>
     Reasoning About Typicality in ALC and EL

Laura Giordano1, Valentina Gliozzi2 , Nicola Olivetti3 , and Gian Luca Pozzato2
1
    Dipartimento di Informatica - Università del Piemonte Orientale “A. Avogadro” -
                                laura@mfn.unipmn.it
           2
             Dipartimento di Informatica - Università edgli Studi di Torino -
                          {gliozzi,pozzato}@di.unito.it
       3
         LSIS-UMR CNRS 6168 Universitè “Paul Cézanne” - Aix-Marseille 3 -
                         nicola.olivetti@univ-cezanne.fr

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


1     Introduction
Description logics (DLs) represent one of the most important formalisms of
knowledge representation. A DL knowledge base (KB) comprises a TBox, con-
taining the definition of concepts (and possibly roles), and a specification of
inclusions relations among them, and an ABox containing instances of concepts
and roles. Since the very objective of the TBox is to build a taxonomy of con-
cepts, the need of representing prototypical properties and of reasoning about
defeasible inheritance of such properties naturally arises.
    Several approaches to handle prototypical reasoning and inheritance with
exceptions in DL have been proposed in the literature, all of them are based
on the integration of DLs with some nonmonotonic reasoning mechanism: either
default logic (see [4, 19, 5]), or autoepistemic logic (see [9, 15] for some recents
developmentes) and circumscription (see [7] and [6]). In particular, [6] analyzes
the complexity of reasoning with circumscribed low complexity description log-
ics, such as DL-lite and the EL family. While reasoning with circumscribed ALC
knowledge bases is NExpNP -hard [7], in circumscribed DL-liteR complexity
drops to the second level of the polynomial hierarchy. In [6] is also shown that
in EL reasoning over circumscribed knowledge bases remain ExpTime-hard in
general. However, by limiting occurrences of existential restrictions, complexity
drops to the second level of the polynomial hierarchy.
    In this paper, we present an overview of our approach to reasoning about
typicality in DLs, which is based on the idea of introducing in the language a
typicality operator T. First, we present the monotonic logic ALC + T, obtained
by adding the operator T to ALC. Then we introduce a minimal model seman-
tics for it, which allows typical instances of concepts to be maximized. Finally,
                           ⊥                                        ⊥
we present the logic EL+ T, obtained by extending the logic EL+ with T. We
analyze and compare the complexity of these logics.
    The intended meaning of the operator T, for any concept C, is that T(C)
singles out the instances of C that are considered as “typical” or “normal”.
Thus assertions as “normally students do not pay taxes” are represented by
T(Student) ⊑ ¬TaxPayer . The operator T is characterised by a set of pos-
tulates that are essentially a reformulation of KLM [16] axioms of preferential
logic P, namely the assertion T(C) ⊑ P is equivalent to the conditional asser-
tion C |∼ P of P. It turns out that the semantics of the typicality operator can
be equivalently specified by a suitable modal logic.
    The idea underlying the modal interpretation is that there is a global prefer-
ence relation (a strict partial order) < on individuals, so that typical instances
of a concept C can be defined as the instances of C that are minimal with
respect to <. In this modal logic, < works as an accessibility relation R with
R(x, y) ≡ y < x, so that we can define T(C) as C ⊓¬C. The preference relation
< does not have infinite descending chains as we adopt the so-called Smooth-
ness condition or Limit Assumption of conditional logics. As a consequence, the
corresponding modal operator  has the same properties as in Gödel-Löb modal
logic G of arithmetic provability.
    In this setting, we assume that a KB comprises, in addition to the standard
TBox and ABox, a set of assertions of the type T(C) ⊑ D where D is a concept
not mentioning T. For instance, let the KB contain:

    T(Student) ⊑ ¬TaxPayer
    T(Student ⊓ Worker ) ⊑ TaxPayer
    T(Student ⊓ W orker ⊓ ∃HasChild .⊤) ⊑ ¬TaxPayer

corresponding to the assertions: normally a student does not pay taxes, nor-
mally a working student pays taxes, but normally a working student having
children does not pay taxes. Suppose further that the ABox contains alter-
natively the following facts about john: 1. Student(john); 2. Student(john),
Worker (john); 3. Student(john), Worker (john), ∃HasChild .⊤(john). We would
like to infer the expected (defeasible) conclusion about john in each case: 1.
¬TaxPayer (john), 2. TaxPayer (john), 3. ¬TaxPayer (john). Furthermore, we
would like to infer (defeasible) properties also of individuals implicitly intro-
duced by existential restrictions, for instance, if the ABox further contains
∃HasChild .(Student ⊓ Worker )(jack ) it should derive (defeasibly) the “right”
conclusion ∃HasChild .TaxPayer (jack ) in the latter. Finally, adding irrelevant
information should not affect the conclusions. Given the KB as above, one
should be able to infer as well T(Student ⊓ SportLover ) ⊑ ¬TaxPayer and
T(Student ⊓ Worker ⊓ SportLover ) ⊑ TaxPayer , as SportLover is irrelevant
with respect to being a TaxPayer or not. For the same reason, the conclu-
sion about john being a TaxPayer or not should not be influenced by adding
SportLover (john) to the ABox.
    The monotonic logic ALC + T allows some weak forms of inference through
cautious monotonicity. For instance, if typical students are young, from the KB
above we can derive that typical young students do not pay taxes. Inference in
ALC + T is in ExpTime. However, ALC + T is not sufficient to perform the
kind of defeasible reasoning illustrated above. Concerning the example, we get
for instance that: KB ∪ {Student(john), Worker (john)} 6|= TaxPayer (john);
KB 6|= T(Student ⊓ SportLover ) ⊑ ¬TaxPayer . In order to derive the conclusion
about john we should know (or assume) that john is a typical working student,
but we do not dispose of this information. Similarly, in order to derive that also
a typical student who loves sport does not have to pay taxes, we must be able
to infer or assume that a “typical student loving sport” is also a “typical stu-
dent”, since there is no reason why it should not be the case; this cannot be
derived by the logic itself given the nonmonotonic nature of T. The basic mono-
tonic logic ALC + T is then too weak to enforce these extra assumptions. In
order to perform defeasible inferences, we strenghten the semantics of ALC + T
by proposing a minimal model semantics. Intuitively, the idea is to restrict our
consideration to models that maximise typical instances of a concept. In order
to define the preference relation on models we take advantage of the modal se-
mantics of ALC + T: the preference relation on models (with the same domain)
is defined by comparing, for each individual, the set of modal (or more pre-
cisely -ed) concepts containing the individual in the two models. Similarly to
circumscription, where we must specify a set of minimised predicates, here we
must specify a set of concepts LT of which we want to maximise the set of typical
instances (it may just be the set of all concepts occurring in the knowledge base).
We call the new logic ALC + Tmin and we denote by |=L     min semantic entailment
                                                             T


determined by minimal models. Taking the KB of the examples above we obtain,
for instance, KB ∪ {Student(john), Worker (john)} |=L    min TaxPayer (john); KB
                                                           T

                                               LT
∪ {∃HasChild .(Student ⊓ Worker )(jack)} |=min ∃HasChild .TaxPayer (jack ) and
KB |=L min T(Student ⊓SportLover ) ⊑ ¬TaxPayer . As the second example shows,
        T


we are able to infer the intended conclusion also for the implicit individuals. In
[11] we have provided a decision procedure for checking satisfiability and validity
in ALC + Tmin . Our procedure, not presented here, can be used to determine
constructively an upper bound of the complexity of ALC + Tmin . Namely we
obtain that checking query entailment for ALC + Tmin is in co-NExpNP .
                                                       ⊥
    Finally, we introduce an extension of the logic EL+ with typicality. The log-
ics of the EL family allow for conjunction (⊓) and existential restriction (∃R.C).
Despite their relatively low expressivity, a renewed interest has recently emerged
for these logics. Indeed, it has been shown that EL has better algorithmic prop-
erties than F L0 , which allows for conjunction and value restriction (∀R.C). [1, 8]
show that reasoning in EL and several of its extensions remains tractable (i.e.,
polynomial-time decidable) in the presence of the TBox, and even of general
concept inclusions (GCIs). Furthermore, it has turned out that the logics of the
EL family are relevant for several applications, in particular in the bio-medical
domain; for instance, medical terminologies, such as the Galen Medical Knowl-
edge Base (GALEN, [17]), the Systemized Nomenclature of Medicine (SNOMED
[18]), and the Gene Ontology [20] used in bioinformatics, can be formalized in
small extensions of EL.                                                    ⊥
    We present some preliminary results about the complexity of EL+ T. In
                                            ⊥
particular, we show that a consistent EL+ T knowledge base has a small model
whose size is polynomial in the size of the knowledge base. In the paper, we
sketch the construction of the model. We show that, as a consequence of this
                                                    ⊥
result, the problem of deciding entailment in EL+ T is in co-NP.


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

Definition 1 (Semantics of T with selection function). A model is any
structure h∆, I, fT i, where: ∆ is the domain; I is the extension function that
maps each extended concept C to C I ⊆ ∆, and each role r to a rI ⊆ ∆I × ∆I .
I is defined in the usual way (as for ALC) and, in addition, (T(C))I = fT (C I ).
fT : P ow(∆) → P ow(∆) is a function satisfying the following properties:
(fT − 1) fT (S) ⊆ S                              (fT − 2) if S "= ∅, then also fT (S) "= ∅
                                                                       !        !
(fT − 3) if fT (S) ⊆ R, then fT (S) = fT (S ∩ R)        (fT − 4) fT ( Si ) ⊆       fT (Si )
          !                 "
(fT − 5)     fT (Si ) ⊆ fT ( Si )

Intuitively, given the extension of some concept C, fT selects the typical instances
of C. (fT − 1) requests that typical elements of S belong to S. (fT − 2) requests
that if there are elements in S, then there are also typical such elements. The next
properties constraint the behavior of fT wrt ∩ and ∪ in such a way that they do
not entail monotonicity. According to (fT − 3), if the typical elements of S are in
R, then they coincide with the typical elements of S ∩ R, thus expressing a weak
form of monotonicity (namely cautious    S monotonicity).
                                                  S        (fT − 4) corresponds to
one direction of the equivalence fT ( Si ) = fT (Si ), the one that does      T not
entail
T       monotonicity.   Similar  considerations
                                        T       apply toT the equation   f T (  Si ) =
   fT (Si ), of which only the inclusion fT (Si ) ⊆ fT ( Si ) is derivable. (fT −5) is
a further constraint on the behavior of fT wrt arbitrary unions and intersections;
it would be derivable if fT were monotonic.
    We can give an alternative semantics for T based on a preference relation.
The idea is that there is a global preference relation among individuals and that
the typical members of a concept C, i.e. selected by fT (C I ), are the minimal
elements of C wrt this preference relation. Observe that this notion is global,
that is to say, it does not compare individuals wrt a specific concept (something
like y is more typical than x wrt concept C). In this framework, an object x ∈ ∆
is a typical instance of some concept C, if x ∈ C I and there is no C-element in
∆ more typical than x. The typicality preference relation is partial since it is not
always possible to establish which object is more typical than which other. The
following definition is needed:
Definition 2. Given a relation <, which is a strict partial order (i.e. an ir-
reflexive and transitive relation) over a domain ∆, for all S ⊆ ∆, we define
M in< (S) = {x : x ∈ S and ∄y ∈ S s.t. y < x}. We say that < satisfies the
Smoothness Condition iff for all S ⊆ ∆, for all x ∈ S, either x ∈ M in< (S) or
∃y ∈ M in< (S) such that y < x.
In [10] it is shown that given a model with a selection function, it is possible
to define on the same domain a preference relation < such that, for all S ⊆ ∆,
fT (S) = M in< (S). Formally, given any model h∆, I, fT i, fT satisfies postulates
(fT − 1) to (fT − 5) above if and only if it is possible to define on ∆ a strict
partial order <, satisfying the Smoothness Condition, such that for all S ⊆ ∆,
fT (S) = M in< (S). By this result, we can refer to the following semantics for
ALC + T:
Definition 3 (Semantics of ALC +T). A model M is any structure h∆, <, Ii,
where ∆ and I are defined as in Definition 1, and < is a strict partial order over
∆ satisfying the Smoothness Condition (see Definition 2 above). As a difference
wrt Definition 1, the semantics of the T operator is: (T(C))I = M in< (C I ). For
concepts (built from operators of ALC), C I is defined in the usual way.
We introduce the following definition:
Definition 4 (Model satisfying a Knowledge Base). Consider a model M,
as defined in Definition 3. We extend I so that it assigns to each individual a of
O an element aI of the domain ∆. Given a KB (TBox,ABox), we say that:
 – M satisfies TBox if for all inclusions C ⊑ D in TBox, and all elements
    x ∈ ∆, if x ∈ C I then x ∈ DI .
 – M satisfies ABox if: (i) for all C(a) in ABox, we have that aI ∈ C I , (ii)
    for all r(a, b) in ABox, we have that (aI , bI ) ∈ rI .
M satisfies a knowledge base if it satisfies both its TBox and its ABox.

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

Theorem 1 (Complexity of ALC + T). Given an ALC + T-knowledge base
(TBox,ABox), the problem of checking whether it is satisfiable can be solved in
exponential time.


3    The logic ALC + Tmin
The logic ALC + T allows one to reason about typicality. As a difference with
respect to standard ALC, in ALC + T we can consistently express, for instance,
the fact that three different concepts, as student, working student and work-
ing student with children, have a different status as taxpayers. As we have seen
in the introduction, this can be consistently expressed by including in a knowl-
edge base the three formulas: T(Student) ⊑ ¬TaxPayer ; T(Student ⊓Worker ) ⊑
TaxPayer ; T(Student ⊓Worker ⊓∃HasChild .⊤) ⊑ ¬TaxPayer . Assume that john
is an instance of the concept Student ⊓Worker ⊓∃HasChild .⊤. What can we con-
clude about john? If the ABox contains the assertion (∗) T(Student ⊓ Worker ⊓
∃HasChild .⊤)(john), then, in ALC +T, we can conclude that ¬TaxPayer (john).
However, in the absence of (*), we cannot derive ¬TaxPayer (john).
    We would like to infer that individuals are typical instances of the concepts
they belong to, if consistent with the KB. In order to maximize the typicality of
instances, we define a preference relation on models, and we introduce a semantic
entailment determined by minimal models. Informally, we prefer a model M to
a model N if M contains more typical instances of concepts than N .
    Given a KB, we consider a finite set LT of concepts occurring in the KB, the
typicality of whose instances we want to maximize. The maximization of the set
of typical instances will apply to individuals explicitly occurring in the ABox as
well as to implicit individuals. We assume that the set LT contains at least all
concepts C such that T(C) occurs in the KB.
    We have seen that a is a typical instance of a concept C (a ∈ (T(C))I )
when it is an instance of C and there is not another instance of C preferred to
a, i.e. a ∈ (C ⊓ ¬C)I . In the following, in order to maximize the typicality
of the instances of C, we minimize the instances of ¬¬C. Notice that this is
different from maximising the instances of T(C). We have adopted this solution
since it allows to maximise the set of typical instances of C without affecting
the extension of C (whereas maximising the extension of T(C) would imply
maximising also the extension of C).
                         −
    We define the set MLT of negated boxed formulas holding in a model, relative
                                                              −
to the concepts in LT . Given a model M = h∆, <, Ii, let M  LT = {(a, ¬¬C) |
a ∈ (¬¬C)I , with a ∈ ∆, C ∈ LT }.

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

A query α is either a formula of the form C(a) or a subsumption relation C ⊑ D.

Definition 6 (Minimal Entailment in ALC+Tmin ). A query α is minimally
entailed from a knowledge base KB with respect to LT if α holds in all models
of KB minimal with respect to LT . We write KB |=Lmin α.
                                                   T



While the original ALC+T is monotonic (see [10]), ALC+Tmin is nonmonotonic.
   In [11] we have defined a tableaux calculus for ALC + Tmin and we have
proved that:

Theorem 2 (Complexity of ALC + Tmin ). The problem of deciding whether
KB |=L                  NP .
     min α is in co-NExp
      T




                         ⊥
4    The logic EL+ T
                                                   ⊥
Let us now consider the case of the logic EL+ , namely we apply the above
                                            ⊥             ⊥
semantics to describe an extension EL+ T of EL+ with the T operator. In
    ⊥
EL+ T, concepts are restricted only to the cases of A ∈ C, ⊤, ⊥, C ⊓ D, and
                                           ⊥
∃r.C, where C, D are concepts of EL+ T and r ∈ R. Concerning extended
                                                                                  ⊥
concepts, if C is a concept, then C and T(C) are extended concepts of EL+ T.
A knowledge base is a pair (TBox,ABox). TBox contains (i) a finite set of GCIs
C ⊑ D, where C is an extended concept (either C ′ or T(C ′ )), and D is a concept,
and (ii) a finite set of role inclusions (RIs) r1 ◦ r2 ◦ · · · ◦ rn ⊑ r. ABox contains
expressions of the form C(a) and r(a, b) where C is an extended concept, r ∈ R,
and a, b ∈ O.
                        ⊥
    Notice that an EL+ T TBox can formalize transitive roles, role hierarchies,
as well as the so-called right identities on roles (r ◦ s ⊑ s); these constructs are
very useful to formalize medical ontologies.
    We can show that, given a model M = h∆, <, Ii of a KB, we can build a
small model of KB whose size is polynomial in the size of the KB. As we will
                                                                      ⊥
see, this will provide a complexity upper bound for the logic EL+ T.
    First of all, we must introduce an appropriate normal form for KBs, in par-
ticular for TBoxes. Given a KB=(TBox,ABox), we say that it is normal if:
 – all the inclusion relations in TBox have one of the following forms: C1 ⊑ D;
   C1 ⊓ C2 ⊑ D; C1 ⊑ ∃r.C2 ; ∃r.C1 ⊑ D; T(C1 ) ⊑ C2 ; T(C1 ⊓ C2 ) ⊑ D;
   T(C1 ) ⊑ ∃r.C2 ; T(∃r.C1 ) ⊑ D, where C1 , C2 ∈ C ∪ {⊤} and D ∈ C ∪ {⊥};
 – all role inclusions in TBox are of the form r ⊑ s or r1 ◦ r2 ⊑ s.
By extending the results presented in [2], we can show that any KB can be turned
into a normalized KB’ that is a conservative extension of KB, that is to say every
model satisfying KB’ is also a model of KB, whereas every model of KB can be
extended to a model of KB’ by appropriately choosing the interpretations of the
additional concept and role names introduced by the normalization procedure.
Furthermore, it can be shown that the size of KB’ is linear in the size of KB,
and that the normalization procedure can be done in linear time. Without loss
of generality, from now on we only refer to normalized KBs. Starting from a
normalized KB, we can now prove the following theorem:
                                                                                ⊥
Theorem 3 (Small model theorem). Let KB=(TBox,ABox) be an EL+ T
knowledge base. For all models M = h∆, <, Ii of KB and all x ∈ ∆, there exists
                                                                                ⊥
a model N = h∆◦ , <◦ , I ◦ i of KB such that (i) x ∈ ∆◦ , (ii) for all EL+ T
                               ◦
concepts C, x ∈ C I iff x ∈ C I , and (iii) | ∆◦ | is polynomial in the size of KB.
We sketch the proof through the following steps. In the first step, we build a
model M′ by means of the following algorithm. Intuitively, we keep only those
worlds needed to retain the values of formulas in x. Roughly speaking, we reuse
the same domain element to make true existential formulas in different domain
elements. For technical reasons, we need to add new elements to the domain
of the constructed model, in order to keep the same evaluation of existential
formulas as in the initial model. For each concept C ∈ C and for each role r ∈ R
we let S(C) and R(r) be the mappings computed by the algorithm defined in
[3] to compute subsumption in EL by means of completion rules. As usual, for
a given individual a occurring in ABox, we write aI to denote the element of ∆
corresponding to the extension of a in M. In the algorithm, we make use of three
sets of elements: ∆0 will be part of the domain of the model being constructed,
and it contains a portion of the domain ∆ of the initial model. All the elements
introduced in the domain must be processed in order to satisfy the existential
formulas. Unres is used to keep track of the elements not yet processed. Finally,
∆1 is a set of elements that will belong to the domain of the constructed model.
Each element of ∆1 is created for one atomic concept C, and is used to satisfy
all existential formulas ∃r.C throughout the whole model.
   1. ∆0 := {x} ∪ {aI ∈ ∆ | a occurs in the ABox }
   2. Unres:={x} ∪ {aI ∈ ∆ | a occurs in the ABox }
   3. ∆1 :=∅
   4. while Unres 6= ∅ do
   5.        extract one y from Unres
   6.        for each ∃r.C occurring in KB s.t. y ∈ (∃r.C)I do
   7.            if ∄wC ∈ ∆1 then
   8.                choose w ∈ ∆ s.t. (y, w) ∈ rI and w ∈ C I
   9.                ∆0 := ∆0 ∪ {w}
   10.                Unres:=Unres ∪ {w}
   11.                ∆1 := ∆1 ∪ {wC }, where wC is a new world
   12.                add w <′ wC
                                         ′
   13.                add (y, wC ) to rI
   14.             else
                                         ′
   15.                add (y, wC ) to rI
   16.        for each yi ∈ ∆ such that yi < y do
   17.             ∆0 := ∆0 ∪ {yi }
   18.             Unres:=Unres ∪{yi }
   19. for each wC , wD ∈ ∆1 with C 6= D do
                                                         ′
   20.        if (C, D) ∈ R(r) then add (wC , wD ) to rI

The model M′ = h∆′ , <′ , I ′ i is defined as follows:

 – ∆′ = ∆0 ∪ ∆1
 – we extend <′ computed by the algorithm by adding u <′ v if u < v, for each
   u, v ∈ ∆′ ;
 – the extension function I ′ is defined as follows:
     • for all atomic concepts C ∈ C, for all worlds in ∆′ , we define:
                                             ′
          ∗ for each u ∈ ∆0 , we let u ∈ C I if u ∈ C I ;
                                                 ′
          ∗ for each wD ∈ ∆1 , we let wD ∈ C I if C ∈ S(D).
                                      ′
     • for all roles r, we extend rI constructed by the algorithm by means of
        the following role closure rules:
                                                           ′                      ′
          ∗ for all inclusions r ⊑ s ∈ TBox, if (u, v) ∈ rI then add (u, v) to sI ;
                                                                  ′                 ′
          ∗ for all inclusions r1 ◦ r2 ⊑ s ∈ TBox, if (u, v) ∈ r1I and (v, w) ∈ r2I
                                   ′
            then add (u, w) to sI .
         ′
     • I is extended so that it assigns aI to each individual a in the ABox.

It can be shown that M′ is a model of KB. M′ is not guaranteed to have
polynomial size in the KB because in line 17 we add an element yi for each
yi < y, then the size of ∆0 may be arbitrarily large. For this reason, we refine our
construction in order to build a multi-linear model, that we will be able to further
refine in order to obtain a model of polynomial size. First of all, we introduce
the notion of multi-linear model of a KB. Given a model M = h∆, <, Ii, we
say that it is multi-linear if the following properties hold for every u, v, z ∈ ∆:
(i) if u < z and v < z and u 6= v, then u < v or v < u; (ii) if z < u and
z < v and u 6= v, then u < v or v < u. The construction of a multi-linear
model is similar to the one presented in [12] and it requires two steps. In the
first step, we replicate some domain elements, namely those belonging to more
than one descending chain of <′ . In the second step, we build a multi-linear
                              ′′
model M∗ = h∆′′ , <∗ , I i. Details can be found in [14]. The proof is ended by
constructing a model N = h∆◦ , <◦ , I ◦ i whose domain has polynomial size in the
size of KB. Let the size of the initial KB be n. We know that M∗ contains a
polynomial number of linear chains of domain elements related by <∗ , each one
starting from a domain elements in ∆1 (built by the algorithm above) or from
one domain element in {x, a1 , . . . , ak }, where a1 , . . . , ak are the domain elements
corresponding to the individuals in the ABox. We know that there are O(n)
                                                                                        ⊥
chains, as ∆1 contains one domain element for each atomic concept in EL+
and the domain elements a1 , . . . , ak are O(n). However, we have no bound on
the length of the chains.
    We want to show that the linear chains in the model can be reduced to finite
chains of polynomial length in the size of the KB. To this purpose, given M∗ ,
we build a new multi-linear model N = h∆◦ , <◦ , I ◦ i whose descending chains
have polynomial length.
    Let us consider a chain w0 , w1 , w2 , . . . in the model M∗ , with w0 in ∆1 or w0
in {x, a1 , . . . , ak }. Starting from w1 , we consider each element wi in the chain
and compare it with its predecessor wi−1 : we remove from the chain wi if wi
is an instance of exactly the same negated box formulas ¬¬C1 , . . . , ¬¬Ch as
its predecessor wi−1 . After processing an element of the chain, we consider the
next one. We keep on removing domain elements from the chain until, for each
element w of the chain, there is at least a box formula ¬C of which w is an
instance, while the domain element preceding w in the chain is not an instance
of ¬C. As there is only a finite polynomial number of such box formulas, we
can only retain a finite polynomial number of worlds in the chain.
    The same transformation is applied to all the O(n) chains in the model M∗ .
The resulting model N = h∆◦ , <◦ , I ◦ i is defined as follows: ∆◦ is the set of
all the domain elements in ∆∗ which have not been removed during the chain
transformation process; the relation <◦ is defined so that, for all x, y ∈ ∆∗ ,
x <◦ y if and only if x <∗ y; the interpretation of atomic formulas in the domain
elements is left unchanged.
    It can be shown that N is a multi-linear model of the KB and that the
valuation in x is the same in N and in M∗ . By construction, the descending
chains in N are of polynomial length.
    Given the small model theorem above, we can conclude that, when evaluating
the entailment, we can restrict our consideration to small models, namely, to
polynomial multi-linear models of the KB. As usual, we write KB |= α to say
that a query α holds in all the models of the KB. We write KB |=s α to say that
α holds in all polynomial multi-linear models of the KB.

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

Proof. From left to right, the statement is obvious. From right to left: using
contraposition, we prove that if KB 6|=s α then KB 6|= α. Let M = h∆, <, Ii be
a model of KB falsifying α, that is, x 6∈ αI , for some domain element x ∈ ∆.
By Theorem 3 above, we can construct a polynomial multi-linear model N =
                                                         ⊥
h∆◦ , <◦ , I ◦ i of KB, such that x ∈ ∆◦ and, for all EL+ T concepts C, x ∈ C I iff
       I◦                 I◦
x ∈ C . Hence, x ∈ α .

Given the result above, we can prove an upper bound on the complexity of
                 ⊥
entailment in EL+ T.
                                                   ⊥
Theorem 5 (Complexity entailment in EL+ T). The problem of deciding
whether KB |= α is in co-NP.

Proof. Let us consider the complementary problem of deciding whether KB 6|= α.
This problem can be solved by a nondeterministic polynomial time algorithm
which guesses a model N of polynomial size and a domain element x of the
model, and then checks in polynomial time that N is a model of the KB and
that x falsifies α.
                                 ⊥
As a consequence, for logic EL+ T the problems of satisfiability of a knowledge
base and of concept satisfiability are in NP. The problems of subsumption and
of instance checking are in co-NP.


5   Conclusions and Future Works

This work presents our approach to handle prototypical reasoning in DL by
means of a typicality operator T, the latter is intended to select the “most
normal” instances of a concept. In this work, we have considered the descrip-
                                ⊥
tion logics ALC + T and EL+ T. Whereas for ALC + T deciding satisfiability
                                                            ⊥
(subsumption) is EXPTIME complete (see [13]), for EL+ T the complexity is
significantly smaller, namely it reduces to NP for satisfiability (and co-NP for
subsumption). This result is obtained by a “small” model property that fails for
the whole ALC + T as well as for ALC. We believe that this bound is also a
lower bound, but we have not proved it yet.
    Concerning ALC, we have observed that this logic is not sufficient to perform
defeasible reasoning. Therefore, we have also proposed a nonmonotonic exten-
sion called ALC + Tmin of ALC. This nonmonotonic extension is based on a
(nonmonotonic) entailment relation determined by restricting the entailment of
ALC + T to “minimal models”. Intuitively minimal models are those that max-
imise “typical instances” of a concept. We have proved that deciding ALC +Tmin
entailment is in co-NExpNP . We believe that for EL+ Tmin we can obtain a
                                                          ⊥


smaller complexity upper bound on the base of the results presented here.
    In future work we will deal with the precise relation between our T-DLs
with the other nonmonotonic extensions of DLs mentioned above, notably with
                                                                           ⊥
circumscription. In this setting, a natural question is to compare EL+ Tmin
with circumscribed EL and see whether we get the same complexity bounds or
not.
References
 1. F. Baader. Terminological cycles in a description logic with existential restrictions.
    In Proc. of IJCAI’03, pp. 325-330, 2003.
 2. F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In LTCS-
    Report LTCS-05-01, Inst. for Theoretical Computer Science, TU Dresden,
    http://lat.inf.tudresden.de/research/reports.html, 2005.
 3. F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In Proc. of IJCAI’05,
    Professional Book Center pp. 364-369, 2005.
 4. F. Baader and B. Hollunder. Embedding defaults into terminological knowledge
    representation formalisms. J. Autom. Reasoning, 14(1):149–180, 1995.
 5. F. Baader and B. Hollunder. Priorities on defaults with prerequisites, and their
    application in treating specificity in terminological default logic. J. of Automated
    Reasoning (JAR), 15(1):41–68, 1995.
 6. P. Bonatti, M. Faella, and L. Sauro. Defeasible inclusions in low-complexity dls:
    Preliminary notes. In Proc. IJCAI2009, to appear.
 7. P. A. Bonatti, C. Lutz, and F. Wolter. Description logics with circumscription. In
    Proc. of KR, pages 400–410, 2006.
 8. S. Brandt. Polynomial time reasoning in a description logic with existential re-
    strictions, gci axioms, andwhat else? In Proc. of ECAI’04, pp. 298-302, 2004.
 9. F. M. Donini, D. Nardi, and R. Rosati. Description logics of minimal knowledge
    and negation as failure. ACM Trans. Comput. Log., 3(2):177–225, 2002.
10. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. Preferential Description
    Logics. In Nachum Dershowitz and Andrei Voronkov, editors, Proceedings of LPAR
    2007 (14th Conference on Logic for Programming, Artificial Intelligence, and Rea-
    soning), volume 4790 of LNAI, pages 257–272, Yerevan, Armenia, October 2007.
    Springer-Verlag.
11. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. Reasoning About Typical-
    ity in Preferential Description Logics. In S. Hólldobler, C. Lutz, and H. Wansing,
    editors, Proceedings of JELIA 2008 (11th European Conference on Logics in Ar-
    tificial Intelligence), volume 5293 of LNAI, pages 192–205, Dresden, Germany,
    September 2008. Springer-Verlag.
12. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. Analytic Tableaux Calculi
    for KLM Logics of Nonmonotonic Reasoning. ACM Transactions on Computational
    Logic, 10(3), 2009.
13. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. On Extending De-
    scription Logics for Reasoning About Typicality: a First Step. In Technical Re-
    port 116/09, Dipartimento di Informatica, Universitá degli Studi di Torino, Italy,
    http://www.di.unito.it/∼argo/papers/RT 11609.pdf, 2009.
14. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. Reasoning About Typical-
    ity in Low Complexity Description Logics: Preliminary Results. In Technical Re-
    port 150/09, Dipartimento di Informatica, Universitá degli Studi di Torino, Italy,
    http://www.di.unito.it/∼argo/papers/RT 15009.pdf, 2009.
15. P. Ke and U. Sattler. Next Steps for Description Logics of Minimal Knowledge
    and Negation as Failure. In DL2008, 2008.
16. S. Kraus, D. Lehmann, and M. Magidor. Nonmonotonic reasoning, preferential
    models and cumulative logics. Artificial Intelligence, 44(1-2):167–207, 1990.
17. A. Rector and I. Horrocks. Experience building a large, re-usable medical ontol-
    ogy using a description logic with transitivity and concept inclusions. In Proc.
    Workshop on Ontological Engineering, 1997.
18. K.A. Spackman. Managing clinical terminology hierarchies using algorithmic cal-
    culation of subsumption: Experience with snomed-rt. J. of the American Medical
    Informatics Association, Fall Symposium Special Issue, 2000.
19. U. Straccia. Default inheritance reasoning in hybrid kl-one-style logics. In Proc.
    of IJCAI, pages 676–681, 1993.
20. The GO Consortium. Gene ontology: Tool for the unification of biology. Nature
    Genetics, 25, 2000.

</pre>