, we have proposed a logical encoding of argumentation frameworks with higher-order interactions (i.e. attacks/supports whose targets are arguments or other attacks/supports) with an evidential meaning for supports (such frameworks are called REBAF).

In this new work, we propose an extension of this previous works in order to take into account another kind of higher-order bipolar argumentation frameworks, those using the necessary meaning for the support relation.

Introduction

Formal argumentation has become an essential paradigm in Artificial Intelligence, e.g. for reasoning from incomplete and/or contradictory information or for modelling the interactions between agents [START_REF] Rahwan | Argumentation in Artificial Intelligence[END_REF]. Formal abstract frameworks have greatly eased the modelling and study of argumentation. The original Dung's argumentation framework (AF) [START_REF] Minh | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] consists of a collection of arguments interacting with each other through a relation reflecting conflicts between them, called attack, and enables to determine acceptable sets of arguments called extensions.

AF have been extended along different lines, e.g. by enriching them with positive interactions between arguments (usually expressed by a support relation), or higher-order interactions (i.e. interactions whose targets are other interactions).

Positive interactions between arguments. They have been first introduced in [START_REF] Karacapilidis | Computer supported argumentation and collaborative decision making: the HERMES system[END_REF][START_REF] Verheij | Deflog: on the logical interpretation of prima facie justified assumptions[END_REF]. In [START_REF] Cayrol | Gradual valuation for bipolar argumentation frameworks[END_REF], the support relation is left general so that the bipolar framework keeps a high level of abstraction. The associated semantics are based on the combination of the attack relation with the support relation which results in new complex attack relations. However, there is no single interpretation of the support, and a number of researchers proposed specialized variants of the support relation (deductive support [START_REF] Boella | Support in abstract argumentation[END_REF], necessary support [START_REF] Nouioua | Bipolar argumentation frameworks with specialized supports[END_REF][START_REF] Nouioua | Argumentation frameworks with necessities[END_REF], evidential support [START_REF] Oren | Semantics for evidence-based argumentation[END_REF][START_REF] Oren | Moving between argumentation frameworks[END_REF]). Each specialization can be associated with an appropriate modelling using an appropriate complex attack. These proposals have been developed quite independently, based on different intuitions and with different formalizations. [START_REF] Cayrol | Bipolarity in argumentation graphs: towards a better understanding[END_REF] presents a comparative study in order to restate these proposals in a common setting, the bipolar argumentation framework (see also [START_REF] Cohen | A survey of different approaches to support in argumentation systems[END_REF] for another survey).

Higher-order interactions. The idea of encompassing attacks to attacks in abstract argumentation frameworks has been first considered in [START_REF] Barringer | Temporal dynamics of support and attack networks : From argumentation to zoology[END_REF] in the context of an extended framework handling argument strengths and their propagation. Then, higher-order attacks have been considered for representing preferences between arguments (second-order attacks in [START_REF] Modgil | Reasoning about preferences in argumentation frameworks[END_REF]), or for modelling situations where an attack might be defeated by an argument, without contesting the acceptability of the source of the attack [START_REF] Baroni | AFRA: Argumentation framework with recursive attacks[END_REF]. Attacks to attacks and supports have been first considered in [START_REF] Gabbay | Fibring argumentation frames[END_REF] with higher level networks, then in [START_REF] Villata | Modelling defeasible and prioritized support in bipolar argumentation[END_REF]; and more generally, [START_REF] Cohen | An approach to abstract argumentation with recursive attack and support[END_REF] proposes an Attack-Support Argumentation Framework which allows for nested attacks and supports, i.e. attacks and supports whose targets can be other attacks or supports, at any level.

Here is an example of higher-order interactions (attacks and supports) in the legal field (this example is borrowed from [START_REF] Arisaka | Voluntary Manslaughter? A Case Study with Meta-Argumentation with Supports[END_REF] and modified in order to introduce some supports).

Example 1 The prosecutor says that the defendant had intention to kill the victim (argument b). A witness says that she saw the defendant throwing a sharp knife towards the victim (argument a). Argument a can be considered as a support for argument b. The lawyer argues back that the defendant was in a habit of throwing the knife at his wife's foot once drunk. This latter argument (argument c) is better considered attacking the support from a to b, than arguments a or b themselves. And so, the prosecutor's argumentation seems no longer sufficient for proving the intention to kill.

A natural idea that has proven useful to define semantics for these extended frameworks, known as "flattening technique", consists in turning the original extended framework into an AF, by introducing meta-arguments and a new simple (first-order) attack relation involving these meta-arguments [START_REF] Baroni | AFRA: Argumentation framework with recursive attacks[END_REF][START_REF] Boella | Attack relations among dynamic coalitions[END_REF][START_REF] Cayrol | Towards a new framework for recursive interactions in abstract bipolar argumentation[END_REF][START_REF] Cohen | An approach to abstract argumentation with recursive attack and support[END_REF], or by reducing higher-order attacks to first-order joint attacks [START_REF] Gabbay | Semantics for higher level attacks in extended argumentation frames[END_REF]. More recently, alternative acceptability semantics have been defined in a direct way for argumentation frameworks with higher-order attacks [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF] or for higher-order attacks and supports (necessary supports: [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF][START_REF] Cohen | On the acceptability semantics of argumentation frameworks with recursive attack and support[END_REF], evidential supports: [START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF]). The idea is to specify the conditions under which the arguments (resp. the interactions) are considered as accepted directly on the extended framework, without translating the original framework into an AF. Morever, in [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], a logical encoding of argumentation frameworks with higher-order attacks and evidential supports (REBAF) has been proposed. This encoding is able to take into account the most general definition of REBAF (with support cycles and collective interactions). So the aim of the current work is to do the same thing but for argumentation frameworks with higher-order attacks and necessary supports (RAFN).

The paper is organized as follows: the necessary background about argumentation frameworks is given in Section 2; the logical encoding for REBAF is recalled in Section 3; the new proposition that can handle RAFN is given in Section 5; Section 6 concludes the paper. The proofs are given in Appendix B. [START_REF] Arisaka | Voluntary Manslaughter? A Case Study with Meta-Argumentation with Supports[END_REF]

Background on argumentation frameworks

Note that the text (definitions, propositions and examples) of this section is extracted from [START_REF] Cayrol | Logical encoding of argumentation frameworks with higher-order attacks and evidential supports[END_REF].

The Standard Abstract Framework

The standard case handles only one kind of interaction: attacks between arguments.

Definition 1 [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] A Dung's argumentation framework (AF) is a tuple AF = A, R , where A is a finite and nonempty set of arguments and R ⊆ A × A is a binary attack relation on the arguments, with (a, b) ∈ R indicates that a attacks b.

A graphical representation can be used for an AF. We recall the definitions1 of some well-known extension-based semantics. Such a semantics specifies the requirements that a set of arguments should satisfy. The basic requirements are the following ones:

An extension can "stand together". This corresponds to the conflict-freeness principle.

An extension can "stand on its own", namely is able to counter all the attacks it receives. This corresponds to the defence principle.

Reinstatement is a kind of dual principle. An attacked argument which is defended by an extension is reinstated by the extension and should belong to it.

Stability: an argument that does not belong to an extension must be attacked by this extension.

Definition 2 [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] Let AF = A, R and S ⊆ A.

S is conflict-free iff (a, b) ∈ R for all a, b ∈ S. a ∈ A is acceptable w.r.t. S (or equivalently S defends a) iff for each b ∈ A with (b, a) ∈ R, there is c ∈ S with (c, b) ∈ R.

The characteristic function F of AF is defined by: F(S) = {a ∈ A such that a is acceptable w.r.t. S}. S is admissible iff S is conflict-free and S ⊆ F(S).

S is a complete extension of AF iff it is conflict-free and a fixed point of F.

S is the grounded extension of AF iff it is the minimal (w.r.t. ⊆) fixed point2 of F.

S is a preferred extension of AF iff it is a maximal (w.r.t. ⊆) complete extension.

S is a stable extension of AF iff it is conflict-free and for each a ∈ S, there is b ∈ S with (b, a) ∈ R.

Note that the complete (resp. grounded, preferred, stable) semantics satisfies the conflict-freeness, defence and reinstatement principles.

A Framework with Higher-Order Evidential Supports and Attacks

In this section, we recall the extension of [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF] proposed in [START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF] for handling recursive attacks and evidence-based supports.

Definition 3 [START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF] An evidence-based recursive argumentation framework (REBAF) is a sextuple A, R, E, s, t, P where A, R and E are three (possible infinite) pairwise disjunct sets respectively representing arguments, attacks and supports names, and where P ⊆ A ∪ R ∪ E is a set representing the prima-facie elements that do not need to be supported. Functions s : (R ∪ E) -→ 2 A \ ∅ and t : (R ∪ E) -→ (A ∪ R ∪ E) respectively map each attack and support to its source and its target.

Note that the source of attacks and supports is a set of arguments, the set P may contain several prima-facie elements (arguments, attacks and supports) and no constraint on the prima-facie elements is assumed (they can be attacked or supported). Example 1 (cont'd): The argumentation framework corresponding to the second example given in the introduction can be represented as follows (argument names are given in circular nodes, interaction names in square nodes, primafacie elements are in grey nodes and non prima-facie element in white nodes; supports are represented by double edges):

a α b β c
Semantics of REBAF are defined in [START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF] using the extension of the notion of structure introduced in [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF]. The idea is to characterize which arguments are regarded as "acceptable", and which attacks and supports are regarded as "valid", with respect to some structure.

Consider a given framework REBAF = A,R,E,s,t,P .

Definition 4 [8]

A triple U = (S, Γ, ∆) is said to be a structure of REBAF iff it satisfies: S ⊆ A, Γ ⊆ R and ∆ ⊆ E.

Intuitively, the set S represents the set of "acceptable" arguments w.r.t. the structure U , while Γ and ∆ respectively represent the set of "valid attacks" and "valid supports" w.r.t. U . Any attack 3 α ∈ Γ is understood as "non-valid" and, in this sense, it cannot defeat the element that it is targeting. Similarly, any support β ∈ ∆ is understood as "non-valid" and it cannot support the element that it is targeting.

The following definitions are extensions of the corresponding ones defined in [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF] in order to take into account the evidential supports.

Definition 5 [START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF] Given a structure U = (S, Γ, ∆),

The sets of defeated elements w.r.t. U are: The set of supported elements Sup(U ) is recursively defined as follows:4

Def X (U ) def = {x ∈ X|∃α ∈ Γ, s(α) ⊆ S and t(α) = x} with X ∈ {A, R, E} Def (U ) def = Def A (U ) ∪ Def R (U ) ∪ Def E (U )
Sup(U

) def = P∪ {t(α)|∃α ∈ ∆ ∩ Sup(U \{t(α)}), s(α) ⊆ (S ∩ Sup(U \{t(α)}))}
Note that a standard element is supported if there is a "chain"5 of supported supports leading to it, rooted in primafacie arguments. Acceptability is more complex. Intuitively, an element is acceptable if it supported and in addition, every attack against it can be considered as "non-valid" because either the source or the attack itself is defeated or cannot be supported. The elements that cannot be supported w.r.t. a structure U are called unsupportable w.r.t. U . An element is supportable w.r.t. U if there is a support for it which is non-defeated by U , with its source being non-defeated by U , and the support and its source being in turn supportable. The elements that are defeated or unsupportable are called unacceptable. Then an attack is said unactivable if either some argument in its source or itself is unacceptable.

Formally, Definition 6 Let U be a structure.

The set of unsupportable elements w.r.t. U is:

UnSupp(U ) def = Sup(U ) with U = (Def A (U ), R, Def E (U )).
The set of unacceptable elements w.r.t. U is:

UnAcc(U ) def = Def (U ) ∪ UnSupp(U )
The set of unactivable attacks w.r.t. U is:

UnAct(U ) def = {α ∈ R|α ∈ UnAcc(U ) or s(α) ∩ UnAcc(U ) = ∅} Definition 7 [8] An element x ∈ A ∪ R ∪ E is said to be acceptable w.r.t. a structure U iff (i) x ∈ Sup(U ) and (ii) every attack α ∈ R with t(α) = x is unactivable, that is, α ∈ UnAct(U ).
Acc(U ) denotes the set containing all arguments, attacks and supports that are acceptable with respect to U .

The following order relations will help defining preferred structures: for any pair of structures U = (S, Γ, ∆) and U = (S , Γ , ∆ ), we write U ⊆ U iff (S ∪Γ∪∆) ⊆ (S ∪Γ ∪∆ ). As usual, we say that a structure U is ⊆-maximal (resp. ⊆-minimal) iff every U that satisfies U ⊆ U (resp. U ⊆ U ) also satisfies U ⊆ U (resp. U ⊆ U ).

Definition 8 [START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF] A structure U = (S, Γ, ∆) is:

1. self-supporting iff (S ∪ Γ ∪ ∆) ⊆ Sup(U ), 2. conflict-free iff X ∩Def Y (U ) = ∅ for any (X, Y ) ∈ {(S, A), (Γ, R), (∆, E)}, 3. admissible iff it is conflict-free and S ∪ Γ ∪ ∆ ⊆ Acc(U ), 4. complete iff it is conflict-free and Acc(U ) = S ∪ Γ ∪ ∆, 5. grounded iff it is a ⊆-minimal complete structure, 6 6. preferred iff it is a ⊆-maximal admissible structure, 7. stable 7 iff (S ∪ Γ ∪ ∆) = UnAcc(U ).
From the above definitions, it follows that if U is a conflict-free structure, unsupportable elements w.r.t. U are not supported w.r.t. U , that is UnSupp(U ) ⊆ Sup(U ).

Note that every admissible structure is also self-supporting. Moreover, the usual relations between extensions also hold for structures: every complete structure is also admissible, every preferred structure is also complete, and every stable structure is also preferred and so admissible. Other properties of REBAF are described in [START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF], which enable to prove for instance that there is a unique grounded structure.

The previous definitions are illustrated on the following example. Example 1 (cont'd): In this framework, neither β nor its source is attacked and β and its source are prima-facie. So, for any structure U , it holds that neither β nor its source c is unacceptable w.r.t. U . As a consequence, for any structure U , α is not acceptable w.r.t. U as α is attacked by β and β is not unactivable w.r.t. U . As b is not prima-facie, and α is the only support to b, no admissible structure contains b. As a consequence, there is a unique complete, preferred and stable structure U = ({a, c}, {β}, ∅). Example 3 In this example, there are a collective attack and a collective support using the same source. Arguments c and e are the only elements that are not prima-facie. Since c is unsupportable, then neither β nor can be activable and there is one preferred structure that is: ({b, d}, {β, π}, { }). Trivially, an interaction can be activable w.r.t. a structure only if all the arguments in its source are in this structure.

Finally, REBAF is a conservative generalization of RAF described in [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF] with the addition of supports and joint attacks. Every RAF can be easily translated into a corresponding REBAF with no support and where every element (argument or attack) is prima-facie (see [START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF]).

In [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], some notions related to directed cycles of supports have been defined in order to take into account support cycles and collective interactions in the logical computation of structures for the REBAF.

Definition 9 [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF] Let REBAF = A,R,E,s,t,P . A directed cycle of supports (DCS) in this REBAF is a sequence C = (x 0 , . . . , x n-1 , x n ) such that:8 n > 0 and n is the size of the DCS ∀i = 0 . . . n, either x i ∈ E, or x i = (a, S) with S ∈ 2 A \ ∅ and a ∈ A ∩ S (a is called the "target field" of x i and S is called the "source field" of x i ),

x n = x 0 ∀i = 0 . . . n -1, if x i = (a, S) ∈ (A, 2 A \ ∅) then x i+1 ∈ E and s(x i+1 ) = S, ∀i = 0 . . . n -1, if x i ∈ E then -if x i+1 ∈ E then t(x i ) = x i+1 -if x i+1 = (a, S) ∈ (A, 2 A \ ∅) then t(x i ) = a. A simple DCS C = (x 0 , . . . , x n-1 , x n ) is a DCS in which ∀i, j = 0 . . . n -1, if i = j then x i = x j .
An input support of a DCS C = (x 0 , . . . , x n-1 , x n ) is: either a support y ∈ E such that y ∈ C and ∃x i ∈ C and x i = t(y), or an argument y ∈ A such that y ∈ C and ∃x i ∈ E ∩ C and y = s(x i ).

The set of inputs of the DCS C is denoted by C In and it is partitioned into

C In A = C In ∩ A and C In E = C In ∩ E. Let C = (x 0 , . . . , x n-1 ,
x n ) and C = (x 0 , . . . , x m-1 , x m ) be two DCS of this REBAF s.t. there exist x i ∈ C and x j ∈ C and x i = x j . The aggregation of C and C , denoted by C ∪ C , is the directed cycle corresponding to the union of the sets {x 0 , . . . , x n-1 } and {x 0 , . . . , x m-1 }.

Let C = (x 0 , . . . , x n-1 , x n ) be a DCS. C is a maximal DCS iff there does not exist another DCS that could be aggregated with C.

Note that a DCS is an "hybrid" sequence composed either with interactions, or with pairs (an argument, a nonempty set of arguments).

Example 4 This example gives an example of support cycles with an higher-order support and some collective supports. Here β, d and e are not prima-facie. Here there is one DCS: ((d, {a, d}), α, β, (e, {e}), γ, (d, {a, d})).

Note that the only preferred structure is ({a, b, c}, ∅, {α, γ}).

It is also interesting to notice that a DCS can be represented by several sequences (n sequences if n is the size of the DCS, each sequence being obtained by shifting to the right -or to the left). For instance, the DCS of this REBAF can also be expressed with: (β, (e, {e}), γ, (d, {a, d}), α, β).

Example 5 This example gives an example of several support cycles that can be aggregated Here there are three DCS (only the last one is a maximal DCS): The interesting point is the fact that the set {a, b} that is the source of α 1 and α 2 corresponds to two distinct elements in a DCS: (a, {a, b}) and (b, {a, b}); and each of them can be used as the preceding element of the supports α 1 or α 2 in the DCS. Note that the only preferred structure is ({e, d, a}, ∅, {α 1 , α 2 , β 1 , β 2 , γ}).

((d,
Another notion will be important in order to compute the logical characterization of REBAF semantics: the impacting support elements for an element of a REBAF.

Consider the following example:

Example 6 Consider the following REBAF with only arguments and supports; among these, there exist 2 collective supports (one from {a, b} to x and the another one from {c, d, e} to y). Let consider the elements that impact the supported status of argument z. Clearly, because of the collective interactions, we must use the notion of "trees"; indeed, any element of the source of a collective support must be supported if we want the target of this support to be also supported. Here, three "trees" must be taken into account for computing the supported status of z:

a 0 α 1 a b β 1 x γ 1 z d 0 e 0 α 2 α 3 c d e β 2 y γ 2 z d 0 e 0 α 2 α 4 c d e β 2 y γ 2 z
Other interesting examples show that some elements could appear several times in such a tree, since an argument can appeared in the source of several supports. Let consider the elements that impact the supported status of argument x. Here 2 trees must be considered:

a α x a γ b β x
In this case, there is no repetition since there are 2 distinct trees.

Example 8 Consider the following REBAF:

β a b α x
Let consider the elements that impact the supported status of argument x. Here a single tree must be taken into account:

a β b α x a
In this case, argument a must be repeated but in another branch and so as the source of another support.

Example 9 Consider the following REBAF:

a b α x β
Let consider the elements that impact the supported status of argument x. Here a single tree must be taken into account:

x β b α x a
In this case, argument x must be repeated but in the same branch that leads to x. And here this is a clue of an existing problem: x cannot be supported without itself.

The previous examples give the main ideas for defining the notion of "impacting support tree" for an element of the REBAF:

Definition 10 [23] Let REBAF = A,R,E,s,t,P . Let x be an element of this REBAF. An impacting support tree for x is a set IST = {x 0 , . . . , x n } with n > 0 s.t.:

∀x i , i ∈ [0 . . . n], x i ∈ (A ∪ E) \ {x}
and is called a node of the tree;

Let IST P = (IST ∩ P ∩ A). IST P = ∅; !∃x i ∈ IST s.t. x i ∈ E and t(x i ) = x; x i is called the root of the tree;9 ∀x i ∈ IST ∩ A, either ∃x j ∈ IST ∩ E s.t. x i = t(x j ), or x i ∈ IST P (in this case x i is called a leaf of the tree);

∀x i ∈ IST ∩ E, ∀x j ∈ s(x i ), x j ∈ IST.
Note that an element x cannot belong to its impacting support tree, and by definition repetition is not authorized since an IST is a set.

Example 3 (cont'd):

There is no IST for any interaction or argument. Indeed the ony element that is the target of a support is e and e has no IST, because the support cannot belong to an IST for e (one argument of its source, c, cannot belong to an IST; it is neither prima-facie, nor targeted by a support).

Example 4 (cont'd): In this example, there are 3 non prima-facie elements that are in a DCS: d, e and β. Nevertheless, there exists an IST for d ({γ, e, β, b, c}) and another one for e ({β, b, c}) Let now consider β; there is no IST for β since it cannot be supported without itself. Example 7 (cont'd): In this example, the supports and a have no IST. For b, the IST is the set {γ, a} and for x there are two sets {a, b, β, γ} and {a, α}.

Example 8 (cont'd): In this example, the supports and a have no IST. For b, the IST is the set {β, a} and for x the IST is {a, b, α, β}.

Example 9 (cont'd): In this example, the supports and a have no IST. For x and for b, the same thing occurs but for a complete different reason: for the supports and a, they are not the target of a support; for b and x the non-existence of an IST is due to the fact that these elements cannot be supported without themselves and so an IST cannot be defined.

A Framework with Higher-Order Necessary Supports and Attacks

We recalled here the main definitions and properties concerning RAFN (see [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF]), i.e. an higher-order bipolar argumentation framework using in the same time the RAF approach introduced in [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF] and the necessary meaning for supports 10Definition 11 [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF] A Recursive Argumentation Framework with Necessity (RAFN) is a tuple A, R, N, s, t , where A, R and N are three pairwise disjunct sets respectively representing arguments, attacks and necessary supports names, s is a function from R ∪ N to (2 A \ ∅) mapping each interaction to its source and t is a function from R ∪ N to (A ∪ R ∪ N) mapping each interaction to its target. It is assumed that ∀α ∈ R, s(α) is a singleton.

Note that the source of a support in a RAFN is a set of arguments, whereas the source of an attack is a singleton (it is a difference with REBAF).

It is worth to notice that correspondences have been provided between frameworks using evidential supports and those using necessary supports when we consider first-order frameworks (see [START_REF] Polberg | Revisiting support in abstract argumentation systems[END_REF]). Nevertheless, in [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF], it has been proven that these correspondences cannot be generalized in presence of higher-order interactions. So direct definitions for the semantics of RAFN have been provided in [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF], in a similar way as for a REBAF.

The definition for a structure is kept as in Definition 4:

Definition 12 [10] Let RAFN = A,R,N,s,t . A triple U = (S, Γ, ∆) is a structure of RAFN iff S ⊆ A, Γ ⊆ R and ∆ ⊆ N.
Moreover, for any pair of structures U = (S, Γ, ∆) and U = (S , Γ , ∆ ), the definitions of "U ⊆ U " and "U is ⊆-maximal (resp. ⊆-minimal)" are those given in Definition 4.

Some specific sets of elements w.r.t. a given structure must be redefined in order to take into account the necessary meaning for supports:

Definition 13 [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF] Let RAFN = A,R,N,s,t and given a structure U = (S, Γ, ∆).

The sets of defeated elements w.r.t. U are:

DefX (U ) def = {x ∈ X|∃α ∈ Γ, s(α) ∈ S and t(α) = x} with X ∈ {A, R, N} Def (U ) def = Def A (U ) ∪ Def R (U ) ∪ Def N (U )
The set of supported elements Sup(U ) is recursively defined as follows:

Sup(U ) def = {x|∀α ∈ ∆ st t(α) = x, if α ∈ Sup(U \ {x}) then s(α) ∩ (S ∩ Sup(U \ {x})) = ∅}
The set of unactivable attacks w.r.t. U is:

U nAct(U ) def = {α ∈ R|α ∈ U nAcc(U ) or s(α) ∈ U nAcc(U )}
Note that the definitions for the sets of unsupportable elements (U nSupp(U )), acceptable elements (Acc(U )) and unacceptable elements (U nAcc(U )) are similar to the definitions given in Definition 5.

Then using all these definitions, semantics for RAFN can be defined. Note that the definitions for the selfsupporting, conflict-free, admissible, complete and grounded structures are similar to the definitions given for REBAF (see Definition 8). So the only difference concerns the preferred and the stable semantics: 11Definition 14 [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF] Let RAFN = A,R,N,s,t and given a structure U = (S, Γ, ∆), U is

preferred iff it is a ⊆-maximal complete structure stable iff it is complete and (S ∪ Γ ∪ ∆) = U nAcc(U ) Example 1 (cont'd):
The argumentation framework corresponding to the example given in the introduction can be represented as follows (argument names are given in circular nodes, interaction names in square nodes, the source of a collective interaction is given in a "dotted diamond" ; attacks are represented by simple edges and supports by double edges):

a α b β c
In this framework, neither β, nor its source c are attacked. Moreover they are not the source or the target of a support, so they can be supported by any structure. So, for any structure U , it holds that neither β nor its source c is unacceptable w.r.t. U . As a consequence, for any structure U , α is not acceptable w.r.t. U as α is attacked by β and β is not unactivable w.r.t. U . Concerning b and a, they are not attacked and, since the support α from a to b is not acceptable, they are also suppoted by any structure. So it is possible to have an admissible structure containing b and not a, or containing a and not b. In this example, there is a unique complete, grounded, preferred and stable structure U = ({a, b, c}, {β}, ∅).

Example 10 Consider the following example:

a α b β δ d c
In this framework, β can be unactivable and so α can be acceptable. In this case, when α and b are in the structure, then a must also be in the structure. So we cannot have an admissible structure in which α and b are present, and a is not. In this example, there is a unique complete, grounded, preferred and stable structure U = ({a, b, c, d}, {δ}, {α}).

Background on the Logical Description of a REBAF

Here, we recall the logical description of a REBAF proposed in [START_REF] Cayrol | Logical encoding of argumentation frameworks with higher-order attacks and evidential supports[END_REF] then improved in [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], that allows an explicit representation of arguments, attacks, evidential supports and their properties.

Vocabulary

In [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], the following unary predicate symbols and unary functions symbol are used with the following meaning:

Predicate symbol Arg(x): x is an argument Attack(x) (resp. ESupport(x)):
x is an attack (resp. evidential support)

P rimaF acie(x): x is a prima-facie element Acc(x): x is accepted, with x ∈ A N Acc(x): x cannot be accepted, with x ∈ A V al(α): α is valid, with α ∈ (R ∩ E) Supp(x): x is supported, with x ∈ (A ∪ R ∩ E) U nSupp(x): x is unsupportable, with x ∈ (A ∪ R ∩ E) sAcc(x):
x is accepted and supported, with x ∈ A sV al(α): α is valid and supported, with α ∈ (R ∩ E) S(a, α): "the argument a belongs to the source of α" Function symbol

T (α): denotes the target (resp. source) of α, with α ∈ (R ∩ E)
The binary equality predicate is also used. Note that the quantifiers ∃ and ∀ range over some domain D. To restrict them to subsets of D, bounded quantifiers will be used:

∀x ∈ E (P (x)) means ∀x (x ∈ E → P (x)) or equivalently ∀x(E(x) → P (x)). So we will use:

∀x ∈ Attack (Φ(x)) (resp. ∃x ∈ Attack (Φ(x))) ∀x ∈ ESupport (Φ(x)) (resp. ∃x ∈ ESupport (Φ(x)))
and ∀x ∈ Arg (Φ(x)) (resp. ∃x ∈ Arg (Φ(x))).

Note that the meaning of N Acc(x) is not "x is not accepted" but rather "x cannot be accepted" (for instance because x is the target of a valid attack whose source is accepted). Hence, N Acc(x) is not logically equivalent to ¬Acc(x). However, the logical theory will enable to deduce ¬Acc(x) from N Acc(x), as shown below.

Logical theory for describing REBAF

In [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], several formulae describing a given REBAF are given using the following ideas.

First the meaning of an attack is described under the form of constraints on its source (an argument) and its target (an argument or an attack). Moreover, as attacks may be attacked by other attacks, some attacks may not be valid. And finally supports must be taken into account in order to define this "validity". So we have:

If an attack from an argument to an attack (or a support) is e-valid, then if its source is e-accepted, its target is not valid.

If an attack between two arguments is e-valid and if its source is e-accepted, then its target cannot be accepted. In that case, the target is not accepted.

Moreover, an evidential support can be described by the following constraints:

If an element (argument or interaction) is prima-facie, it is supported.

If an element is the target of an evidential support, it is supported if the source of the support is e-accepted and if the support is itself e-valid.

Using the vocabulary defined above, these constraints have been expressed in [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF] by the following formulae:

(1) ∀x ∈ (Attack ∪ ESupport) ∀y ∈ Attack (sV al(y) ∧ (T (y) = x) ∧ ∀z ∈ Arg(S(z, y) → sAcc(z))) → ¬V al(x)
Note that the subformula ∀z ∈ Arg(S(z, y) → sAcc(z)) means that the source of y can be viewed as accepted and supported (so e-accepted).

(

) ∀x ∈ Arg ∀y ∈ Attack (sV al(y) ∧ (T (y) = x) ∧ ∀z ∈ Arg(S(z, y) → sAcc(z))) → N Acc(x) (3) ∀x ∈ Arg (N Acc(x) → ¬Acc(x)) (1bis) ∀x ∈ (Attack ∪ ESupport ∪ Arg)       P rimaF acie(x) ∨ ∃y ∈ ESupport (sV al(y) ∧ (T (y) = x) ∧ ∀z ∈ Arg(S(z, y) → sAcc(z)))   → Supp(x)     2
The following formulae define the e-acceptability (resp. e-validity). Recall that sAcc(x) (resp. sV al) means "x is accepted (resp. valid) and supported":

(2bis) ∀x ∈ Arg ((Acc(x) ∧ Supp(x)) ↔ sAcc(x)) (3bis) ∀x ∈ (Attack ∪ ESupport) ((V al(x) ∧ Supp(x)) ↔ sV al(x))
Other formulae limit the domain to arguments, attacks, supports.

(4) ∀x (Attack(x) → ¬Arg(x)) (4bis) ∀x (Attack(x) → ¬ESupport(x)) (4ter) ∀x (ESupport(x) → ¬Arg(x)) (5) ∀x (Arg(x) ∨ Attack(x) ∨ ESupport(x))
Then the logical encoding of specificities of a given REBAF leads to the following set of formulae. Let A = {a 1 , . . . a n }, R = {α 1 , . . . , α k }, E = {α k+1 , . . . , α m } and P = {x 1 , . . . x l }.

6) S(a 1 , α)∧S(a 2 , α), ∧ . . .∧S(a n , α)∧(T (α) = b), for all α ∈ R∪E with s(α) = {a 1 , a 2 , . . . , a n } and t(α) = b (7) ∀x (Arg(x) ↔ (x = a 1 ) ∨ . . . ∨ (x = a n )) (8) ∀x (Attack(x) ↔ (x = α 1 ) ∨ . . . ∨ (x = α k )) (8bis) ∀x (ESupport(x) ↔ (x = α k+1 ) ∨ . . . ∨ (x = α m )) (8ter) ∀x (P rimaF acie(x) ↔ (x = x 1 ) ∨ . . . ∨ (x = x l )) (9) a i = a j for all a i , a j ∈ A with i = j (10) α i = α j for all α i , α j ∈ R ∪ E with i = j
Given REBAF a higher-order argumentation framework, Σ(REBAF) will denote the set of first-order logic formulae describing REBAF. And so the logical theory Σ(REBAF) is the union of all the previous formulae. It is obviously consistent.

Logical Formalization of REBAF semantics

In presence of higher-order attacks and supports, the conflict-freeness, defence, reinstatement and stability principles must take into account the fact that acceptability for an argument or an interaction requires that any attack against it is unactivable. Moreover acceptability requires support.

Conflict-freeness

In [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], the conflict-freeness principle has been formulated as follows:

If there is an e-valid attack between two arguments, these arguments cannot be jointly e-accepted.

If there is an e-valid attack from an e-accepted argument to an interaction (attack or support), this interaction cannot be e-valid.

Note that these properties are already expressed in Σ(REBAF) (by the formulae (1), ( 2), ( 3), (2bis), (3bis)).

Self-supporting

The self-supporting principle states that each supported element must receive evidential support. In [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], it has been formulated as follows:

If an element is supported then, either it is prima-facie, or it is the target of an e-valid support from an e-accepted source:

(17) ∀x ∈ (Attack ∪ ESupport ∪ Arg)     Supp(x) →   P rimaF acie(x)∨ ∃y ∈ ESupport (sV al(y) ∧ (T (y) = x) ∧ ∀z ∈ Arg(S(z, y) → sAcc(z)))      
Supportability is a weaker notion, as elements that are not supportable (i.e. unsupportable) cannot be supported. An element is unsupportable iff it is not prima-facie and for each of its supports, either the support itself or its source is defeated, or the support or its source is in turn unsupportable:

(18) ∀x ∈ (Attack ∪ ESupport ∪ Arg)           U nSupp(x) ↔         ¬P rimaF acie(x) ∧ ∀y ∈ ESupport(T (y) = x →     ∃β ∈ Attack((T (β) = y ∨ ∃z ∈ Arg(S(z, y) ∧ T (β) = z))∧ sV al(β) ∧ ∀z ∈ Arg(S(z, β) → sAcc(z)))) ∨ ∃z ∈ Arg(S(z, y) ∧ U nSupp(z)) ∨ U nSupp(y))                      
Note that the subformula ∃z ∈ Arg(S(z, y) ∧ U nSupp(z)) means that the source of y can be viewed as unsupportable. Moreover the suformula (T (β) = y ∨ ∃z ∈ Arg(S(z, y) ∧ T (β) = z)) means that T (β) is either y or belongs to the source of y.

Formulae [START_REF] Cohen | On the acceptability semantics of argumentation frameworks with recursive attack and support[END_REF] and ( 18) are added to the base Σ(REBAF), thus producing the base Σ ss (REBAF).

Defence

As stated in Definition 7, an attacked element is acceptable if (i) it is supported and (ii) for each attack against it, either the source or the attack itself is defeated (by an e-valid attack from an e-accepted argument), or the source or the attack itself is unsupportable (w.r.t. e-valid elements and e-accepted arguments). So, in [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], the principle corresponding to the previous item (ii) has been expressed by the following formulae that are associated with formulae (17) and ( 18):

(11) ∀α ∈ Attack       Acc(T (α)) →     ∃β ∈ Attack ((T (β) = α ∨ ∃z ∈ Arg(S(z, α) ∧ T (β) = z)) ∧ sV al(β) ∧ ∀z ∈ Arg(S(z, β) → sAcc(z))) ∨ ∃z ∈ Arg(S(z, α) ∧ U nSupp(z)) ∨ U nSupp(α)           (12) ∀α ∈ Attack ∀δ ∈ (Attack ∪ ESupport)       ((δ = T (α)) ∧ V al(δ)) →     ∃β ∈ Attack ((T (β) = α ∨ ∃z ∈ Arg(S(z, α) ∧ T (β) = z)) ∧ sV al(β) ∧ ∀z ∈ Arg(S(z, β) → sAcc(z))) ∨ ∃z ∈ Arg(S(z, α) ∧ U nSupp(z)) ∨ U nSupp(α)          
Formulae [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF] and (12) are added to the base Σ ss (REBAF), thus producing the base Σ d (REBAF).

Reinstatement

In [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], the reinstatement principle has been expressed by the following formulae that are be associated with formulae [START_REF] Cohen | On the acceptability semantics of argumentation frameworks with recursive attack and support[END_REF] and (18):

(13) ∀c ∈ Arg                   ∀α ∈ Attack       T (α) = c →     ∃β ∈ Attack((T (β) = α ∨ ∃z ∈ Arg(S(z, α) ∧ T (β) = z)) ∧ sV al(β) ∧ ∀z ∈ Arg(S(z, β) → sAcc(z))) ∨ ∃z ∈ Arg(S(z, α) ∧ U nSupp(z)) ∨ U nSupp(α)                   → Acc(c)           (14) ∀δ ∈ (Attack ∪ ESupport)                   (∀α ∈ Attack       T (α) = δ →     ∃β ∈ Attack((T (β) = α ∨ ∃z ∈ Arg(S(z, α) ∧ T (β) = z)) ∧ sV al(β) ∧ ∀z ∈ Arg(S(z, β) → sAcc(z))) ∨ ∃z ∈ Arg(S(z, α) ∧ U nSupp(z)) ∨ U nSupp(α)                   → V al(δ)          
Formulae (13) and ( 14) are added to the base Σ ss (REBAF), thus producing the base Σ r (REBAF).

Stability

In [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF], the stability principle has been expressed by the three following formulae that are associated with formulae (17) and (18):13

(15) ∀c ∈ Arg   ¬Acc(c) → ∃β ∈ Attack(T (β) = c ∧ sV al(β) ∧ ∀z ∈ Arg(S(z, β) → sAcc(z)))   (16) ∀α ∈ (Attack ∪ ESupport)   ¬V al(α) → ∃β ∈ Attack(T (β) = α ∧ sV al(β) ∧ ∀z ∈ Arg(S(z, β) → sAcc(z)))   (19) ∀x ∈ (Arg ∪ Attack ∪ ESupport) (¬Supp(x) → U nSupp(x))
Formulae (15), ( 16) and ( 19) are added to the base Σ ss (REBAF), thus producing the base Σ s (REBAF).

I is a ⊆-maximal model of Σ(REBAF) iff there is no model I of Σ(REBAF) with (S I ∪ Γ I ∪ ∆ I ) ⊂ (S I ∪ Γ I ∪ ∆ I ). I is a ⊆-minimal model of Σ(REBAF) iff there is no model I of Σ(REBAF) with (S I ∪ Γ I ∪ ∆ I ) ⊂ (S I ∪ Γ I ∪ ∆ I ).
Let recall that the existence of support cycles leads to the following definition in order to avoid the models in which some elements could be supported only with themselves: Definition 15 Let REBAF = A,R,E,s,t,P . I is a support-founded interpretation iff the two following conditions hold:

1. for each argument (resp. support) x non prima-facie, belonging to a maximal DCS and s.t. I(sAcc(x)) = true (resp. I(sV al(x)) = true), there exists at least one impacting support tree IST = {x 0 , . . . , x n } for x that is satisfied by Let Σ y be a base of formulae built over REBAF. A support-founded model of Σ y is a support-founded interpretation which is a model of Σ y .

I, i.e. ∀x i ∈ IST, if x i ∈ A then I(sAcc(x i )) =
Then using these support-founded models, the following characterization of REBAF semantics is given in [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF]:

Proposition 1 [START_REF]Handling support cycles and collective interactions in the logical encoding of higher-order bipolar argumentation frameworks[END_REF] Let REBAF = A,R,E,s,t,P . Let U = (S, Γ, ∆) be a structure on REBAF.

Towards a new version of RAFN 4.1 Analysis of the RAFN behaviour

Before to encode logically a RAFN we must identify more precisely its behaviour.

Of course, some results concerning REBAF can be reused since some definitions are common. For instance, let RAFN = A, R, N, s, t , let U and U be 2 structures of RAFN, if U ⊆ U then Def (U ) ⊆ Def (U ). 14Nevertheless many other results cannot be reused due to the differences concerning the support relation. Indeed, consider the following very simple example. In this case, consider three different and admissible structures: U 1 = (∅, ∅, ∅), U 2 = (∅, ∅, {α}) and U 3 = ({a}, ∅, {α}) Then we have: 15Sup(U 1 ) = {a, b, α} Sup(U 2 ) = {a, α} (b cannot belong to the set of supported elements by the structure since the support α is in the structure and its source a is not)

Sup(U 3 ) = {a, b, α}
So U ⊆ U does not imply that Sup(U ) ⊆ Sup(U ). 16 This non-monotonicity of the Sup relation implies the fact that there is no fundamental lemma for RAFN (see in [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF]).

Another negative result is the following: in the general case and even if U is conflict-free and self-supporting, Acc(U ) ⊆ U nAcc(U ). 17 this implies that Acc(U ) = {b, c, α, β} (since β is not unactivable, a cannot be acceptable).

An important point appears here: there may exist some structures U such that Sup(U ) ∩ U nSupp(U ) = ∅ and Acc(U ) ∩ U nAcc(U ) = ∅. So for a given structure it may exist an element that can be in the same time supported/acceptable and unsupportable/unacceptable by the structure.

This point is not a blocking point for the semantics computation since a such element is detected and so removed when we compare a structure and its acceptable elements for the admissibility property (in the previous example the structure U = ({b, c}, {β}, ∅) is included in Acc(U ) = {b, c, α, β} but the structure U 1 = ({b, c}, {β}, {α}) is not included in Acc(U 1 ) = {c, α, β}, so U is admissible and U 1 is not). Nevertheless it is a big problem when we try to encode with a classical logic such a behaviour.

Perhaps, it could be interesting to identify in which cases this happens. this implies that Acc(U ) = {b, α, β}.

In this case, we have

Sup(U ) ∩ U nSupp(U ) = ∅ and Acc(U ) ∩ U nAcc(U ) = ∅.
Here the main difference between these 2 cases is the fact that, in the first case, we have in the structure a way to invalidate the source of the support, using an attack targeting this source. Nevertheless, it is not so obvious to identify precisely in all possible cases what is the reason explaining the fact that an element could be at the same time supported and unsupportable. Moreover these elements can also be at the same time acceptable and unacceptable but they are not the only ones. The following example illustrates this fact. this implies that Acc(U ) = {b, c, d, α, β, γ} (since β is not unactivable, a cannot be acceptable and since γ is unactivable then d is acceptable).

So Sup(U ) ∩ U nSupp(U ) = {b} and Acc(U ) ∩ U nAcc(U ) = {b, d}. Here the fact that b can be at the same time supported and unsupportable has an impact on the status of d that becomes at the same time acceptable and unacceptable.

Another interesting point in this example is the following: Acc(U ) ∩ Def (U ) = ∅ whereas U is conflict-free and self-supporting. This shows that Lemma A.2 given in [START_REF] Cayrol | Argumentation Frameworks with Recursive Attacks and Evidence-Based Supports[END_REF] for REBAF cannot be applied for RAFN. And once again that seems to be a side effect of the existence of b as a supported and unsupportable element.

So, in conclusion, the RAFN defined in [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF] is clearly a problematic framework when we are searching a logical encoding. So in this paper, we propose a new version of RAFN in order to avoid all these problems.

A new framework for RAFN

The previous examples clearly show that the problem is in the definition of the U nSupp set. Recall that, in the framework proposed in [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF], this set is defined as follows:

Definition 16 Let RAFN = A, R, N, s, t . Let U be a structure of RAFN. The set of unsupportable elements w.r.t. U is:

UnSupp(U ) def = Sup(U ) with U = (Def A (U ), R, Def N (U ))
So we propose here a very simple solution:

Definition 17 Let RAFN = A, R, N, s, t . Let U be a structure of RAFN. The set of unsupportable elements w.r.t. U is:

UnSupp(U ) def = Sup(U ) \ Sup(U ) with U = (Def A (U ), R, Def N (U ))
The impact of this definition is illustrated with the following example: Example 13 (cont'd): In this example, with the new definition of the U nSupp set and always with the admissible structure U = ({b, c}, {β, γ}, ∅), we have the following results: b,c,d,α,β, γ} and Def (U ) = {a, d}, (unchanged since the U nSupp set is not used for defining the Sup and the Def sets) so U = (Def A (U ), R, Def N (U )) = ({b, c}, {β, γ}, {α}) (unchanged) and U nSupp(U ) = ∅ (changed of course); then U nAcc(U ) = {a, d} and U nAct(U ) = ∅ (changed also); this implies that Acc(U ) = {b, c, α, β, γ} (now γ is not unactivable so d cannot be acceptable).

Sup(U ) = {a,

Formulae

The second adaptation concerns the differences between necessary and evidential supports and their impact on the formulae encoding the framework and the semantics. These differences can be synthetized as follows:

First, in the RAFN case, an element is supported iff, for each support targeting this element and belonging to the structure, at least one element of the source of this support is also supported by the structure. Whereas, in the REBAF case, an element is supported iff, for at least one support targeting this element and belonging to the structure, each element of the source of this support is also supported by the structure.

Secondly, in the RAFN case, an attack is unactivable iff it is unacceptable or its source is included in the set of unacceptable elements. Whereas, in the REBAF case, an attack is unactivable iff it is unacceptable or at least one element of its source belongs to the set of unacceptable elements.

Thirdly, the source of an attack is a singleton. This last point could induce some simplification in the formulae. Nevertheless, here we do not take it into account, since it would imply to distinguish between a source of an attack and a source of a support and so a modification of the vocabulary that is not really necessary.

A consequence of these différences is the fact that the source of a support, that is a set of arguments, is in the same time accepted and supported if at least one element in this set is in the same time accepted and supported. And we have of course the dual situation for the unsupportable status: the source of a support is unsupportable if each element of this set is unsupportable.

So the previous points lead to the following evolution of the formulae for the encoding of any RAFN.

Formula (1) is unchanged except that N Support is used in place of ESupport (see Section 3) Formula (2) is unchanged (see Section 3) Formula (3) is unchanged (see Section 3) Formula (1bis) becomes:

∀x ∈ (Attack ∪ N Support ∪ Arg)   ∀y ∈ N Support ((sV al(y) ∧ (T (y) = x)) → ∃z ∈ Arg(S(z, y) ∧ sAcc(z))) → Supp(x)   Formula (2bis) is unchanged (see Section 3)
Formula (3bis) is unchanged except that N Support is used in place of ESupport (see Section 3) Formula (4) is unchanged (see Section 3) Formula (4bis) is unchanged except that N Support is used in place of ESupport (see Section 3) Formula (4ter) is unchanged except that N Support is used in place of ESupport (see Section 3) Formula ( 5) is unchanged except that N Support is used in place of ESupport (see Section 3) Then the logical encoding of specificities of a given RAFN leads to the following set of formulae. Let A = {a 1 , . . . a n }, R = {α 1 , . . . , α k }, N = {α k+1 , . . . , α m }. Formula (6) is unchanged (see Section 3) Formula (7) is unchanged (see Section 3) Formula (8) is unchanged (see Section 3) Formula (8bis) is unchanged except that N Support is used in place of ESupport (see Section 3) Formula (8ter) is removed Formula (9) is unchanged (see Section 3) Formula (10) is unchanged (see Section 3)

Let consider now the encoding of the principles used in RAFN semantics.

Principle for conflict-freeness: As for REBAF, the conflict-freeness is already expressed by the formulae (1), ( 2), ( 3), (2bis), (3bis).

Principle for self-supporting: For each support that is accepted and supported and that targets a supported element, at least one element of its source must be accepted and supported. And of course, elements that are unsupportable cannot be supported. That leads to the following evolution of formulae [START_REF] Cohen | On the acceptability semantics of argumentation frameworks with recursive attack and support[END_REF] and [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]:

Formula (17): ∀x ∈ (Attack ∪ N Support ∪ Arg) Supp(x) → ∀y ∈ N Support (sV al(y) ∧ (T (y) = x)) → ∃z ∈ Arg(S(z, y) ∧ sAcc(z))
Formula (18):

∀x ∈ (Attack ∪ N Support ∪ Arg)           U nSupp(x) ↔ ¬Supp(x) ∧         ∃y ∈ N Support((T (y) = x) ∧ (∀α ∈ Attack((T (α) = y ∧ sV al(α)) → ∃u ∈ Arg(S(u, α) ∧ ¬sAcc(u)))) ∧¬U nSupp(y) ∧   ∀z ∈ Arg(S(z, y) →   ∃β ∈ Attack((T (β) = z) ∧ sV al(β)∧ ∀u ∈ Arg(S(u, β) → sAcc(u))) ∨ U nSupp(z)                      
Principle for defence: The formulae (11) and (12) related to this principle remain unchanged except that N Support is used in place of ESupport (see Section 3).

Principle for reinstatement: The formulae (13) and ( 14) related to this principle remain unchanged except that N Support is used in place of ESupport (see Section 3).

Principle for stability: The formulae (15), ( 16) and (19) related to this principle remain unchanged except that N Support is used in place of ESupport (see Section 3).

The logical bases for RAFN: The definitions of the 5 logical bases are similar to the ones given for REBAF (see Section 3). So we have: 15), ( 16), (19)}

Σ(RAFN) = {(1), . . . , (10)} Σ ss (RAFN) = Σ(RAFN) ∪ {(17), (18)} Σ d (RAFN) = Σ ss (RAFN) ∪ {(11), (12)} Σ r (RAFN) = Σ ss (RAFN) ∪ {(13), (14)} Σ s (RAFN) = Σ ss (RAFN) ∪ {(

New definitions

Considering the definition of the supported elements, we can see that, in the case of RAFN as in the case of REBAF, the use of the logical bases is not sufficient for avoiding some problematic models when support cycles exist.

Even if the definition of such cycles can be kept the same, we must adapt the definition of support-founded models and consequently the definition of "impacting support elements" since the behaviour of the necessary supports is different to that of evidential supports.

This can be illustrated with the following example. Example 6 (cont'd): Using the definitions related to RAFN, the constraints related to the necessary supports induce the following results:

Consider for instance z: z will be supported by a structure iff, for any support targeting z and belonging to the structure, at least an element of its source is also present in the structure; that means that if γ 1 (resp. γ 2 ) is in the structure then x (resp. y) must also be in the structure and if γ 1 (resp. γ 2 ) is not in the structure then there is no constraint about x (resp. y): it can be in the structure or not.

Consider now x: x will be supported iff, if β 1 is in the structure then a or b are also in the structure.

So if we want to identify the "impacting support elements", we also have trees but not the same trees as the ones proposed for the REBAF. For instance, considering z, there exist 6 trees giving the "impacting support elements" concerning z:18

a 0 d 0 α 1 α 2 a d β 1 β 2 x y γ 1 γ 2 z d 0 α 2 b d β 1 β 2 x y γ 1 γ 2 z a 0 α 1 a c β 1 β 2 x y γ 1 γ 2 z b c β 1 β 2 x y γ 1 γ 2 z a 0 e 0 e 0 α 1 α 3 α 4 a e β 1 β 2 x y γ 1 γ 2 z e 0 e 0 α 3 α 4 b e β 1 β 2 x y γ 1 γ 2 z
Moreover, it is worth to notice that the existence of one of these trees is not required for having z supported. Indeed if γ 1 and γ 2 are not in the structure, z is obviously supported by the structure.

Concerning the possible repetitions, the behaviour for RAFN is once again different that the one for REBAF. The repetition in the second tree illustrates the fact that this tree cannot be used in order to show that x is supported.

In the light of the previous example, we see that the definition and the use of such trees for RAFN are completely different from those for REBAF. So we propose a new definition for the notion of "impacting support tree" for an element of the RAFN: Definition 18 Let RAFN = A,R,N,s,t . Let x be an element of this RAFN. An impacting support tree for x is a set IST = {x} ∪ IST s.t.:

x is called the root of the tree;

IST = ∅ iff y ∈ N s.t. t(y) = x; otherwise IST = {x 0 , . . . , x n } with n > 0 and ∀x i , i ∈ [0 . . . n], x i ∈ (A ∪ N) \ {x} and is called a node of the tree; ∀y ∈ N, if x = t(y) then y ∈ IST ; 19 ∀x i ∈ (IST ∩ A), if x j ∈ N s.t. x i = t(x j ) then x i is called a leaf of the tree; otherwise, ∀x j ∈ N, if x i = t(x j ) then x j ∈ IST ; ∀x i ∈ (IST ∩ N), ∃x j = x, x j ∈ s(x i ) such that x j ∈ IST .
Note that, contrary to the case for REBAF, an element x must belong to its impacting support tree. So in order to avoid the problems due to the support cycles, the selection of x as a source of a support is not authorized. Example 3 (cont'd): There are at least two IST for e: {e, , b} and {e, , c} (and a third one by aggregation). And for all the other elements of this RAFN, each of them has only one IST reduced to a singleton (so {b} for b, {c} for c, . . . ).

Example 4 (cont'd):

Here, contrary to the REBAF case, there is one IST for β: {β, α, a}. It cannot exist an IST for β using d since d is supported by γ whose source e is in turn supported by β, so a repetition that is prohibited by Def. 18. Nevertheless, d itself has at least two IST: {d, γ, e, β, b} and {d, γ, e, β, c} .

Example 5 (cont'd): Once again, the result for RAFN is different of that for REBAF. In the case of RAFN, there is no IST for d; indeed, even if one branch of an IST for d could be composed with γ and e, the other branch concerning the support α 1 cannot be built since, whatever we choose between a or b, we obtain a branch in which a repetition should appear. And the same thing occurs for a, b and c.

In this example, only e and the supports have an IST, each time reduced to a singleton (so {e} for e, {α 1 } for α 1 , . . . ).

Example 14

This example is a part of Ex. 5. Example 7 (cont'd): In this example, each element has only one IST. For each support and for a, the IST is reduced to the singleton containing the corresponding element. For b, the IST is the set {b, γ, a} and for x it is the set {x, a, b, α, β, γ}.

Example 8 (cont'd):

In this example, each support has only one IST, reduced to the singleton containing the corresponding support. The same thing occurs for a. For b, the IST is the set {b, β, a} and for x there are two sets {x, a, α} and {x, a, b, α, β}.

Example 9 (cont'd):

In this example, a, α and β have only one IST, reduced to the singleton containing the corresponding element. For x, only one IST exists, the set {x, α, a} and for b the IST is also unique, {x, a, b, α, β}. Indeed, the set {x, b, α, β} cannot be an IST for b since the source of α cannot be b, since b is the root of the IST. Idem for x: the set {x, b, α, β} cannot be an IST for x since the source of β cannot be x, since x is the root of the IST.

Characterization: a new proposition

At this point, it is worth to note that if there is no support cycles in the RAFN then the use of the formulae bases is enough for characterizing the RAFN semantics without the removal of some models. So the difficulty comes with the existence of these cycles and implies that we are able to remove the models in which an element is supported only because it is satisfied by these models (so in contradiction Def. 13).

So using the definitions of DCS and IST, we are now able to propose a definition for support-founded interpretations and models adapted to the case of RAFN: Definition 19 Let RAFN = A,R,N,s,t and let use RAFN-v2 definitions. I is a support-founded interpretation iff the two following conditions hold:

1. for each argument (resp. support) x of RAFN, belonging to a maximal DCS and s.t. I(sAcc(x)) = true (resp.

I(sV al(x)) = true), two cases must be considered: if there does not exist an impacting support tree IST for x then, ∀β ∈ N belonging to the same DCS that x and s.t. t(β) = x, I does not satisfy β (so I(sV al(β)) = false); otherwise, among the existing impacting support trees for x, there exists at least one IST s.t., considering any support β ∈ IST s.t. t(β) = x, if I satisfies β (so I(sV al(β)) = true) then I must also satisfy at least an element of the source of β that belongs to IST (so

∃x i ∈ s(β) ∩ IST s.t. I(sAcc(x i )) = true). 2. for each element x of RAFN, I(U nSupp(x)) = true iff x ∈ U nSupp(U I ) with U I = (S I , Γ I , ∆ I ).
Let Σ y be a base of formulae built over RAFN. A support-founded model of Σ y is a support-founded interpretation which is a model of Σ y .

Then using these support-founded models, the following characterization of RAFN-v2 semantics can be given:

Proposition 3 Let RAFN = A,R,N,

Conclusion

In this work, we have proposed an adaptation of the logical encoding presented for REBAF in order to take into account argumentation frameworks with higher-order attacks and necessary supports (RAFN).

This leads to a new notion of impacting support trees (IST), in order to adapt the notion of support-founded models to RAFN.

Then using all these elements, we provided a characterization of admissible (resp. complete, preferred, stable and grounded) structures for the most general definition of RAFN.

A Differences between REBAF and RAFN-v2

These differences are due to the interpretation of the meaning of the supports and to some constraints existing in a framework and not in the other framework. So we have an impact on the definition of the semantics (and so on the notions used for defining these semantics), and another impact in the logical encoding of these frameworks and the corresponding characterization.

A.1 In terms of semantics

Here two main differences: the first one could be neglicted: in REBAF and in RAFN, the source of an attack is a set of arguments, but in RAFN, this set is a singleton. This impacts the definition of the sets Def (U ) and U nAct(U ); the second difference concerns the meaning of the supports and impacts the definition of the sets Sup(U ), U nSupp(U ) and the definition of the preferred and stable semantics.

These differences are synthetized in the following table (the important points are given in a red box):

Let U = (S, Γ, ∆) be a structure Notions REBAF case RAFN case

Def X (U ) def = {x ∈ X|∃α ∈ Γ, s(α) ⊆ S and t(α) = x} {x ∈ X|∃α ∈ Γ, s(α) ∈ S and t(α) = x} Sup(U ) def = P∪ {t(α)| ∃ α ∈ ∆ ∩ Sup(U \{t(α)}), s(α) ⊆ (S ∩ Sup(U \{t(α)}))} {x| ∀ α ∈ ∆ st t(α) = x, if α ∈ Sup(U \ {x}) then s(α) ∩ (S ∩ Sup(U \ {x})) = ∅} UnSupp(U ) def = Sup(U ) with U = (Def A (U ), R, Def E (U )) Sup(U ) \Sup(U ) with U = (Def A (U ), R, Def E (U )) UnAct(U ) def = {α ∈ R|α ∈ UnAcc(U ) or s(α) ∩ UnAcc(U ) = ∅ } {α ∈ R|α ∈ U nAcc(U ) or s(α) ∈ U nAcc(U )} U is pref. iff it is a ⊆-maximal admissible structure it is a ⊆-maximal complete structure U is stab. iff (S ∪ Γ ∪ ∆) = UnAcc(U ) it is complete and (S ∪ Γ ∪ ∆) = U nAcc(U )
A.2 In terms of logical encoding

The differences are of course induced by the differences in terms of semantics evoked in the previous section, particularly the second one, and are synthetized in the following table (the important points are given in a red box): REBAF case RAFN case

(1bis) ∀x ∈ (Attack ∪ ESupport ∪ Arg)             P rimaF acie(x) ∨ ∃y ∈ ESupport (sV al(y) ∧ (T (y) = x)∧ ∀z ∈ Arg(S(z, y) → sAcc(z)))      → Supp(x)        ∀x ∈ (Attack ∪ N Support ∪ Arg)         ∀y ∈ N Support ((sV al(y) ∧ (T (y) = x)) → ∃z ∈ Arg(S(z, y) ∧ sAcc(z)))    → Supp(x)      REBAF case RAFN case (17) ∀x ∈ (Attack ∪ ESupport ∪ Arg)        Supp(x) →      P rimaF acie(x)∨ ∃y ∈ ESupport (sV al(y) ∧ (T (y) = x) ∧ ∀z ∈ Arg(S(z, y) → sAcc(z)))             ∀x ∈ (Attack ∪ N Support ∪ Arg)      Supp(x) →    ∀y ∈ N Support (sV al(y) ∧ (T (y) = x)) → ∃z ∈ Arg(S(z, y) ∧ sAcc(z))              
So an element is unsupportable iff it is not supported and at least one of its supports is not unsupportable and not defeated and has no effective source Moreover, the notion of IST completely differs between the two frameworks: An impacting support tree for x is a set IST s.

∀x i ∈ IST ∩ E, ∀x j ∈ s(x i ), x j ∈ IST. IST = {x} ∪ IST s.t.:
x is called the root of the tree;

IST = ∅ iff y ∈ N s.t
∀x i ∈ (IST ∩A), if x j ∈ N s.t. x i = t(x j ) then x i is called a leaf of the tree; otherwise, ∀x j ∈ N, if x i = t(x j ) then x j ∈ IST ; ∀x i ∈ (IST ∩ N), ∃x j = x, x j ∈ s(x i ) such that x j ∈ IST .
The last difference exists concerning the notion of support-founded interpretation:

I is a support-founded interpretation iff the two following conditions REBAF case RAFN case 1. for each argument (resp. support) x non prima-facie, belonging to a maximal DCS and s.t.

I(sAcc(x)) = true (resp. I(sV al(x)) = true), there exists at least one impacting support tree IST = {x 0 , . . . , x n } for x that is satisfied by I, i.e. ∀x i ∈ IST, if x i ∈ A then I(sAcc(x i )) = true, otherwise I(sV al(x i )) = true; 1. either no supported support targets y 2. or for any supported support β that targets y either β ∈ U or β and a part of its source belong to U y ∈ U nSupp 1 (U ) corresponds to the fact that there exists at least one supported support β not defeated by U whose source is defeated by U or not supported.

So considering the aggregation of constraints and the fact that U is conflict-free, we must be in the case where there exists at least one supported support β not defeated by U but also not belonging to U and whose source is defeated by U or not supported; however U is complete 1 then, since β is supported and not defeated, it should be in Acc 1 (U ) and so in U ; so contradiction. So x ∈ Acc 2 (U ).

Thus U is complete 1 iff U is complete 2 .
σ is preferred: following the previous item and the definition of the preferred semantics in the RAFN case (see Def. 14), it is obvious to see that U is preferred 1 iff U is preferred 2 σ is grounded: following the item about completeness and the definition of the grounded semantics in the RAFN case (similar to the one given for the REBAF case, see Def. 8), it is obvious to see that U is grounded

1 iff U is grounded 2
σ is stable: following the item about completeness and the definition of the stable semantics in the RAFN case (see Def. 14), for proving that U is stable

1 iff U is stable 2 , it remains to prove that U = U nAcc 1 (U ) iff U = U nAcc 2 (U ), i.e. U = U nAcc 1 (U ) iff U = U nAcc 2 (U )
. This proof is similar to the one given in the item about completeness.

Consider first an element

x ∈ U = U nAcc 1 (U ): since U nAcc 2 (U ) ⊆ U nAcc 1 (U ) then x ∈ U nAcc 2 (U ). So U = U nAcc 1 (U ) ⊆ U nAcc 2 (U ).
Consider now an element x ∈ U = U nAcc 2 (U ) and show that x ∈ U nAcc 1 (U ). Assume that there exists an element x st x ∈ U = U nAcc 2 (U ) and x ∈ U nAcc 1 (U ), i.e. x ∈ U , x ∈ U nAcc 2 (U ) and x ∈ U nAcc 1 (U ). Since U nAcc(U ) = Def (U ) ∪ U nSupp(U ), considering that x ∈ U nAcc 2 (U ) means that x ∈ Def 2 (U ) and x ∈ U nSupp 2 (U ) and considering that x ∈ U nAcc 1 (U ) means that x ∈ Def 1 (U ) or x ∈ U nSupp 1 (U ); x ∈ Def 1 (U ) is clearly in contradiction with x ∈ Def 2 (U ) since Def 1 (U ) = Def 2 (U ); so the only possible case remains x ∈ U nSupp 1 (U ), knowing that x ∈ U nSupp 2 (U ), so x ∈ Sup 1 (U ). This is exactly the same configuration that the one described in the proof of the completeness item for the variable y and the same reasoning can be applied leading to a contradiction: there exists at least one supported support β for x not defeated by U but also not belonging to U and whose source is defeated by U or not supported; however U is complete 1 then, since β is supported and not defeated, it should be in Acc 1 (U ) and so in U ; so contradiction. So x ∈ U nAcc 1 (U ).

Thus U is stable 1 iff U is stable 2 .

B.2 Some additional results

For the next proofs, a notation and some lemmas will be useful.

Notation 1 Let U = (S, Γ, ∆) be a structure of RAFN, and x ∈ A ∪ R ∪ N. x will be said to be defended by U , iff every attack α ∈ R with t(α) = x is unactivable w.r.t. U . Defended (U ) will denote the set of elements that are defended by U . Note that x ∈ Acc(U ) iff x ∈ Sup(U ) and x ∈ Defended (U ).

Lemma 1 Let RAFN = A, R, N, s, t and let use RAFN-v2 definitions. Any conflict-free structure U satisfies Acc(U ) ∩ Def (U ) = ∅.

Lemma 4 Let RAFN = A, R, N, s, t and let use RAFN-v2 definitions. Let U = (S, Γ, ∆) be a structure. Consider an element x such that, for any support y ∈ ∆ ∩ Sup(U ) that targets x, then s(y) ∩ S ∩ Sup(U ) = ∅. Then, x ∈ Sup(U ).

Proof of Lemma 4 Assume that x ∈ Sup(U ). So, by the definition of the Sup set, ∃y st t(y) = x and y ∈ ∆ ∩ Sup(U \ {x}) and s(y)∩S∩Sup(U \{x}) = ∅. Since s(y)∩S∩Sup(U ) = ∅, there exists z ∈ s(y)∩S and z ∈ Sup(U )\Sup(U \{x}). So, for any couple (z, y), we have a chain of supports (each support and a part of its source belong to U ) leading to x and containing z and y. This chain can be schematically represented by: either x β1

. . . The idea is to define I by successively adding constraints that I should satisfy: For all

x ∈ A ∪ R ∪ N, I(Arg(x)) = true iff x ∈ A, I(Attack(x)) = true iff x ∈ R and I(N Support(x)) = true iff x ∈ N. For all x ∈ A ∪ R ∪ N, I(Supp(x)) = true iff x ∈ Sup(U ). For all x ∈ A ∪ R ∪ N, I(U nSupp(x)) = true iff x ∈ U nSupp(U . For all x ∈ A, I(Acc(x)) = true iff x ∈ S or (x / ∈ S, x / ∈ Sup(U ) and x ∈ Defended (U )).
For all x ∈ A, I(N Acc(x)) = true iff I(Acc(x)) = false. For all x ∈ R (resp. ∈ N), I(V al(x)) = true iff x ∈ Γ (resp. ∆) or (x / ∈ Γ (resp. ∆), x / ∈ Sup(U ) and x ∈ Defended (U )). For all x ∈ A, I(sAcc(x)) = true iff (I(Acc(x)) = true and I(Supp(x)) = true). For all x ∈ R ∪ N, I(sV al(x)) = true iff (I(V al(x)) = true and I(Supp(x)) = true). We have to prove that S I = S, Γ I = Γ, ∆ I = ∆, and that I is a support-founded model of Σ d (RAFN). And for proving that I is a support-founded model of Σ d (RAFN) it is sufficient to prove that I satisfies the formulae (1), ( 2), ( 3), (1bis), (2bis), (3bis) and ( 17), ( 18), ( 11), [START_REF] Cayrol | Gradual valuation for bipolar argumentation frameworks[END_REF] and that is a support-founded interpretation. 21Let x ∈ S I . By definition of S I , I(sAcc(x)) = true, that is I(Acc(x)) = true and I(Supp(x)) = true. By definition of I(Acc) and I(Supp) it follows that x ∈ S. Conversely, given x ∈ S, it holds that I(Acc(x)) = true. As U is admissible, U is self-supporting, so x ∈ Sup(U ), then it holds that I(Supp(x)) = true. As a consequence, I(sAcc(x)) = true and x ∈ S I . Proving that Γ I = Γ and ∆ I = ∆ is similar.

Obviously I satisfies formulae (3), (2bis), (3bis).

Let us first consider formula (2). Let y ∈ R and x ∈ A with x = T (y), I(sV al(y)) = true and I(∀z ∈ Arg(S(z, y) → sAcc(z))) = true (so, since in the case of RAFN the source of any attack is a singleton, here denoted by x y , we have I(sAcc(x y )) = true). Then s y ∈ S and y ∈ Γ. Let us assume that I(N Acc(x)) = false. Then I(Acc(x)) = true, by definition of I(N Acc). As U is admissible, U is conflict-free, so x cannot belong to S, and, by definition of I(Acc), it follows that x ∈ Def ended(U ) and so y ∈ U nAct(U ), that is y or s y belong to U nAcc(U ). However, y and s y being elements of the admissible structure U , due to Lemma 2, we obtain a contradiction. Hence, we have proved that I(N Acc(x)) = true and formula (2) is satisfied by I. Proving that formula (1) is satisfied by I is similar.

Let us first consider formula [START_REF] Cohen | On the acceptability semantics of argumentation frameworks with recursive attack and support[END_REF]. Let x such that I(Supp(x)) = true. By definition of I(Supp), x ∈ Sup(U ). By definition of Sup(U ), for any support α targeting x and such that α ∈ ∆ and α ∈ Sup(U \ {x}), then s α ∩ S ∩ Sup(U \ {x}) = ∅. As S = S I and ∆ = ∆ I it holds that there exists an element z in s α st I(sAcc(z)) = true and I(sV al(α)) = true. Hence formula (17) is satisfied by I.

Let us consider formula (1bis). If x is not the target of a support belonging to U then x ∈ Sup(U ) and formula (1bis) is trivially satisfied by I. Consider now the case of any support y that targets x and such that I(∃z ∈ Arg(S(z, y) ∧ sAcc(z))) = true and I(sV al(y)) = true. We have to prove that I(Supp(x)) = true. As S I = S and ∆ I = ∆ it holds that y ∈ ∆ and s y ⊆ S. Moreover, as U is admissible, U is selfsupporting, so y and some elements of s y belong to Sup(U ). From Lemma 4, it follows that x ∈ Sup(U ) hence I(Supp(x)) = true. So formula (1bis) is satisfied by I.

Let us now consider formula [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. First, for the "only if part", consider x such that I(U nSupp(x)) = true. By definition of I(U nSupp), x ∈ U nSupp(U ). So x / ∈ Supp(U ) and I(¬Supp(x)) = true. Moreover, since U nSupp(U ) = Sup(U ) (where U = (Def A (U ), R, Def N (U ))), x ∈ Sup(U ). So using the contrapositive of Lemma 4, applied to the structure U , it follows that for at least one support y leading to x, y ∈ Def (U ) ∩ Sup(U ) and s(y) ∩ Def (U ) ∩ Sup(U ) = ∅. so we have: if y ∈ Def (U ): so y ∈ Def (U ); that implies that for any attack α in U and targeting y, s(α) is not included in U ; so the subformula ∀α ∈ Attack((T (α) = y ∧ sV al(α)) → ∃u ∈ Arg(S(u, α) ∧ ¬sAcc(u))) is satisfied by I; if y ∈ Sup(U ): so y ∈ U nSup(U ); this implies that the formula ¬U nSupp(y) is satisfied by I; if s(y) ∩ Def (U ) ∩ Sup(U ) = ∅: so for any z ∈ s(y), either z is defeated by U (so the subformula ∃β ∈ Attack((T (β) = z) ∧ sV al(β) ∧ ∀u ∈ Arg(S(u, β) → sAcc(u))) is satisfied by I), or z ∈ Sup(U ) (so the subformula U nSupp(z) is satisfied by I). So the "only if" part of formula (18) is satisfied by I. For the "if" part, let us consider x such that x / ∈ Sup(U ) and there exists a support that is not defeated by U , that is not unsupportable by U and whose source components are either defeated or unsupportable by U . So x / ∈ Sup(U ) and x / ∈ Sup(U ); thus, by the definition of the U nSupp set, we have x ∈ U nSupp(U ) and so I(U nSupp(x)) = true. So formula [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] is satisfied by I.

Let us now consider formula [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF]. Let α ∈ R and x ∈ A such that x = T (α) and I(Acc(x)) = true. By definition of I(Acc), either x ∈ S or (x / ∈ S, x / ∈ Sup(U ) and x ∈ Defended (U )). As U is admissible, in both cases, it holds that α ∈ U nAct(U ). Then the fact that I satisfies formula [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF] follows directly from the definition of U nAct(U ), the definition of I(U nsupp) and the fact that for an argument (resp. an attack) x, I(sAcc(x)) = true (resp. I(sV al(x)) = true) iff x ∈ S (resp. x ∈ Γ). Proving that formula (12) is satisfied by I is similar. Either there is no IST for x: so by the definition of IST, there exist some supports targeting x; moreover, the only reason explaining the non-existence of an IST for x is the fact that, when we build the IST, an element that should be added to the IST part of the IST is x and, this addition being impossible following the definition of IST , the building of the IST fails; moreover, it is trivial to see that this problem occurs only when we consider the branches of the tree originated in the supports targeting x and belonging to the same DCS that x; thus it is not possible to support x with U if at least one of these supports is present; so no support targeting x and belonging to the same DCS can belong to U and so I does not satisfy these supports. Or there are some IST for x: so two subcases are possible:

either there is no support targeting x in U , so I cannot satisfy any support for x and the condition is trivially satisfied; or there are some supports β targeting x in U : by definition of IST, β ∈ IST; moreover since β ∈ U , then at least one element x i of its source is also in U ; so consider the IST containing at the same time β and x i ; since they are in U and U is self-supporting and following the definition of I, we have I(sV al(β)) = true and I(sAcc(x i )) = true; so Condition 1 is satisfied. So, in both cases, I is a support-founded model.

⇐ Let I be a support-founded model of Σ d (RAFN). We have to prove that the structure U = (S I , Γ I , ∆ I ) is admissible.

Let prove that U is conflict-free w.r.t. RAFN. If it is not the case, there exist x ∈ S I ∪ Γ I ∪ ∆ I and y ∈ Γ I , with s y ⊆ S I and T (y) = x. By definition, it holds that I(∀z ∈ Arg(S(z, y) → sAcc(z))) = true and I(sV al(y)) = true. Moreover, in the case when x ∈ S I , it holds that I(sAcc(x)) = true and so I(Acc(x)) = true (as I satisfies formula (2bis)). Then it holds that I(N Acc(x)) = false (as I satisfies formula (3)). As a consequence, formula (2) is falsified. In the case when x ∈ Γ I ∪ ∆ I , it holds that I(sV al(x)) = true and so I(V al(x)) = true (as I satisfies formula (3bis)). As a consequence, formula (1) is falsified. In both cases, there is a contradiction with I being a model of Σ(RAFN).

Let us prove that U is self-supporting. Assume that x ∈ S I (resp. x ∈ Γ I ∪ ∆ I ). By definition, it holds that I(sAcc(x)) = true (resp. I(sV al(x)) = true). As I satisfies formula (2bis), I(Supp(x)) = true. As I satisfies formula [START_REF] Cohen | On the acceptability semantics of argumentation frameworks with recursive attack and support[END_REF], two cases must be considered: either there does not exist a support targeting x: so x is trivially supported and belongs to Sup(U ); or there exist some supports y targeting x: if none of the y belong to U then x is trivially supported and belongs to Sup(U ); consider now a support y that belongs to U ; since formula (17) is satisfied, there exists an element z in the source of y that is also in U ; so it holds that I(sAcc(z)) = true and I(sV al(y)) = true, and formula (17) can still be used, thus enabling to build a tree of supports. As U is finite and I is support founded, this process will end and an IST can be exhibited for x showing that x is supported without itself and so belongs to Sup(U ). Hence U is self-supporting.

It remains to prove that, given x an element of the structure, if x is the target of an attack α, then α is unactivable w.r.t. U . Assume that x ∈ S I is the target of an attack α. By definition, it holds that I(sAcc(x)) = true. It follows that I(Acc(x)) = true. As I satisfies formula [START_REF] Cayrol | Valid attacks in argumentation frameworks with recursive attacks[END_REF], it follows that either there exists an attack β targeting α (or an element of s α ) with β ∈ ∆ I and s β ⊆ S I , or I satisfies U nSupp(α) (or I satisfies ∃z ∈ Arg(S(z, α) ∧ U nSupp(z)), i.e. at least for one element x i of s α we have I(U nSupp(x i )) = true).

In the first case, it holds that α (resp. an element of s α ) belongs to Def (U ).

In the second case, we prove that α (resp. an element of s α ) belongs to U nSupp(U ). For that purpose, we must prove the following intermediary result: Property: For any element u, if I satisfies U nSupp(u), then u ∈ U nSupp(U ).

Proof: The proof is done taking the contrapositive: if u ∈ Sup(U ) ∪ Sup(U ), with U = (Def A (U ), R, Def N (U )), then I does not satisfy U nSupp(u). Let us consider u ∈ Sup(U ). Several cases must be taken into account:

no support targets u: so following formula (18), we trivially obtain that I(U nSupp(u)) is false;

a support y targets u but it is defeated by U : so following formula (18), we trivially obtain that I(U nSupp(u)) is false;

the supports targeting u are not defeated by U : so they belong to U ; let y be one of these supports, two subcases appear here:

either there is at least one element of the source of y that is not defeated, so that belongs to U ; then following formula (18), we trivially obtain that I(U nSupp(u)) is false;

or any element in the source of y is defeated; this implies that u ∈ Sup(U ), so u ∈ Sup(U ); considering that for any y that supports u, its source cannot belong to U (since U is conflict-free, see a previous item in this proof), then we can conclude that y cannot belong to U otherwise u ∈ Sup(U ); then, following formula (17), we can deduce that I(Supp(u)) is true and so, following formula [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF], we obtain that I(U nSupp(u)) is false. So, in every case, α is unactivable w.r.t. U . The same reasoning can be done for x ∈ Γ I ∪ ∆ I using formula [START_REF] Cayrol | Gradual valuation for bipolar argumentation frameworks[END_REF]. Hence, we can prove that U is admissible.

(complete semantics)

⇒ Assume that the structure U = (S, Γ, ∆) is complete. Let us build an interpretation I of Σ d (RAFN) ∪ Σ r (RAFN):

We keep the same interpretation as the one used in Item 1 of the current proof except for Acc, V al. For all x ∈ A, I(Acc(x)) = true iff x ∈ S or (x / ∈ S and x ∈ Defended (U )). For all x ∈ R (resp. ∈ N), I(V al(x)) = true if and only x ∈ Γ (resp. ∆) or (x / ∈ Γ (resp. ∆) and x ∈ Defended (U )). We have to prove that S I = S, Γ I = Γ and ∆ I = ∆, and that I is a support-founded model of Σ d (RAFN) ∪ Σ r (RAFN).

Example 2

 2 An attack (a, b) ∈ R is represented by two nodes a, b (in a circle) and a simple edge from a to b: a b

Example 7

 7 Consider the following REBAF:

Example 5 (

 5 cont'd): In this example, considering the non prima-facie elements, there are an IST for d ({γ, e}) and another for a ({β 1 , d, γ, e}), but nothing for c, nor b. Indeed, c needs the support of b and b needs the support of c, so its own support that is forbidden by Def. 5. Example 6 (cont'd): Considering a, there is one IST = {α 1 , a 0 }. Considering d, there is one IST = {α 2 , d 0 }. Considering e, there are two IST, {α 3 , e 0 } and {α 4 , e 0 }. Considering x, there is one IST, {β 1 , a, b, α 1 , a 0 }. Considering y, there are two IST, {β 2 , c, d, e, α 2 , d 0 , α 3 , e 0 } and {β 2 , c, d, e, α 2 , d 0 , α 4 , e 0 }. Considering z, there are three IST: {γ 1 , x, β 1 , a, b, α 1 , a 0 } (root: γ 1 , leaves: a 0 and b),{γ 2 , y, β 2 , c, d, e, α 2 , d 0 , α 3 , e 0 } (root: γ 2 , leaves: c, d 0 and e 0 ), {γ 2 , y, β 2 , c, d, e, α 2 , d 0 , α 4 , e 0 } (root: γ 2 , leaves: c, d 0 and e 0 ). The other elements of the REBAF have no IST.

12

 12

(

Example 1 (

 1 cont'd): Σ ss (REBAF) is obtained from Σ(REBAF) by adding formulae among which:Supp(b) → (sAcc(a) ∧ sV al(α)) ¬U nSupp(a) ¬U nSupp(c) ¬U nSupp(α) ¬U nSupp(β) U nsupp(b) ↔   (sV al(β) ∧ sAcc(c)) ∨ U nSupp(a) ∨ U nSupp(α)   Then Σ d (REBAF) is obtained from Σ ss (REBAF) by adding formulae among which: V al(α) → (U nSupp(β) ∨ U nSupp(c)) Σ r (REBAF) is obtained from Σ ss (REBAF) by adding the formulae: Acc(a) Acc(b) Acc(c) V al(β) (U nSupp(c) ∨ U nSupp(β)) → V al(α) Σ s (REBAF) is obtained from Σ ss (REBAF)by adding the formulae: Acc(a) Acc(b) Acc(c) V al(β) ¬V al(α) → sV al(β) ∧ sAcc(c) ¬Supp(b) → U nSupp(b) and also ¬Supp(x) → U nSupp(x) for x ∈ {a, c, α, β} 3.4 Characterizing Semantics of a REBAF [23] proposed characterizations of the REBAF structures under different semantics in terms of models of the bases Σ(REBAF), Σ d (REBAF), Σ r (REBAF), Σ s (REBAF). The common idea is that a structure gathers the acceptable elements w.r.t. it. Let REBAF = A,R,E,s,t,P . Given I an interpretation of Σ(REBAF), we define: S I = {x ∈ A|I(sAcc(x)) = true} Γ I = {x ∈ R|I(sV al(x)) = true} ∆ I = {x ∈ E|I(sV al(x)) = true} Moreover, let I be a model of Σ(REBAF):

  true, otherwise I(sV al(x i )) = true; 2. for each element x of REBAF, I(U nSupp(x)) = true iff x ∈ U nSupp(U I ) with U I = (S I , Γ I , ∆ I ).

1 .

 1 U is admissible iff there exists a support-founded model I of Σ d (REBAF) (in the sense of Def. 15) with S I = S, Γ I = Γ and ∆ I = ∆. 2. U is complete iff there exists a support-founded model I of (Σ d (REBAF) ∪ Σ r (REBAF)) (in the sense of Def. 15) with S I = S, Γ I = Γ and ∆ I = ∆. 3. U is a preferred structure iff there exists a ⊆-maximal support-founded model I of Σ d (REBAF) (in the sense of Def. 15) with S I = S, Γ I = Γ and ∆ I = ∆. 4. U is the grounded structure iff S = S I , Γ I = Γ and ∆ I = ∆ where I is a ⊆-minimal support-founded model of (Σ d (REBAF) ∪ Σ r (REBAF)) (in the sense of Def. 15). 5. U is stable iff there exists a support-founded model I of Σ s (REBAF) (in the sense of Def. 15) with S I = S, Γ I = Γ and ∆ I = ∆. Let us illustrate the above results on the previous examples: Example 3 (cont'd): The ⊆-maximal support-founded models I of Σ d (REBAF) (in the sense of Def. 15) correspond to the preferred structure ({b, d}, {β, π}, { }).Example 4 (cont'd):The ⊆-maximal support-founded models I of Σ d (REBAF) (in the sense of Def. 15) correspond to the preferred structure ({a, b, c}, ∅, {α, γ}). The models that satisfy sAcc(d) (resp. sAcc(e), sV al(β)) are not kept since they are not support-founded (no IST for these arguments or this interaction that could be satisfied). Example 5 (cont'd): The ⊆-maximal support-founded models I of Σ d (REBAF) (in the sense of Def. 15) correspond to the preferred structure ({e, d, a}, ∅, {α 1 , α 2 , β 1 , β 2 , γ}). Example 6 (cont'd): The ⊆-maximal support-founded models I of Σ d (REBAF) (in the sense of Def. 15) correspond to the preferred structure (A, R, E).

Example 11

 11 In this example, we have two arguments a and b with a necessary support α from a to b. a α b

  Indeed consider the following example. Example 12 In this example, we have three arguments a, b and c with a necessary support α from a to b and an attack β from c to a. Then consider the admissible structure U = ({b, c}, {β}, ∅): in this case, Sup(U ) = {a, b, c, α, β} and Def (U ) = {a}, so U = (Def A (U ), R, Def N (U )) = ({b, c}, {β}, {α}) and U nSupp(U ) = {b}; then U nAcc(U ) = {a, b} and U nAct(U ) = ∅;

  Example 12 (cont'd): Consider now the admissible structure U = ({b}, ∅, ∅): in this case, Sup(U ) = {a, b, c, α, β} and Def (U ) = ∅, so U = (Def A (U ), R, Def N (U )) = ({a, b, c}, {β}, {α}) and U nSupp(U ) = ∅; then U nAcc(U ) = ∅ and U nAct(U ) = ∅;

Example 13

 13 In this example, we have four arguments a, b, c and d with a necessary support α from a to b and two attacks, β from c to a and γ from b to d. Then consider the admissible structure U = ({b, c}, {β, γ}, ∅): in this case, Sup(U ) = {a, b, c, d, α, β, γ} and Def (U ) = {a, d}, so U = (Def A (U ), R, Def N (U )) = ({b, c}, {β, γ}, {α}) and U nSupp(U ) = {b}; then U nAcc(U ) = {a, b, d} and U nAct(U ) = {γ};

α x a β b α x Example 9 (

 9 Example 7 (cont'd): In this case, only one tree must be considered with the repetition of argument a: Example 8 (cont'd): In this case, two distinct trees must be considered without any repetition: a cont'd): In this case, two distinct trees must be considered:

α

  In this case, each element has an IST: for d: {d, α, b} and for a: {a, β, d, α, b}; for b: {b}, for β: {β} and for α: {α}.

1 .

 1 s,t and let use RAFN-v2 definitions. Let U = (S, Γ, ∆) be a structure on RAFN. U is admissible iff there exists a support-founded model I of Σ d (RAFN) (in the sense of Def. 19) with S I = S, Γ I = Γ and ∆ I = ∆. 2. U is complete iff there exists a support-founded model I of Σ d (RAFN) ∪ Σ r (RAFN) (in the sense of Def. 19) with S I = S, Γ I = Γ and ∆ I = ∆. 3. U is a preferred structure iff there exists a ⊆-maximal support-founded model I of Σ d (RAFN) ∪ Σ r (RAFN) (in the sense of Def. 19) with S I = S, Γ I = Γ and ∆ I = ∆. 4. U is the grounded structure iff S = S I , Γ I = Γ and ∆ I = ∆ where I is a ⊆-minimal support-founded model of Σ d (RAFN) ∪ Σ r (RAFN) (in the sense of Def. 19). 5. U is stable iff there exists a support-founded model I of Σ s (RAFN) (in the sense of Def. 19) with S I = S, Γ I = Γ and ∆ I = ∆. Using Prop. 3, consider the previous examples and the preferred semantics: Example 3 (cont'd): The ⊆-maximal support-founded models I of Σ d (RAFN) ∪ Σ r (RAFN) (in the sense of Def. 19) correspond to the preferred structure ({b, c, e, f }, {β, π}, { }). Example 4 (cont'd): The ⊆-maximal support-founded models I of Σ d (RAFN) ∪ Σ r (RAFN) (in the sense of Def. 19) correspond to the preferred structure (A, R, N). Even if a support cycle exists, all models are kept since they are compatible with Def. 13. Example 5 (cont'd): The ⊆-maximal support-founded models I of Σ d (RAFN) ∪ Σ r (RAFN) (in the sense of Def. 19) correspond to the preferred structure ({e}, ∅, {α 1 , α 2 , β 1 , β 2 , γ}). Example 6 (cont'd): The ⊆-maximal support-founded models I of Σ d (RAFN) ∪ Σ r (RAFN) (in the sense of Def. 19) correspond to the preferred structure (A, R, N).

2 .

 2 for each element x of REBAF,I(U nSupp(x)) = true iff x ∈ U nSupp(U I ) with U I = (S I , Γ I , ∆ I ).

2 .

 2 for each element x of RAFN = A,R,N,s,t , I(U nSupp(x)) = true iff x ∈ U nSupp(U I ) with U I = (S I , Γ I , ∆ I ).

z⇒

  Let complete these chains by adding z and y that support x: So it is obvious to see that, in each case and for any couple (z, y) with z ∈ s(y) ∩ S ∩ Sup(U ), z ∈ Sup(U \ {z}).So by definition of theSup set, z ∈ Sup(U ). Contradiction with the assumption saying that s(y) ∩ S ∩ Sup(U ) = ∅ So x ∈ Sup(U ) B.3 Proofs of Section 5.4 Proof of Proposition 3. 20 Let RAFN = A, R, N, s, t . 1. (admissibility) Assume that the structure U = (S, Γ, ∆) is admissible. Let us define an interpretation I of Σ d (RAFN).

Finally, we have

  to prove that I is support-founded. Condition 2 of Definition 19 is trivially satisfied. Consider now Condition 1. Let x an element such that there exists a DCS C containing x. Assume that I(sAcc(x)) (or I(sV al(x))) = true. So x ∈ U and, since U is admissible (so self-supporting), two cases are possible:

  {d}), β 1 , (a, {a, b}), α 1 , (d, {d})) ((c, {c}), β 2 , (b, {a, b}), α 2 , (c, {c})) ((d, {d}), β 1 , (a, {a, b}), α 2 , (c, {c}), β 2 , (b, {a, b}), α 1 , (d, {d}))

  Let IST P = (IST ∩ P ∩ A). IST P = ∅;!∃x i ∈ IST s.t. x i ∈ E and t(x i ) = x; x i is called the root of the tree; ∀x i ∈ IST ∩ A, either ∃x j ∈ IST ∩ E s.t. x i = t(x j ), or x i ∈ IST P (in this case x i is called a leaf of the tree);

	t.
	REBAF case	RAFN case
	IST = {x 0 , . . . , x n } with n > 0 s.t.
	∀x i , i ∈ [0 . . . n], x i ∈ (A ∪ E) \ {x} and is called
	a node of the tree;

  . t(y) = x; otherwise IST = {x 0 , . . . , x n } with n > 0 and ∀x i , i ∈ [0 . . . n], x i ∈ (A ∪ N) \ {x} and is called a node of the tree;

∀y ∈ N, if x = t(y) then y ∈ IST ;

  1. for each argument (resp. support) x, belonging to a maximal DCS and s.t. I(sAcc(x)) = true (resp. I(sV al(x)) = true), two cases must be considered: if there does not exist an impacting support tree IST for x then, ∀β ∈ N belonging to the same DCS that x and s.t. t(β) = x, I does not satisfy β (so I(sV al(β)) = false); otherwise, among the existing impacting support trees for x, there exists at least one IST s.t., considering any support β ∈ IST s.t. t(β) = x, if I satisfies β (so I(sV al(β)) = true) then I must also satisfy at least an element of the source of β that belongs to IST (so ∃x i ∈ s(β) ∩ IST s.t. I(sAcc(x i )) = true).

Where "iff" (resp. "w.r.t.") stands for "if and only if" (resp. "with respect to").

It can be proved that the minimal fixed point of F is conflict-free.

By abuse of notation, we write U \T instead of (S\T, Γ\T, ∆\T ) with T ⊆ (A ∪ R ∪ E).

In fact, strictly speaking, this chain is in reality a "tree". That is due to several reasons. The first one is that each support can be in turn supported. And the second reason is the fact that interactions are collective; so the source of a support can be a set of arguments and in this case all elements in the source are needed for supporting the target.

The definition for the grounded extension is not given in[START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF] but can be easily proposed following the definition used in the AF case.

Note that this is also equivalent to U is self-supporting, conflict-free and S ∪ Γ ∪ ∆ ⊆ U nAcc(U ).

By abuse of language, the set of the elements composing C will be also denoted by C and C will be used with set operators as ∩ ou ∪ and will be comparable with other sets.

!∃x i ∈ IST means "there exists only one x i ∈ IST.

Binary necessary support was initially introduced in[START_REF] Nouioua | Argumentation frameworks with necessities[END_REF], then discussed in[START_REF] Cayrol | Towards a new framework for recursive interactions in abstract bipolar argumentation[END_REF][START_REF] Cohen | An approach to abstract argumentation with recursive attack and support[END_REF][START_REF] Cohen | On the acceptability semantics of argumentation frameworks with recursive attack and support[END_REF] in a more general context (particularly with higher-order interactions in the so-called ASAF).

Indeed, in[START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF], it has been proven that there is no Fundamental Lemma for RAFN since the function Sup is not monotonic. Due to this point, preferred and stable extensions are assumed to be complete sets.

We recall that P ⊆ A ∪ R ∪ E.

Let us recall that a stable structure U = (S, Γ, ∆) satisfies: S ∪ Γ ∪ ∆ ⊆ U nAcc(U ).

First part of Lemma A.1 in[START_REF] Cayrol | Argumentation Frameworks with Recursive Attacks and Evidence-Based Supports[END_REF], long version of[START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF]

Indeed, considering any structure, each element that is not a target of a support belonging to the structure is always supported by this structure; and an element that is the target of a support belonging to the structure is supported only if the source of the support is also in the structure.

So the second part of Lemma A.1 in[START_REF] Cayrol | Argumentation Frameworks with Recursive Attacks and Evidence-Based Supports[END_REF], long version of[START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF] cannot be used in the case of RAFN. And it is the same for Lemma A.3 in[START_REF] Cayrol | Argumentation Frameworks with Recursive Attacks and Evidence-Based Supports[END_REF].

So Lemma A.7 in[START_REF] Cayrol | Argumentation Frameworks with Recursive Attacks and Evidence-Based Supports[END_REF], long version of[START_REF] Cayrol | Argumentation frameworks with recursive attacks and evidence-based support[END_REF] cannot be applied for RAFN.

Note that other trees are possible. For instance, the tree corresponding to the aggregation of the first and the second trees is also a possibility (in this case, for β 1 , the two elements of the source are kept).

Note that, if x is self-supported then this condition will be false and the IST set cannot be built; and so there is not an IST for x.

This proof is inspired by the proof of the corresponding propositions in[START_REF] Nicholas | Handling support cycles in the logical encoding of argumentation frameworks with higher-order attacks and evidential supports[END_REF][START_REF]Logical encoding of argumentation frameworks with higher-order attacks and evidential supports: Taking into account the collective interactions[END_REF].

By definition, formulae (4) to[START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF] are satisfied by I.

So Sup(U ) ∩ U nSupp(U ) = ∅ but also Acc(U ) ∩ U nAcc(U ) = ∅ and Acc(U ) ∩ Def (U ) = ∅.

So the only difference with the framework proposed in [START_REF] Cayrol | Structure-based Semantics of Argumentation Frameworks with Higher-order Attacks and Supports[END_REF] is the fact that an element cannot be in the same time supported and unsupportable or acceptable and unacceptable.

Knowing that all other definitions remain unchanged, it would be interesting to verify if the results given by the semantics remain also unchanged. A first answer can be found through the following example: Example 13 (cont'd): Consider now another structure: U = ({b, c, d}, {β}, ∅), we have the following results: So considering U , we can conclude that U is admissible if Def 16 is used, but it is not admissible if Def 17 is used.

Nevertheless, if we consider the complete semantics, we can see that the Acc set obtained with Def 16 being not conflict-free, it cannot be a complete structure, whereas that obtained with Def 17 will be a complete structure.

And indeed the following proposition holds:

Proposition 2 Let RAFN = A, R, N, s, t . Let U be a structure of RAFN. Let σ be one semantics among the following ones: conflict-free, self-supporting, complete, preferred, grounded and stable. U is a σ-structure obtained using Definition 16 for the UnSupp(U ) set iff U is a σ-structure obtained using Definition 17 for the UnSupp(U ) set.

The new version of the RAFN framework will be called RAFN-v2.

Logical encoding for RAFN-v2

Considering the logical translation of a REBAF, and the fact that the similarities between the definitions of semantics for REBAF and for RAFN, we propose to adapt the previous encoding in order to take into account higher-order bipolar argumentation frameworks using the necessary meaning for the supports.

Vocabulary

The first adaptation concerns the vocabulary. It is almost unchanged, except that the predicate ESupport is obviously replaced by the predicate N Support and the predicate P rimaF acie is removed since it becomes useless. So we have:

Predicate symbol

Arg(x), Attack(x), Acc(x), N Acc(x), V al(α), Supp(x), U nSupp(x), sAcc(x), sV al(α), S(a, α): unchanged (see in Section 3) ESupport(x), P rimaF acie(x): removed N Support(x) means that "x is a necessary support" Function symbol T (α): unchanged (see in Section 3)

B Proofs

B.1 Proofs of Section 4.2

Proof of Proposition 2

Recall that 2 definitions for the U nSupp set exist for a given structure U :

1. either Def. 16:

2. or Def. 17:

In order to simplify the reading of this proof, we add an indice to a given semantics in order to identify which definition is used. So, a σ 1 structure will correspond to the definition of the σ semantics using Def. 16, whereas a σ 2 structure will correspond to the definition of the σ semantics using Def. 17.

Using this notation, the proof of Prop. 2 corresponds to: for each semantics σ, we must prove that U is a σ 1 structure iff U is a σ 2 structure, σ taken in {conflict-free, self-supporting, admissible, complete, preferred, grounded, stable}.

First of all, we can give some trivial results for any structure U :

Consider now the different semantics:

σ is complete: U is complete iff it is conflict-free and U = Acc(U ). The conflict-freeness being conserved between the two RAFN versions, it remains to prove that

Consider now an element x ∈ U = Acc 1 (U ) and show that x ∈ Acc 2 (U ). Assume that there exists an element

corresponds to the existence of an attack α st t(α) = x and α ∈ U nAct 2 (U ); let denote α or its source by y, we have so

The second case leads to the fact that

Let study the different constraints related to these conditions:

y ∈ Sup 1 (U ) corresponds to the following cases:

Proof of Lemma 1 Consider an element x ∈ Acc(U ) and assume that x ∈ Def (U ). Since x ∈ Def (U ) then there exists an attack α ∈ U st t(α) = x and s(α) ∈ U . But x ∈ Acc(U ) then α must be unactivable, so either α or s(α) belong to U nAcc(U ); since U nAcc(U ) = Def (U ) ∪ U nSupp(U ), then α (or s(α)) belongs to Def (U ) or to U nSupp(U ); the first case leads to a contradiction since U is conflict-free; the second case leads also to a contradiction since α and s(α) belong to Sup(U ) (U being self-supporting) and, following Def. 17, they cannot belong to U nSupp(U )).

So Acc(U ) ∩ Def (U ) = ∅.

Lemma 2 Let RAFN = A, R, N, s, t and let use RAFN-v2 definitions. Any conflict-free and self-supporting structure U satisfies:

Proof of Lemma 2

Proof for U nAcc(U ) ⊆ Def (U ):

Proof for Acc(U ) ⊆ U nAcc(U ): Consider an element x ∈ Acc(U ) and assume that x ∈ U nAcc(U ); so x ∈ U nAcc(U ); by definition U nAcc(U ) = Def (U ) ∪ U nSupp(U ), so:

either x ∈ Def (U ): using Lemma 1, this is in contradiction with x ∈ Acc(U );

or x ∈ U nSupp(U ): since, by definition of Acc(U ), each element in Acc(U ) is supported then x ∈ Sup(U ); so following Definition 17, we obtain a contradiction.

So each case leading to a contradiction, we can conclude that Acc(U ) ⊆ U nAcc(U ).

Lemma 3 Let RAFN = A, R, N, s, t and let use RAFN-v2 definitions. Any stable structure U satisfies: Sup(U ) = U nSupp(U ).

Proof of Lemma 3

Assume that U is a stable structure. Following Def. 17, we already know that U nSupp(U ) ⊆ Sup(U ). It remains to prove the reverse inclusion. Let us recall that U nSupp(U ) = Sup(U ) \ Sup(U ) where U = (Def A (U ), R, Def N (U )). So we have to prove that Sup(U ) ∪ Sup(U ) ⊆ Sup(U ), so that Sup(U ) ⊆ Sup(U ). Let x ∈ Sup(U ). So for any support α ∈ Def (U ) targeting x if α ∈ Sup(U \ {x}) then s α ∩ Def (U ) ∩ Sup(U \ {x}) = ∅. Assume that x ∈ Sup(U ) and consider the following cases:

Either there is no support α targeting x: so x ∈ Sup(U ) and contradiction with the assumption.

Or there are some supports α targeting x but they are all defeated by U : since U is stable, U is conflict-free and so α ∈ U ; thus x ∈ Sup(U ) and contradiction with the assumption.

Or there exists at least one support α targeting x that is not defeated by U : so α ∈ U and since x ∈ Sup(U ) there also exist in U some elements y of s(α); α and the corresponding y belong to Sup(U \ {x}); so neither α, nor y need x to be supported; this implies that they also belong to Sup(U ); so they do not belong to U nsupp(U ); since α (resp. y) / ∈ Def (U ) and / ∈ U nsupp(U ) then, following the definition of the U nAcc set, they belong to U nAcc(U ); since U is stable, we have α (resp. y) ∈ U ; so they are in Sup(U ); so x ∈ Sup(U ) and contradiction with the assumption.

Hence we have proved that x ∈ Sup(U ) and so that Sup(U ) = U nSupp(U ) Note that if U is complete, for all x ∈ A∪R∪N, if x / ∈ S and x ∈ Defended (U ) then x / ∈ Sup(U ). So the above constraint expressed for the definition of I(Acc) (resp. I(V al)), x / ∈ S and x ∈ Defended (U ), is stronger than the one used for defining a model of an admissible structure (x / ∈ S, x / ∈ Sup(U ) and x ∈ Defended (U )). Due to the above remark and the proof of Item 1 of this proof, it holds that I satisfies S I = S, Γ I = Γ, ∆ I = ∆, and that I is a model of Σ d (RAFN). Now let prove that I satisfies formulae (13) and [START_REF] Cayrol | Logical encoding of argumentation frameworks with higher-order attacks and evidential supports[END_REF]. Let us consider formula [START_REF] Cayrol | Bipolarity in argumentation graphs: towards a better understanding[END_REF]. Let x ∈ A such that for each attack α targeting x, either I(U nSupp(α)) = true, or I(∃z ∈ Arg(S(z, α) ∧ U nSupp(z))) = true, or α (or an element of s α ) is attacked by β with β ∈ Γ I and s β ⊆ S I . Due to the definition of I(U nSupp), for each attack α targeting x, either α ∈ U nSupp(U ), or an element of s α ∈ U nSupp(U ), or α (or an element of s α ) belongs to Def (U ). In other words, for each attack α targeting x, α ∈ U nAct(U ), so x ∈ Defended (U ). Now, by definition of I(Acc), it holds that I(Acc(x)) = true. We have proved that I satisfies formula [START_REF] Cayrol | Bipolarity in argumentation graphs: towards a better understanding[END_REF]. Proving that I satisfies formula (14

It remains to prove that I is support-founded. For that purpose, the proof written in Item 1 of the current proof can be used as U is self-supporting.

⇐ Let I be a support-founded model of Σ d (RAFN) ∪ Σ r (RAFN). We have to prove that the structure U = (S I , Γ I , ∆ I ) is complete. For that purpose, it is enough to prove that Acc(U ) is included in S I ∪Γ I ∪∆ I . Consider x ∈ A ∩ Acc(U ). So x ∈ Sup(U ) and x ∈ Defended (U ). The first condition implies that I(Supp(x)) = true, as I satisfies formula (1bis) and following the definition of Sup(U ). The second condition means that for each attack α targeting x, either α ∈ U nSupp(U ), or an element of s α ∈ U nSupp(U ), or α (or an element of s α ) belongs to Def (U ) (i.e. α -or an element of s α -is attacked by β ∈ U with s β ⊆ U ). So, since I is a support-founded models (so Condition 2 of the definition of a support-founded model holds) and the fact that if an element β belongs to (resp. s β is included in) the structure then I(sV al(β)) (resp. I(∀z ∈ Arg(S(z, β) → sAcc(z)))) is also true, the premisse of formula ( 13) is true, and as I satisfies formula [START_REF] Cayrol | Bipolarity in argumentation graphs: towards a better understanding[END_REF], it follows that I(Acc(x)) = true. As I satisfies formula (2bis) it holds that I(sAcc(x)) = true, so x ∈ S I . Similarly, it can be proved that for all x ∈ R ∩ Acc(U ) (resp. x ∈ N ∩ Acc(U )), x ∈ Γ I (resp. x ∈ ∆ I ). We have proved that U is a complete structure.

3. (preferred semantics) Let I be an interpretation of a set of formulae Σ x . Let U I denote the structure (S I , Γ I , ∆ I ).

It is easy to see that I is a ⊆-maximal support-founded model of Σ x iff the structure U I is ⊆-maximal among all the structures of the form U J = (S J , Γ J , ∆ J ), where J denotes a support-founded model of Σ x . Then taking Σ x = Σ d (RAFN) ∪ Σ r (RAFN), it follows that the preferred structures correspond to the structures U I where I is a ⊆-maximal support-founded model of Σ d (RAFN) ∪ Σ r (RAFN).

4. (grounded semantics) Let I be an interpretation of a set of formulae Σ x . Let U I denote the structure (S I , Γ I , ∆ I ).

It is easy to see that I is a ⊆-minimal support-founded model of Σ x iff the structure U I is ⊆-minimal among all the structures of the form U J = (S J , Γ J , ∆ J ), where J denotes a support-founded model of Σ x . Taking

, it follows that the grounded structure correspond to the structure U I where I is a ⊆-minimal support-founded model of Σ d (RAFN) ∪ Σ r (RAFN).

(stable semantics)

⇒ Assume that the structure U = (S, Γ, ∆) is stable. Let us define an interpretation I of Σ s (RAFN) as follows:

Once again, we keep the same interpretation as the one used in Item 1 of the current proof except for Acc, V al. For all x ∈ A, I(Acc(x)) = true iff x ∈ S or x / ∈ Def (U ).

For all x ∈ R (resp. ∈ N), I(V al(x)) = true iff x ∈ Γ (resp. ∆) or x / ∈ Def (U ). We have to prove that S I = S, Γ I = Γ and ∆ I = ∆, and that I is a support-founded model of Σ s (RAFN). And, for proving that I is a support-founded model of Σ s (RAFN) it is sufficient to prove that I satisfies formulae (1), ( 2), ( 3), (1bis), (2bis), (3bis) and ( 17), ( 18), ( 15), ( 16), [START_REF] Minh | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] and that I is support-founded. Let x ∈ S I . By definition, I(Acc(x)) = true and I(Supp(x)) = true. By definition of I(Acc) and I(Supp), it follows that x ∈ Sup(U ) and (x ∈ S or x / ∈ Def (U )). Following Lemma 3, x / ∈ U nSupp(U ) and (x ∈ S or x / ∈ Def (U )). If x / ∈ S, as U is stable, it follows that x ∈ Def (U ) or x ∈ U nSupp(U ). We obtain a contradiction, hence x ∈ S. Conversely, given x ∈ S, it holds that I(Acc(x)) = true. As U is stable, U is self-supporting, so x ∈ Sup(U ), then it holds that I(Supp(x)) = true. As a consequence, I(sAcc(x)) = true and x ∈ S I . Proving that Γ I = Γ and ∆ I = ∆ is similar.

Obviously I satisfies formulae (3), (2bis), (3bis).

Let us first consider formula [START_REF] Baroni | AFRA: Argumentation framework with recursive attacks[END_REF]. Let y ∈ R and x ∈ A with x = T (y), I(sV al(y) = true and I(∀z ∈ Arg(S(z, y) → sAcc(z)) = true. Then s y ⊆ S and y ∈ Γ, and it holds that x ∈ Def (U ). As U is stable, U is conflict-free, so x cannot belong to S. Hence we have x / ∈ S and x ∈ Def (U ), or equivalently I(Acc(x)) = false, by definition of I(Acc) and then I(N Acc(x)) = true, by definition of I(N Acc). We have proved that I satisfies formula [START_REF] Baroni | AFRA: Argumentation framework with recursive attacks[END_REF]. Proving that formula (1) is satisfied by I is similar.

Proving that I satisfies formulae (1bis), ( 17), ( 18) can be done with exactly the same reasoning as the one used in Item 1 of the current proof.

Let us now consider formula [START_REF] Cohen | A survey of different approaches to support in argumentation systems[END_REF]. Let x ∈ A such that I(Acc(x)) = false. By definition of I(Acc), it holds that x / ∈ S and x ∈ Def (U ). So, there is y ∈ Γ with x = T (y) and s y ⊆ S. Hence, there is y ∈ Γ I with x = T (y) and s y ⊆ S I , or equivalently, there is y ∈ R with x = T (y) and I(sV al(y)) = true and I(∀z ∈ Arg(S(z, y) → sAcc(z))) = true. We have proved that I satisfies formula [START_REF] Cohen | A survey of different approaches to support in argumentation systems[END_REF]. Proving that formula (16) is satisfied by I is similar.

Lastly, we consider formula [START_REF] Minh | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. Let x ∈ A ∪ R ∪ N such that I(Supp(x)) = false. By definition of I(Supp), x / ∈ Sup(u). Due to Lemma 3, it follows that x ∈ U nSupp(U ), hence I(U nSupp(x)) = true, by definition of I(U nSupp). We have proved that I satisfies formula [START_REF] Minh | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. So I is a model of Σ s (RAFN).

It remains to prove that I is support-founded. For that purpose, the proof written in Item 1 of the current proof can be used as U is self-supporting.

⇐ Let I be a support-founded model of Σ s (RAFN). We have to prove that the structure U = (S I , Γ I , ∆ I ) is stable. Σ s (RAFN) contains Σ(RAFN) and formulae (17), [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. So, with exactly the same reasoning as the one used in Item 1 for the admissible case, it can be proved that U is conflict-free and self-supporting. It remains to prove that U = Acc(U ) = U nAcc(U ). First, consider x ∈ A such that x ∈ U . So x / ∈ S I and by definition of S I , I(sAcc(x)) = false. As I satisfies formula (2bis), it follows that I(Acc(x)) = false or I(Supp(x)) = false. In the case when I(Acc(x)) = false, as I satisfies formula (15), it follows that x ∈ Def (U ). If I(Acc(x)) = true, it holds that I(Supp(x)) = false. As I satisfies formula [START_REF] Minh | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF], it follows that I(U nSupp(x)) = true, so x ∈ U nSupp(U ) (following Condition 2 of Definition 19 since I is support-founded). In both cases, we have that x ∈ U nAcc(U ). The same proof can be done for x ∈ R ∩ N. So U nAcc(U ) ⊆ U . Moreover following Lemma 2, we have Acc(U ) ⊆ U nAcc(U ) ⊆ U .

Second, let prove that U ⊆ Acc(U ). Consider x ∈ A such that x ∈ U . So x ∈ S I and by definition of S I , I(sAcc(x)) = true. As I satisfies formula (2bis), it follows that I(Acc(x)) = true and I(Supp(x)) = true. Since I(Acc(x)) = true, then using the contrapositive of formula (3), we obtain that I(N Acc(x)) = false; then following the contrapositive of formula (2), we must have that, for any attack y targeting x, I(sV al(y) ∧ sAcc(s y )) = false (here we simplify the original formula since in a RAFN the source of an attack is a singleton); at this step, four cases are possible: either I(V al(y)) = false, or I(Supp(y)) = false, or I(Acc(s y )) = false, or I(Supp(s y )) = false; consider for instance the first case: since I(V al(y)) = false then using formula [START_REF] Cohen | An approach to abstract argumentation with recursive attack and support[END_REF], we can conclude that y ∈ Def (U ), so y ∈ U nAcc(U ) and thus y ∈ U nAct(U ); this reasoning can be applied for the three other cases, using either formula (15) (for the third case), or formula [START_REF] Minh | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] (for the two other cases) and leads to the same conclusion: y ∈ U nAct(U ); so in each case, x ∈ Acc(U ) (recalled that, U being self-supporting, x ∈ Sup(U )). The same proof can be done for x ∈ R ∩ N. And so U ⊆ Acc(U ). In conclusion, U = Acc(U ) = U nAcc(U ). So U is stable.