{'fraction_non_alphanumeric': 0.04817837945450926, 'fraction_numerical': 0.011319359517647393, 'mean_word_length': 4.1899630996309964, 'pattern_counts': {'":': 1, '<': 6, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
An argumentation system for reasoning with conflict-minimal paraconsistent ALC

The semantic web is an open and distributed environment in which it is hard to guarantee consistency of knowledge and information. Under the standard two-valued semantics everything is entailed if knowledge and information is inconsistent. The semantics of the paraconsistent logic LP offers a solution. However, if the available knowledge and information is consistent, the set of conclusions entailed under the three-valued semantics of the paraconsistent logic LP is smaller than the set of conclusions entailed under the two-valued semantics. Preferring conflict-minimal three-valued interpretations eliminates this difference. Preferring conflict-minimal interpretations introduces non-monotonicity. To handle the non-monotonicity, this paper proposes an assumption-based argumentation system. Assumptions needed to close branches of a semantic tableaux form the arguments. Stable extensions of the set of derived arguments correspond to conflict minimal interpretations and conclusions entailed by all conflict-minimal interpretations are supported by arguments in all stable extensions.


Introduction
In the semantic web, the description logics SHOIN (D) and SROIQ(D) are the standard for describing ontologies using the TBox, and information using the Abox. Since the semantic web is an open and distributed environment, knowledge and information originating from different sources need not be consistent. In case of inconsistencies, no useful conclusion can be derived when using a standard two-valued semantics. Everything is entailed because the set of two-valued interpretations is empty. Resolving the inconsistencies is often not an option in an open and distributed environment. Therefore, methods that allow us to derive useful conclusions in the presence of inconsistencies are preferred.
One possibility to draw useful conclusions from inconsistent knowledge and information is by focussing on conclusions supported by all maximally consistent subsets. This approach was first proposed by Rescher (1964) and was subsequence worked out further by others (Brewka 1989;Roos 1988; Roos 1992). A simple implementation of this approach focusses on conclusions entailed by the intersection of all maximally consistent subsets. Instead of focussing on the intersection of all maximally consistent subsets, one may also consider a single consistent subset for each conclusion (Poole 1988; Huang, van Harmelen, and ten Teije 2005). For conclusions entailed by all (preferred) maximally consistent subsets of the knowledge and information, a more sophisticated approach is needed. An argumentation system for this more general case has been described by Roos (1992). Since these approaches need to identify consistent subsets of knowledge and information, they are non-monotonic.
A second possibility for handling inconsistent knowledge and information is by replacing the standard two-valued semantics by a three-valued semantics such as the semantics of the paraconsistent logic LP (Priest 1989). An important advantage of this paraconsistent logic over the maximally consistent subset approach is that the entailment relation is monotonic. A disadvantage is that consistent knowledge and information entail less conclusions when using the three-valued semantics than when using the two-valued semantics. Conflict-minimal interpretations reduce the gap between the sets of conclusions entailed by the two semantics (Priest 1989;Priest 1991). Priest (1991) calls resulting logic: LPm. The conflict-minimal interpretations also makes LPm non-monotonic (Priest 1991).
In this paper we present an argumentation system for conclusions entailed by conflict-minimal interpretations of the description logic ALC (Schmidt-Schauß and Smolka 1991) when using the semantics of the paraconsistent logic LP. We focus on ALC instead of the more expressive logics SHOIN (D) and SROIQ(D) to keep the explanation simple. The described approach can also be applied to more expressive description logics.
The proposed approach starts from a semantic tableaux method for the paraconsistent logic LP described by Bloesch (1993), which has been adapted to ALC. The semantic tableaux is used for deriving the entailed conclusions when using the LP-semantics. If a tableaux cannot be closed, the desired conclusion may still hold in all conflict-minimal interpretations. The open tableaux enables us to identify assumptions about conflict-minimality. These assumptions are used to construct an assumption-based argumentation system, which supports conclusions entailed by all conflict minimal interpretations.
The remainder of the paper is organized as follows. First, we describe ALC, a three-valued semantics for ALC based on the semantics of the paraconsistent logic LP, and a corre-sponding semantic tableaux method. Second, we describe how a semantic tableaux can be used to determine arguments for conclusions supported by conflict-minimal interpretations. Subsequently, we present the correctness and completeness proof of the described approach. Next we describe some related work. The last section summarizes the results and points out directions of future work.

Paraconsistent ALC
The language of ALC We first give the standard definitions of the language of ALC. We start with defining the set of concepts C given the atomic concepts C, the role relations R, the operators for constructing new concepts ¬, and , and the quantifiers ∃ and ∀. Moreover, we introduce to special concepts, and ⊥, which denote everything and nothing, respectively. Definition 1 Let C be a set of atomic concepts and let R be a set of atomic roles.
The set of concepts C is recursively defined as follows: • C ⊆ C; i.e. atomic concepts are concepts.
• ∈ C and ⊥ ∈ C. • If C ∈ C and D ∈ C, then ¬C ∈ C, C D ∈ C and C D ∈ C. • If C ∈ C and R ∈ R, then ∃R.C ∈ C and ∀R.C ∈ C. • Nothing else belongs to C.
In the description logic ALC, we have two operators: and =, for describing a relation between two concepts: Definition 2 If {C, D} ⊆ C, then we can formulate the following relations (terminological definitions): • C D; i.e., C is subsumed by D, • C = D; i.e., C is equal to D.
A finite set T of terminological definitions is called a TBox.
In the description logic ALC, we also have an operator ":", for describing that an individual from the set of individual names N is an instance of a concept, and that a pair of individuals is an instance of a role.
Definition 3 Let {a, b} ⊆ N be two individuals, let C ∈ C be a concept and let R ∈ R be a role. Then assertions are defined as: A knowledge base K = (T , A) is a tuple consisting of a TBox T and an ABox A. In this paper we will denote elements of the TBox and ABox T ∪ A as propositions.
We define a three-valued semantics for ALC which is based on the semantics of the paraconsistent logic LP . We do not use the notation I = (∆, · I ) that is often used for the semantics of description logics. Instead we will use a notation that is often used for predicate logic because it is more convenient to describe projections and truth-values. Definition 4 A three-valued interpretation I = O, π is a couple where O is a non-empty set of objects and π is an interpretation function such that: • for each atomic concept C ∈ C, π(C) = P, N where P, N ⊆ O are the positive and negative instances of the concept C, respectively, and where P ∪ N = O, • for each individual i ∈ N it holds that π(i) ∈ O, and • for each atomic role R ∈ R it holds that π(R) ⊆ O × O.
We will use the projections π(C) + = P and π(C) − = N to denote the positive and negative instances of a concept C, respectively.
We do not consider inconsistencies in roles since we cannot formulate inconsistent roles in ALC. In a more expressive logic, such as SROIQ, roles may become inconsistent, for instance because we can specify disjoint roles.
Using the three-valued interpretations I = O, π , we define the interpretations of concepts in C.
Definition 5 The interpretation of a concept C ∈ C is defined by the extended interpretation function π * .
, (x, y) ∈ π(R) and y ∈ π(C) − } Note that we allow inconsistencies in the concepts and ⊥. There may not exist a tree-valued interpretation for a knowledge-base K = (T , A) if we require that X = ∅. Consider for instance: a : C, a : D and C D ⊥.
We also use the extended interpretation function π * to define the truth values of the propositions: C D, a : C and (a, b) : R. The truth values of the three-valued semantics are defined using sets of the "classical" truth values: t and f . We use three sets in the LP-semantics: {t}, {f } and {t, f }, which correspond to TRUE, FALSE and CONFLICT.
Definition 6 Let {a, b} ⊆ N be two individuals, let C ∈ C be a concept and let R ∈ R be a role. Then an interpretation I = O, π of propositions is defined as: The interpretation of the subsumption relation given above was proposed by Patel-Schneider (1989) for their four-valued semantics. Patel-Schneider's interpretation of the subsumption relation does not correspond to the material implication ∀x[C(x) → D(x)] in first-order logic. The latter is equivalent to ∀x[¬C(x) ∨ D(x)] under the twovalued semantics, which corresponds to: "for every o ∈ O, o ∈ π * (C) − or o ∈ π * (D) + " under the three-valued semantics. No conclusion can be drawn from a : C and C D under the three-valued semantics since there always exists an interpretation such that π(a : C) = {t, f }.
The entailment relation can be defined using the interpretations of propositions. Definition 7 Let I = O, π be an interpretation, let ϕ be a proposition, and let Σ be a set of propositions. The the entailment relation is defined as:

Semantic tableaux
We use a semantic tableaux method that is based on the semantic tableaux method for LP described by Bloesch (1993). This tableaux method will enable us to identify the assumptions underlying relevant conflict minimal interpretations.
Based on Bloesch's semantic tableaux method for LP, the following tableaux rules have been formulated. The soundness and completeness of the set of rules are easy to prove.
The individual a in the following tableaux rules for the subsumption relation must be an existing individual name, while the individual x must be a new individual name. T An important issue is guaranteeing that the constructed semantic tableaux is always finite. The blocking method described by (Buchheit, Donini, and Schaerf 1993;Baader, Buchheit, and Hollander 1996) is used to guarantee the construction of a finite tableaux. A rule that is blocked, may not be not be used in the construction of the tableaux. Definition 8 Let Γ be a node of the tableau, and let x and y be two individual names. Moreover, let • y is blocked if there is an individual name x such that: x < + r y and Γ(y) ⊆ Γ(x), or x < r y and x is blocked.
Conflict Minimal Interpretations A price that we pay for changing to the three-valued LP-semantics in order to handle inconsistencies is a reduction in the set of entailed conclusions, even if the knowledge and information is consistent.
Example 1 The set of propositions Σ = {a : ¬C, a : C D} does not entail a : D because there exists an interpretation I = O, π for Σ such that π(a : C) = {t, f } and π(a : D) = {f }. Priest (1989;1991) points out that more useful conclusions can be derived from the paraconsistent logic LP if we would prefer conflict-minimal interpretations. The resulting logic is LPm. Here we follow the same approach. First, we define a conflict ordering on interpretations.
Definition 9 Let C be a set of atomic concepts, let N be a set of individual names, and let I 1 and I 2 be two threevalued interpretations. The interpretation I 1 contains less conflicts than the interpretation I 2 , denoted by I 1 < c I 2 , iff: {a : C | a ∈ N, C ∈ C, π 1 (a : C) = {t, f }} ⊂ {a : C | a ∈ N, C ∈ C, π 2 (a : C) = {t, f }} The following example gives an illustration of a conflict ordering for the set of propositions of Example 1. Example 2 Let Σ = {a : ¬C, a : C D} be a set of propositions and let I 1 , I 2 , I 3 , I 4 and I 5 be five interpretations such that: Using the conflict ordering, we define the conflict minimal interpretations.
Definition 10 Let I 1 be a three-valued interpretation and let Σ be a set of propositions.
I 1 is a conflict minimal interpretation of Σ, denoted by I 1 |= <c Σ, iff I 1 |= Σ and for no interpretation I 2 such that I 2 < c I 1 , I 2 |= Σ holds.
In Example 2, I 1 is the only conflict-minimal interpretation.
The conflict-minimal entailment of a proposition by a set of propositions can now be defined.
Definition 11 Let Σ = (T ∪ A) be a set of propositions and let ϕ be a proposition.
The conflict-minimal interpretations in Example 2 entail the conclusion a : D.
The subsumption relation The conflict-minimal interpretations enables us to use an interpretation of the subsumption relation based on the material implication.
This semantics of the subsumption relation resolves a problem with the semantics of Patel-Schneider (1989). Under Patel-Schneider's semantics, {a : C, a : ¬C, C D} entails a : D. This entailment is undesirable if information about a : C is contradictory.
The tableaux rules of the new interpretation are:

Arguments for conclusions supported by conflict minimal interpretations
The conflict-minimal interpretations of a knowledge base entail more useful conclusions. Unfortunately, focusing on conclusions supported by conflict-minimal interpretations makes the reasoning process non-monotonic. Adding the assertion a : ¬D to the set of propositions in Example 2 eliminates interpretations I 1 and I 3 , which includes the only conflict-minimal interpretation I 1 . The interpretations I 2 and I 4 are the new conflict-minimal interpretations. Unlike the original conflict-minimal interpretation I 1 , the new conflict-minimal interpretations I 2 and I 4 do not entail a : D.
Deriving conclusions supported by the conflictminimal interpretations is problematic because of the non-monotonicity. The modern way to deal with nonmonotonicity is by giving an argument supporting a conclusion, and subsequently verifying whether there are no counter-arguments (Dung 1995). Here we will follow this argumentation-based approach.
We propose an approach for deriving arguments that uses the semantic tableaux method for our paraconsistent logic as a starting point. The approach is based on the observation that an interpretation satisfying the root of a semantic tableaux will also satisfy one of the leafs. Now suppose that the only leafs of a tableaux that are not closed; i.e., leaf in which we do not have "Tα and Tα" or "Fα and Fα" or "Tα and Fα", are leafs in which "Tα and Fα" holds for some proposition α. So, in every open branch of the tableaux, Cα holds for some proposition α. If we can assume that there are no conflicts w.r.t. each proposition α in the conflict-minimal interpretations, then we can also close the open branches. The set of assumptions Cα, equivalent to "Tα or Fα", that we need to close the open branches, will be used as the argument for the conclusion supported by the semantic tableaux.
An advantage of the proposed approach is that there is no need to consider arguments if a conclusion already holds without considering conflict-minimal interpretations.
A branch that can be closed assuming that the conflictminimal interpretations contain no conflicts with respect to the proposition α; i.e., assuming Cα, will be called a weakly closed branch. We will call a tableaux weakly closed if some branches are weakly closed and all other branches are closed. If we can (weakly) close a tableaux for Γ = {Tσ | σ ∈ (T ∪ A)} ∪ Tϕ, we consider the set of assumptions Cα needed to weakly close the tableaux, to be the argument supporting Σ |= ≤c ϕ. Example 3 gives an illustration.
Example 3 Let Σ = {a : ¬C, a : C D} be a set of propositions. To verify whether a : D holds, we may construct the following tableaux: T a : D × Only the left branch is weakly closed in this tableau. We assume that the assertion a : C will not be assigned CON-FLICT in any conflict-minimal interpretation. That is, we assume that C a : C holds.
In the following definition of an argument, we consider arguments for Tϕ and Fϕ. The next step is to verify whether the assumptions: Cα i are valid. If one of the assumptions does not hold, we have a counter-argument for our argument supporting Σ |= ≤c ϕ. To verify the correctness of an assumption, we add the assumption to Σ. Since an assumption Cα is equivalent to: "Tα or Fα", we can consider Tα and Fα separately. Example 4 gives an illustration for the assumption C a : C used in Example 3.
Example 4 Let Σ = {a : ¬C, a : C D} be a set of propositions. To verify whether the assumption C a : C holds in every conflict minimal interpretation, we may construct a tableaux assuming T a : C and a tableaux assuming F a : C: The right branch of the first tableaux cannot be closed. Therefore, the assumption T a : C is valid, implying that the assumption C a : C is also valid. Hence, there exists no counter-argument.
Since the validity of assumptions must be verified with respect to conflict-minimal interpretations, assumptions may also be used in the counter-arguments. This implies that we may have to verify whether there exists a counter-argument for a counter-argument. Example 5 gives an illustration. T a : D × This weakly closed tableaux implies the argument A 0 = ({C a : C}, T a : D). Next, we have to verify whether there exists a counter-argument for A 0 . To verify the existence of a counter-argument, we construct two tableaux, one for T a : C and one for F a : C. As we can see below, both tableaux are (weakly)-closed, and therefore form the counter-argument A 1 = ({C a : D, C a : E}, C a : C). We say that the argument A 1 attacks the argument A 0 because the former is a counter-argument of the latter. Argument A 1 is equivalent to two other arguments, namely: A 2 = ({C a : C, C a : E}, C a : D) and A 3 = ({C a : C, C a : D}, C a : E). A proof of the equivalence will be given in the next section, Proposition 1.
The arguments A 2 and A 3 implied by A 1 are both counter-arguments of A 1 . Moreover, A 1 is a counterargument of A 2 and A 3 , and A 2 and A 3 are counterarguments of each other. No other counter-arguments can be identified in this example. Figure 1 show all the arguments and the attack relation, denoted by the arrows, between the arguments. We will now formally define the arguments and the attack relations that we can derive from the constructed semantic tableaux.
Definition 13 Let Σ be set of propositions and let Cα ="Tα or Fα" be an assumption in the argument A. Moreover, let T 1 be a (weakly) closed semantic tableaux with root Γ 1 = {Tσ | σ ∈ Σ} ∪ Tα and let T 2 be a (weakly) closed semantic tableaux with root Γ 2 = {Tσ | σ ∈ Σ} ∪ Fα. Finally, let {Cα 1 , . . . , Cα k } be the set of assumptions on which the weakly closed branches in the tableaux T 1 or the tableaux T 2 are based.
Then A = ({Cα 1 , . . . , Cα k }, Cα) is a counter-argument of the argument A. We say that the argument A attacks the argument A, denoted by: A −→ A.
The form of argumentation that we have here is called assumption-based argumentation (ABA), which has been developed since the end of the 1980's (Bondarenko et al.  Roos 1992).
Example 5 shows that an argument can be counterargument of an argument and vice versa; e.g., arguments A 2 and A 3 . This raises the question which arguments are valid. Argumentation theory and especially the argumentation framework (AF) introduced by Dung (1995) provides an answer.
Arguments are viewed in an argumentation framework as atoms over which an attack relation is defined. Figure 1 shows the arguments and the attack relations between the arguments forming the argumentation framework of Example 5. The formal specification of an argumentation framework is given by the next definition.
Definition 14 An argumentation framework is a couple AF = (A , −→) where A is a finite set of arguments and −→⊆ A × A is an attack relation over the arguments.
For convenience, we extend the attack relation −→ to sets of arguments.
Definition 15 Let A ∈ A be an argument and let S , P ⊆ A be two sets of arguments. We define: Dung (1995) describes different argumentation semantics for an argumentation framework in terms of sets of acceptable arguments. These semantics are based on the idea of selecting a coherent subset E of the set of arguments A of the argumentation framework AF = (A , −→). Such a set of arguments E is called an argument extension. The arguments of an argument extension support propositions that give a coherent description of what might hold in the world. Clearly, a basic requirement of an argument extension is being conflict-free; i.e., no argument in an argument extension attacks another argument in the argument extension. Besides being conflict-free, an argument extension should defend itself against attacking arguments by attacking the attacker.
Definition 16 Let AF = (A , −→) be an argumentation framework and let S ⊆ A be a set of arguments.
Not every conflict-free set of arguments that defends itself, is considered to be an argument extension. Several additional requirements have been formulated by Dung (1995), resulting in three different semantics: the stable, the preferred and the grounded semantics.
Definition 17 Let AF = (A , −→) be an argumentation framework and let E ⊆ A .
• E is a stable extension iff E is conflict-free,and for every argument A ∈ (A \ E ), E −→ A; i.e., E defends itself against every possible attack by arguments in A \E .
• E is a preferred extension iff E is maximal (w.r.t. ⊆) set of arguments that (1) is conflict-free,and (2) E defends every argument A ∈ E . • E is a grounded extension iff E is the minimal (w.r.t. ⊆) set of arguments that (1) is conflict-free, (2) defends every argument A ∈ E , and (3) contains all arguments in A it defends.
We are interested in stable semantics. We will show in the next section that stable extensions correspond to conflictminimal interpretations. More specifically, we will prove that a conclusion supported by an argument in every stable extension, is entailed by every conflict-minimal interpretation, and vice versa.
Is it possible that a conclusion is supported by a different argument in every stable extension? The answer is Yes, as is illustrated by Example 6. In this example we have two arguments supporting the conclusion a : E, namely A 0 and A 1 . As can be seen in Figure 2, there are two stable extensions of the argumentation framework. One extension contains the argument A 0 and the other contains the argument A 1 . So, in every extension there is an argument supporting the conclusion a : E. Hence, Σ |= ≤c a : E. T a : E

×
The assumption C a : C in argument A 0 makes it possible to determine a counter-argument A 2 = ({C a : D}, C a : C) using of the following two tableaux: is also a counter-argument of A 3 . Figure 2 shows the attack relations between the arguments A 0 , A 1 , A 2 and A 3 . Figure 2: The attack relations between the arguments of Example 6.
Example 7 gives an illustration of the semantic interpretations of Example 6. The example shows two conflictminimal interpretations. These conflict-minimal interpretations correspond with the two stable extensions. Interpretation I 1 entails a : E because I 1 must entail a : C E and I 1 does not entail a : C, and interpretation I 2 entails a : E because I 2 must entail a : D E and I 2 does not entail a : D. Example 7 Let Σ = {a : ¬C, a : C D, a : ¬D, a : C E, a : D E} be a set of propositions. There are two conflict-minimal interpretations containing the following interpretation functions: In both interpretations a : E is entailed.

Correctness and completeness proofs
In this section we investigate whether the proposed approach is correct. That is whether a proposition supported by an argument in every stable extension is entailed by every conflict-minimal interpretation. Moreover, we investigate whether the approach is complete. That is, whether a proposition entailed by every conflict-minimal interpretation is supported by an argument in every stable extension.
In the following theorem we will use the notion of "a complete set of arguments relevant to ϕ". This set of arguments A consists of all argument A supporting ϕ, all possible counter-arguments, all possible counter arguments of the counter-arguments, etc. Definition 18 A complete set of arguments A relevant to ϕ satisfies the following requirements: • If A ∈ A and B is a counter-argument of A that we can derive, then B ∈ A and (B, A) ∈ −→. Theorem 1 (correctness and completeness) Let Σ be a set of propositions and let ϕ be a proposition. Moreover, let A be a complete set of arguments relevant to ϕ, let −→⊆ A × A be the attack relation determined by A , and let (A , −→) be the argumentation framework. Finally, let E 1 , . . . , E k be all stable extensions of the argumentation framework (A , −→).
Σ entails the proposition ϕ using the conflict-minimal three-valued semantics; i.e., Σ |= ≤c ϕ, iff ϕ is supported by an argument in every stable extension E i of (A , −→).
To prove Theorem 1, we need the following lemmas. In these lemmas we will use the following notations: We will use I |= Tα to denote that t ∈ I(α) ( I |= α ), and I |= Fα to denote that f ∈ I(α). Moreover, we will use Σ |= Tα and Σ |= Fα to denote that Tα and Fα, respectively, hold in all three-valued interpretations of Σ.
The first lemma proves the correctness of the arguments in A .
Lemma 1 (correctness of arguments) Let Σ be a set of propositions and let ϕ be a proposition. Moreover, let L be either the label T or F.
Hence, the lemma holds. 2 The above lemma implies that the assumptions of an argument A = ({Cα 1 , . . . , Cα k }, Lϕ) together with Σ entail the conclusion of A. The next lemma proves the completeness of the set of arguments A .
Lemma 2 (completeness of arguments) Let Σ be a set of propositions and let ϕ be a proposition. Moreover, let L be either the label T or F.
Hence, the lemma holds. 2 The above lemma implies that we can find an argument A = ({Cα 1 , . . . , Cα k }, Lϕ) for any set of assumption that, together with Σ, entails a conclusion Lϕ.
The following lemma proves that for every conflict Cϕ entailed by a conflict-minimal interpretation, we can find an argument supporting Cϕ of which the assumptions are entailed by the conflict-minimal interpretation. Lemma 3 Let Σ be a set of propositions and let I = O, π be a conflict-minimal interpretation of Σ. Moreover, let ϕ be a proposition.
Proof Let I be a conflict-minimal interpretation of Σ.
Suppose that I |= Cϕ holds. We can construct a tableaux for: Suppose that this tableaux is not strongly closed. Then there is an interpretation I = O, π satisfying the root Γ. Clearly, I < c I because for every a : C with C ∈ C, if π(a : C) = {t, f }, then π (a : C) = {t, f }. Since I is a conflict-minimal interpretation and since I |= Cϕ, we have a contradiction. Hence, the tableaux is closed. Since the tableaux with root Γ is closed, we can identify all assertions in {C a : C | C ∈ C, π(a : C) = {t, f }} that are not used to close a leaf of the tableaux. These assertions C a : C play no role in the construction of the tableaux and can therefore be removed from every node of the tableaux. The result is still a valid and closed semantic tableaux with a new root Γ . The assertions in {C a : C | C ∈ C, π(a : C) = {t, f }} ∩ Γ must all be used to strongly close leafs of the tableaux Γ , and also of Γ. A leaf that is strongly closed because of C a : C can be closed weakly under the assumption C a : C. So, we may remove the remaining assertions C a : C from the root Γ . The result is still a valid semantic tableaux with root Γ = {Tσ | σ ∈ Σ} ∪ {Cϕ}. This tableaux with root Γ is weakly closed, and by the construction of the tableaux, I |= C a : C holds for every assumption C a : C implied by a weak closure. Hence, we have constructed an argument A = ({Cα 1 , . . . , Cα k }, Cϕ) supporting Cϕ and for every assumption Cα i , I |= Cα i holds.
Hence, the lemma holds. 2 For the next lemma we need the following definition of a set of assumptions that is allowed by an extension.

Definition 19
Let Ω be the set of all assumptions Cα in the arguments A . For any extension E ⊆ A , is the set of assumptions allowed by the extension E .
The last lemma proves that for every conflict-minimal interpretation there is a corresponding stable extension. Lemma 4 Let Σ be a set of propositions and let ϕ be a proposition. Moreover, let A be the complete set of arguments relevant to ϕ, let −→⊆ A × A be the attack relation determined by A , and let (A , −→) be the argumentation framework.
For every conflict-minimal interpretation I of Σ, there is a stable extension E of (A , −→) such that I |= Ω(E ).
Proof Let I be a conflict-minimal interpretation and let Suppose E is not conflict-free. Then there is an argument B ∈ E such that B −→ A with A ∈ E . So, B supports Cψ and Cψ is an assumption of A. Since I entails the assumptions of A, I |= Cψ. Since I is a conflictminimal interpretation of Σ entailing the assumptions of B, according to Lemma 1, I |= Cψ. Contradiction.
Hence, E is a conflict-free set of argument.
Suppose that there exists an argument A ∈ A such that A ∈ E . Then, for some assumption Cα of A, I |= Cα. So, I |= Cα, and according to Lemma 3, there is an argument B ∈ E supporting Cα. Therefore, B −→ A.
Hence, E attacks every argument A ∈ A \E . Since E is also conflict-free, E is a stable extension of (A , −→).
Hence, I |= Ω(E ). 2 Using the results of the above lemmas, we can now prove the theorem.
Suppose that there is stable extension E i that does not contain an argument for ϕ. Then according to Lemma 2, {Tσ | σ ∈ Σ} ∪ Ω(E i ) |= Tϕ. So, there exists an interpretation I such that I |= {Tσ | σ ∈ Σ} ∪ Ω(E i ) but I |= Tϕ. There must also exists a conflict-minimal interpretation I of Σ and I ≤ c I. Since the assumptions C a : C ∈ Ω(E i ) all state that there is no conflict concerning the assertion a : C, I |= Ω(E i ) must hold. So, I is a conflict-minimal interpretation of Σ and I |= Ω(E i ) but according to Lemma 2, I |= Tϕ. This implies Σ |= ≤c ϕ. Contradiction.
Hence, every stable extension E i contains an argument for ϕ.
(⇐) Let ϕ be supported by an argument in every stable extension E i .
Suppose that Σ |= ≤c ϕ. Then there is a conflict-minimal interpretation I of Σ and I |= ϕ. Since I is a conflictminimal interpretation of Σ, according to Lemma 4, there is a stable extension E i and I |= Ω(E i ). Since E i contains an argument A supporting ϕ, the assumptions of A must be a subset of Ω(E i ), and therefore I satisfies these assumptions. Then, according to Lemma 1, I |= ϕ. Contradiction.
Hence, Σ |= ≤c ϕ. 2 In Example 5 in the previous section, we saw that one counter-argument implies multiple counter-arguments. The following proposition formalizes this observation.

Related Works
Reasoning in the presences of inconsistent information has been addressed using different approaches. Rescher (1964) proposed to focus on maximal consistent subsets of an inconsistent knowledge-base. This proposal was further developed by (Brewka 1989 (1992) defines a preferential semantics (Kraus, Lehmann, and Magidor 1990;Makinson 1994;Shoham 1987) entailing the conclusions that are entailed by every preferred maximal consistent subsets, and provides an assumption-based argumentation system capable of identifying the entailed conclusions. Paraconsistent logics form another approach to handle inconsistent knowledge bases. Paraconsistent logics have a long history starting with Aristotle. From the beginning of the twentieth century, paraconsistent logics were developed by Orlov (1929), Asenjo (1966), da Costa (1974), Belnap (1977), Priest (1989) and others. For a survey of several paraconsistent logics, see for instance (Middelburg 2011).
This paper uses the semantics of the paraconsistent logic LP (Priest 1989;Priest 1991) as starting point. Belnap's four-values semantics (1977) differs from the LP semantics in allowing the empty set of truth-values. Belnap's semantics was adapted to description logics by Patel-Schneider (1989). Ma et al. (2006;2008; extend Patel-Schneider's work to more expressive description logics, and propose two new interpretations for the subsumption relation. Qiao and Roos (2011) propose another interpretation.
A proof theory based on the semantic tableaux method was first introduced by Beth (1955). The semantic tableaux methods have subsequently been developed for many logics. For an overview of several semantic tableaux methods, see (Hähnle 2001). Bloesch (1993) developed a semantic tableaux method for the paraconsistent logics LP and Belnap's 4-valued logic. This semantic tableaux method has been used as a starting point in this paper.
Argumentation theory has its roots in logic and rhetoric. It dates back to Greek philosophers such as Aristotle. Modern argumentation theory started with the work of Toulmin (1958). In Artificial Intelligence, the use of argumentation was promoted by authors such as Pollock (1987), Simari and Loui (1992), and others. Dung (1995) introduced the argumentation framework (AF) in which he abstracts from the structure of the argument and the way the argument is derived. In Dung's argumentation framework, arguments are represented by atoms over which an attack relation is defined. The argumentation framework is used to define an argumentation semantics in terms of sets of conflictfree arguments that defend themselves against attacking arguments. Dung defines three semantics for argumentation frameworks: the grounded, the stable and the preferred semantics. Other authors have proposed additional semantics to overcome some limitations of these three semantics. For an overview, see (Bench-Capon and Dunne 2007).
This paper uses a special type argumentation system called assumption-based argumentation (ABA). Assumption-based argumentation has been developed since the end of the 1980's (Bondarenko et al. 1997;Bondarenko, Toni, and Kowalski 1993;Gaertner and Toni 2007;Roos 1988;Roos 1992). Dung et al. (2009) formalized assumption-based argumentation in terms of an argumentation framework.

Conclusions
This paper presented a three-valued semantics for ALC, which is based on semantics of the paraconsistent logic LP. An assumption-based argumentation system for identifying conclusions supported by conflict-minimal interpretations was subsequently described. The assumption-based arguments are derived from open branches of a semantic tableaux. The assumptions close open branches by assuming that some proposition will not be assigned the truth-value CONFLICT. No assumptions are needed if conclusions hold is all three-valued interpretations. The described approach has also been implemented.
In future work we intend to extend the approach to the description logic SROIQ. Moreover, we wish to investigate the computational efficiency of our approach in handling inconsistencies.