Leila Amgoud

Farid Nouioua

An argumentation system for defeasible reasoning 1

Keywords: Defeasible reasoning, Rule-based systems, Argumentation

Rule-based argumentation systems are developed for reasoning about defeasible information. They take as input a theory made of a set of facts, a set of strict rules, which encode strict information, and a set of defeasible rules which describe general behavior with exceptional cases. They build arguments by chaining such rules, define attacks between them, use a semantics for evaluating the arguments, and finally identify the plausible conclusions that follow from the theory.

Undercutting is one of the main attack relations of such systems. It consists of blocking the application of defeasible rules when their exceptional cases hold. In this paper, we consider this relation for capturing all the different conflicts in a theory. We present the first argumentation system that uses only undercutting, and show that it satisfies the rationality postulates proposed in the literature. Finally, we fully characterize both its extensions and its plausible conclusions under various acceptability semantics. Indeed, we show full correspondences between extensions and sub-theories of the theory under which the argumentation system is built.

Introduction

Argumentation is a promising approach for reasoning with conflicting information [START_REF] Bondarenko | An abstract, argumentationtheoretic approach to default reasoning[END_REF]. It consists of generating arguments, defining attacks between them, evaluating the arguments using a semantics, then identifying plausible conclusions.

In the computational argumentation literature, there are two families of semantics: extension semantics, initiated in [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF], and ranking semantics, introduced in [START_REF] Amgoud | Ranking-based semantics for argumentation frameworks[END_REF]. The first family looks for sets of arguments, called extensions, that are acceptable together. Then, an absolute acceptability degree (accepted or rejected) is assigned to each argument on the basis of its extensions membership. Ranking semantics look for rank-ordering arguments from the most to the least acceptable ones. The ranking may come from the comparison of pairs or sets of arguments, or from degrees assigned to arguments, etc. Gradual semantics from [START_REF] Cayrol | Graduality in argumentation[END_REF] are a sub-class of ranking semantics. In this paper, we focus on extension semantics, in particular those proposed in [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF].

Dung proposed in [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] various semantics at an abstract level, i.e., without taking into account the structure of arguments or the nature of attacks. His abstract framework was instantiated by several scholars. The idea is as follows. Start with a knowledge base whose elements are encoded in a logical language, generate arguments using the consequence operator attached to the language, identify the attacks and apply Dung's semantics for the evaluation task. There are two major categories of instantiations for this abstract framework. The first category uses deductive logics (such as propositional logic [START_REF] Amgoud | Inferring from inconsistency in preference-based argumentation frameworks[END_REF][START_REF] Gorogiannis | Instantiating abstract argumentation with classical logic arguments: Postulates and properties[END_REF] or any Tarskian logic [START_REF] Amgoud | Logical limits of abstract argumentation frameworks[END_REF]) whereas the second category uses rule-based languages.

Rule-based argumentation systems, which use rule-based languages, are developed for reasoning about defeasible information. As a major feature, they take as input a theory made of three types of information: facts, strict rules, which encode general strict information, and defeasible rules which describe general behavior with exceptional cases. They build arguments by chaining such rules, define attacks between them, use a semantics for evaluating the arguments, and finally identify the plausible conclusions that follow from the theory. Examples of such systems are ASPIC [START_REF] Amgoud | Towards a consensual formal model: inference part[END_REF], its extended version ASPIC+ [START_REF] Prakken | An abstract framework for argumentation with structured arguments[END_REF], DeLP [START_REF] García | Defeasible logic programming: an argumentative approach[END_REF] and the systems developed in [START_REF] Governatori | Argumentation semantics for defeasible logic[END_REF][START_REF] Wyner | On the instantiation of knowledge bases in abstract argumentation frameworks[END_REF][START_REF] Wyner | Senses of 'argument' in instantiated argumentation frameworks[END_REF][START_REF] Strass | Instantiating knowledge bases in abstract dialectical frameworks[END_REF]. Some of these systems satisfy the rationality postulates proposed in [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF]. However, their plausible conclusions have never been characterized. In other words, they have never been expressed in a way that clarifies how they are chosen among all the possible conclusions that follow from the theory. Thus, despite the wide use of these systems, their outputs are still unknown.

The system DeLP uses rebuttal as attack relation. Rebuttal captures the fact that the conclusions of two arguments are conflicting. Systems like ASPIC [START_REF] Amgoud | Towards a consensual formal model: inference part[END_REF] and Pollock's system [START_REF] Pollock | How to reason defeasibly[END_REF] use, in addition to rebuttal, undercut which blocks the application of defeasible rules in particular contexts. Let us illustrate this relation by an example borrowed from [START_REF] Pollock | How to reason defeasibly[END_REF]. Consider the following argument A:

The object is red (or) because it looks red (lr).

The argument A uses the defeasible rule lr ⇒ or (meaning that generally, if an object looks red, then it is red). Assume now the following argument B:

The defeasible rule lr ⇒ or is not applicable because the object is illuminated by a red light.

The argument B undercuts A and the conclusion (or) of A does not hold. Undercut deals with the exceptions of defeasible rules. Indeed, every exception of a defeasible rule gives birth to an attack from any argument concluding the exception toward any argument using the rule. In the example, being illuminated by a red light is a specific case where the rule lr ⇒ or cannot be applied.

In this paper, we show that undercut can do more than dealing with exceptions of defeasible rules. It can also perfectly play the role of rebuttal and assumption attack [START_REF] Elvang-Gøransson | Acceptability of arguments as 'logical uncertainty[END_REF], and deals thus with inconsistency in a theory. The basic idea is the following: any defeasible rule x ⇒ y should be blocked when ¬y follows from the theory. We propose the first rule-based argumentation system that uses undercutting as its single attack relation. We show that it satisfies the rationality postulates discussed in [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF] under naive, complete, grounded, stable and preferred semantics. From a conceptual point of view, this system is much simpler than existing ones that combine rebuttal and undercut. Indeed, in order to satisfy the postulates, ASPIC requires one variant of rebuttal per semantics: unrestricted rebut is used under grounded semantics and restricted rebut is used under complete and preferred semantics. Our system satisfies the postulates under all semantics. Moreover, restricted rebut is based on an assumption which is not intuitive. Indeed, this relation compares only the rules whose heads are inconsistent, and neglects the remaining structure of the arguments. For instance, it considers that the argument (x 1 , x 1 ⇒ y 1 , y 1 → z) attacks the argument (x 2 , x 2 → y 2 , y 2 ⇒ ¬z) since z follows from a strict rule while ¬z follows from a defeasible one. Note that the converse is not true even if the first rule of the first argument is defeasible while that of the second argument is strict. Our system does not make such assumptions.

The second main contribution of the paper consists of providing the first and full characterizations of the extensions as well as the set of plausible conclusions of our system under all the semantics proposed in [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. Indeed, we show one-to-one correspondences between extensions and sub-theories of the theory over which the argumentation system is built. We also show that the plausible conclusions are the formulas that follow from all the sub-theories characterizing the extensions under a given semantics. These correspondences ensure the correctness and completeness of the outcomes of the proposed system.

The paper is organized as follows: Section 2 defines the rule-based system we are interested in. Section 3 analyses its properties, namely it shows that the system satisfies the existing rationality postulates as well as a new one. Section 4 charac-terizes its outputs (extensions and plausible conclusions), and Section 5 compares it with existing rule-based systems and concludes.

Rule-based argumentation system

As in any paper in defeasible reasoning (e.g. [START_REF] Amgoud | A formal characterization of the outcomes of rulebased argumentation systems[END_REF][START_REF] Benferhat | Contextual handling of conditional knowledge[END_REF][START_REF] Lam | What are the necessity rules in defeasible reasoning?[END_REF]), three kinds of information are distinguished: Facts representing factual information like 'Tweety is a bird', strict rules representing general information which do not have exceptions like 'Penguins do not fly' and defeasible rules describing general behaviors with exceptional cases like 'Birds fly'. In other words, any rule which has exceptions is considered as defeasible.

In what follows, L is a set of literals, i.e. atoms or negation of atoms, representing knowledge. The negation of an atom x from L is denoted by ¬x. L ′ is a set of atoms used for naming rules. The two sets satisfy the constraint L ∩ L ′ = ∅. Every rule has a single name and two rules cannot have the same name. Throughout the paper, rules are named r, r 1 , r 2 , . . . . The function Rule(r i ) returns the rule whose name is r i .

Facts are elements of L.

Defeasible rules are of the form x 1 , . . . , x n ⇒ x and x, x 1 ..., x n are literals in L. Such rules are read as follows: If x 1 , . . . , x n hold, then generally x holds as well.

Strict rules are of the form x 1 , . . ., x n → x where x 1 , . . ., x n are literals of L and x ∈ L or x ∈ L ′ and Rule(x) is defeasible.

These rules are read as follows: If x 1 , . . . , x n hold, then always x holds as well.

Note that defeasible rules may have an empty body, i.e. the set {x 1 ..., x n } may be empty. However, strict rules are not allowed to have empty bodies. The reason is that a strict rule with an empty body represents a fact and thus a factual information and not a general behavior with no exceptions. Furthermore, the names of rules cannot appear in bodies of (strict or defeasible) rules. This means that it is not possible to represent information of the form "if rule r is applied (or is blocked), then y holds". We also assume that a strict rule cannot be blocked since it represents certain information (i.e., if its body holds, then necessarily its head holds as well). Things are different with defeasible rules. By default, any defeasible rule can be applied, unless explicitly mentioned in the language by strict rules. Indeed, a strict rule x 1 , . . ., x n → x with x ∈ L ′ is read as follows: If x 1 , . . . , x n hold, then the defeasible rule x is always not applicable.

Definition 1 (Theory).

A theory is a triple T = (F, S, D) where F ⊆ L is a set of facts, and S ⊆ L ′ (respectively D ⊆ L ′ ) is a set of strict (defeasible) rule names.

It is worth pointing out that the two sets S and D contain names of rules and not the rules themselves.

Notations: For each rule x 1 , . . . , x n → x (as well as x 1 , . . . , x n ⇒ x) whose name is r, the head of the rule is Head(r) = x and the body of the rule is Body(r) = {x 1 , . . . , x n }. Let T = (F, S, D) and T ′ = (F ′ , S ′ , D ′ ) be two theories. We say that T is a sub-theory of T ′ , written T ⊑ T ′ , iff F ⊆ F ′ and S ⊆ S ′ and D ⊆ D ′ . The relation ⊏ is the strict version of ⊑ (i.e., it is the case that at least one of the three inclusions is strict). Finally, let Defs(T ) = D.

We show how new information is produced from a given theory. This is generally the case when (strict and/or defeasible) rules are fired in a derivation schema. Definition 2 (Derivation schema). Let T = (F, S, D) be a theory and x ∈ L ∪ L ′ . A derivation schema for x from T is a finite sequence d = (x 1 , r 1 ), . . . , (x n , r n ) such that:

x n = x for i ∈ {1, . . . , n},
x i ∈ F and r i = ∅, or r i ∈ S ∪ D and Head(r i ) = x i and Body(r i ) ⊆ {x 1 , .., x i-1 }

Seq(d) = {x 1 , . . . , x n }. Facts(d) = {x i | i ∈ {1, . . . , n}, r i = ∅}. Strict(d) = {r i | i ∈ {1, . . . , n}, r i ∈ S}. Def(d) = {r i | i ∈ {1, . . . , n}, r i ∈ D}.

CN(T ) denotes the set of all literals that have a derivation schema from T .

It is clear from the definition that CN is monotonic.

Example 1. Let T 1 = (F 1 , S 1 , D 1 ) be a theory such that F 1 = {p, b}, S 1 = {r 1 } and D 1 = {r 2 }
where Rule(r 1 ) = p → ¬f and Rule(r 2 ) = b ⇒ f . From T 1 , we have the following minimal derivations:

d 1 = (p, ∅) d 2 = (b, ∅) d 3 = (p, ∅), (¬f, r 1 ) d 4 = (b, ∅), (f, r 2 )
A notion of consistency and another of coherence are associated with this logical language.

Definition 3 (Consistency-Coherence

). A set X ⊆ L is consistent iff ∄x, y ∈ X such that x = ¬y. It is inconsistent otherwise. A theory T = (F, S, D) is consistent iff CN(T ) is consistent. It is coherent iff CN(T ) ∩ D = ∅.
The set of strict rules should be closed under transposition. However, only rules whose head is an element of L (i.e., not a name of a rule) are transposed. Transposition is required for ensuring the rationality postulates proposed in [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF].

Definition 4 (Closure under transposition).

A transposition of a strict rule x 1 , . . ., x n → x, with x ∈ L, is a strict rule x 1 , . . ., x i-1 , ¬x, x i+1 , . . ., x n → ¬x i for some 1 ≤ i ≤ n. Let S be a set of strict rules' names. We define Cl t (S) as the minimal set such that:

S ⊆ Cl t (S), and If r ∈ Cl t (S) and Rule(r ′ ) is a transposition of Rule(r) then r ′ ∈ Cl t (S).
We say that S is closed under transposition iff Cl t (S) = S.

Throughout the paper, we will consider undercut for capturing all the possible conflicts between arguments. Thus, undercut will be used both for blocking general rules in presence of exceptions of these rules, and also for handling inconsistency. For that purpose, for each defeasible rule whose name is r, the theory should contain the name of the strict rule ¬Head(r) → r. The latter is read as follows: if ¬Head(r) follows from a theory, then the rule r should be blocked. This closure captures simply the fact that the two literals Head(r) and ¬Head(r) cannot hold at the same time.

Definition 5 (Closed theory). A theory T = (F, S, D) is closed iff

S is closed under transposition, and for every r ∈ D such that Head(r) = x, it holds that r ′ ∈ S with Rule(r ′ ) = ¬x → r.

Example 1 (Cont) The closed version of T

1 is T ′ 1 = (F 1 , S ′ 1 , D 1 ) such that S ′ 1 = {r 1 , r 3 , r 4 } where Rule(r 1 ) = p → ¬f , Rule(r 3 ) = f → ¬p, and Rule(r 4 ) = ¬f → r 2 .
The backbone of an argumentation system is naturally the notion of arguments. They are built from a closed theory using the notion of derivation schema. Definition 6 (Argument). Let T = (F, S, D) be a closed theory. An argument defined from T is a pair (d, x) such that:

x ∈ L ∪ L ′ d is a derivation schema for x from T ∄T ′ ⊏ (Facts(d), Strict(d), Def(d)) such that x ∈ CN(T ′ ) An argument (d, x) is strict iff Def(d) = ∅.
Unlike ASPIC and ASPIC+ systems, arguments are minimal in our system. This definition of argument is more akin with the intuitive idea that an argument is a logical proof of a conclusion.

An argument may have several sub-parts, each of which is called sub-argument.

Th(E) = ( (d,x)∈E Facts(d), (d,x)∈E Strict(d), (d,x)∈E Def(d)).
The undercutting relation is defined as follows:

Definition 8 (Undercutting). Let T = (F, S, D) be a closed theory and

(d, x), (d ′ , x ′ ) ∈ Arg(T ). The argument (d, x) undercuts the argument (d ′ , x ′ ), denoted by (d, x) R u (d ′ , x ′ ), iff x ∈ Def(d ′ ).
Let us illustrate this relation by some examples.

Example 1 (Cont)

The set Arg(T ′ 1 ) contains: Obviously, strict arguments cannot be attacked using this relation.

Proposition 1. Let T = (F, S, D) be a theory. For any argument a ∈ Arg((F, S, ∅)), ∄b ∈ Arg(T ) such that bR u a.

Note that self-attacking arguments may exist.

Example 2. Consider the closed theory

T 2 = (F 2 , S 2 , D 2 ) such that F 2 = {p}, S 2 = {r 1 , r 2 }, D 2 = {r 3 } with Rule(r 1 ) = t → r 3 , Rule(r 2 ) = ¬t → r 3 and Rule(r 3 ) = p ⇒ t.
The set Arg(T 2 ) contains the three arguments:

a 1 : ( (p, ∅) , p)
a 2 : ( (p, ∅), (t, r 3 ) , t) a 3 : ( (p, ∅), (t, r 3 ), (r 3 , r 1 ) , r 3 )

The argument a 3 undercuts itself and a 2 .

Throughout the paper, we study the following rule-based argumentation system.

Definition 9 (AS). An argumentation system (AS) defined over a closed theory T = (F, S, D) is a pair H = (Arg(T ), R u ) where R u ⊆ Arg(T ) × Arg(T ) and R u is defined according to Definition 8.

Arguments are evaluated using extension-based semantics proposed by Dung is his seminal paper [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. These semantics are based on two key notions:

Conflict-freeness: A set E of arguments is conflict-free iff ∄a, b ∈ E such that aR u b.
Defence: A set E of arguments defends an argument a iff for any argument b such that bR u a, ∃c ∈ E such that cR u b.

Let us now recall the semantics that will be used for evaluating the arguments of any argumentation system (in the sense of Definition 9). Definition 10 (Semantics). Let H = (Arg(T ), R u ) be an argumentation system defined over a closed theory T , and let E ⊆ Arg(T ).

E is a naive extension iff it is a maximal (with respect to set inclusion) conflict-free subset of Arg(T ).

E is a complete extension iff it is a conflict-free set which defends all its elements and contains any argument it defends.

E is a preferred extension iff it is a maximal (with respect to set inclusion) complete extension.

E is a stable extension iff E is conflict-free and ∀a ∈ Arg(T ) \ E, ∃b ∈ E such that bR u a.

E is a grounded extension iff it the minimal (with respect to set inclusion) complete extension.

Notations: Ext y (H) denotes the set of all extensions of system H under semantics y where y ∈ {n, p, s, c, g}, n (respectively p, s, c, g) stands for naive (respectively preferred, stable, complete, grounded).

It is worth recalling that an argumentation system may not have stable extensions, and it has a single grounded extension.

The extensions of a system are used for defining the plausible conclusions to be drawn from the theory over which the system is built. A literal is a plausible conclusion iff it is a common conclusion to all the extensions. Note that a similar definition was used in [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF] for drawing conclusions with ASPIC system.

Definition 11 (Plausible conclusions)

. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T = (F, S, D). The set of plausible conclusions of H under semantics y (y ∈ {n, p, s, c, g}) is

Output y (H) = ∅ if Ext y (H) = ∅ E i ∈ Exty(H) Concs(E i ) else.
It is worth noticing that an argumentation system aims at weakening the inference power of the consequence operator CN from which the system is built. Indeed, the inclusion Output y (H) ⊆ CN(T ) holds. As we will see later, when the theory T is consistent and coherent the equality Output y (H) = CN(T ) holds under any of the recalled semantics. Note also that when the argumentation system has no extensions, it does not recommend any conclusion as plausible.

Example 1 (Cont) The argumentation system H 1 = (Arg(T ′ 1 ), R u ) has a single stable extension which is also preferred:

E = {a 1 , a 2 , a 3 , a 4 }. Thus, Output s (H 1 ) = Output p (H 1 ) = {p, b, ¬f, r 2 }.
Example 2 (Cont) The argumentation system H 2 = (Arg(T 2 ), R u ) has a single preferred extension: E = {a 1 } and thus Output p (H 2 ) = {p}. However under stable semantics, Output s (H 2 ) = ∅ since Ext s (H) = ∅.

Remark: One may wonder why admissible semantics is not investigated in this paper. The main reason is that, as shown by Dung himself in his paper [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF], the emptyset is an admissible extension of any argumentation system. Consequently, according to Definition 11, the set of plausible conclusions of any argumentation system is always empty (Output(H) = ∅) whatever the theory at hand. Even if the theory T = (F, S, D) over which the system is built is consistent, the system will not be able to infer any conclusion, missing thus intuitive conclusions. This shows that admissible semantics is not suitable for defeasible reasoning.

Satisfaction of rationality postulates

Let us now analyze the properties of the argumentation system defined in the previous section. We show that it satisfies all the rationality postulates proposed in [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF], namely consistency, indirect consistency, and closure under strict rules. Recall that indirect inconsistency follows from the two other postulates.

Under complete, grounded, preferred and stable semantics, every extension returns a consistent set of conclusions (unless the strict part of the theory is inconsistent) and the set of conclusions of every extension is closed under strict rules, that is, it is not possible that an extension supports a conclusion x and forgets y if x → y ∈ S. However, both properties are violated under naive semantics. This is not surprising since naive semantics does not take into account the orientation of attacks, and thus the distinction between strict and defeasible rules is neglected. Theorem 1. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T = (F, S, D) such that Ext y (H) = ∅ with y ∈ {s, p, c, g}. For any E ∈ Ext y (H), the following two properties hold:

Concs(E) is consistent iff CN((F, S, ∅)) is consistent.
(Consistency)

Concs(E) = CN((Concs(E), S, ∅)). (Closure under strict rules) CN((Concs(E), S, ∅)) is consistent iff CN((F, S, ∅)) is consistent. (Indirect Consistency)
The following properties follow from the previous theorem.

Corollary 1. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T = (F, S, D) such that Ext y (H) = ∅ with y ∈ {s, p, c, g}. The following two properties hold:

Output y (H) is consistent iff CN((F, S, ∅)) is consistent, Output y (H) = CN((Output y (H), S, ∅)).
In [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF][START_REF] Amgoud | Postulates for logic-based argumentation systems[END_REF] another desirable property, closure under sub-arguments, was discussed. It states that every extension should contain all the sub-arguments of its arguments. Hopefully, our system satisfies this property under all the reviewed semantics. It also satisfies a novel property of coherence, which ensures that it is not possible for an extension to use a defeasible rule in one of its arguments, and at the same time to block that rule by another argument.

Theorem 2. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T = (F, S, D) such that Ext y (H) = ∅, where y ∈ {n, p, s, c, g}.

For any E ∈ Ext y (H), the following two properties hold:

For each a ∈ E, Sub(a) ⊆ E.
(Closure under sub-arguments)

The theory

Th(E) is coherent. (Coherence)
The previous results show that the outcomes of the new argumentation system (its extensions and set of plausible conclusions) satisfy nice properties under grounded, complete, stable and preferred semantics. However, they do not say anything about the kind of conclusions the system draws from a theory. We answer this question in the next section in which we provide full characterizations of the system's outcomes.

Formal characterization of extensions and plausible conclusions

This section provides formal characterizations of the outcomes of the system under the five reviewed semantics. For each semantics, we characterize the extensions in terms of sub-theories of the theory over which the system is built. Indeed, we show one-to-one correspondences between extensions (under a given semantics) and particular sub-theories of the theory over which the system is built. In other words, we show that extensions and those sub-theories are the two faces of the same coin. We also delimit the number of extensions, and characterize the set of plausible conclusions. As we will see an argumentation system may return different results under the studied semantics.

Naive semantics

A sub-theory that corresponds to a naive extension is called naive option. A naive option represents the possible states of the world that may be reached in a theory. Formally, it is a maximal (for set inclusion) sub-theory of the initial theory that considers all the facts and all the strict and defeasible rules that are applicable (i.e., their bodies hold).

Definition 12 (Naive option). A naive option of a closed theory

T = (F, S, D) is a sub-theory (F ′ , S ′ , D ′ ) such that F ′ = F, S ′ ⊆ S and D ′ ⊆ D (F ′ , S ′ , D ′ ) is coherent ∀r ∈ S ′ ∪ D ′ , Body(r) ⊆ CN((F ′ , S ′ , D ′ )) ∄S ′′ , D ′′ such that (F ′ , S ′ , D ′ ) ⊏ (F ′ , S ′′ , D ′′ ) and (F ′ , S ′′ , D ′′ ) satisfies the previous conditions.

NOpt(T ) denotes the set of naive options of the closed theory T .

Thus, a naive option is obtained by taking all the facts and a maximal (w.r.t. set inclusion) subset of (strict and defeasible) rules so that the sub-theory remains coherent and all the added rules are applicable. Notice that no priority is given to strict rules over defeasible ones. This is explained by the fact that naive semantics does not distinguish between attackers and attacked arguments.

Example 3. Consider the closed version of theory

T 3 = (F 3 , S 3 , D 3 ) where F 3 = {x, y}, S 3 = {r 4 , r 5 , r 6 }, D 3 = {r 1 , r 2 , r 3 }, Rule(r 1 ) = x ⇒ t, Rule(r 2 ) = y ⇒ u, Rule(r 3 ) = t ⇒ s, Rule(r 4 ) = t → r 2 , Rule(r 5 ) = u → r 1 ,

and

Rule(r 6 ) = s → r 3 . The theory T 3 has three naive options:

O n0 = (F 3 , ∅, {r 1 , r 2 , r 3 }) CN(O n0 ) = {x, y, t, u, s} O n1 = (F 3 , {r 4 }, {r 1 , r 3 }) CN(O n1 ) = {x, y, t, s, r 2 } O n2 = (F 3 , {r 5 }, {r 2 }) CN(O n2 ) = {x, y, u, r 1 }
Let us now establish the relationship between the naive extensions of an argumentation system and the naive options of the closed theory over which the system is built. Each naive extension returns one naive option and two naive extensions cannot return the same naive option. Theorem 3. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T .

For any E ∈ Ext n (H), there exists a single naive option O ∈ NOpt(T ) such that Th(E) = O and Concs(E) = CN(O). We define NOption(E)

def = O. For all E, E ′ ∈ Ext n (H), if NOption(E) = NOption(E ′ ) then E = E ′ .
For any E ∈ Ext n (H), E = Arg(NOption(E)).

The following theorem shows that inversely, each naive option leads to one naive extension and two different naive options cannot return the same naive extension.

Theorem 4. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T .

For any O ∈ NOpt(T ), Arg(O) ∈ Ext n (H). For any O ∈ NOpt(T ), O = NOption(Arg(O)). For all O 1 , O 2 ∈ NOpt(T ), if Arg(O 1 ) = Arg(O 2 ), then O 1 = O 2 .
Let us illustrate the two results on the running example.

Example 3 (Cont)

The arguments built from T 3 are summarized below.

a 1 : ( (x, ∅) , x)
a 2 : ( (y, ∅) , y) a 3 : ( (x, ∅), (t, r 1 ) , t) a 4 : ( (x, ∅), (t, r 1 ), (r 2 , r 4 ) , r 2 ) a 5 : ( (y, ∅), (u, r 2 ) , u) a 6 : ( (y, ∅), (u, r 2 ), (r 1 , r 5 ) , r 1 ) a 7 : ( (x, ∅), (t, r 1 ), (s, r 3 ) , s) a 8 : ( (x, ∅), (t, r 1 ), (s, r 3 ), (r 3 , r 6 ) , r 3 )

The graph of attacks is depicted in Figure 1. It is easy to check that the argumentation system H 3 = (Arg(T 3 ), R u ) has three naive extensions: The previous results show a bijection between naive options and naive extensions. Since any argumentation system always admits at least one naive extension (since at least arguments of the form (p, ∅) where p ∈ F are not attacked), a closed theory admits at least one naive option (unless the set of facts is empty). The number of naive extensions is delimited as follows.

E 0 = {a 1 , a 2 , a 3 , a 5 , a 7 }, E 1 = {a 1 , a 2 , a 3 , a 4 , a 7 } and E 2 = {a 1 , a 2 , a 5 , a 6 } which capture the naive options O n0 , O n1 and O n2 respectively. Indeed, Th(E 0 ) = O n0 (resp. Th(E 1 ) = O n1 , Th(E 1 ) = O n1 ) and Concs(E 0 ) = CN(O n0 ) (resp. Concs(E 1 ) = CN(O n1 ), Concs(E 2 ) = CN(O n2 )).
Corollary 2. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory

T . It holds that |Ext n (H)| = |NOpt(T )|.
The plausible conclusions of an argumentation system under naive semantics are the literals that follow from all the naive options of the theory over which the system is built. Formally: Corollary 3. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T .

Output n (H) =

O∈NOpt(T ) CN(O). Example 3 (Cont) Under naive semantics, Output n (H) = CN(O n0 ) ∩ CN(O n1 ) ∩ CN(O n2 ) = {x, y}.
To conclude, under naive semantics, a rule-based argumentation system infers the literals that follow from all the options of the closed theory over which the system is built.

Stable semantics

The purpose of this section is to characterize the extensions as well as the set of plausible conclusions of the system described in this paper under stable semantics. As we will show later, the sub-theories of a closed theory that capture stable extensions are called stable options and are defined as follows:

Definition 13 (Stable Option). A stable option of a closed theory

T = (F, S, D) is a sub-theory (F ′ , S ′ , D ′ ) such that F ′ = F, S ′ = S and D ′ ⊆ D (F ′ , S ′ , D ′ ) is coherent ∀r ∈ D ′ , Body(r) ⊆ CN((F ′ , S ′ , D ′ )) ∀r / ∈ D ′ we have: either r ∈ CN((F ′ , S ′ , D ′ )) or ∃x ∈ Body(r) such that x / ∈ CN((F ′ , S ′ , D ′ ))
SOpt(T ) denotes the set of stable options of theory T .

The strict rules of a stable option O = (F, S, D ′ ) are not necessarily all applicable. Let S ′′ be the subset of strict rules that are applicable in O, i.e., S ′′ = {r ∈ S | Body(r) ⊆ CN(O)}. Then, the sub-theory O ′ = (F, S ′′ , D ′ ) is a naive option of T which clearly has the same conclusions as O (i.e., CN(O) = CN(O ′ )). In addition, every strict (respectively defeasible) rule r which is kept outside O ′ is not applicable (respectively is not applicable or is such that r ∈ CN(O ′ )). The latter constraint does not hold necessarily for every naive option. Accordingly, every stable option corresponds to a single naive option but the converse is not true. Thus, in addition to an "internal condition" (coherence) satisfied by both naive options and stable options, the latter require an additional "external condition" which consists of justifying each rule kept outside. Notice, that this idea is not new in non-monotonic reasoning. We find it namely in the distinction between Reiter's extensions [START_REF] Reiter | A logic for default reasoning[END_REF] and Lukaszewicz's extensions [START_REF] Lukaszewicz | Considerations on default logic : An alternative approach[END_REF] in default logic as well as between answer sets [START_REF] Gelfond | Classical negation in logic programs and disjunctive databases[END_REF] and ι-answer sets [START_REF] Gebser | Monotonic answer set programming[END_REF] in logic programming. Let us illustrate stable options and their relationship with naive options.

Example 3 (Cont)

The closed theory T 3 has one stable option O = (F 3 , S 3 , {r 2 }). Note that the only strict rule in S 3 which is applicable for O is r 5 . If we discard from O the remaining non-applicable strict rules, we get exactly the naive option O n2 and CN(O) = CN(O n2 ). Note also that each rule which is not included in O n2 is justified. Namely, the strict rules r 4 and r 6 are note applicable (t ∈ Body(r 4 ), t / ∈ CN(O n2 ), s ∈ Body(r 6 ), and s / ∈ CN(O n2 )); the defeasible rule r 1 is such that r 1 ∈ CN(O n2 ) and the defeasible rule r 3 is not applicable (t ∈ Body(r 3 ) and t / ∈ CN(O n2 )). So O n2 gives rise to a stable option by adding all the non-applicable strict rules. This is not the case for O n0 and O n1 . Indeed, adding the missing strict rules to them leads to incoherent sub-theories.

It is worthy to say that a closed theory may not have stable options. This is not surprising since as we will show, there is a bijection between the set of stable extensions and the set of stable options. Indeed, every stable extension gives birth to a stable option and two stable extensions cannot return the same stable option. Theorem 5. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T such that Ext s (H) = ∅.

For any E ∈ Ext s (H), there exists a single stable option O ∈ SOpt(T ) such that Th(E) ⊑ O and Concs(E) = CN(O). We define SOption(E)

def = O. For all E, E ′ ∈ Ext s (H), if SOption(E) = SOption(E ′ ) then E = E ′ . For any E ∈ Ext s (H), E = Arg(SOption(E)).
Inversely, every stable option leads to one stable extension and two stable options cannot lead to the same stable extension. Theorem 6. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T such that Ext s (H) = ∅.

For any O ∈ SOpt(T ), Arg(O) ∈ Ext s (H). For any O ∈ SOpt(T ), O = SOption(Arg(O)). For all O 1 , O 2 ∈ SOpt(T ), if Arg(O 1 ) = Arg(O 2 ) then O 1 = O 2 .
Example 3 (Cont) Among the three naive extensions of the argumentation system H 3 built from T 3 , the only stable extension is E 2 = {a 1 , a 2 , a 5 , a 6 } which captures the stable option O = (F 3 , S 3 , {r 2 }). Indeed, Th(E 2 ) ⊑ O and Concs(E 2 ) = CN(O).

We have seen so far that there is a one to one correspondence between naive (respectively stable) extensions and naive options (respectively stable options). We have also shown that every stable option is a sub-theory of one naive option. Thus, the number of stable extensions of a rule-based system is delimited as follows.

Corollary 4. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T . The following inequalities hold:

|Ext s (H)| = |SOpt(T )| ≤ |NOpt(T )|.
Under stable semantics, the plausible conclusions of an argumentation system are the literals that follow from all the stable options of the theory over which the system is built. Let us summarize: The rule-based argumentation system defined in the previous section may not have stable extensions, in which case it may miss intuitive conclusions like facts. When the system has stable extensions, it returns exactly the literals that follow from all the stable options of the closed theory at hand.

Preferred semantics

Preferred semantics was proposed in [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] in order to palliate the limit of stable semantics which does not guarantee the existence of extensions. The family of argumentation systems we are investigating in this paper suffers from this drawback. Preferred semantics guarantees extensions. We show next that the sub-theories that capture preferred extensions are the so-called preferred options.

Definition 14 (Preferred Option).

A preferred option of a closed theory T = (F, S, D) is a sub-theory (F ′ , S ′ , D ′ ) s.t.

F ′ = F, S ′ = S and D ′ ⊆ D (F ′ , S ′ , D ′ ) is coherent ∀r ∈ D ′ , Body(r) ⊆ CN((F ′ , S ′ , D ′ )) ∀D ′′ ⊆ D, if ∃r ′ ∈ D ′ such that r ′ ∈ CN(F, S, D ′′ ) then ∃r ′′ ∈ D ′′ such that r ′′ ∈ CN(F, S, D ′ ) ∄D ′′ such that D ′ ⊂ D ′′
Op 0 = (F 3 , S 3 , ∅), Op 1 = (F 3 , S 3 , {r 2 }), Op 2 = (F 3 , S 3 , {r 1 }).
The maximal ones (that satisfy also the last condition of Definition 16) are Op 1 and Op 2 . Notice that Op 1 is exactly the unique stable option of T 3 . The other preferred option Op 2 captures a sub-part of the naive option O 2 = (F 3 , {r 4 }, {r 1 , r 3 }). Indeed, by keeping in Op 2 only the strict rues that are applicable we obtain: Op ′ 2 = (F 3 , {r 4 }, {r 1 }). We have :

Op ′ 2 ⊑ O 2 and CN(Op 2 ) = CN(Op ′ 2 ) ⊆ CN(O 2 ).
The following theorem shows that every preferred extension leads to a single preferred option.

Theorem 7. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T .

For any E ∈ Ext p (H), there exists a single preferred option O ∈ POpt(T )

s.t. Th(E) ⊑ O and Concs(E) = CN(O). We define POption(E) def = O. For all E, E ′ ∈ Ext p (H), if POption(E) = POption(E ′ ) then E = E ′ .
For any E ∈ Ext p (H), E = Arg(POption(E)).

Inversely, every preferred option corresponds to a single preferred extension and two preferred options cannot return the same preferred extension.

For all O 1 , O 2 ∈ POpt(T ), if Arg(O 1 ) = Arg(O 2 ) then O 1 = O 2 .
Example 3 (Cont) The argumentation system H 3 constructed from the theory T 3 has two preferred extensions:

Ep 1 = {a 1 , a 2 , a 5 , a 6 }, Ep 2 = {a 1 , a 2 , a 3 , a 4 }.
They capture the preferred options Op 1 and Op 2 respectively. Indeed, Th(Ep 1 ) ⊑ Op 1 (resp. Th(Ep 2 ) ⊑ Op 2 ) and Concs(Ep

1 ) = CN(Op 1 ) (resp. Concs(Ep 2 ) = CN(Op 2 )).
The number of preferred extensions of an argumentation system H is exactly the number of preferred options of the closed theory over which the system is built. Corollary 6. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T . The following property holds:

|Ext p (H)| = |POpt(T )|.
The plausible conclusions of an argumentation system, under preferred semantics, are the literals that follow from all the preferred options of the theory at hand.

Corollary 7.

Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T .

Output p (H) =

O∈POpt(T ) CN(O). Example 3 (Cont) Output p (H 3 ) = CN(Op 1 ) ∩ CN(Op 2 ) = {x, y}.
Unlike stable semantics, facts are always plausible consequences under preferred semantics.

Complete semantics

Let us now define the sub-theories corresponding to complete extensions, we call them complete options.

Definition 15 (Complete Option).

A complete option of a closed theory T = (F, S, D) is a sub-theory (F ′ , S ′ , D ′ ) s.t.

F ′ = F, S ′ = S and D ′ ⊆ D (F ′ , S ′ , D ′ ) is coherent ∀r ∈ D ′ , Body(r) ⊆ CN((F ′ , S ′ , D ′ )) ∀D ′′ ⊆ D, if ∃r ′ ∈ D ′ such that r ′ ∈ CN(F, S, D ′′ ) then ∃r ′′ ∈ D ′′ such that r ′′ ∈ CN(F, S, D ′ ) ∀r / ∈ D ′ , ∀D 1 ⊆ D such that r ∈ D 1 and Body(r) ⊆ CN(F, S, D 1 ), ∃D ′′ ⊆ D, D 1 ∩ CN(F, S, D ′′ ) = ∅ and ∀r ′′ ∈ D ′′ , r ′′ / ∈ CN(F ′ , S ′ , D ′ )
COpt(T ) denotes the set of complete options of theory T .

Example 3 (Cont) Consider again the closed theory T 3 . There are three complete options of T 3 :

Oc 0 = (F 3 , S 3 , ∅), Oc 1 = (F 3 , S 3 , {r 2 }), Oc 2 = (F 3 , S 3 , {r 1 }).
Let us show for instance that Oc 0 is a complete option of T 3 . The first four conditions are clearly satisfied. Let us show that the fifth condition holds for the three rules We show that every complete extension leads to a complete option and two complete extensions cannot return the same complete option. Theorem 9. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T .

For any E ∈ Ext c (H), there exists a single complete option O ∈ COpt(T )

such that Th(E) ⊑ O and Concs(E) = CN(O). Let COption(E) def = O. For all E, E ′ ∈ Ext c (H), if COption(E) = COption(E ′ ) then E = E ′ .
For any E ∈ Ext c (H), E = Arg(COption(E)).

Inversely, every complete option corresponds to a single complete extension and two complete options cannot return the same complete extension.

For all O 1 , O 2 ∈ COpt(T ), if Arg(O 1 ) = Arg(O 2 ) then O 1 = O 2 .
Example 3 (Cont) The argumentation system H 3 constructed from T 3 has three complete extensions:

Ec 0 = {a 1 , a 2 }, Ec 1 = {a 1 , a 2 , a 5 , a 6 } and Ec 2 = {a 1 , a 2 , a 3 , a 4 }.
They capture the complete options Oc 0 , Oc 1 and Oc 2 respectively. Indeed, Th(Ec 0 ) ⊑ Oc 0 (resp. Th(Ec 1 ) ⊑ Oc 1 , Th(Ec 2 ) ⊑ Oc 2 ) and Concs(Ec 0 ) = CN(Oc 0 ) (resp. Concs(Ec 1 ) = CN(Oc 1 ), Concs(Ec 2 ) = CN(Oc 2 )).

From the bijection between the set of complete extensions and the set of complete options, it follows that the number of complete extensions of an argumentation system H is exactly the number of complete options of the theory over which the system is built. Corollary 8. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T . It holds that

|Ext c (H)| = |COpt(T )|.
The plausible conclusions of an argumentation system, under complete semantics, are the literals that follow from all the complete options of the theory at hand. Corollary 9. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T .

Output c (H) =

O∈COpt(T ) CN(O). Example 3 (Cont) Output c (H 3 ) = CN(Oc 0 ) ∩ CN(Oc 1 ) ∩ CN(Oc 2 ) = {x, y}.

Grounded semantics

We introduce in this section the sub-theory, called grounded option, which corresponds to the grounded extension of an argumentation system. It is the minimal (for set inclusion) complete option.

Definition 16 (Grounded Option).

The grounded option of a closed theory T = (F, S, D) is the sub-theory (F ′ , S ′ , D ′ ) such that

(F ′ , S ′ , D ′ ) is a complete option, ∄D ′′ ⊂ D ′ such that (F ′ , S ′ , D ′′ ) is a complete option.

GOpt(T ) denotes the grounded option of theory T .

Example 3 (Cont)

There are three complete options of T 3 : Oc 0 = (F 3 , S 3 , ∅), Oc 1 = (F 3 , S 3 , {r 2 }) and Oc 2 = (F 3 , S 3 , {r 1 }). Clearly, Oc 3 is the grounded option (i.e., GOpt(T 3 ) = Oc 3 ) since it has the minimal (wrt set inclusion) set of defeasible rules. Now, let us show that the grounded extension leads to the grounded option, and from the grounded option, one can get the grounded extension.

Stable Option Naive Option Preferred Option

Complete Option

Grounded Option Theorem 11. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T . Let E be the grounded extension of H. The following two properties hold.

Th(E) ⊑ GOpt(T ) and Concs(E) = CN(GOpt(T )). E = Arg(GOpt(T )).

Example 3 (Cont)

The grounded extension of the system H 3 constructed from T 3 is: E = {a 1 , a 2 }. It captures the grounded option Oc 3 . Indeed, Th(E) ⊑ Oc 3 and Concs(E) = CN(Oc 3 ).

The plausible conclusions of an argumentation system, under grounded semantics, are the literals that follow from the grounded option of the theory at hand. Corollary 10. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T . Output g (H) = CN(GOpt(T )).

Example 3 (Cont) Output g (H 3 ) = CN(Oc 3 ) = {x, y}.

Relationships between the different kinds of options and their outputs

From the one to one correspondences established in theorems 3-11, it follows that the same well-known relationships between the extensions of the five semantics exist between the five families of options. Figure 2 depicts the relationships between the different kinds of options and their outputs. A plain (respectively dotted) arrow from X-Option to Y-Options means that every X option is a Y Option (respectively Output X (.) ⊆ Output Y (.)).

Conclusion

There are a couple of rule-based argumentation systems in the literature. Some of them like ASPIC and its extended version ASPIC+ are shown to satisfy the rationality postulates defined in [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF], namely the consistency and closure under strict rules of their sets of plausible conclusions. While this is testimony to some strength of these formalisms, it does not say anything about the kind of plausible conclusions they draw from a theory. Surprisingly, the outputs of these systems (their extensions and their plausible conclusions) have never been characterized. The authors of those systems provide only examples to show that the outputs are meaningful. This is certainly not sufficient. Our paper is the first that attempts a systematic study of the outcomes of rule-based systems under naive, grounded, complete, stable and preferred semantics. There are two notable exceptions. The first work, done in [START_REF] Amgoud | A formal characterization of the outcomes of rulebased argumentation systems[END_REF], considered a fragment of our logical language and rebuttal as attack relation. Blocking rules was not allowed. Extensions were characterized in terms of sub-theories. However, some sub-theories may not have corresponding extensions. Thus, there is no bijection between the two. Our formalism is thus more general and our characterizations of its outcomes are more accurate since they are one-to-one correspondences. The second work, done in [START_REF] Caminada | On the equivalence between logic programming semantics and argumentation semantics[END_REF][START_REF] Caminada | On the equivalence between logic programming semantics and argumentation semantics[END_REF], investigated the link between logic programming semantics and argumentation ones. The theory over which an argumentation system is built is a logic program, that is, only one type of rules is used. The paper shows that Dung's semantics have counterparts in logic programming. Another well-known argumentation system is ABA [START_REF] Bondarenko | An abstract, argumentationtheoretic approach to default reasoning[END_REF]. Unlike all other rule-based argumentation systems, the initial version of ABA is not based on the notion of argument. It manipulates sets of assumptions and the attack relation is between pairs of assumption sets. In [START_REF] Gaertner | Computing arguments and attacks in assumption-based argumentation[END_REF], the authors proposed an equivalent version which makes use of arguments. The logical language considered in ABA is different from ours since it uses assumptions while in our paper we do not. As argued in [START_REF] Modgil | A general account of argumentation with preferences[END_REF], ABA does not satisfy in general the consistency postulate while our system satisfies all the postulates proposed in [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF]. Finally, we fully characterized the plausible conclusions of our system under various semantics while such characterization is not available for ABA. In [START_REF] Dung | An argument-based approach to reasoning with specificity[END_REF] another system was proposed for reasoning about stratified default theories. Like the initial version of ABA, the system is not based on the notion of argument thus somehow different from our approach. It allows subsets of a theory to attack a given default. Stable semantics was used for solving the conflicts. Unlike our paper, no characterization results are provided. However, the authors have shown that their system satisfies basic properties of a nonmonotonic consequence relation such as deduction, conditioning, and cumulativity.

In addition to the characterizations of the system's outcomes, the other main novelty of our paper is the exclusive use of undercut for encoding conflicts between arguments. This relation is always coupled with rebuttal and/or assumption attack which handle inconsistency in other systems. In our paper, we have shown that undercut is powerful enough to perfectly fulfill the role of rebuttal. Indeed, the characterization results show that extensions under any of the reviewed semantics are consistent and coherent sub-theories. This means that they do not contain pairs of arguments which are in conflict wrt one of the two relations. Furthermore, the maximality for set inclusion in case of naive, preferred and stable semantics suggests that not only all possible conflicts are captured but are also correctly solved. Finally, the system satisfies all the rationality postulates under any semantics while in ASPIC and ASPIC+, for each semantics, one should use a different definition of rebuttal (restricted vs unrestricted) in order to satisfy the postulates.

Regarding the definition of undercut, there are three proposals in the literature which are all equivalent. The first definition is the one followed in our paper and in [START_REF] Prakken | An abstract framework for argumentation with structured arguments[END_REF]. The idea is to assign a name to every defeasible rule and to allow these names to be in heads of other rules. Unlike in [START_REF] Prakken | An abstract framework for argumentation with structured arguments[END_REF], in our paper, names of rules may only be in heads of strict rules. The reason is that undercut shows exceptions of defeasible rules, and exceptions are certain information. For instance, in case of penguin, the rule "birds fly" is not applicable. The second proposal, given in [START_REF] Pollock | How to reason defeasibly[END_REF] and followed in [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF], uses an objectivation operator which transforms any defeasible rule into a literal. The latter plays the role of the name of the rule in our system. The last definition, proposed in [START_REF] Cohen | Backing and undercutting in defeasible logic programming[END_REF][START_REF] Cohen | Backing and undercutting in abstract argumentation frameworks[END_REF][START_REF] Cohen | A structured argumentation system with backing and undercutting[END_REF], extends the logical language by a new form of rules with which one can block defeasible rules. Whatever the definition is, none of these systems characterized its outcomes. This work will be extended in two ways. First, we will consider weighted theories, i.e., theories in which defeasible rules may not have the same importance. Second, we plan to use ranking semantics [START_REF] Amgoud | Ranking-based semantics for argumentation frameworks[END_REF] for evaluating arguments. Such semantics were already used in argumentation systems developed for handling inconsistency in propositional knowledge bases [START_REF] Amgoud | Argumentation-based ranking logics[END_REF]. The results show that they lead to more discriminating results than those of extension semantics. Furthermore, the argumentation approach goes beyond the maximal consistent subbases computed by the well-known coherence-based approach [START_REF] Rescher | On inference from inconsistent premises[END_REF].

Appendix: Proofs

Notations: Throughout this section, when we do not need to refer to a particular semantics, we write Ext(H) to denote the set of extensions of the argumentation system H. The function Name returns the name of a (strict or defeasible) rule.

Proof of Proposition 1. Follows immediately from the fact that Def(d) = ∅ for all (d, x) ∈ Arg((F, S, ∅)).

Proof of Theorem 1. Let H = (Arg(T ), R u ) be an argumentation system built over theory T = (F, S, D). Assume that Ext(H) = ∅ and let E ∈ Ext(H). Closure under strict rules: Let E ∈ Ext c (H). Assume that x ∈ CN((Concs(E), S, ∅)) and x / ∈ Concs(E). Let X = {x 1 , . . . , x n } be the minimal for set inclusion subset of Concs(E) such that x ∈ CN((X, S, ∅)). For each x i , there exists a i ∈ E such that Conc(a i ) = x i . There exists a minimal derivation schema for x using a 1 , . . . , a n and additional strict rules. Let d be that derivation. (d,x) is an argument and (d, x) / ∈ E. There are two cases:

i) E ∪ {(d, x)} is conflicting, i.e, there exists b = (d ′ , x ′ ) ∈ E such that bR u (d, x) or (d, x)R u b. If bR u (d, x), then Conc(b) ∈ Def(d).
However, Def(d) = ∪Def(a i ). Thus, there exists i ∈ {1, . . . , n} such that Conc(b) ∈ Def(a i ), i.e., bR u a i . This contradicts the fact that E is conflict-free. If (d, x)R u b, then since E defends its elements, ∃c ∈ E such that cR u (d, x), i.e., Conc(c) ∈ Def(d). Then, ∃a i ∈ Sub((d, x)) such that cR u a i . But, a i ∈ E. ii) E does not defend (d, x). Let b ∈ Arg(T ) such that bR u (d, x). Then, Conc(b) ∈ Def(d). Then, bRa i for some a i ∈ Sub((d, x)) and a i ∈ E. Since E defends its elements, then E attacks b. Since preferred, grounded and stable extensions are complete, then the property holds under those semantics as well. Consistency: Let E ∈ Ext y (H) where y ∈ {p, s, g, c}, and assume that Concs(E)

is inconsistent. Thus, ∃a, b ∈ E such that a = (d, x), b = (d ′ , ¬x), d = (x 1 , r 1 ), . . . , (x n , r n ) , d ′ = (x ′ 1 , r ′ 1 ), . . . , (x ′ m , r ′ m ) , x n = x and x ′ m = ¬x. Moreover, x, ¬x ∈ L.
If a and b are both strict (i.e., Def(d) = ∅ and Def(d ′ ) = ∅), then CN((F, S, ∅)) is inconsistent. Assume now that CN((F, S, ∅)) is consistent. It follows that a or/and b is defeasible (i.e., Def(d) = ∅ or/and Def(d ′ ) = ∅). Assume that a is defeasible. If r n ∈ D, then Name(¬x → r n ) ∈ S (since T is closed). Since E is closed under strict rules and ¬x ∈ Concs(E), then r n ∈ Concs(E). Thus, CN(Th(E)) ∩ Defs(Th(E)) = ∅. This contradicts the fact that Th(E) is coherent by Theorem 2. Assume now that r n / ∈ D. Let r i ∈ Def(d) be such that for all j > i, r j is either a fact or a strict rule. By definition of a derivation, r n ∈ S.

Let r n = y 1 , . . . , y l → x. Since S is closed under contraposition, then for all 1 ≤ j ≤ l, Name(y 1 , . . . , y j-1 , y j+1 , . . . , y l → ¬y j ) ∈ S. Moreover, there exists a minimal sub-derivation d j of d for each y j . Thus,

X j = d 1 , d j-1 , d j+1 , .
. . , d l , d ′ , (¬y j , y 1 , y j-1 , y j+1 , . . . , y l → ¬y j , ¬y j ) is a derivation of ¬y j . Since arguments are minimal, then (X j , ¬y j ) ∈ Arg(T ). Note that (d i , y i ) ∈ Sub(a). Since H is closed under sub-arguments, then (d i , y i ) ∈ E and thus y i ∈ Concs(E). Since H is closed under strict rules, ¬y j ∈ Concs(E) for all j = 1, . . . , l.

The same reasoning holds for each strict rule y 1 , . . . , y l → y between r i and r n . Indeed, ¬y i ∈ Concs(E) for all i = 1, . . . , l. By definition of derivation, there exists a strict rule r after r i such that Head(r i ) ∈ Body(r) thus ¬Head(r i ) ∈ Concs(E). Thus, Name(¬Head(r i ) → r i ) ∈ S. Since H is closed under strict rules, r i ∈ Concs(E). But, r i ∈ Defs(E) (since r i ∈ Def(d)). This contradicts the fact that Th(E) is coherent by Theorem 2. Indirect consistency: If CN((F, S, ∅)) is inconsistent, we have seen that consistency is violated, i.e., there exists at least one extension E such that Concs(E) is inconsistent. Since by monotony of CN, Concs(E) ⊆ CN(Concs(E)). Hence, CN(Concs(E)) is inconsistent, and indirect consistency is violated. Assume now that CN((F, S, ∅)) is consistent. From previous result, consistency is satisfied. We know also that closure under strict rules is satisfied. Then, indirect consistency is satisfied, since it was shown in [START_REF] Caminada | On the evaluation of argumentation formalisms[END_REF] that indirect consistency follows from Consistency and Closure under strict rules.

Proof of Theorem 2. Let H = (Arg(T ), R u ) be an argumentation system built over theory T = (F, S, D). Assume that Ext(H) = ∅ and let E ∈ Ext(H). Coherence: Assume that ∃x ∈ Concs(E) ∩ Defs(Th(E)). Thus, x ∈ L ′ . Moreover, ∃a, b ∈ E such that Conc(a) = x and x ∈ Defs({b}). Then, aR u b. This contradicts the fact that E is conflict-free.

Closure under sub-arguments

: Let a = (d, x), b = (d ′ , x ′ ) ∈ Arg(T ) such that a ∈ E, b / ∈ E and b ∈ Sub(a). Assume that E ∈ Ext s (H). There exists c ∈ E such that cR u b. Let c = (d ′′ , x ′′ ). Then, x ′′ ∈ Def(d ′ ) and thus x ′′ ∈ Def(d) since Def(d ′ ) ⊆ Def(d).
Consequently, cR u a. This contradicts the fact that E is conflict-free.

Assume now that E ∈ Ext n (H), then E ∪ {b} is conflicting. Then, there exists c ∈ E such that cR u b or bR u c. Assume that bR u c. Then x ′ ∈ L ′ . Since elements of L ′ cannot be in the body of any rule then a = b, thus aR u c. This contradicts the fact that it is conflict-free. Assume now that cR u b. As above, it follows that cR u a and this contradicts the fact that E is conflict-free.

Assume now that E ∈ Ext c (H). Since b / ∈ E then there are two cases: i) E ∪{b} is conflicting, i.e., there exists c ∈ E such that cR u b or bR u c. As above, we get either cR u a or aR u c. In both cases, E is not conflict-free and this contradicts the fact that it is a complete extension. ii) E does not defend b. Thus, there exists c = (d ′′ , x ′′ ) ∈ Arg(T ) such that cR u b. Then, x ′′ ∈ Def(d ′ ) and thus x ′′ ∈ Def(d) meaning that cR u a. Since E is a complete extension ∃d ∈ E such that dR u c. Thus, E defends b. Since grounded and preferred extensions are complete, then the property holds under the two semantics as well.

Proof of Corollary 1. Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T = (F, S, D) s.t. Ext(H) = ∅. Assume that Output(H) is inconsistent then ∃x, ¬x ∈ Output(H). Thus, for all E ∈ Ext(H), x, ¬x ∈ Concs(E). From Theorem 1, this is only possible if CN((F, S, ∅)) is inconsistent.

Since CN is monotonic, Output(H) ⊆ CN((Output(H), S, ∅)). Let x ∈ CN((Output(H), S, ∅)) and assume that x / ∈ Output(H), thus, there exists E ∈ Ext(H) such that x / ∈ Concs(E). This contradicts Theorem 2.

Proof of Theorem 3. Let H = (Arg(T ), R u ) be a system built over a theory T .

Let E ∈ Ext n (H) and let O = Th(E). It is clear that O is uniquely de- termined from E. Let us show that O is a naive option. O = (F ′ , S ′ , D ′ ) such that F ′ = (d,x)∈E Facts(d), S ′ = (d,x)∈E Strict(d) and D ′ = (d,x)∈E Def(d).
It is obvious that S ′ ⊆ S and D ′ ⊆ D. Now, for every x ∈ F there is an argument ( (x, ∅) , x) ∈ Arg(T ). By definition of undercutting, such argument has no conflict with any other argument. Thus, all arguments of this form belong to every naive extension, i.e., F ′ = F.

For the sake of contradiction, suppose that ∃x ∈ CN(F ′ , S ′ , D ′ ) s.t.

x ∈ D ′ . Let d be a minimal derivation of x in O. Thus (d, x) is an argument of E. since x ∈ D ′ then, from the definition of Th(E), x must be used in at least an argument of E, say (d ′ , x ′ ), i.e., x ∈ d ′ . Therefore, (d, x)R u (d ′ , x ′ ). Contradiction with conflict-freeness of E.

Let r ∈ S ′ ∪ D ′ . r is used in at least one argument, say a, of E. So, a has a sub-argument b = ( (x 1 , r 1 ), . . . , (x n , r n ) , x n ) with r n = r and x n = Head(r). By closeness under sub-arguments (by Theorem 2), b is also an argument of E. From the definition of derivation schema, for every x ∈ Body(r), x = x i for some i s.t. 1 ≤ i < n. Thus, there is a sub-argument of b, and hence an argument in E and a derivation in O, for every x ∈ Body(r). This means that for every x ∈ Body(r),

x ∈ CN(O), i.e., Body(r) ⊆ CN(O).

Suppose that ∃S ′′ , D ′′ s.t. (F ′ , S ′ , D ′ ) ⊏ (F ′ , S ′′ , D ′′ ) and (F ′ , S ′′ , D ′′ ) satisfies the previous conditions. For every rule r ∈ (S ′′ ∪ D ′′ ) \ (S ′ ∪ D ′ ), there is at least an argument a = (d, x)

s.t. r ∈ Strict(d) ∪ Def(d).
Clearly, a / ∈ E. But from the coherence of (F ′ , S ′′ , D ′′ ) it must be the case that ∄b ∈ E s.t. aR u b or bR u a. Indeed, suppose for example that aR u b and that b = (d ′ , x ′ ), then x ∈ d ′ . That is, x ∈ CN(F ′ , S ′′ , D ′′ ) and x ∈ D ′′ which contradicts the coherence of (F ′ , S ′′ , D ′′ ). We can show in a similar way that it must not be the case that bR u a. But, it this case E ∪ a is conflict-free. Contradiction with the fact that E is a naive extension.

Let E, E ′ ∈ Ext n (H) and NOption(E) = NOption(E ′ ). Let us show that E ⊆ E ′ . Let a (d, x) ∈ E. Then, d is a derivation for x in NOption(E). Suppose that a / ∈ E ′ . Then d is not a derivation for x in NOption(E ′ ). Contradiction, since NOption(E) = NOption(E ′ ). We show similarly that E ′ ⊆ E. Let E ∈ Ext s (H) and let Th(E) = (F ′ , S ′ , D ′ ). We can show that F ′ = F in a similar way as in Theorem 3, first point. We take O = (F, S, D ′ ) (we complete S ′ by the remaining strict rules). Clearly, O is uniquely determined from E. We have that Concs(E) = CN(Th(E)). Let us show that CN((F, S, D ′ )) = CN(Th(E)). To do so, it is sufficient to show that every rule r ∈ S \ S ′ is not applicable in (F, S ′ , D ′ ). Suppose for the sake of contradiction that there is r ∈ S \ S ′ s.t. r is applicable in (F, S ′ , D ′ ), i.e. Body(r) ⊆ CN((F, S ′ , D ′ )). Thus, there is a minimal derivation in (F, S, D ′ ) for Head(r) using r as a last rule: d, (x, r) s. Similar to the proof of point 3 in Theorem 3.

Let E ∈ Ext

Let O 1 = (F, S ′ 1 , D ′ 1 )
Suppose that ∃r / ∈ D ′ s.t. r / ∈ CN((F, S, D ′ )) and ∀x ∈ Body(r), x ∈ CN((F, S, D ′ )). Let Body(r) = {x 1 , . . . , x k } and Head(r) = y. Since for 1 ≤ i ≤ k, x i ∈ CN((F, S, D ′ )), then there is an argument

a i = (d i , x i ) ∈ E (1 ≤ i ≤ k)
for each x i . Thus, we can construct an argument a for y using r as last rule, i.e., a = ( d, (y, r) , y) where Facts(d

) = i Facts(d i ), Strict(d) = i Strict(d i ) and Def(d) = i Def(d i ). Since r / ∈ D ′ , a / ∈ E, so there is b = (d ′ , x ′ ) ∈ E s.t. bR u a, i.e., x ′ ∈ Def(d) ∪ {r}. Since r /
∈ CN((F, S, D ′ )), it cannot be the case that x ′ = r, thus x ′ ∈ Def(d), so x ′ ∈ Def(d i ) for some i s.t. 1 ≤ i ≤ k. This means that bR u a i which contradicts the conflict-freeness of E.

Let E, E ′ ∈ Ext s (H) and SOption(E) = SOption(E ′ ). Let us show that E ⊆ E ′ . Let a = (d, x) ∈ E. Then, d is a derivation for x in SOption(E). Suppose that a / ∈ E ′ . Then d is not a derivation for x in SOption(E ′ ). Contradiction, since SOption(E) = SOption(E ′ ). We show similarly that E ′ ⊆ E.

Let E ∈ Ext s (H). Since Th(E) ⊑ SOption(E) and from the definition of functions Th and Arg it is obvious that E ⊆ Arg(SOption(E)). Now let a = (d, x) ∈ Arg(SOption(E)). a = (d, x) is constructed from SOption(E). So, Def(d) ⊆ Defs(SOption(E)). Suppose that a / ∈ E. Since E is a stable extension then there is b = (d ′ , x ′ ) ∈ E such that bR u a. From b ∈ E we easily deduce that x ′ ∈ CN(SOption(E)). But then, from bR u a, SOption(E) must be incoherent. Contradiction with the fact that SOption(E) is a stable option.

Proof of Theorem 6. Let

H = (Arg(T ), R u ) s.t. Ext s (H) = ∅.
Let O = (F, S, D ′ ) ∈ SOpt(T ) and let E = Arg(O). We prove that E is conflict-free and ∀b ∈ Arg(T ) \ E, ∃a ∈ E s.t. aR u b.

Proof of Corollary 5. Follows immediately from the bijection between stable options and stable extensions (theorems 5 -6). Let E ∈ Ext p (H) and let Th(E) = (F ′ , S ′ , D ′ ). We can show that F ′ = F in a similar way as in Theorem 3, first point. We take O = (F, S, D ′ ) (we complete S ′ by the remaining strict rules). Clearly, O is uniquely determined from E. We have that Concs(E) = CN(Th(E)). Let us show that: CN((F, S, D ′ )) = CN(Th(E)). To do so, it suffices to show that every rule r ∈ S \ S ′ is not applicable in (F, S ′ , D ′ ). Suppose for the sake of contradiction that there is r ∈ S \ S ′ s.t. r is applicable in (F, S ′ , D ′ ). Thus, there is a minimal derivation in (F, S ′ , D ′ ) for Head(r)) using r as a last rule: d, (x, r) s.t. x = Head(r), Def(d) ⊆ D ′ and Strict(d) ⊆ S ′ . Thus, a = ( d, (x, r) , x) is an argument outside E. a does not attack any argument of E. Indeed, if we suppose the contrary then, since E is a preferred extension, there is b ∈ E s.t. bR u a. So, there is a sub-argument of a: a ′ = ( d ′ , (x ′ , r ′ ) , x ′ ) with r ′ ∈ D ′ and b = (d ′′ , r ′ ). However since a ′ ∈ E (because it uses only rules from S ′ ∪D ′ ), this means that E is not conflict-free which contradicts the fact that E is a preferred extension. So E ∪ {a} is conflict free. Moreover, for every c ∈ Arg(T ) \ (E ∪ {a}), if cR u a then there is a sub-argument of a: a ′ = ( d ′ , (x ′ , r ′ ) , x ′ ) with x ′ ∈ D ′ and c = (d ′′ , x ′ ). However since a ′ ∈ E (because it uses only rules from S ′ ∪ D ′ ) and E is a preferred extension, then there is a ′ ∈ E such that a ′ R u c. This means that E ∪ {a} is conflict-free and defends all its elements. Contradiction with the fact that E is maximal. Now let us prove that O = (F, S, D ′ ) ∈ POpt(T ).

It is obvious that D ′ ⊆ D

Similar to the proof of point 2 in Theorem 3.

Similar to the proof of point 3 in Theorem 3. x ∈ D ′′ . But, from the fourth condition of preferred options, there is r ′′ ∈ Def(d) such that r ′′ ∈ CN(O). So, there is an argument a ′ ∈ E ′ such that a ′ R u b. Consequently, E ′ is a preferred extension and E ⊂ E ′ which contradicts the fact that E is a preferred extension.

∀D ′′ ⊆ D, if ∃r ′ ∈ D ′ s.t. r ′ ∈ CN(F, S, D ′′ ) then there is a min- imal derivation d ′ for r ′ in (F, S, D ′′ ), i.e., (d ′ , r ′ ) is an argument of Arg(T ). Since r ′ ∈ D ′ , there in an argument a = (d, x) ∈ E s.t.
We show by a similar way as in the second point of Theorem 5 that: for all

E, E ′ ∈ Ext p (H) if POption(E) = POption(E ′ ), E = E ′ .
Let E ∈ Ext p (H). Since Th(E) ⊑ POption(E) and from the definition of functions Th and Arg it is obvious that E ⊆ Arg(POption(E)). Now let a = (d, x) ∈ Arg(POption(E)). a = (d, x) is constructed from POption(E). So, Def(d) ⊆ Defs(POption(E)). Suppose that a / ∈ E. Since E is a preferred extension then we have two cases. The first case is that there is b = (d ′ , x ′ ) ∈ E such that bR u a. From b ∈ E we easily deduce that x ′ ∈ CN(POption(E)). But then, from bR u a, POption(E) must be incoherent. Contradiction with the fact that POption(E) is a preferred option. The second case is that E does not attack a, a does not attack E but E does not defend a: there is Finally, Suppose that E is not maximal w.r.t. previous conditions. Thus, there is E ′ s.t. E ⊂ E ′ and E ′ is preferred, i.e., E ′ is an maximal conflict-free set of arguments that defends all its elements. Let O ′ (F, S, D ′′ ) = POption(E ′ ). Clearly, D ′ = D, because there every argument in E ′ \ E uses at least a rule which is not in D ′ . Since O ′ is a preferred option (Theorem 7), D ′′ is maximal, so D ′ ⊂ D ′′ . This contradicts the fact that O is a preferred option.

b = (d ′ , x ′ ) / ∈ E such that
Similar to the proof of point 2 of Theorem 6.

Similar to the proof of point 3 of Theorem 6.

Proof of Corollary 6. Follows immediately from the bijection between preferred options and preferred extensions (theorems 7 -8).

Proof of Corollary 7. Follows immediately from the bijection between preferred options and preferred extensions (theorems 7 -8). Let E ∈ Ext c (H) and let Th(E) = (F ′ , S ′ , D ′ ). We can show that F ′ = F in a similar way as in Theorem 3, first point. We take O = (F, S, D ′ ) (we complete S ′ by the remaining strict rules). Clearly, O is uniquely determined from E. We have that Concs(E) = CN(Th(E)). Let us show that: CN((F, S, D ′ )) = CN(Th(E)). To do so, it suffices to show that every rule r ∈ S \ S ′ is not applicable in (F, S ′ , D ′ ). Suppose for the sake of contradiction that there is r ∈ S \ S ′ s.t. r is applicable in (F, S ′ , D ′ ). Thus, there is a minimal derivation in (F, S ′ , D ′ ) for Head(r)) using r as a last rule: d, (x, r) s.t. x = Head(r), Def(d) ⊆ D ′ and Strict(d) ⊆ S ′ . Thus, a = ( d, (x, r) , x) is an argument outside E. a does not attack any argument of E. Indeed, if we suppose the contrary then, since E is a complete extension, there is b ∈ E s.t. bR u a. So, there is a sub-argument of a: a ′ = ( d ′ , (x ′ , r ′ ) , x ′ ) with r ′ ∈ D ′ and b = (d ′′ , r ′ ). However since a ′ ∈ E (because it uses only rules from S ′ ∪D ′ ), this means that E is not conflict-free which contradicts the fact that E is a complete extension. So E ∪ {a} is conflict free. Moreover, for every c ∈ Arg(T ) \ (E ∪ {a}), if cR u a then there is a sub-argument of a: a ′ = ( d ′ , (x ′ , r ′ ) , x ′ ) with x ′ ∈ D ′ and c = (d ′′ , x ′ ). However since a ′ ∈ E (because it uses only rules from S ′ ∪ D ′ ) and E is a complete extension, then there is a ′ ∈ E such that a ′ R u c. This means that E defends a. Contradiction with the fact that E contains all the arguments it defends. Now let us prove that O = (F, S, D ′ ) ∈ POpt(T ). A similar reasoning as that used in the third point of Theorem 7 may be used to prove that if E = Ext g (H), then E = Arg(GOption(E)).

Definition 7 (

 7 Sub-argument). An argument (d, x) is a sub-argument of (d ′ , x ′ ) iff (Facts(d), Strict(d), Def(d)) ⊑ (Facts(d ′ ), Strict(d ′ ), Def(d ′ )). Notations: Arg(T ) denotes the set of all arguments built from theory T in the sense of Definition 6. If a = (d, x) is an argument, Conc(a) = x and Sub(a) is the set of all its sub-arguments. For a set E of arguments, Concs(E) = {x | (d, x) ∈ E} and Th(E) is a theory such that:

a 1 :

 1 ( (b, ∅) , b) a 2 : ( (p, ∅) , p) a 3 : ( (p, ∅), (¬f, r 1 ) , ¬f ) a 4 : ( (p, ∅), (¬f, r 1 ), (r 2 , r 4 ) , r 2 ) a 5 : ( (b, ∅), (f, r 2 ) , f ) a 6 : ( (b, ∅), (f, r 2 ), (¬p, r 3 ) , ¬p) a 4 undercuts both a 5 and a 6 since r 2 ∈ Def(d 5 ) and r 2 ∈ Def(d 6 ).

7 Figure 1 :

 71 Figure 1: Graph of attacks built from the theory T3

Corollary 5 .

 5 Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T such that Ext s (H) = ∅. Output s (H) = O∈SOpt(T ) CN(O). Example 3 (Cont) The theory T 3 has one stable option O = (F 3 , S 3 , {r 2 }). Thus, Output s (H) = CN(O) = {x, y, u, r 1 }.

  and (F ′ , S ′ , D ′′ ) satisfies the previous conditions.POpt(T ) denotes the set of preferred options of theory T .Example 3 (Cont) Consider again the closed theory T 3 . There are three subtheories of T 3 that satisfy the first four conditions of Definition 16:

Theorem 8 .

 8 Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T . For any O ∈ POpt(T ), Arg(O) ∈ Ext p (H). For any O ∈ POpt(T ), O = POption(Arg(O)).

r 1 , r 2 and r 3 .

 13 Let us start by r 1 and let D 1 = {r 1 }, we have r 1 ∈ D 1 and Body(r 1 ) ⊆ CN(F, S, D 1 ). Take D ′′ = {r 2 }, we have D 1 ∩ CN(F, S, D ′′ ) = {r 1 } = ∅ and r 2 / ∈ CN(F ′ , S ′ , ∅). A similar reasoning is valid for the other choices of D 1 , namely for D 1 = {r 1 , r 2 }, D 1 = {r 1 , r 3 } and D 1 = {r 1 , r 2 , r 3 }.

Theorem 10 .

 10 Let H = (Arg(T ), R u ) be an argumentation system built over a closed theory T . For any O ∈ COpt(T ), Arg(O) ∈ Ext c (H). For any O ∈ COpt(T ), O = COption(Arg(O)).

Figure 2 :

 2 Figure 2: Relationships between options (plain arrows) (resp. outputs (dotted arrows)).

  n (H). Since NOption(E) = Th(E) and from the definition of functions Th and Arg it is obvious that E ⊆ Arg(NOption(E)). Now let a = (d, x) ∈ Arg(NOption(E)). This means that a = (d, x) is constructed from NOption(E). So, x ∈ CN(NOption(E)) and Def(d) ⊆ Defs(NOption(E)). Suppose that a / ∈ E. Since E is a naive extension then there is b = (d ′ , x ′ ) ∈ E such that aR u b or bR u a. From b ∈ E we easily deduce that x ′ ∈ CN(NOption(E)) and Def(d ′ ) ⊆ Defs(NOption(E)). But then, from aR u b or bR u a, NOption(E) must be incoherent. Contradiction with the fact that NOption(E) is a naive option.Proof of Theorem 4. Let H = (Arg(T ), R u ) be a system built over a theory T .Let O = (F, S ′ , D ′ ) ∈ NOpt(T ) and let E = Arg(O). We prove that E is a maximal conflict-free set of Arg(T ). Suppose that there are two arguments a = (d, x) and b = (d ′ , x ′ ) in E s.t. aR u b, i.e., x ∈ Def(d ′ ). But since d and d ′ are derivation schemas for x and x ′ respectively in O we have:x ∈ CN(O) and Def(d ′ ) ⊆ D ′ , so x ∈ D ′ . Contradiction with the coherence of naive option O. E = Arg(O) is conflictfree. Now, suppose that E is not maximal. Thus there is E ′ ⊆ Arg(T ) s.t. E ⊂ E ′ and E ′ is a naive extension of H. From Theorem 3, NOption(E ′ ) = Th(E ′ ) = O ′ is a naive option of T . Let O ′ = (F, S ′′ , D ′′ ).Since all the arguments that use exclusively rules from S ′ ∪ D ′ belong to E, every argument in E ′ \ E uses at least a rule r which is not in S ′ ∪ D ′ . So, either (S ′ ⊂ S ′′ ) or (D ′ ⊂ D ′′ ) or both, i.e, O ⊏ O ′ . Contradiction with the fact that O is a naive option of T . Let O = (F, S ′ , D ′ ) ∈ NOpt(T ) and let NOption(Arg(O)) = (F ′′ , S ′′ , D ′′ ). F ′′ = F follows from the fact that Arg(O) contains every argument ( x, ∅ , x). Let x ∈ S ′′ (resp. x ∈ D ′′ ). x is used in at least an argument of Arg(O), so x ∈ S ′ (resp. x ∈ D ′ ). Thus, we have: S ′′ ⊆ S ′ and D ′′ ⊆ D ′ . Inversely, let x ∈ S ′ (resp. x ∈ D ′ ), since Body(x) ⊆ CN(O) (from the definition of a naive option), x must be used in at least one argument of Arg(O). Thus x ∈ F ′′ (resp. x ∈ D ′′ ). So, F ′ ⊆ F ′′ and D ′ ⊆ D ′′ . In summary, F = F ′′ , S ′ = S ′′ and D ′ = D ′′ , i.e., O = NOption(Arg(O)).

  t. x = Head(r), Def(d) ⊆ D ′ and Strict(d) ⊆ S ′ . Thus, a = ( d, (x, r) , x) is an argument outside E but since E is a stable extension, there is b ∈ E s.t. bR u a. So, there is a sub-argument of a: a ′ = ( d ′ , (x ′ , r ′ ) , x ′ ) with r ′ ∈ D ′ and b = (d ′′ , r ′ ). However since a ′ ∈ E (because it uses only rules from S ′ ∪ D ′ ), this means that E is not conflict-free. Contradiction. Now let us prove that O = (F, S, D ′ ) is a stable option.It is obvious that D ′ ⊆ D Similar to the proof of point 2 in Theorem 3.

Proof of Theorem 7 .

 7 Let H = (Arg(T ), R u ) s.t. Ext p (H) = ∅. Let us show that for all E ∈ Ext p (H), there is a unique O ∈ POpt(T ) s.t. Th(E) ⊑ O and Concs(E) = CN(O).

  r ′ ∈ Def(d) and we have bR a a. Since E is a preferred extension, there is an argument c = (d ′′ , x ′′ ) ∈ E s.t. cR u b, i.e., there is a derivationd ′′ for r ′′ in (F, S, D ′ ) s.t. d ′′ ∈ Def(d ′ ). This means that r ′′ ∈ CN(F, S, D ′ ) and r ′′ ∈ D ′′ .Suppose that there is D ′′ s.t. D ′ ⊂ D ′′ and D ′′ satisfies the previous conditions. Let O ′ = (F, S, D ′′ ) and E ′ = Arg(O ′ ). The conflictfreeness of E ′ follows from the fact that O ′ is coherent. Let b = (d, x) be an argument of Arg(T ) \ E ′ s.t. there is an argument a = (d ′ , x ′ ) ∈ E ′ and bR u a. Thus, x ∈ CN(F, S, Def(d)) and x ∈ Def(d ′ ), i.e.

  bR u a and E does not attack b. From bR u a we have x ′ ∈ d. Since Def(d) ⊆ Defs(POption(E)) then x ⊆ Defs(POption(E)). So, x is used in at least an argument c = (d ′′ , x ′′ ) of E i.e., x ∈ d ′′ . Thus, c is attacked by b. But since E is a preferred extension, then it must contain an argument which attacks b. This contradict the hypothesis that E does not attack b.Proof of Theorem 8. LetH = (Arg(T ), R u ) s.t. Ext p (H) = ∅. Let O = (F, S, D ′ ) ∈ POpt(T ) and let E = Arg(O). We prove that E is conflict-free, ∀b ∈ Arg(T ) \ E, if ∃a ∈ E s.t. bR u a then ∃c ∈ E s.t.cR u b and E is a maximal subset of Arg(T ) satisfying the previous two conditions. Suppose that there are two argument a = (d, x) and b = (d ′ , x ′ ) in E s.t. aR u b, i.e., x ∈ Def(d ′ ). But since d and d ′ are derivation schemas for x and x ′ respectively in O we have: x ∈ CN(O) and Def(d ′ ) ⊆ D ′ , so x ∈ D ′ . Contradiction with the coherence of preferred option O. So, E is conflictfree. Now, let us show that: ∀b ∈ Arg(T ) \ E, if ∃a ∈ E s.t. bR u a then ∃c ∈ E s.t. cR u b. Let b = (d, x) ∈ Arg(T ) \ E and let a = (d ′ , x ′ ) ∈ E s.t. bR u a, i.e., x ∈ CN(F, S, Def(d)) and x ∈ Def(d ′ ). From the fourth conditions of the definition of a preferred option, there is r ′′ ∈ Def(d) s.t. r ′′ ∈ CN(F, S, D ′ ). So, there is an argument c = (d ′′ , r ′′ ) with d ′′ a minimal derivation of r ′′ in O. Clearly, cR u b.

Proof of Theorem 9 .

 9 Let H = (Arg(T ), R u ) s.t. Ext c (H) = ∅. Let us show that for all E ∈ Ext c (H), there is a unique O ∈ COpt(T ) s.t. Th(E) ⊑ O and Concs(E) = CN(O).

  It is obvious that D ′ ⊆ D Similar to the proof of point 2 in Theorem 3.Similar to the proof of point 3 in Theorem 3.Similar to the proof of point 4 in Theorem 7.For the sake of contradiction, suppose that ∃r ∈ D \ D ′ , ∃D 1 ⊆ D s.t. r ∈ D 1 and Body(r) ∈ CN((F, S, D 1 )) and∀D ′′ ⊆ D, if D 1 ∩ CN((F, S, D ′′ )) = ∅ then ∃r ′′ ∈ D ′′ , r ′′ ∈ CN((F, S, D ′ )).From the fact: ∃D 1 ⊆ D s.t. r ∈ D 1 and Body(r) ∈ CN((F, S, D 1 )) we deduce that r is applicable in (F, S, D 1 ), so there is at least an argument a ∈ Arg((F, S, D 1 )) where Defs(a) ⊆ D 1 and clearly a / ∈ E. From the fact:∀D ′′ ⊆ D, if D 1 ∩ CN((F, S, D ′′ )) = ∅ then ∃r ′′ ∈ D ′′ , r ′′ ∈ CN((F, S, D ′ )). Let a ∈ Arg((F, S, D 1 )). If D ′′ ⊆ D is s.t.Defs(a) ∩ CN((F, S, D ′′ )) = ∅ then there is at least argument in Arg((F, S, D ′′ )) which attacks a. Moreover, for all such argument b, we have Defs(b) ⊆ D ′′ and Defs(a) ∩ CN((F, S, Defs(b))) = ∅. It follows that ∃r ′′ ∈ Def(b), r ′′ ∈ CN((F, S, D ′ )). This means that for all argument b R u a there is and argument c in E s.t. c R u b, i.e. E defends a. But this contradicts the fact that E is a complete extension since a / ∈ E.We show by a similar way as in the second point of Theorem 5 that: for allE, E ′ ∈ Ext c (H) if COption(E) = COption(E ′ ), E = E ′ .A similar reasoning as that used in the third point of Theorem 7 may be used to prove that for all E ∈ Ext c (H), E = Arg(COption(E)).Proof of Theorem 10.Let H = (Arg(T ), R u ) s.t. Ext c (H) = ∅. Let O = (F, S, D ′ ) ∈ COpt(T ) and let E = Arg(O). We prove that E is conflict-free, ∀b ∈ Arg(T ) \ E, if ∃a ∈ E s.t. bR u a then ∃c ∈ E s.t. cR u b and E contains every argument it defends. The two first conditions are proved in similar way as in Theorem 8. Now, suppose for the sake of contradiction that the third condition does not hold which means that we suppose that there is a / ∈ E s.t. E defends a, i.e.for all b ∈ Arg(T ), if ¯Ru a then there exists c ∈ E s.t. c R u b. Let us put a = (d, x) and D 1 = Defs(d). Since, a / ∈ E then there is r ∈ D \ D ′ such that r 1 ∈ Defs(d) = D 1 and clearly Body(r) ⊆ CN((F, S, D 1 )). For all D ′′ ⊆ D suppose that D 1 ∩ CN((F, S, D ′′ )) = ∅. It follows that there is an arguments b = (d ′ , x ′ ) s.t. Defs(d ′ ) ⊆ D ′′ and x ′ ∈ D 1 , i.e., b R u a. In this case, there is an argument c = (d 1 , x 1 ) s.t. c R u b, i.e., there exists r ′′ ∈ Defs(d ′ ) hence r ′′ ∈ D ′′ s.t. x 1 = r ′′ . Since clearly x 1 ∈ CN((F, S, D ′ )) it follows that: r 1 ∈ CN((F, S, D ′ )). This contradicts the last condition of the definition of a complete option. Similar to the proof of point 2 of Theorem 6. Similar to the proof of point 3 of Theorem 6. Proof of Corollary 8. Follows immediately from the bijection between complete options and complete extensions (theorems 9 -10). Proof of Corollary 9. Follows immediately from the bijection between complete options and complete extensions (theorems 9 -10). Proof of Theorem 11. Let H = (Arg(T ), R u ) be an AS built over a closed theory T = (F, S, D). Let E = Ext g (H). E is the minimal (wrt set inclusion) complete extension of H. From Theorem 9, it follows that there exists a complete option O ∈ COpt(T ) s.t. Th(E) ⊑ O and Concs(E) = CN(O). Let us put O = (F, S, D ′ ) and suppose for the sake of contradiction that O is not the grounded option of T , i.e., that there exists D ′′ ⊂ D ′ such that O ′ = (F, S, D ′′ ) is a complete option. From Theorem 10, E ′ = Arg(O ′ ) is a complete extension of H. Let us show that E ′ ⊂ E. Let r be a rule in D ′ \D ′′ . From the definition of complete options (third point), it follows that there is (at least) an argument a = (d, x) ∈ Arg(O) = E s.t. r ∈ Defs(a). Clearly a / ∈ Arg(O ′ ) = E ′ since r / ∈ D ′′ . It follows that E ′ ⊂ E. Contradiction with the fact that E is the grounded extension of H.

Proof of Theorem 5. Let

  and O 2 = (F, S ′ 2 , D ′ 2 ) be two naive options. Suppose that O 1 = O 2 , i.e., either S ′ . Suppose the first case. Then, x is used in at least an argument of Arg(O 1 ) and never used in Arg(O 2 ). So, Arg(O 1 ) = Arg(O 2 ). By a similar reasoning, we obtain the same conclusion for the other case (there is x s.t. x ∈ S ′ 2 and x / ∈ S ′ 1 ) and for the case of defeasible rules. H = (Arg(T ), R u ) s.t. Ext s (H) = ∅. Let us show that for all E ∈ Ext s (H), there is a unique O ∈ SOpt(T ) s.t. Th(E) ⊑ O and Concs(E) = CN(O).

	1 = S ′ 2 or D ′ 1 = D ′ 2 or both. Suppose that 2 . This means that either there is x s.t. x ∈ S ′ 1 = S ′ S ′ 1 and x / ∈ S ′ 2 or there is x s.t. x ∈ S ′ 2 and x / ∈ S ′ 1 Proof of Corollary 2. Follows immediately from the bijection between naive op-
	tions and naive extensions (Theorems 3 -4).
	Proof of Corollary 3. Follows immediately from the bijection between naive op-
	tions and naive extensions (Theorems 3 -4).

This paper extensively develops the content of the conference paper[START_REF] Amgoud | Undercutting in argumentation systems[END_REF]. Indeed, it investigates the properties of the new system under two additional semantics, and characterizes the outcomes of the system under those semantics.

Acknowledgments.

This work benefited from the support of AMANDE ANR-13-BS02-0004 and ASPIQ ANR-12-BS02-0003 projects of the French National Research Agency.

From the definition of a stable option, we have two possible cases. The first case is that r ∈ CN(F, S, D ′ ), so there is a minimal derivation

Again, from the definition of a stable option, we have two possible cases. The first case is that r 1 ∈ CN(F, S, D ′ ), so there is a minimal derivation d ′′ for r 1 in O, i.e., a = (d ′′ , r 1 ) is an argument of E. Clearly aR u b 1 since r ∈ Def(d 1 ), hence , so aR u b. The second case is that Proof of Corollary 4. Follows immediately from the bijection between stable options and stable extensions (theorems 5 -6).