<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Quasi-Classical Semantics for Expressive Description Logics?</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Xiaowang Zhang</string-name>
          <xref ref-type="aff" rid="aff2">2</xref>
          <xref ref-type="aff" rid="aff3">3</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Guilin Qi</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Yue Ma</string-name>
          <email>Yue.Ma@lipn.univ-paris13.fr</email>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Zuoquan Lin</string-name>
          <xref ref-type="aff" rid="aff3">3</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Institute AIFB, University of Karlsruhe</institution>
          ,
          <addr-line>Karlsruhe 76131</addr-line>
          ,
          <country country="DE">Germany</country>
        </aff>
        <aff id="aff1">
          <label>1</label>
          <institution>Laboratoire d'Informatique de l'universit Paris-Nord (LIPN) - UMR 7030</institution>
          ,
          <country country="FR">France</country>
        </aff>
        <aff id="aff2">
          <label>2</label>
          <institution>School of Mathematical Sciences, Anhui University</institution>
          ,
          <addr-line>Hefei 230039</addr-line>
          ,
          <country country="CN">China</country>
        </aff>
        <aff id="aff3">
          <label>3</label>
          <institution>School of Mathematical Sciences, Peking University</institution>
          ,
          <addr-line>Beijing 100871</addr-line>
          ,
          <country country="CN">China</country>
        </aff>
      </contrib-group>
      <abstract>
        <p>Inconsistency handling in expressive description logics is an important problem because inconsistency may naturally occur in an open world. In this paper, we first present the quasi-classical semantics for description logic SHIQ, which is based on quasi-classical logic. We show that this semantics can be used to deal with inconsistency and that it is reduced to the standard semantics when there is no inconsistency. Compared with the existing four-valued semantics for description logics, it strengthens the reasoning capability in the sense that it can satisfy some important inference rules, such as Modus Ponens. Finally, we analyze the computational complexity of consistency checking based on the quasiclassical semantics.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>Introduction</title>
      <p>In an open, constantly changing and collaborative environment like the forthcoming
Semantic Web, a knowledge base (or an ontology) may well contain inconsistencies
because of many reasons, such as modeling errors, migration from other formalisms,
merging ontologies, and ontology evolution (see [1]). As the logical foundation of
Ontology Web Language (OWL), expressive description logics (for short DLs) fail to
tolerate inconsistent data. Therefore, handling inconsistency in expressive DLs, such as
SHIQ, is becoming an important topic in recent years.</p>
      <p>There are two fundamentally different approaches to handling inconsistency. One is
to repair inconsistency in ontologies to obtain consistent ontologies [2,3,4]. The other,
called paraconsistent approach, does not simply repair inconsistencies but applies a
nonstandard reasoning to obtain meaningful answers from inconsistent ontologies [5,6]. For
the latter, having inconsistencies is treated as a natural phenomenon in realistic data and
is tolerated during reasoning, whilst inconsistencies are viewed as erroneous data for the
first approach. So far, the main idea of paraconsistent methods for handling inconsistent
ontologies [5] is based on Belnap’s four-valued semantics [7]. However their reasoning
capability is rather weak [6]. For instance, they fail in holding some important inference
rules, such as Modus Ponens, Modus Tollens and Disjunctive Syllogism. In [6], a total
negation is introduced to enable the resolution principle for paraconsistent reasoning
? This paper is supported by the EU under the IST project NeOn.
in four-valued DLs. However, four-valued DLs with total negation still don’t satisfy
some intuitive equivalences mentioned above. The main problem of four-valued DLs
is that they can not overcome those inherent shortcomings of four-valued semantics in
reasoning [7].</p>
      <p>To avoid shortcomings of four-valued DLs and strengthen paraconsistent
reasoning capability, in this paper, following [8], we study a quasi-classical description logic
SHIQ (QC SHIQ for short), which is based on quasi-classical logic [9,10] and
description logic (for short DL) SHIQ. We concentrate on SHIQ since it is the core of
OWL DL [11,12]. Main contributions of this paper are summarized as follows:
– QC semantics is introduced to SHIQ to handle inconsistent ontologies. It
composes of two kinds of semantics, namely, QC weak semantics |=w and QC strong
semantics |=s. QC weak semantics inherits the characteristics of four-valued
semantics and QC strong semantics redefines the interpretation for disjunction and
conjunction of concepts to make the three important inference rules hold.
– A new notion called complement of concept is introduced. We use C to denote
the complement of concept C. The semantics of an inclusion axiom defined under
the weak semantics and the strong semantics satisfy the intuitive equivalences. For
instance, I |=w C v D iff I |=w C tD(a); and I |=s C v D iff I |=s ¬C tD(a)
for any individual a.
– A QC model is defined to express a possible world under QC strong semantics. A
QC entailment based on QC model, written by “|=Q”, between an ontology and an
axiom is presented which is shown to be able to handle inconsistency. Compared
with the four-valued DLs, QC DLs satisfy three important inference rules: Modus
Ponens (MP): {C(a), C v D} |=Q D(a), Modus Tollens (MT): {¬D(a), C v
D} |=Q ¬C(a), and Disjunctive Syllogism (DS): {¬C(a), C t D} |=Q D(a).
– Two basic query entailment problems, namely, instance checking and subsumption
checking are defined and discussed. We show that the two basic inference problems
can be reduced into the QC consistency problem.
– We prove that the complexity of deciding QC consistency for an ABox is
EXPTIME</p>
      <p>Complete.</p>
      <p>
        Compared with QC ALC studied in [13], QC SHIQ studied in this paper has the
following significant improvements: (
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) we redefine the QC strong semantics of concept
inclusion C1 v C2 so that intuitive logical equivalences w.r.t. classical negation can
be satisfied, which is not the case for QC ALC; (
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) we properly introduce the weak
and strong satisfactions in QC SHIQ, which avoids redundant definition of the
semantics of disjunction and conjunction of concepts in QC ALC; (
        <xref ref-type="bibr" rid="ref3">3</xref>
        ) we show that instance
checking and subsumption checking can be reduced to the QC consistency problem,
which has not been achieved in QC ALC; and (
        <xref ref-type="bibr" rid="ref4">4</xref>
        ) we study the QC semantics for more
expressive language constructors than those in ALC.
      </p>
      <p>The paper is organized as follows. Section 2 briefly reviews SHIQ. Section 3
introduces QC semantics for SHIQ. Section 4 discusses the reasoning problems in QC
SHIQ. Section 5 concludes this paper and discusses the future work. Due to the space
limitation, proofs are omitted but are available in a technical report1.
1 http://www.is.pku.edu.cn/˜zxw/publication/TRQCSHIQ.pdf</p>
    </sec>
    <sec id="sec-2">
      <title>Preliminaries</title>
      <p>In this section, we briefly review some basic notations in description logic (DL) SHIQ.
For comprehensive background reading, please refer to [11].</p>
      <p>Let L be the language of SHIQ, which contains a set of atomic concepts (or
concept names), denoted by NC ; a set of individuals, denoted by NI ; and a set of role
names, denoted by NR. NR+ is a set of transitive role names in NR and R is a
transitive closure set of NR. We denote R = R ∪ {R− | R ∈ R} where R− is the inverse
role of R. The inverse role of R can be also taken as the inverse transformation on R.
In this way, the inverse role of R can be denoted by Inv(R), i.e., Inv(R) = R− and
Inv(R−) = R. A role inclusion axiom is of the form R v S where roles R, S can be
inverse. A role hierarchy, denoted R, is a set of role inclusion axioms. A role R is a
sub-role of S, denoted by R v∗S, where “ v∗” is the transitive-reflexive closure of v over
R ∪ {Inv(R) v Inv(S) | R v S ∈ R}. A simple role S is a role which is neither
transitive nor has any transitive sub-roles.</p>
      <p>Concept descriptions in SHIQ are formed according to the following syntax rule:
C, D → A | &gt; | ⊥ | ¬A | C t D | C u D | ∃R.C | ∀R.C |≥ nS.C |≤ nS.C
where &gt; is the top concept, ⊥ is the bottom concept, A is a concept name, C, D are
concepts, R is a role, S is a simple role and n is nonnegative integer.</p>
      <p>Let C, D be concepts, a, b individuals and R a role. In SHIQ, assertions are of
.
the form C(a) or R(a, b) or a 6= b. A general concept inclusion axiom (GCI) is of the
form C v D. Informally, an axiom C(a) means that the individual a is an instance of
concept C, and an axiom R(a, b) means that individual a is related with individual b
via the property R. The inclusion axiom C v D means that each individual of C is an
individual of D.</p>
      <p>A knowledge base (or ontology) comprises two components, a TBox and an ABox.
In SHIQ, a TBox includes two parts: a set of concept inclusion axioms T and a role
hierarchy R; an ABox consists of concept assertions, role assertions, and individual
inequalities.</p>
      <p>The formal definition of the classical (model-theoretic) semantics of SHIQ is given
by means of an interpretation I = (ΔI , ·I ) which consists of a non-empty domain ΔI
and a mapping ·I satisfying the conditions in Table 1, where the mapping ·I interprets
concepts as subsets of the domain and roles as binary relations on the domain ΔI .</p>
      <p>An interpretation I satisfies a terminology T (role hierarchy R) iff for any concept
inclusion C v D (role inclusion R v S) in T (R), I is an interpretation of C v D
(R v S). In this case, I is named a model of T (R), denoted I |= T (I |= R). A
concept C is called satisfiable w.r.t. a terminology T and a hierarchy R iff there is a
model I of T and R with CI 6= ∅. A concept D subsumes a concept C w.r.t T and R
iff CI ⊆ DI holds for each model I of T and R. For an interpretation I, an element
aI ∈ ΔI is called an instance of a concept C iff aI ∈ CI . An interpretation I satisfies
an ABox A (written I |= A) if it satisfies every assertion in A. An ABox A is consistent
w.r.t. T and R iff there is a model I of T and R that satisfies each assertion in A.
Constructor Name</p>
      <p>Syntax
atomic concept A
abstract role R
individuals I
trans.role
inverse role</p>
      <p>A
R
o
R ∈ NR+</p>
      <p>R−</p>
      <p>Semantics</p>
      <p>AI ⊆ ΔI
RI ⊆ ΔI × ΔI</p>
      <p>oI ∈ ΔI</p>
      <p>RI = (RI )+
{(x, y) | (y, x) ∈ RI }
ΔI
top concept &gt;
bottom concept ⊥ ∅
conjunction C1 u C2 C1I ∩ C2I
disjunction C1 t C2 C1I ∪ C2I
negation ¬C ΔI \ CI
exists restriction ∃R.C {x | ∃y, (x, y) ∈ RI and y ∈ CI }
value restriction ∀R.C {x | ∀y, (x, y) ∈ RI implies y ∈ CI }
qualifying atleast restriction ≥ nR.C {x | ]({y.(x, y) ∈ RI } and y ∈ CI ) ≥ n}
qualifying atmost restriction ≤ nR.C {x | ]({y.(x, y) ∈ RI } and y ∈ CI ) ≤ n}</p>
      <p>Axiom Name
concept assertion</p>
      <p>role assertion
concept inclusion</p>
      <p>role inclusion
individual inequality</p>
      <p>Syntax
C(a)
R(a, b)
C1 v C2
R v S</p>
      <p>.
a 6= b</p>
      <p>Semantics
aI ∈ CI
(aI , bI ) ∈ RI</p>
      <p>C1I ⊆ C2I
RI ⊆ SI
aI 6=. bI
3</p>
      <sec id="sec-2-1">
        <title>Quasi-Classical Description Logic S HI Q</title>
        <p>Quasi-classical DL SHIQ is based on quasi-classical logic defined in [9] and SHIQ.
In this section, we present the syntax and the semantics of QC SHIQ.
3.1</p>
      </sec>
    </sec>
    <sec id="sec-3">
      <title>Syntax of QC SHIQ</title>
      <p>The syntax of QC SHIQ is almost the same as that of SHIQ. One difference is that
a new concept constructor called complement of a concept is introduced, which is the
syntax form of “total negation” in [14]. The complement of concept C is denoted by C.
The intuition behind a complement of a concept is that we want to use it to characterize
QC inconsistency, i.e., to reverse both the information of being true and of being false.
Its formal interpretation will be given in Section 3.2.</p>
      <p>The definition of a QC ABox (resp. QC terminology, QC role hierarchy) is similar
to that of an ABox (resp. terminology, role hierarchy). The only difference is that we
allow a complement of a concept in a complex concept. A QC ontology comprises a
QC terminology, a QC role hierarchy and a QC ABox.</p>
      <p>Given the language L of SHIQ, the language of QC SHIQ is denoted L∗ and
is defined by L∗ = L ∪ {C | C is a concept in L}. In the following, we discuss QC
SHIQ based on the language L∗.</p>
      <p>For an atomic concept A, we call A, ¬A, A and ¬A as concept literals. A concept
C is in Negation Normal Form (NNF) if negation (¬) occurs only in front of concept
names. A concept C is in QC NNF, if concept C is in NNF and complement only
occurs over a concept name or negation of a concept name. A role-involved literal has
the form ∀R.C or ∃R.C with C a concept in NNF. A role-involved literal has the form
∀R.C, ∃R.C, ≥ nR.C or ≤ nR.C with C a concept in QC NNF. A literal is either
a concept literal or a role-involved literal, written by L. A clause is the disjunction of
finite literals. Let L1 t · · · t Ln be a clause, then Lit(L1 t · · · t Ln) is the set of literals
{L1, . . . , Ln} that are in the clause. A clause is the empty clause, denoted by ♦, if it
has no literals. We define ∼ be a complementation operation such that ∼ A is ¬A and
∼ (¬A) is A.</p>
      <p>Let L1t· · ·tLn be a clause that includes a literal disjunct Li. The focus of L1t· · ·t
Ln by Li, denoted ⊗(L1 t · · · t Ln, Li), is defined as the clause obtained by removing
Li from Lit(L1 t · · · t Ln). In the case of a clause with just one disjunct, we assume
⊗(L, L) = ⊥. For instance, given a clause L1tL2tL3, ⊗(L1tL2tL3, L2) = L1tL3.
3.2</p>
    </sec>
    <sec id="sec-4">
      <title>Semantics of QC SHIQ</title>
      <p>In this subsection, we define the QC semantics for QC SHIQ by introducing two
semantics, namely, QC weak semantics and QC strong semantics.</p>
      <p>Firstly, we introduce the notion of a weak interpretation and the notion of a strong
interpretation over domain ΔI by assigning to each concept C a pair h+C, −Ci of
subsets of ΔI . Intuitively, +C is the set of elements known to belong to the extension
of C, while −C is the set of elements known to be not contained in the extension of
C. +C and −C are not necessarily disjoint or mutually complemental with respect to
the domain. The complemental set of a set S w.r.t. an interpretation I, denoted by S, is
S = ΔI \ S.</p>
      <p>In QC SHIQ, a weak interpretation is a reformulation of a four-valued
interpretation in four-valued DLs (see [6]).</p>
      <p>Definition 1 Let I be a pair (ΔI , ·I ) with ΔI as domain, where ·I is a function
assigning elements of ΔI to individuals, subsets of ΔI × ΔI to concepts and subsets
of (ΔI × ΔI )2 to roles. I is a weak interpretation in QC SHIQ if the conditions in
Table 2 are satisfied, where CI = h+Ci, −Cii for i = 1, 2, CI = h+C, −Ci and
i
RI = h+R, −Ri.</p>
      <p>
        Definition 2 Let |=w be a satisfiability relation between a set of weak interpretation
and a set of axioms, called weak satisfaction. For a weak interpretation I, we define
|=w as follows, where C, C1, C2 are concepts, R, R1, R2 are roles and a is an
individual:
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) I |=w R1 v R2 iff +R1 ⊆ +R2, if RiI = h+Ri, −Rii, i = 1, 2;
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) I |=w Trans(R) iff +R = (+R)+, if RI = h+R, −Ri and (R+)I = h+R+, −R+i;
(
        <xref ref-type="bibr" rid="ref3">3</xref>
        ) I |=w C(a) iff aI ∈ +C, CI = h+C, −Ci;
(
        <xref ref-type="bibr" rid="ref4">4</xref>
        ) I |=w R(a, b) iff (aI , bI ) ∈ +R, RI = h+R, −Ri;
(
        <xref ref-type="bibr" rid="ref5">5</xref>
        ) I |=w C1. v C2 iff +C1 ⊆ +C2, for i = 1, 2, CiI = h+Ci, −Cii;
(
        <xref ref-type="bibr" rid="ref6">6</xref>
        ) I |=w a 6= b iff aI 6= bI .
      </p>
      <p>In QC SHIQ, the concept inclusion under weak satisfaction is defined by the
internal inclusion in four-valued DLs because other inclusion, namely, material inclusion
and strong inclusion can be transformed into internal inclusion (see [6]).</p>
      <p>The following property shows that there exists a close relationship between weak
models and 4-models in fourv-alued DLs defined in [6].</p>
      <p>
        Proposition 1 Let C, D be concepts, a an individual, R a role and I an interpretation
in QC SHIQ. We have
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) I |=w C(a) iff I |=4 C(a);
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) I |=w C v D iff I |=4 C @ D.
      </p>
      <p>The following proposition shows that intuitive equivalence w.r.t. the complement of
a concept is satisfied under QC weak semantics.</p>
      <p>Proposition 2 Let I be an interpretation and let C, D be concepts, we have</p>
      <p>I |=w C v D iff I |=w C t D(a) for any individual a ∈ NI .</p>
      <p>The QC weak satisfaction has the drawback that it does not satisfy some basic
inference rules, such as MP, MT and DS. Therefore, we define a QC strong interpretation
that redefines interpretation of disjunction of concepts and conjunction of concepts.
Definition 3 Let I be a pair (ΔI , ·I ) with ΔI as the domain, where ·I is a function
assigning elements of ΔI to individuals, subsets of ΔI × ΔI to concepts and subsets
of (ΔI × ΔI )2 to roles. I is a strong interpretation in QC SHIQ if the conditions in
Table 2, except conditions for conjunction of concepts and disjunction of concepts, are
satisfied and the following conditions hold, let CiI = h+Ci, −Cii for i = 1, 2:
conjunction of concepts:
(C1 u C2)I = h+C1 ∩ +C2, (−C1 ∪ −C2) ∩ (−C1 ∪ +C2) ∩ (+C1 ∪ −C2)i
disjunction of concepts:
(C1 t C2)I = h(+C1 ∪ +C2) ∩ (−C1 ∪ +C2) ∩ (+C1 ∪ −C2), −C1 ∩ −C2i</p>
      <p>Compared with the weak interpretation, the strong interpretation of disjunction of
concepts tightens the condition that an individual is known to belong to a concept; and
the strong interpretation of conjunction of concepts is defined by relaxing the condition
that an individual known to be not contained in the extension of a concept. The strong
interpretation for the disjunction and conjunction characterizes the relationship between
concepts and individuals with holding resolution rule.</p>
      <p>
        Definition 4 Let |=s be a satisfiability relation between a set of weak interpretation
and a set of axioms, called strong satisf action. For a strong interpretation I, we
define |=s as follows, where C, C1, C2 are concepts, R, R1, R2 are roles and a is an
individual:
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) I |=s R1 v R2 iff +R1 ⊆ +R2, if RiI = h+Ri, −Rii, i = 1, 2;
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) I |=s Trans(R) iff +R = (+R)+, if RI = h+R, −Ri and (R+)I = h+R+, −R+i;
(
        <xref ref-type="bibr" rid="ref3">3</xref>
        ) I |=s C(a) iff aI ∈ +C where CI = h+C, −Ci;
(
        <xref ref-type="bibr" rid="ref4">4</xref>
        ) I |=s R(a, b) iff (aI , bI ) ∈ +R where RI = h+R, −Ri;
(
        <xref ref-type="bibr" rid="ref5">5</xref>
        ) I |=s C1 v C2 iff −C1 ⊆ +C2, +C1 ⊆ +C2 and −C2 ⊆ −C1,
for i = 1, 2, .CiI = h+Ci, −Cii;
(
        <xref ref-type="bibr" rid="ref6">6</xref>
        ) I |=s a 6= b iff aI 6= bI .
      </p>
      <p>In Definition 4, when defining the strong satisfaction of a concept inclusion under
a QC strong interpretation, we use conditions for interpreting a concept inclusion by
internal inclusion, material inclusion and strong inclusion in four-valued DLs. By doing
so, our strong satisfaction satisfies intuitive equivalence that is falsified by four-valued
satisfaction relations.</p>
      <p>Proposition 3 Let I be an interpretation and let C, D be concepts. We have</p>
      <p>I |=s C v D iff I |=s ¬C t D(a) for any individual a ∈ NI .</p>
      <p>Proposition 2 and Proposition 3 provide the theoretical base of transforming the
problem of reasoning with ABoxes and terminologies into the problem of reasoning
with ABoxes.</p>
      <p>The following proposition provides a slightly different view on the QC semantics
of disjunction of concepts.</p>
      <p>Proposition 4 Let C1 and C2 be two concepts and a be an individual. We have
I |=s C1 t C2(a) iff for some Ci, aI ∈ +Ci and aI 6∈ −Ci; or</p>
      <p>for all Ci, aI ∈ +Ci and aI ∈ −Ci;
where CiI = h+Ci, −Cii and i = 1, 2.</p>
      <p>Proposition 5 Let I be an interpretation and φ be an axiom in QC S HIQ respectively.</p>
      <p>If I |=s φ then I |=w φ.</p>
      <p>Proposition 5 shows that a strong model is a weak model. However, the converse
does not hold. For instance, given an ABox A = {C(a), ¬C(a)}. We can construct an
interpretation I such that aI ∈ +C, aI ∈ −C and aI 6∈ +D where CI = h+C, −Ci
and DI = h+D, −Di. Then I 6|=s C t D(a) because I 6|=s D(a). Clearly, I |=w
C t D(a).</p>
      <p>
        Proposition 6 Let C be a concept, R a role and n a natural number. For any QC weak
( or QC strong) interpretation I, we have
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) (¬(≤ nR.C))I = (&gt; nR.C)I ;
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) (¬(≥ nR.C))I = (&lt; nR.C)I ;
(
        <xref ref-type="bibr" rid="ref3">3</xref>
        ) (∃R.C)I = (≥ 1R.C)I ;
(
        <xref ref-type="bibr" rid="ref4">4</xref>
        ) (∀R.C)I = (&lt; 1R.¬C)I .
      </p>
      <p>
        Proposition 7 Let A be a concept name, C, D concepts, a, b individuals, R a role and
n a natural number in QC SHIQ. If I is a QC weak or QC strong interpretation, then
the follows properties hold.
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) I |=x A(a) iff I 6|=x A(a) (
        <xref ref-type="bibr" rid="ref6">6</xref>
        ) I |=x &gt;(a) iff I |=x ⊥(a)
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) I |=x A(a) iff I |=x A(a) (
        <xref ref-type="bibr" rid="ref7">7</xref>
        ) I |=w C t D(a) iff I |=w C u D(a)
(
        <xref ref-type="bibr" rid="ref3">3</xref>
        ) I |=x ¬A(a) iff I |=x ¬A(a) (
        <xref ref-type="bibr" rid="ref8">8</xref>
        ) I |=w C u D(a) iffI |=w C t D(a)
(
        <xref ref-type="bibr" rid="ref4">4</xref>
        ) I |=x (∀R.C)(a) iff I |=x ∃R.C(a) (
        <xref ref-type="bibr" rid="ref9">9</xref>
        ) I |=x (≥ nR.C)(a) iff I |=x≤ n-1 R.C(a)
(
        <xref ref-type="bibr" rid="ref5">5</xref>
        ) I |=x (∃R.C)(a) iff I |=x ∀R.C(a) (
        <xref ref-type="bibr" rid="ref10">10</xref>
        ) I |=x (≤ nR.C)(a) iff I |=x≥ n+1R.C(a)
where |=x is a place-holder for both |=w and |=s.
      </p>
      <p>Definition 5 Given a QC ontology O and an axiom φ in SHIQ, we say O
quasiclassically entails (for short QC entails) φ, denoted by O |=Q φ, iff for every
interpretation I, for any axiom ψ of O if I |=s ψ then I |=w φ. In this case, |=Q is called a
quasi-classical entailment (relation) (for short QC entailment) between O and φ.</p>
      <p>The following example shows that |=Q is non-trivializable in the sense that when
an ontology O is classically inconsistent.</p>
      <p>Example 1 Given an ABox A = {B(a), ¬B(a)} and a concept name A in QC SHIQ.
It is clear that A is classically inconsistent. However A |=Q A(a) does not hold. This
is because there exists an interpretation I such that aI ∈ +B and aI ∈ −B where
BI = h+B, −Bi. So I |=s B u ¬B(a), but I 6|=w A(a) since A(a) does not occur in
A.</p>
      <p>The following proposition shows that |=Q satisfies the resolution rule.</p>
      <p>Proposition 8 Let C, D, E be concepts and a be an individual.</p>
      <p>{C t D(a), ¬C t E(a)} |=Q D t E(a).</p>
      <p>
        By Proposition 8, |=Q satisfies three important inferences: MP, MT and DS.
Example 2 Suppose O is an empty QC ontology.
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) Consider the concept A t ¬A. We have O 6|=Q A t ¬A(a), since O strongly satisfies
every formula in O, but O does not weakly satisfy A t ¬A(a).
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) Consider the concept A t A. We have O |=Q A t A(a), since O strongly satisfies
every axiom in O and O |=w A(a) or O |=w A(a), i.e., O |=w A t A(a).
      </p>
      <p>Example 2 shows that, for some concept name A in QC SHIQ, the concept A t A
can be considered as the top concept &gt; under QC entailment. However, this is not the
case for concept A t ¬A.</p>
      <p>In the following, we show that some properties of QC entailment satisfied in QC
propositional logic (see [9]) still hold in QC SHIQ.</p>
      <p>
        Proposition 9 Given a QC ontology O, axioms φ, ψ, two concepts C, D and an
individual a, the following properties hold.
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) (Reflexivity) O ∪ {φ} |=Q φ.
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) (Monotonicity) if O |=Q φ then O ∪ {ψ} |=Q φ.
(
        <xref ref-type="bibr" rid="ref3">3</xref>
        ) (And-introduction) if O |=Q C(a) and O |=Q D(a) then O |=Q C u D(a).
(
        <xref ref-type="bibr" rid="ref4">4</xref>
        ) (Or-elimination) if O ∪ {C(a)} |=Q φ and O ∪ {D(a)} |=Q φ then O ∪ {C t
D(a)} |=Q φ.
      </p>
      <p>The following proposition shows that QC entailment is weaker than classical
entailment in SHIQ.</p>
      <p>Proposition 10 Let O be an ontology and φ be an axiom in SHIQ.</p>
      <p>If O |=Q φ then O |= φ.</p>
      <p>The converse of Proposition 10 does not hold. In Example 1, A |= φ for any axiom
because A is classically inconsistent while A 6|=Q A(a).</p>
      <p>Proposition 11 Let O be an ontology and φ be an axiom in SHIQ.</p>
      <p>If O |=4 φ then O |=Q φ.</p>
      <p>In QC SHIQ, a strong interpretation I satisfies a terminology T (role hierarchy
R) iff I |=s C v D (R v S) for each C v D in T (R v S in R). In this case, I is
called a QC model of T , written I |=s T (a QC model of R, written I |=s R). A strong
interpretation I satisfies an ABox A iff I |=s.φ for each assertion φ in A, where φ is
one of the following forms: C(a), R(a, b), a 6= b. In this case, I is called a QC model
of A, written I |=s A.</p>
      <p>The following proposition shows the close relationship between the QC entailment
and the QC model.</p>
      <p>
        Proposition 12 Let O be a QC ontology, C, D two concepts and a an individual.
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) O |=Q C(a) iff there is no any QC model of O ∪ {C(a)}.
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) O |=Q C v D iff there is no any QC model of O ∪ {C u D(t)} for some new
individual t not occurring in O.
      </p>
      <sec id="sec-4-1">
        <title>Reasoning in Quasi-Classical Description Logic S HI Q</title>
        <p>The QC Consistency Problem
In QC SHIQ, a concept C is QC satisfiable w.r.t. a QC ABox A if there exists a QC
model I of A such that I |=s C(a) for some individual a, and QC unsatisfiable w.r.t.
A otherwise. A concept C is QC satisfiable w.r.t. a QC role hierarchy R and a QC
terminology T if there exists a QC model I of R and T such that I |=s C(a) for
some individual a, and QC unsatisfiable w.r.t. R and T otherwise. A QC ABox A is
QC consistent if there exists a QC model I of A, and QC inconsistent otherwise. A QC
ABox A is QC consistent w.r.t. a QC role hierarchy R and a QC terminology T if there
exists a QC model I of R and T such that I is a QC model of A, and QC inconsistent
w.r.t. R and T otherwise.</p>
        <p>We are able to show that the complexity of QC consistency checking in QC SHIQ
is in the same level as that of satisfiability check in SHIQ.</p>
        <p>Proposition 13 Checking QC consistency of a QC SHIQ ABox w.r.t. a QC role
hierarchy R and a QC terminology T is EXPTIME-Complete.
4.2</p>
        <p>The Inference Problems
In QC SHIQ, there are two basic inference problems given as follows.
– instance checking: an individual a is called a QC instance of a concept C w.r.t. a</p>
        <p>QC ABox A iff for any QC model I of A, I is a QC model of C(a).
– subsumption: a concept C QC subsumes a concept D w.r.t. a QC role hierarchy R
and a QC terminology T iff for any QC model I of R and T , I is a QC model of
C v D.</p>
        <p>
          Proposition 14 Given a QC SHIQ ontology O, two concepts C, D and an individual
a, we have
(
          <xref ref-type="bibr" rid="ref1">1</xref>
          ) O |=Q C(a) iff O ∪ {C(a)} is QC inconsistent.
(
          <xref ref-type="bibr" rid="ref2">2</xref>
          ) O |=Q C v D iff O ∪ {C u D(t)} is QC inconsistent for some new individual t not
occurring in O.
        </p>
        <p>Proposition 14 shows that two basic inference problems can be reduced to the
problem of QC consistency checking.
5</p>
      </sec>
    </sec>
    <sec id="sec-5">
      <title>Conclusions</title>
      <p>In this paper, we presented QC SHIQ to handle inconsistency in SHIQ. The syntax
of SHIQ was extended by introducing the notion of the complement of a concept.
QC semantics was defined by two kinds of semantics: weak semantics and strong
semantics. We showed that both of them satisfy some important inference rules. A QC
entailment relation based on strong interpretations and weak interpretations was
introduced and we showed that this entailment relation satisfies some desirable properties.
We introduced the notion of QC consistency of a QC ontology and two basic QC
entailment problems and showed that these two entailment problems can be reduced to
the problem of QC consistency checking. Furthermore, we showed that QC consistency
problem of ABoxes is EXPTIME-Complete. As a future work, following [8], we will
develop an algorithm based on the classical tableau for querying. In the other
direction, we will consider employing a classical DL reasoner, such as KAON2 or Pellet,
to implement paraconsistent reasoning based on QC semantics. Further, we will also
consider introducing QC semantics into more expressive DLs such as SHOIN (D).</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <surname>Bell</surname>
            ,
            <given-names>D.A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Qi</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Liu</surname>
            ,
            <given-names>W.</given-names>
          </string-name>
          :
          <article-title>Approaches to inconsistency handling in description-logic based ontologies</article-title>
          .
          <source>In: Proc. of OTM Workshops'07</source>
          ,
          <string-name>
            <surname>Portugal</surname>
          </string-name>
          ,
          <year>2007</year>
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <surname>Schlobach</surname>
            ,
            <given-names>S.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Cornet</surname>
          </string-name>
          , R.:
          <article-title>Non-standard reasoning services for the debugging of description logic terminologies</article-title>
          .
          <source>In: Proc.of IJCAI'03</source>
          ,
          <string-name>
            <surname>Mexico</surname>
          </string-name>
          ,
          <year>2003</year>
          , Morgan Kaufmann (
          <year>2003</year>
          )
          <fpage>355</fpage>
          -
          <lpage>362</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <surname>Huang</surname>
            ,
            <given-names>Z.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>van Harmelen</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>ten Teije</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          :
          <article-title>Reasoning with inconsistent ontologies</article-title>
          .
          <source>In: Proc. of IJCAI'05</source>
          ,
          <string-name>
            <surname>Scotland</surname>
          </string-name>
          , UK,
          <year>2005</year>
          , Professional Book Center (
          <year>2005</year>
          )
          <fpage>454</fpage>
          -
          <lpage>459</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <surname>Qi</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Yang</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          :
          <article-title>A survey of revision approaches in description logics</article-title>
          .
          <source>In: Proc. of DL'08</source>
          ,
          <string-name>
            <surname>Germany</surname>
          </string-name>
          ,
          <year>2008</year>
          . CEUR Workshop Proceedings 353,
          <string-name>
            <surname>CEUR-WS.org</surname>
          </string-name>
          (
          <year>2008</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <surname>Straccia</surname>
            ,
            <given-names>U.</given-names>
          </string-name>
          :
          <article-title>A sequent calculus for reasoning in four-valued description logics</article-title>
          .
          <source>In: Proc. of TABLEAUX '97</source>
          , France,
          <year>1997</year>
          . LNCS 1227, Springer (
          <year>1997</year>
          )
          <fpage>343</fpage>
          -
          <lpage>357</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          6.
          <string-name>
            <surname>Ma</surname>
            ,
            <given-names>Y.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Hitzler</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lin</surname>
            ,
            <given-names>Z.</given-names>
          </string-name>
          :
          <article-title>Paraconsistent reasoning for expressive and tractable description logics</article-title>
          .
          <source>In: Proc. of DL'08</source>
          ,
          <string-name>
            <surname>Germany</surname>
          </string-name>
          ,
          <year>2008</year>
          . CEUR Workshop Proceedings 353, CEURWS.org (
          <year>2008</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          7.
          <string-name>
            <surname>Belnap</surname>
            ,
            <given-names>N.D.:</given-names>
          </string-name>
          <article-title>A useful four-valued logic. Modern uses of multiple-valued logics (</article-title>
          <year>1977</year>
          )
          <fpage>7</fpage>
          -
          <lpage>73</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          8.
          <string-name>
            <surname>Zhang</surname>
            ,
            <given-names>X.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Xiao</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lin</surname>
            ,
            <given-names>Z.</given-names>
          </string-name>
          :
          <article-title>A tableau algorithm for handling inconsistency in OWL</article-title>
          .
          <source>In: Proc. of ESWC'09</source>
          ,
          <string-name>
            <surname>Greece</surname>
          </string-name>
          ,
          <year>2009</year>
          . LNCS 5554, Springer (
          <year>2009</year>
          )
          <fpage>399</fpage>
          -
          <lpage>413</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          9.
          <string-name>
            <surname>Besnard</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Hunter</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          :
          <article-title>Quasi-classical logic: Non-trivializable classical reasoning from incosistent information</article-title>
          .
          <source>In: Proc. of ECSQARU'95</source>
          ,
          <string-name>
            <surname>Switzerland</surname>
          </string-name>
          ,
          <year>1995</year>
          . LNCS 946, Springer (
          <year>1995</year>
          )
          <fpage>44</fpage>
          -
          <lpage>51</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          10.
          <string-name>
            <surname>Hunter</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          :
          <article-title>Reasoning with contradictory information using quasi-classical logic</article-title>
          .
          <source>J. Log. Comput</source>
          .
          <volume>10</volume>
          (
          <issue>5</issue>
          ) (
          <year>2000</year>
          )
          <fpage>677</fpage>
          -
          <lpage>703</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          11.
          <string-name>
            <surname>Horrocks</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Sattler</surname>
            ,
            <given-names>U.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Tobies</surname>
            ,
            <given-names>S.</given-names>
          </string-name>
          :
          <article-title>Practical reasoning for expressive description logics</article-title>
          .
          <source>In: Proc. of LPAR'99</source>
          ,
          <string-name>
            <surname>Georgia</surname>
          </string-name>
          ,
          <year>1999</year>
          . LNCS 1705, Springer (
          <year>1999</year>
          )
          <fpage>161</fpage>
          -
          <lpage>180</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          12.
          <string-name>
            <surname>Baader</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Nutt</surname>
            ,
            <given-names>W.</given-names>
          </string-name>
          :
          <article-title>Basic description logics</article-title>
          .
          <source>In: The Description Logic Handbook: Theory</source>
          , Implementation, and Applications. (
          <year>2003</year>
          )
          <fpage>43</fpage>
          -
          <lpage>95</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          13.
          <string-name>
            <surname>Zhang</surname>
            ,
            <given-names>X.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lin</surname>
            ,
            <given-names>Z.</given-names>
          </string-name>
          :
          <article-title>Paraconsistent reasoning with quasi-classical semantics in alc</article-title>
          .
          <source>In: Proc. of RR'08</source>
          ,
          <string-name>
            <surname>Germany</surname>
          </string-name>
          ,
          <year>2008</year>
          . LNCS 5341, Springer (
          <year>2008</year>
          )
          <fpage>222</fpage>
          -
          <lpage>229</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          14.
          <string-name>
            <surname>Ma</surname>
            ,
            <given-names>Y.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Hitzler</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lin</surname>
            ,
            <given-names>Z.</given-names>
          </string-name>
          :
          <article-title>Algorithms for paraconsistent reasoning with owl</article-title>
          .
          <source>In: Proc. of ESWC'07</source>
          ,
          <string-name>
            <surname>Austria</surname>
          </string-name>
          ,
          <year>2007</year>
          . LNCS 4519, Springer (
          <year>2007</year>
          )
          <fpage>399</fpage>
          -
          <lpage>413</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          15.
          <string-name>
            <surname>Patel-Schneider</surname>
            ,
            <given-names>P.F.</given-names>
          </string-name>
          :
          <article-title>A four-valued semantics for terminological logics</article-title>
          .
          <source>Artif. Intell</source>
          .
          <volume>38</volume>
          (
          <issue>3</issue>
          ) (
          <year>1989</year>
          )
          <fpage>319</fpage>
          -
          <lpage>351</lpage>
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          16.
          <string-name>
            <surname>Baader</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Hollunder</surname>
            ,
            <given-names>B.</given-names>
          </string-name>
          :
          <article-title>A terminological knowledge representation system with complete inference algorithms</article-title>
          .
          <source>In: Proc. of PDK'91</source>
          ,
          <string-name>
            <surname>Germany</surname>
          </string-name>
          ,
          <year>1991</year>
          . LNCS 567, Springer (
          <year>1991</year>
          )
          <fpage>67</fpage>
          -
          <lpage>86</lpage>
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>