=Paper=
{{Paper
|id=Vol-477/paper-45
|storemode=property
|title=An Argumentative Semantics for Paraconsistent Reasoning in Description Logic ALC
|pdfUrl=https://ceur-ws.org/Vol-477/paper_14.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/ZhangZL09
}}
==An Argumentative Semantics for Paraconsistent Reasoning in Description Logic ALC==
https://ceur-ws.org/Vol-477/paper_14.pdf
An Argumentative Semantics for Paraconsistent
Reasoning in Description Logic ALC
Xiaowang Zhang1,2 , Zhihu Zhang1 and Zuoquan Lin1
1
School of Mathematical Sciences, Peking University, Bejing 100871, China
2
School of Mathematical Sciences, Anhui University, Hefei 230039, China
{zxw,zhzhang,lzq}@is.pku.edu.cn
Abstract. It is well known that description logics cannot tolerate the incom-
plete or inconsistent data. Recently, inconsistency handling in description logics
becomes more and more important. In this paper, we present an argumentative
semantics for paraconsistent reasoning in inconsistent ontologies. An argumen-
tative framework based on argument trees is provided to model argumentation in
description logic ALC. Furthermore, two basic problems, namely, satisfiability of
concepts and query entailment problems, are discussed under our argumentative
semantics in description logic ALC.
1 Introduction
Description logics (or DLs) are considered as a kind of very important knowledge rep-
resentation formalism unifying and giving a logical basis to the well known traditions
of Frame-based systems, Semantic web and KL-ONE-like languages, Object-Oriented
representations, Semantic data models and Type systems. Merging ontologies and on-
tology evolution may cause the occurrence of the inconsistency. In practical reasoning,
it is common to have “too much” information about some situations. According the fact
ex contradictione quodlibet “ α,¬α
β ” in classical logics, any axiom can be entailed from
an inconsistent ontology called explosive entailment. In general, conclusions drawn
from inconsistent ontologies may be completely meaningless.
In recent years, handling inconsistency becomes more and more important in DLs.
The main idea of handling inconsistency is to avoid the explosive entailment and obtain
some valuable information from inconsistent ontologies. Roughly speaking, there are
two fundamentally different approaches to dealing with inconsistency in DLs. The first
is based on the assumption that inconsistencies indicate erroneous data which are to be
repaired in order to obtain consistent knowledge bases, e.g., selecting consistent sub-
sets for the reasoning process [1,2,3]. Unfortunately, based on this approach, we may
lose useful information so that we might not obtain more believable conclusions from
those inconsistent information. Another approach, called paraconsistent approach, is
to tolerate inconsistency by applying a non-standard reasoning method, such as beyond
classical semantics, to obtain meaningful answers [4,5]. In the paraconsistent approach,
inconsistencies are treated as a natural phenomenon in realistic data and they are toler-
ated in reasoning. In general, the idea of paraconsistent approach in DLs is introducing
Belnap’s four-valued semantics [6] for DLs (see [5]). A more prominent one of them is
based on the use of additional truth values standing for underdefined (i.e. neither true
nor false) and overdefined (or contradictory, i.e, both true and false). To a certain extent
four-valued semantics can be employed to handle inconsistency, however, the capabil-
ity of reasoning is rather weaker. For instance, four-valued DLs do not hold three basic
inference rules such as modus ponens (MP), disjunctive syllogism (DS), modus tollens
(MT) or intuitive equivalence. In order to strengthen the ability of paraconsistent rea-
soning, Zhang et al [7,8] introduce quasi-classical (QC for short) semantics into DLs
while tautologies cannot be driven by quasi-classical entailment from some ontology
because the QC logics are relevant logics (see [8]). Besides these two approaches, there
are some “hybrid” approaches to handling inconsistency based on formalisms [9] in
other logics. The main idea of these hybrid approaches to handling inconsistency is rea-
soning with consistent subsets of a knowledge base essentially. However, a problem of
those hybrid approaches is generally short of justice enough since inferences are drawn
from parts of knowledge bases.
Though there are some different characteristics among those existing approaches,
the common problem is that inconsistencies are not analyzed in detail further but either
isolated or ignored in reasoning. In philosophy, there is a classical theory called ar-
gumentation theory (or argumentation), which embraces the arts and sciences of civil
debate, dialogue, conversation and persuasion. Dung researches the fundamental mech-
anism, humans use in argumentation, and explores ways in computer science (see [10]).
Elvang and Hunter [11] have presented an argumentative framework which is different
from Dung’s argumentative framework to resolve inconsistency in propositional logic.
In recent years, a number of logic-based proposals for formalizations of argumentation
theory presented in [12,13] show that the approaches based on argumentation theory
in logics have more predominant properties in handling inconsistency. Moreover, the
approach is increasingly applied in ontologies engineering (see [14]).
In this paper, we introduce argumentation theory into description logic (DL for
short) ALC in order to handle inconsistency. We propose an argumentative framework
based on Elvang and Hunter’s argumentative framework to model argumentative de-
scription logic ALC. The main innovations and contributions of this paper can be sum-
marized as follows:
– defining semantically the notion called quasi-classical negation to characterize the
semantic reverse of axioms in DLs;
– introducing the argumentation theory for ALC by defining some basic notions,
namely, argument, undercut, maximal conservative undercut and canonical under-
cut etc;
– presenting an argumentative framework, which are composed of canonical under-
cuts, is developed to demonstrate the structure of arguments in ontologies;
– providing an argumentative semantics based on binary argumentation for ALC
and discussing two basic problems, namely, satisfiability of concepts and inference
problems based on our argumentative semantics in ALC.
This paper is structured as follows. Section 2 reviews briefly the syntax and seman-
tics of ALC. Section 3 presents argumentation theory for ALC. Section 4 develops ar-
gumentative framework. Section 5 proposes argumentative semantics for ALC. Section
6 discusses reasoning problems under argumentative semantics. Section 7 compares our
work with four-valued DLs. Section 8 concludes and discusses our future work. Due to
the space limitation, proofs are sketched out but they are available in a technical report1
2 Preliminaries
In the section, we briefly review syntax and semantics of the DL ALC, but we basically
assume that the reader is familiar with DLs. For comprehensive background reading,
please refer to [15].
We assume that we are given a set of atomic concepts NC (or concept names), a set
of roles NR (or role names), and a set of individuals NI . With the symbols > and ⊥ we
furthermore denote the top concept and the bottom concept, respectively.
Concepts description in ALC can be formed according to the following syntax rule:
C, D → A | > | ⊥ | ¬A | C u D | C t D | ∀R.C | ∃R.C
Let C, D be concepts, R a role and a, b individuals. In DL ALC, an ontology con-
sists of a set of assertions, called the ABox of the ontology, and a set of inclusion
axioms, called the T Box of the ontology. Assertions are of the form C(a) or R(a, b).
Inclusion axioms are of the form C v D. Informally, an assertion C(a) means that
the individual a is an instance of concept C, and an assertion R(a, b) means that indi-
vidual 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.
Let an ontology O = (T , A). The formal definition of the (model-theoretic) se-
mantics of ALC is given by means of interpretations I = (∆I , ·I ) consisting of a non-
empty domain ∆I and a mapping ·I which assigns to every an individual an member of
∆I , to every atomic concept A a subset AI ⊆ ∆I and to every atomic role R a binary
relation RI ⊆ ∆I × ∆I . The interpretation function is extended to concept descrip-
tions by the following inductive definitions: >I = ∆I , ⊥I = ∅, (¬A)I = ∆I \AI ,
(C u D)I = C I ∩ DI , (C t D)I = C I ∪ DI , (∀R.C)I = {x | ∀y, (x, y) ∈ RI
implies y ∈ C I }, (∃R.C)I = {x | ∃y, (x, y) ∈ RI and y ∈ C I }.
An interpretation I satisfies a concept axiom C(a) if aI ∈ C I , denoted by I |=
C(a). An interpretation I satisfies a role axiom R(a, b) if (aI , bI ) ∈ RI , denoted by
I |= R(a, b). An interpretation I satisfies an inclusion C v D if C I ⊆ DI , denoted
by I |= C v D. An interpretation I is a model of A if I satisfies every assertion
C(a) or , R(a, b) ∈ A, denoted by I |= A. An interpretation I is a model of T if I
satisfies every inclusion axiom C v D ∈ T , denoted by I |= T . An interpretation I
satisfies an ALC ontology O (i.e. is a model of the ontology) iff it satisfies both the
ABox and the TBox of it, denoted by I |= O.
A TBox T is consistent if there is a model of T . An ABox A is consistent if there
is a model of A. An ABox A is consistent w.r.t. T if there is a model of I which is a
model of T . An ontology O is consistent if there is a model of A and T , and otherwise
unsatisfiable. A set of formulae S entails a formula α, denoted by S |= α, if for every
model I of S then I is a model of α. {β} |= α is sometimes denoted by β |= α. A
set of formulae S1 entails a set of formulae S2 , denoted by S1 |= S2 , if S |= α for any
1
http://www.is.pku.edu.cn/˜zxw/publication/TRAALC.pdf
member α of S2 . An ABox A entails a query α if S = A, denoted by A |= α. A TBox
T entails a query α, denoted by T |= α. Analogously, O entails α, denoted by O |= α
if A |= α and T |= α.
3 Argumentation for Description Logic ALC
In this section, we introduce basic definitions of argumentation for DL ALC and bring
some properties.
Let α and β be axioms and S be a set of axioms in ALC. In DLs, there are two
logical connectives “conjunction” (∧) and “disjunction” (∨) defined as follows:
(1) S |= α ∧ β iff S |= α and S |= β;
(2) S |= α ∨ β iff S |= α or S |= β.
Compared with concept conjunction connective ∧ and disjunction connective ∨
connecting with two concepts, logical connectives connect with two axioms. The fol-
lowing lemma shows the relationship between logic connectives and syntax connectives
(“u”, “t”).
Lemma 1 Given concepts C, D, an individual a and a set of axioms S, then
(1) S |= C(a) ∧ D(a) iff S |= C u D(a);
(2) S |= C(a) ∨ D(a) iff S |= C t D(a).
Proof (skeleton). It easily proves the two properties by the definitions of the syntax
connectives and the logical connectives in DLs.
If α, β be axioms in DLs, then α ∧ β (or α ∨ β) is called conjunction of axioms (or
disjunction of axioms).
Definition 1 Given a set of formulae S, concepts C, D, an individual a and two axioms
α, β, a negative transformation written by ∼ on axioms or disjunction (conjunction) of
axioms called quasi-negation is defined as follows:
– S |=∼ C(a) iff S |= ¬C(a);
– S |=∼ C v D iff S |= C u ¬D(ι) for some individual ι in S;
– S |=∼ (α ∧ β) iff S |=∼ α∨ ∼ β;
– S |=∼ (α ∨ β) iff S |=∼ α∧ ∼ β.
Axioms, conjunction of axioms, disjunction of axioms and their quasi-negations
(QN for short) are called extended axioms. In this paper, extended axioms are not mem-
bers of ontologies but are taken as the consequent of arguments presented in the follow-
ing definition.
Definition 2 Let Φ be a set of axioms and α be an extended axiom in ALC. An argument
is a pair hΦ, αi, denoted by A = hΦ, αi, such that:
(1) Φ is consistent;
(2) Φ |= α;
(3) no Φ0 ⊂ Φ satisfies Φ0 |= α. We say that hΦ, αi is an argument for α.
We call α the consequent of the argument and Φ the support of the argument, denoted
by Support(hΦ, αi) = Φ and Consequence(hΦ, αi) = α.
Example 1 Let an ontology O = ({P enguin v Bird, Bird v F ly, P enguin v
¬F ly, Swallow v Bird, Swallow v ∀HasF ood.¬F ish, P enguin v ∃HasF ood.F ish,
Swallow v ¬P enguin}, {P enguin(T weety), ¬F ly(T weety)}).
There are some arguments as follows:
A1 = h{P enguin(T weety), P enguin v Bird, Bird v F ly}, F ly(T weety)i
A2 = h{¬F ly(T weety), P enguin v Bird, Bird v F ly}, ¬P enguin(T weety)i
A3 = h{¬F ly(T weety), P enguin(T weety), P enguin v Bird}, Bird u ¬F ly(T weety)i
A4 = h{¬F ly(T weety), P enguin(T weety), Bird v F ly}, P enguin u ¬Bird(T weety)i
A5 = h{¬F ly(T weety)}, ¬F ly(T weety)i
A6 = h{P enguin(T weety), P enguin v ¬F ly}, ¬F ly(T weety)i
A7 = h{P enguin(T weety), P enguin v Bird, Bird v F ly}, P enguin u F ly(T weety)i
A8 = h{P enguin(T weety), P enguin v ∃HasF ood.F ish}, ∃HasF ood.F ish(T weety)i
A9 = h{P enguin(T weety), Swallow v ¬P enguin}, ¬Swallow(T weety)i
A10 = h{¬F ly(T weety), Bird v F ly}, ¬Bird(T weety)i
An argument hΦ, αi is more conservative than an argument hΨ, βi iff Φ ⊆ Ψ
and β |= α, written by hΨ, βi c hΦ, αi. If α 6|= β then hΦ, αi is called strictly more
conservative than an argument hΨ, βi, written by hΨ, βi ≺c hΦ, αi. In short, we define
a pre-order relationship on arguments using conservative relationship. For instance, the
argument A4 ≺c A10 in Example 1.
It is clear to conclude that A c h∅, >i for any argument A because the empty
ontology is consistent. In this paper, we mainly consider non-empty finite ontologies.
Definition 3 An argument hΨ, βi is a def eater of an argument hΦ, αi such that β |=∼
(φ1 ∧ . . . ∧ φn ) for some {φ1 , . . . , φn } ⊆ Φ. An undercut for an argument hΦ, αi is
an argument hΨ, ∼ (φ1 ∧ . . . ∧ φn )i where {φ1 , . . . , φn } ⊆ Φ.
In Example 1, the argument A5 is a defeater of the argument A1 and A7 ; the argu-
ment A2 , A3 , A4 are undercuts for the argument A1 .
Proposition 1 If A0 is a defeater for A then there exists an undercut A00 for A where
A0 c A00 .
Proof (skeleton). A0 is a defeater for A ⇒ there exists a subset {φ1 , . . . , φm } of
Support(A) such that Consequnece(A0 ) |=∼ (φ1 ∧ · · · ∧ φm ) ⇒ there exists a min-
imal subset Ψ of Support(A0 ) such that Ψ |=∼ (φ1 ∧ · · · ∧ φm ) ⇒ A00 = hΨ, ∼
(φ1 ∧ · · · ∧ φm )i is an undercut for A and A0 c A00 .
Two arguments hΦ, αi and hΨ, βi are equivalent iff Φ is logically equivalent to Ψ
and α is logically equivalent to β. Clearly, if two arguments are equivalent then either of
each is more conservative than the other or neither is. A0 is a maximally conservative
def eater of A iff A0 is a defeater of A for any defeater A00 for A such that A00 ≺c A0 .
A maximally conservative undercut of hΦ, αi is defined analogously. An argument
A0 is a canonical undercut of A iff A0 is a maximally conservative undercut of A.
In Example 1, the arguments A2 , A3 and A4 are canonical undercuts of A1 . The
argument A2 is a canonical undercut of A8 .
Proposition 2 hΨ, ∼ (φ1 ∧ · · · ∧ φn )i is a canonical undercut for an argument hΦ, αi
iff it is an undercut for hΦ, αi and {φ1 , . . . , φn } is the enumeration of Φ.
Proof (skeleton). (⇒) Suppose A0 = hΨ, ∼ (φ1 ∧ · · · ∧ φn )i is not a maximal con-
servative undercut for A = hΦ, αi ⇒ there exists undercut A00 such that A0 ≺c A00
⇒ Consequence(A00 ) |=∼ (φ1 ∧ · · · ∧ φn ) ⇒ there exists a new axiom φ which is
different from φi (1 ≤ i ≤ n) such that Consequence(A00 ) |=∼ (φ1 ∧ · · · ∧ φn ∧ φ)
while it conflicts this fact that {φ1 , . . . , φn } is the canonical enumeration of Φ. (⇐) It
follows similarly.
Proposition 3 Given an argument A, if A0 , A00 are different canonical undercuts for
A then the following claims hold: A0 6c A00 and A00 6c A0 ; Consequence(A0 ) =
Consequence(A00 ).
Proof (skeleton). The first property follows the definition of canonical undercut which
is a maximal conservative undercut. The second property follows Proposition 2 because
the canonical enumeration of a set of formulae is single.
Example 2 Given O = (∅, {C(a), D(a), ¬C(a), ¬D(a)}), both the following A11 =
h{¬C(a)}, ∼ (C u D)(a)i and A12 = h{¬D(a)}, ∼ (C u D)(a)i are canonical
undercuts for A13 = h{C(a), D(a)}, C u D(a)i, but neither is more conservative than
the other.
In Example 2, A11 and A12 are different canonical undercuts for h{C(a), D(a)},
C u D(a)i. Support(A11 ) is different from Support(A12 ) while Consequence(A11 )
is the same as Consequence(A12 ).
Therefore, by Proposition 3 Item 2, we denote hΨ, i denotes a canonical undercut
of hΦ, βi. We easily conclude that is ∼ (φ1 ∧ · · · ∧ φn ) where < φ1 , . . . , φn > is the
canonical enumeration for Φ.
Proposition 4 For each defeater A0 for an argument A, there exists a canonical un-
dercut A00 for A such that A0 c A00 .
Proof (skeleton). There exists a defeater A0 for an argument A ⇒ there exists an un-
dercut A00 for A such that A0 c A00 by Proposition 1 ⇒ if A00 is not a maximal
conservative undercut for A then there exists A00 c A3 for A till finding a maximal
conservative undercut Am for A, i.e., An is a canonical undercut for A.
4 Argumentative Framework
Definition 4 Given an axiom α, an argument tree for α is a tree where the nodes are
arguments such that
(1) the root is an argument for α;
(2) for no node hΦ, βi with ancestor nodes hΦ1 , β1 i . . . hΦn , βn i is Φ a subset of Φ1 ∪
. . . ∪ Φn ;
(3) the children nodes of a node A consist of all canonical undercuts for A, which
obeys (2).
Proposition 5 Any argument tree of an axiom α in a finite O is finite2 .
2
A tree is finite iff it has a finite number of branches and a finite depth.
Proof (skeleton). Since O is finite, the number of subsets of O is finite. In an argu-
ment tree, no branch can be infinite by Condition 2 of Definition4. Also, the number of
canonical undercuts is finite by its definition. The branching factor in an argument tree
is finite by Condition 3 of Definition 4.
Definition 5 An argumentative f ramework of an axiom α is a pair of sets hP, Ci
where P is the set of argument trees of α and C is the set of argument trees for ∼ α.
In Example 1, we obtain the argumentative framework hP, Ci of F ly(T weety) as
follows:
T1 : = AO 1 aCC
{{{ CC
{ CC
{{{ CC
{
A2 A3 A4
T2 : AO 5 T3 : A6 aC
{{= CC
{{ CC
{{ CC
{{ C
= AO 1 aCC = AO 7 aCC A2
{{{ CC {{{ CC
{{ CC {{ CC
{ CC { CC
{{ {{
A2 A3 A4 A2 A3 A4
Here T1 is an argument tree of F ly(T weety) and T2 , T3 are argument trees of
¬F ly(T weety). So the argumentative framework of F ly(T weety) is hh{T1 }, {T2 , T3 }ii.
Proposition 6 Given an argumentative framework hP, Ci, if O is consistent, then each
argument tree in P has exactly one node and C is the empty set.
Proof (skeleton). Given any axiom α, we only show that C of α is the empty set. Sup-
pose that C 6= ∅, i.e., there exists a successful argument tree T of ∼ α. The root of T
is a defeater of α. So there exists a canonical undercut A for α by Proposition 4. That
is to say, there exists an argument tree of α that contains at least two nodes. It conflicts
with Proposition 6.
5 Argumentative Semantics
If A1 , A2 and A3 are three arguments such that A1 is undercut by A2 and A2 is un-
dercut by A3 then A3 is called a defence for A1 . We define the “defend” relation as
the transitive closure of “being a defence”. An argument tree is said to be successful
iff every leaf defends the root node. The categorizer is a function, denoted by c, from
the set of argument trees to {0, 1} such that c(T ) = 1 iff T is successful. The cate-
gorization of a set of trees is the collections of their values by categorizer function on
them. The accumulator of a query α is a function, denoted by a, from categorizations
to the set {(1, 1), (1, 0), (0, 1), (0, 0)}. Let hX, Y i be a categorization of argumenta-
tive framework of an axiom α, then a(hX, Y i) = (w(X), w(Y )) where w(Z) = 1 iff
1 ∈ Z.
Definition 6 The valuation is a function, denoted by v, from a set of axioms to a set
{Both(B),True(T),False(F),Unknown(U)}, defined as follows:
(1) v(α) = B iff a(hX, Y i) = (1, 1);
(2) v(α) = T iff a(hX, Y i) = (1, 0);
(3) v(α) = F iff a(hX, Y i) = (0, 1);
(4) v(α) = U iff a(hX, Y i) = (0, 0);
where hX, Y i is a categorization of argumentative framework of α in O.
Definition 7 Let O be an ontology and α be an axiom in ALC. O argumentatively
entails α, denoted by O |=a α, iff there exists a successful argument tree of α.
Theorem 1 Given an ontology O and an axiom α, then the following properties are
equivalent:
(1) O |=a α;
(2) v(α) ∈ {B, T };
(3) there exists an argument tree T of α such that c(T ) = 1.
Proof (skeleton). O |=a α ⇔ there exists a successful tree T of α in O by Definition
7 ⇔ c(T ) = 1 by the definitions of accumulator ⇔ v(α) ∈ {B, T } by definition of
categorizer and valuation function.
Theorem 2 Given a consistent ontology O and an axiom α, then O |=a α iff O |= α.
Proof (skeleton). Because O is consistent, O |= α ⇔ the argumentative framework
hP, Ci of α whose each argument tree in P 6= ∅ has exactly one node and C is the
empty set by Proposition 6 ⇔ there exists a successful argument tree of α because its
contains only one node ⇔ O |=a α.
However, an ontology O is inconsistent, then |=a is weaker than |=. Clearly, O |=a ∼
α doesn’t possibly hold if O 6|=a α for any axiom α. O |=a β is not inferred from
O |=a α and O |=a ∼ α ∨ β. Since {α, ∼ α} 6|=a β for any query β, we conclude the
following theorem.
We say description logics with argumentative semantics argumentative description
logics (ADLs for short). It easily shows the following property holds.
Theorem 3 Argumentative description logic ALC is a paraconsistent logic.
6 Reasoning in Argumentative Description Logic ALC
In this section, we mainly discuss two basic reasoning problems argumentative satis-
fiability and queries argumentative entailment problem in argumentative ALC under
argumentative semantics.
Definition 8 A concept C is argumentatively satisf iable if there exists a successful
argument tree T of C(a) for some individual a; and argumentatively unsatisf iable
otherwise. An ontology O is argumentatively consistent iff each concept in O is
argumentatively satisfiable; and argumentatively inconsistent otherwise.
The following theorem shows the relationship between satisfiability and argumen-
tative satisfiability of concepts.
Theorem 4 If a concept C is satisfiable in an ontology O then the concept C is argu-
mentatively satisfiable in O.
Proof (skeleton). C is satisfiable in O ⇒ there exists a model I of C ⇒ by definition
of satisfiability of concept in DL ⇒ there exists an individual a such that a ∈ C I and
a 6∈ (¬C)I ⇒ there exists an argument tree of C(a) which contains only one node ⇒
there exists a successful argument tree of C(a) ⇒ C is argumentatively satisfiable in
O.
In Example 1, the concept ¬F ly is argumentatively satisfiable and other concepts
are not argumentatively satisfiable. and the ontology O is neither consistent nor argu-
mentatively consistent.
There are two basic query problems, namely instance checking and subsumption in
an ontology O under argumentative semantics.
– instance checking: given a concept C and an individual a, a is an instance of con-
cept under argumentative semantics iff O |=a C(a).
– subsumption: a concept C is subsumed by a concept D under argumentative se-
mantics iff O |=a C v D.
Two problems can be taken as argumentative entailment problems because a query
is a given axiom. By Theorem 2, two problems of instance checking and subsumption
in a consistent ontology is equivalent to the problems under argumentative semantics.
When an ontology O is inconsistent, some meaningful information can be mined after
reasoning with queries under argumentative semantics by analyzing and evaluating in-
consistency occurring in given ontologies. Compared with “satisfiability ” of queries in
ontologies with classical entailment, argumentative entailment considers “justifiability”
of queries in ontologies.
In Example 1, Since the accumulator of F ly(T weety) is (0, 1), v(¬F ly(T weey))
is “T ”. Therefore, O |=a ¬F ly(T weey) and O 6|=a F ly(T weey). Though O |=
F ly(T weety) and O |= ¬F ly(T weety), it shows that ¬F ly(T weety) is “justifiable”
in O because the fact ¬F ly(T weety) has other facts support it, while F ly(T weety) is
“unjustifiable”. In short, reasoning with argumentative semantics can justify a query by
analyzing other facts for and against the query in a given ontology, distinguishing from
answering the query by “true” or “false”.
7 Related Work
In this section, we mainly compare argumentative semantics for DLs with four-valued
semantics for DLs, ALC4 (see [5]). The similarities and differences between argumen-
tative DLs and four-valued DLs resemble those between argumentative logic and Bel-
nap’s four-valued logics respectively.
At first, we consider their similarities: (1) they are paraconsistent DLs; that is to say,
they don’t hold the fact ex contradictione quodlibet; and (2) the range of their valuation
function are {B, T, F, U }. Argumentative entailment |=a and four-valued entailment
|=4 are based on the subset {B, T } ⊆ {B, T, F, U }.
There are many differences between argumentative DLs and four-valued DLs as
follows: (1) argumentative DLs directly employs the reasoning system of DLs to im-
plement paraconsistent reasoning compared with four-valued DLs; (2) the scope of rea-
soning in argumentative DL is consistent subsets of an inconsistent ontology while the
scope of reasoning in four-valued DLs is a whole ontology; (3) there are some con-
cepts which are not argumentatively satisfiable while all concepts in four-valued DLs
are satisfiable; and (4) argumentation semantics is more outstanding than four-valued
semantics when an ontology contains a lot of inconsistent information.
8 Conclusions
The primary aim of this paper is to extend logic-based proposals for argumentation with
techniques for argumentative DLs. The most difficult problem of argumentative DLs is
that there exist many differences between DLs and other logics. We don’t directly define
the form of canonical undercuts in DLs by applying analogously the form of them in
propositional logic or first-order logic because the connectives ¬, u, t in syntax of DLs
aren’t logical connectives. In this paper, the main innovations in defining the form of
canonical undercut are summarized as follows: (1) compared to defining argument for
propositional logic or first-order logic in syntax, the notion of argument for description
logic is defined in semantics. An argument for DLs contains two part called Support
and Consequent where Support logically entails Consequent; (2) two logical connec-
tives ∧, ∨ are used to express the logical relationship between two axioms; and (3) a
negation transformation ∼ on axioms or conjunctions (disjunctions) of axioms called
quasi-negation is introduced to express the counterpart of these axioms or conjunctions
(disjunctions) of axioms.
Argumentative framework for ALC based on argument trees is inherited from El-
vang and Hunter’s argumentative framework [11]. Binary argumentation is developed
under the aim of capturing the simple form of argumentation in our framework be-
cause binary argumentation and four-valued logic have the same form of expression.
Argumentative entailments based on the set of values {B, T } holds the paraconsistent
property. In the end of the paper, we discuss serval basic problems that argumentative
satisfiability of concepts, argumentative consistency of ontologies, instance checking
and subsumption under argumentative semantics. Though argumentative semantics can
handle inconsistency in ALC, the main work of implementing paraconsistent reason-
ing with argumentative semantics is searching arguments. The problem of searching
arguments is difficult and has higher complexity. Efstathiou and Hunter [16] search for
arguments from propositional knowledge by applying a graph approach. However, the
problem of searching arguments for a query in a given ontology is still an open problem.
Finding an efficient approach to search arguments in DLs will be our future work.
Acknowledgements
The authors would like to thank Yue Ma, Kedian Mu, Guilin Qi, Shuang Ren and Guo-
hui Xiao for helpful comments and discussions. This work is supported by the major
program of the National Natural Science Foundation of China (NSFC).
References
1. Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description
logic terminologies. In: Proc. of IJCAI’03, Acapulco, Mexico, August 9-15, 2003, Morgan
Kaufmann (2003) 355–362
2. Huang, Z., van Harmelen, F., ten Teije, A.: Reasoning with inconsistent ontologies. In: Proc.
of IJCAI’05, Edinburgh, Scotland, UK, July 30-August 5, 2005, Professional Book Center
(2005) 454–459
3. Qi, G., Haase, P., Huang, Z., Ji, Q., Pan, J.Z., Völker, J.: A kernel revision operator for ter-
minologies - algorithms and evaluation. In: Proc. of ISWC’08, Karlsruhe, Germany, October
26-30, 2008. Volume 5318 of Lecture Notes in Computer Science., Springer (2008) 419–434
4. Patel-Schneider, P.F.: A four-valued semantics for terminological logics. Artif. Intell. 38(3)
(1989) 319–351
5. Ma, Y., Hitzler, P., Lin, Z.: Algorithms for paraconsistent reasoning with OWL. In: Proc. of
ESWC’07, Innsbruck, Austria, June 3-7, 2007. Volume 4519 of Lecture Notes in Computer
Science., Springer (2007) 399–413
6. Belnap, N.D.: A useful four-valued logic. Modern uses of multiple-valued logics (1977)
7–73
7. Zhang, X., Lin, Z.: Paraconsistent reasoning with quasi-classical semantic in ALC. In: Proc.
of RR’08, Karlsruhe, Germany, October 31-November 1, 2008. Volume 5341 of Lecture
Notes in Computer Science., Springer (2008) 222–229
8. Zhang, X., Xiao, G., Lin, Z.: A tableau algorithm for handling inconsistency in OWL. In:
Proc. of ESWC’09, Heraklion, Crete, Greece, May 31-June 4, 2009. Volume 5554 of Lecture
Notes in Computer Science., Springer (2009) 399–413
9. Benferhat, S., Dubois, D., Prade, H.: How to infer from inconsisent beliefs without revising?
In: Proc. of IJCAI’95, Montral, Qubec, Canada, August 20-25 1995. (1995) 1449–1457
10. Dung, P.M.: On the acceptability of arguments and its fundamental role in nonmonotonic
reasoning, logic programming and n-person games. Artif. Intell. 77(2) (1995) 321–358
11. Elvang-Gøransson, M., Hunter, A.: Argumentative logics: Reasoning with classically incon-
sistent information. Data Knowl. Eng. 16(2) (1995) 125–145
12. Hunter, A.: Making argumentation more believable. In: Proc. of AAAI’04, San Jose, Cali-
fornia, USA, July 25-29, 2004, AAAI Press / The MIT Press (2004) 269–274
13. Hunter, A.: Reasoning about the appropriateness of proponents for arguments. In: Proc. of
AAAI’08, Chicago, Illinois, USA, July 13-17, 2008, AAAI Press (2008) 89–94
14. Tempich, C., Simperl, E., Luczak, M., Studer, R., Pinto, H.S.: Argumentation-based ontology
engineering. IEEE Intelligent Systems 22(6) (2007) 52–59
15. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P., eds.: The De-
scription Logic Handbook: Theory, Implementation, and Applications. 2 edn. Cambridge
University Press (2007)
16. Efstathiou, V., Hunter, A.: Focused search for arguments from propositional knowledge.
In: Proc. of COMMA’08, Toulouse, France, May 28-30, 2008. Volume 172 of Frontiers in
Artificial Intelligence and Applications., IOS Press (2008) 159–170