Leila Amgoud
email: amgoud@irit.fr

Philippe Besnard

Srdjan Vesic

Equivalence in logic-based argumentation 1

Keywords: argumentation, equivalence, logic

This paper investigates when two abstract logic-based argumentation systems are equivalent. It defines various equivalence criteria, investigates the links between them, and identifies cases where two systems are equivalent with respect to each of the proposed criteria. In particular, it shows that under some reasonable conditions on the logic underlying an argumentation system, the latter has an equivalent finite subsystem, called core. This core constitutes a threshold under which arguments of the system have not yet attained their final status and consequently adding a new argument may result in status change. From that threshold, the statuses of all arguments become stable.

Introduction

Argumentation is a reasoning process in which interacting arguments are built and evaluated. It is widely studied in Artificial Intelligence, namely for reasoning about inconsistent information [START_REF] Bondarenko | An abstract, argumentation-theoretic approach to default reasoning[END_REF][START_REF] Garcia | Defeasible logic programming: An argumentative approach[END_REF][START_REF] Governatori | Argumentation semantics for defeasible logic[END_REF], making decisions [START_REF] Amgoud | Using arguments for making and explaining decisions[END_REF][START_REF] Kakas | Argumentation based decision making for autonomous agents[END_REF][START_REF] Labreuche | Argumentation of the decision made by several aggregation operators based on weights[END_REF], and modelling agents interactions [START_REF] Amgoud | Modelling dialogues using argumentation[END_REF][START_REF] Prakken | Formal systems for persuasion dialogue[END_REF][START_REF] Reed | Dialogue frames in agent communication[END_REF].

One of the most abstract argumentation systems was proposed by [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. It consists of a set of arguments and a binary relation representing conflicts among them. Several semantics were proposed by the same author and by others for evaluating the arguments [START_REF] Baroni | SCC-recursiveness:Ageneral schema for argumentation semantics[END_REF]Caminada, 2006b;[START_REF] Dung | Computing ideal skeptical argumentation[END_REF]. Each of them consists of a set of criteria that should be satisfied by any acceptable set of arguments, called extension. From the extensions, a status is assigned to each argument: an argument is sceptically accepted if it appears in each extension, it is credulously accepted if it belongs to some extensions and not to others, and finally it is rejected if it is not in any extension. Several key decision problems were identified (like whether an argument is sceptically accepted under a given semantics), and their computational complexity investigated [START_REF] Dunne | Computational properties of argument systems satisfying graph-theoretic constraints[END_REF][START_REF] Dunne | Complexity of abstract argumentation[END_REF]. Most of the results concern finite argumentation systems (i.e., systems that have finite sets of arguments).

Almost all existing argumentation systems for reasoning about inconsistent information are instantiations of this abstract system -except the Delp system developed by [START_REF] Garcia | Defeasible logic programming: An argumentative approach[END_REF] and the one proposed by [START_REF] Besnard | Elements of argumentation[END_REF]. An instantiation starts with a logic (L, CN) where L is the language of this logic and CN its consequence operator. It

The goal of this paper is to study when two reasoning systems, i.e., instantiated argumentation systems are equivalent. We do not focus either on a particular logic or on a particular attack relation. Rather, we study abstract but structured argumentation systems. Indeed, we assume systems that are built under the abstract monotonic logics of [START_REF] Tarski | On some fundamental concepts of metamathematics[END_REF] and that use any attack relation. We start by extending the list of equivalence criteria by adding new ones which consider outputs that are proper to logic-based argumentation systems, like the plausible inferences. We show that these criteria are too rigid since they do not take into account the structure of arguments and are syntax-dependent. We then refine them using a new notion of equivalence of arguments and the classical notion of equivalence of formulae. We investigate the links between the different criteria. Some of the results hold for any attack relation while others hold only when the attack relations of the two systems satisfy some intuitive properties. We then identify cases where two systems are equivalent with respect to each of the proposed criteria.

Another contribution of the paper consists of showing that under some reasonable conditions on the logic (L, CN), each argumentation system has an equivalent finite subsystem, called the core. The core is seen as the smallest subsystem that retrieves all the outputs of its target. This notion is of great importance not only for replacing infinite systems with finite ones, but also for replacing finite systems with smaller ones. Indeed, it is well known that building arguments from a knowledge base is a computationally complex task. Consider the case of a propositional base. An argument is usually defined as a logical proof containing a consistent subset of the base, called a support, and a given statement, called a conclusion. Thus, there are at least two tests to be undertaken: a consistency test which is an NP-complete problem and an inference test (i.e., testing whether the conclusion is a logical consequence of the support) which is a co-NP-complete problem. Hence, finding the components of an argumentation system is a real challenge. Exchanging a system with its core may thus considerably reduce the bulk of computation.

The paper is organised as follows. In section 2, we recall the logic-based argumentation systems we are interested in. In section 3, we study equivalence. We propose various equivalence criteria, study their interdependencies and provide conditions under which two systems are equivalent with respect to each of the proposed criteria. In section 4, we define the notion of a core of an argumentation system, study when a core is finite, and investigate its role in dynamic situations. The last section is devoted to some concluding remarks and perspectives. All the proofs are given in the appendix.

Logic-based argumentation systems

This section describes the logic-based argumentation systems we are interested in. They are built around the abstract monotonic logic proposed by [START_REF] Tarski | On some fundamental concepts of metamathematics[END_REF]. Such a logic is a pair (L, CN) where L is any set of well-formed formulae and CN is a consequence operator, i.e., a function from 2 L to 2 L that satisfies the following five postulates:

• X ⊆ CN(X ) (Expansion) • CN(CN(X )) = CN(X ) (Idempotence) • CN(X ) = Y ⊆ f X CN(Y ) 2 (Finiteness) • CN({x}) = L for some x ∈ L (Absurdity) • CN(∅) = L (Coherence)
Intuitively, CN(X ) returns the set of formulae that are logical consequences of X according to the logic at hand. Almost all well-known logics (classical logic, intuitionistic logic, modal logics, etc.) are special cases of Tarski's notion of monotonic logic. In such a logic, the notion of consistency is defined as follows.

Definition 1 (Consistency). A set X ⊆ L is consistent iff CN(X ) = L. It is inconsistent otherwise.

Arguments are built from a knowledge base , a finite subset of L. They are minimal (for set inclusion) proofs for some statements, called their conclusions.

Definition 2 (Argument). Let (L, CN) be a Tarskian logic and ⊆ L. An argument built from is a pair (X, x) s.t.

• X is a finite consistent subset of ;

• x ∈ L; • x ∈ CN(X ); • ∄X ′ ⊂ X s.t. x ∈ CN(X ′ ).
X is the support of the argument and x its conclusion.

The following example illustrates the previous definition.

Example 3 Let (L, CN) be propositional logic (a Tarskian logic) and = {x, ¬y, x → y} be a knowledge base. Examples of arguments that may be built from this base are:

• ({x}, x), ({¬y}, ¬y), ({x → y}, x → y); • ({x, x → y}, y), ({x, ¬y}, x ∧ ¬y), ({¬y, x → y}, ¬x); • ({x}, x ∧ x), ({x}, x ∨ y), ({x}, x ∨ z); • . . .
The previous definition specified what we accept as an argument. It is worth mentioning that the set of all arguments that may be built from a knowledge base may be infinite even when the base is itself finite. This depends on the underlying logic. This is, for instance, the case under propositional logic. Thus, this is also the case in the previous example.

Notations: For an argument a = (X, x), Conc(a) = x and Supp(a) = X . For a set S ⊆ L, Arg(S) = {a|a is an argument (in the sense of Definition 2) and Supp(a) ⊆ S}. For any set E ⊆ Arg(L) of arguments, Base(E) = a∈E Supp(a).

An attack relation R is defined on a given set A of arguments, i.e., R ⊆ A × A. The writing aRb (or (a, b) ∈ R) means that the argument a attacks the argument b. This relation expresses disagreements between arguments. [START_REF] Amgoud | Bridging the gap between abstract argumentation systems and logic[END_REF] argue that it should capture the inconsistency of the knowledge base. An example of such a relation is the so-called assumption attack relation [START_REF] Elvang-Gøransson | Acceptability of arguments as 'logical uncertainty[END_REF]. According to this relation, an argument attacks another if it undermines one of the formulae of its support. In the sequel, the attack relation is left unspecified.

A logic-based instantiation of Dung's argumentation system is defined as follows.

Definition 4 (Argumentation system). An argumentation system built over a knowledge base is a pair

F = (A, R) where A ⊆ Arg( ) and R ⊆ A × A is an attack relation.
Almost all existing argumentation systems consider the whole set Arg( ) of arguments. For the purpose of this paper, we do not need to make this assumption. The reason is that we are looking for equivalent systems, thus, we may be interested in a subsystem which is equivalent to the 'complete' system (i.e., the one with the whole set Arg( ) of arguments). We may also need to compare two subsystems of a given complete system. When the set of arguments is infinite, then the corresponding argumentation system is said to be infinite.

Definition 5 (Finite argumentation system). An argumentation system F

= (A, R) is finite iff the set A is finite. Otherwise it is infinite.
In what follows, arguments are evaluated using the semantics proposed by [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. Before recalling them, let us first introduce the two requirements on which they are based: conflict-freeness and defence.

Definition 6 (Conflict-freeness and Defence). Let F = (A, R) be an argumentation system, E ⊆ A and a ∈ A.

• E is conflict-free iff ∄a, b ∈ E s.t. aRb; • E defends a iff ∀b ∈ A, if bRa then ∃c ∈ E s.t. cRb.
The next definition introduces the different semantics we are considering in this paper. Note that there are several other semantics in the literature like semi-stable semantics (Caminada, 2006b), ideal semantics [START_REF] Dung | Computing ideal skeptical argumentation[END_REF], and the recursive ones [START_REF] Baroni | SCC-recursiveness:Ageneral schema for argumentation semantics[END_REF]. However, for the purpose of this paper, we do not need to recall them. The main aim of the paper is to formalise the concept of equivalence in argumentation, and to show how it can be used for different purposes. The ideas hold under any semantics. Thus, we choose the most common ones.

Definition 7 (Acceptability semantics). Let F = (A, R) be an argumentation system and E ⊆ A. We say that E is admissible iff it is conflict-free and defends all its elements.

• E is a complete extension iff it is admissible and contains any argument it defends.

• E is a preferred extension iff it is a maximal (for set inclusion) admissible set. • E is a stable extension iff it is conflict-free and ∀a ∈ A \ E, ∃b ∈ E s.t. bRa.
• E is a grounded extension iff it is a minimal (for set inclusion) complete extension.

Let Ext x (F) denote the set of all extensions of the argumentation system F under semantics x where x ∈ {c, p, s, g} and c (resp. p, s, g) stands for complete (resp. preferred, stable and grounded). When we do not need to refer to a particular semantics, we use the notation Ext(F) for short.

Throughout the paper, we use the term 'all reviewed semantics' to refer to the four semantics stated in the previous definition (i.e., complete, preferred, stable and grounded semantics). When a result is stated without referring to a particular semantics, it means that it holds for all the reviewed semantics. It is worth recalling that grounded semantics guarantees one extension while all the other semantics may ensure several extensions. Note also that, in general, an argumentation system may have an infinite number of extensions even if the knowledge base is finite. Let us consider the following example.

Example 8. Let (L, CN) be a Tarski's logic such that the set L contains an infinite number of formulae, L = {x 0 , x 1 , x 2 , . . .}) and

CN(X ) = ∅ if X = ∅ {x i , x i+1 , x i+2 , . . .} else, where i is the minimal number s.t. x i ∈ X.
Consider now the knowledge base = {x 1 } and the attack relation defined as follows:

For two arguments a and b, aRb iff Conc(a) = Conc(b).

The argumentation system (Arg( ), R) has an infinite number of stable extensions:

{({x 1 }, x 1 )}, {({x 1 }, x 2 )}, {({x 1 }, x 3 )}, . . ..
An extension (under a given semantics) represents a coherent position or point of view. Thus, it contains arguments that can be accepted together. However, the status of a given argument is determined with respect to all the extensions.An argument is either 1) sceptically accepted (if it belongs to all the extensions), or 2) credulously accepted (if it belongs to some but not all extensions), or 3) rejected (if it does not belong to any extension).

Definition 9 (Status of arguments). Let F = (A, R) be an argumentation system and a ∈ A.

• a is sceptically accepted iff a

∈ E i ∈Ext(F ) E i . • a is credulously accepted iff a ∈ E i ∈Ext(F ) E i . • a is rejected iff a / ∈ E i ∈Ext(F ) E i .
Let Status(a, F) be a function which returns the status of argument a in system F.

The following definition summarises all the possible outputs of an argumentation system.

Definition 10 (Outputs). Let F = (A, R) be an argumentation system built over a knowledge base .

• Ext(F) is the set of extensions of F under a given semantics.

• Sc(F) = {a ∈ A|a is sceptically accepted}.

• Cr(F) = {a ∈ A|a is credulously accepted}.

• Output sc (F) = {Conc(a)|a is sceptically accepted}. • Output cr (F) = {Conc(a)|a is credulously accepted}. • Bases(F) = {Base(E)|E ∈ Ext(F)}.
The first set contains the extensions of a system F under a given semantics. The four next sets contain the sceptically and credulously accepted arguments (resp. conclusions). The set Bases(F) contains the sub-bases of which are computed by the extensions of F. Note that the three last outputs can only be defined for structured argumentation systems. Finally, it is worth noticing that all the five last outputs follow from the extensions.

Equivalence

The notion of equivalence in argumentation theory is of great importance since it defines which systems are interchangeable. This is crucial for comparing systems using different attack relations, or for replacing a system with a smaller one.

Equivalence criteria

We assume a fixed Tarskian logic (L, CN). This means that we study the equivalence of two systems that are grounded on the same logic. This assumption is not strong since:

(1) the kind of applications in which equivalence is needed assume that the two systems to be compared use the same logic; and (2) it is difficult to compare different logics since they may have different expressive power.

We consider two arbitrary argumentation systems F = (A, R) and F ′ = (A ′ , R ′ ) that are defined using the fixed logic. Note that the two systems may be built over different knowledge bases (respectively and ′ ).

The study of equivalence of two argumentation systems passes through the definition of equivalence criteria. We propose two families of criteria. Both compare the outputs of the two systems. However, the first family is syntax-dependent while the second family takes advantage of similarities between arguments (respectively formulae). The following definition introduces the criteria of the first family. Recall that the first three criteria were already proposed by [START_REF] Oikarinen | Characterizing strong equivalence for argumentation frameworks[END_REF].

Definition 11 (Equivalence criteria). Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems built using the same Tarskian logic (L, CN).F and F ′ are equivalent with respect to criterion EQi, denoted by F ≡ E Qi F ′ , iff EQi holds where i ∈ {1, . . . , 6} and:

EQ1 Ext(F) = Ext(F ′ ); EQ2 Sc(F) = Sc(F ′ ); EQ3 Cr(F) = Cr(F ′ ); EQ4 Output sc (F) = Output sc (F ′ ); EQ5 Output cr (F) = Output cr (F ′ ); EQ6 Bases(F) = Bases(F ′ ).
The first three criteria concern arguments whereas the other three refer to formulae. For instance, criterion E Q1 ensures that the two argumentation systems have exactly the same extensions (under a given semantics) whereas criterion E Q4 compares the conclusions that are drawn from the knowledge bases of the two systems. Note that rejected arguments are not considered when comparing two argumentation systems. Indeed, the set of rejected arguments is not an important output of a system (compared to sceptical and credulous arguments). Moreover, it is exactly the complement of the set of credulous arguments. Let us consider the following example.

Example 12. Let (L, CN) be propositional logic. Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems such that:

• A = {a 1 , a 2 } and R = {(a 1 , a 2 )}; • A ′ = {a 2 , a 3 } and R ′ = {(a 3 , a 2 )};
with:

• a 1 = ({t ∧ ¬x}, ¬x); • a 2 = ({x, y}, x ∧ y);

• a 3 = ({w ∧ ¬y}, ¬y).

Under grounded (resp. complete, preferred, stable) semantics, Ext(F) = {{a 1 }} and Ext(F ′ ) = {{a 3 }}. It is easy to see that F and F ′ would be equivalent if we compare rejected arguments since their sets of rejected arguments coincide (i.e., the set {a 2 }). However, the two systems have almost nothing in common since neither their conclusions (¬x resp. ¬y) nor their arguments coincide.

The previous criteria do not take into account the possible similarities/equivalences between arguments or between formulae. Consequently, they are too rigid and may miss some clear equivalences between argumentation systems as illustrated by the following example.

Example 13. Let (L, CN) be propositional logic. Let us consider two argumentation systems F and F ′ such that Ext(F) = {E}, Ext(F ′ ) = {E ′ } and

• E = {({x → y}, x → y)}; • E ′ = {({x → y}, ¬x ∨ y)}.
The two systems F and F ′ are equivalent with respect to criterion EQ6 since Bases(F) = Bases(F ′ ) = {{x → y}}. However, they are not equivalent with respect to the remaining criteria since the two arguments ({x → y}, x → y) and ({x → y}, ¬x ∨ y) (resp. the two formulae x → y and ¬x ∨ y) are considered as different.

This example shows that the six criteria are syntax-dependent. Indeed, they consider the two arguments ({x → y}, x → y) and ({x → y}, ¬x ∨ y) as different even if they have the same supports and logically equivalent conclusions. Let us now consider a different example which shows another limit of the previous criteria.

Example 14. Let (L, CN) be propositional logic. Let us consider two argumentation systems F and

F ′ such that Ext(F) = {E}, Ext(F ′ ) = {E ′ } and • E = {({x, ¬¬y}, x ∧ y)}; • E ′ = {({x, y}, x ∧ y)}.
The two systems F and F ′ are equivalent with respect to EQ4 and EQ5 but are not equivalent with respect to the remaining criteria, including EQ6. However, for each formula in Bases(F) = {{x, ¬¬y}}, there is an equivalent one in Bases(F) = {{x, y}} and vice versa.

The two previous examples show that in order to have more refined equivalence criteria, the logical equivalence between formulae and between sets of formulae should be considered.

Definition 15 (Equivalence of formulae). Let x, y ∈ L and X, Y ⊆ L.

• The two formulae x and y are equivalent, denoted by x ≡ y, iff CN({x}) = CN({y}).

We write x ≡ y otherwise.

• X and Y are equivalent, denoted by X ∼ = Y , iff ∀x ∈ X , ∃y ∈ Y s.t. x ≡ y and ∀y ∈ Y, ∃x ∈ X s.t. x ≡ y. We write X ∼ = Y otherwise.
Example 16. In the case of propositional logic, the two sets {x, ¬¬y} and {x, y} from Example 14 are equivalent.

Note that if X ∼ = Y , then CN(X ) = CN(Y ). However, the converse is not true. For instance, CN({x ∧ y}) = CN({x, y}) while {x ∧ y} ∼ = {x, y}. One might ask why the equality of CN(X ) and CN(Y ) is not used in order to state that X and Y are equivalent. The previous example might have already given some of our motivation for such a definition: wanting to make a distinction between {x, y} and {x ∧ y}. The following example of two argumentation systems whose credulous conclusions are respectively {x, ¬x} and {y, ¬y} is more drastic: it is clear that CN({x, ¬x}) = CN({y, ¬y}) while the two sets are in no way similar.

In order to define an accurate notion of equivalence between two argumentation systems, we also take advantage of the equivalence of arguments. There are three ways of defining such equivalence, as shown in the next definition.

Definition 17 (Equivalence of arguments

). Let a, a ′ ∈ Arg(L). • a ≈ 1 a ′ iff Supp(a) = Supp(a ′ ) and Conc(a) ≡ Conc(a ′ ). • a ≈ 2 a ′ iff Supp(a) ∼ = Supp(a ′ ) and Conc(a) = Conc(a ′ ). • a ≈ 3 a ′ iff Supp(a) ∼ = Supp(a ′ ) and Conc(a) ≡ Conc(a ′ ).
Example 18. The two arguments ({x → y}, x → y) and ({x → y}, ¬x ∨ y) from Example Note that each criterion ≈ i is an equivalence relation (i.e., reflexive, symmetric and transitive).

Property 19. Each criterion ≈ i is an equivalence relation (with i ∈ {1, 2, 3}).

The following property summarises the links between the three criteria and shows that criterion ≈ 3 is more general than the two others.

Property 20. Let a, a ′ ∈ Arg(L).

• If a ≈ 1 a ′ , then a ≈ 3 a ′ ; • If a ≈ 2 a ′ , then a ≈ 3 a ′ .
It is worth mentioning that two argumentation systems may have arguments that are equivalent with respect to ≈ 1 and other arguments that are equivalent with respect to ≈ 2 . Thus, neither of the two criteria (≈ 1 , ≈ 2 ) can capture both equivalences. However, criterion ≈ 3 does. Thus, for the purpose of our paper, we will consider criterion ≈ 3 . Throughout the paper, we refer to this criterion by ≈ for short.

The notion of equivalence of two arguments is extended to an equivalence of sets of arguments as follows.

Definition 21 (Equivalence of sets of arguments). Let E, E ′ ⊆ Arg(L). The two sets E and

E ′ are equivalent, denoted by E ∼ E ′ , iff ∀a ∈ E, ∃a ′ ∈ E ′ s.t. a ≈ a ′ and ∀a ′ ∈ E ′ , ∃a ∈ E s.t. a ≈ a ′ . Example 22. The two extensions {({x → y}, x → y)} and {({x → y}, ¬x ∨ y)} from Example 13 are equivalent.
We are now ready to introduce the family of refined equivalence criteria.

Definition 22 (Refined equivalence criteria). Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems built using the same Tarskian logic. F and F ′ are equivalent with respect to criterion EQib, denoted by F ≡ E Qib F ′ , iff EQib holds where i ∈ {1, 2, 3, 4, 5, 6} and:

• EQ1b there exists a bijection f :

Ext(F) → Ext(F ′ ) s.t. ∀E ∈ Ext(F), E ∼ f (E); • EQ2b Sc(F) ∼ Sc(F ′ ); • EQ3b Cr(F) ∼ Cr(F ′ ); • EQ4b Output sc (F) ∼ = Output sc (F ′ ); • EQ5b Output cr (F) ∼ = Output cr (F ′ ); • EQ6b ∀S ∈ Bases(F), ∃S ′ ∈ Bases(F ′ ) s.t. S ∼ = S ′ and ∀S ′ ∈ Bases(F ′ ), ∃S ∈ Bases(F) s.t. S ∼ = S ′ .
Example 23. The two argumentation systems F and F ′ from Example 13 are equivalent with respect to the six refined criteria.

Example 24. The two argumentation systems F and F ′ from Example 14 are equivalent with respect to the six refined criteria.

It is easy to check that each criterion E Qib refines its strong version E Qi.

Property 25. For two argumentation systems F and

F ′ , if F ≡ E Qi F ′ then F ≡ E Qib F ′ with i ∈ {1, . . . , 6}.
Finally, we show that each of the twelve criteria is an equivalence relation.

Property 26. For all i ∈ {1, . . . , 6}, the criterion E Qi (resp. E Qib) is an equivalence relation.

Links between criteria

In the previous section, we proposed twelve equivalence criteria between argumentation systems. The following result establishes the dependencies between them.

Theorem 27. Let F and F ′ be two argumentation systems built on the same logic (L, CN).

Table 1 summarises the dependencies

(F ≡ x F ′ ) ⇒ (F ≡ x ′ F ′ ) under any of the reviewed semantics.
Table 1 is read as follows: for two criteria, c in row i and c ′ in column j, the + sign at the intersection of row i and column j means that if two systems are equivalent with respect to c then they are equivalent with respect to c ′ . For example, the + sign at the intersection of the row corresponding to E Q1b and the column corresponding to E Q3b means that if two argumentation systems are equivalent with respect to E Q1b then they must be equivalent with respect to E Q3b. It is worth noticing that two argumentation systems that are equivalent with respect to E Q1 are also equivalent with respect to any of the remaining criteria. This is not the case for its refined version E Q1b. For instance, two systems that are equivalent with respect to E Q1b are not necessarily equivalent with respect to E Q2b and E Q4b. Thus, E Q1 is the most general criterion. This is not surprising since the extensions of a system are at the heart of all the other outputs of an argumentation system. However, as seen in the previous section, the criterion E Q1 is too rigid since it does not take into account the internal structure of arguments.

Note that Theorem 27 is a full characterisation in the sense that no other links exist between criteria. In other words, if there is no + sign in Table 1, then it is not the case that the criterion in the corresponding row implies the criterion in the corresponding column. Note some dependencies that might at first glance be expected to hold but do not in the general case. Given the huge number of cases, we do not provide counter-examples for all of them, since the paper would become unfeasibly long. The next two examples serve as counter-examples for several cases and we strongly believe that the reader can construct counter-examples for other missing dependencies. The next example shows that EQ1b does not imply EQ1, EQ2, EQ3, EQ4, EQ5 nor EQ6 (in the general case). Even more interestingly, from this example we see that EQ1b does not imply either EQ2b or EQ4b.

Example 28. Suppose stable semantics and let L = {r 1 , r 2 , r 3 , r 4 , r 5 , r 6 , r 7 , r 8 , r 9 , r 10 , c} with CN defined as follows: for all X ⊆ L,

CN(X ) =    L \ {c}, if c / ∈ X and X = ∅ L, if c ∈ X ∅, if X = ∅. Let a 1 = ({r 1 }, r 2 ), a 2 = ({r 3 }, r 4 ), a 3 = ({r 5 }, r 6 ), a 4 = ({r 7 }, r 8 ), a 5 = ({r 9 }, r 10 ). Let A = {a 1 , a 2 , a 3 }, R = {(a 2 , a 3 ), (a 3 , a 2 )}, A ′ = {a 4 , a 5 } and R ′ = {(a 4 , a 5 ), (a 5 , a 4 )}. Sc(F) = {a 1 }, Sc(F ′ ) = ∅. F ≡ E Q1b F ′ since a bijection verifying conditions of EQ1b can be defined as: f : Ext(F) → Ext(F ′ ), f ({a 1 , a 2 }) = {a 4 }, f ({a 1 , a 3 }) = {a 5 }.
However, criteria like EQ2b and EQ4b are not satisfied.

We can also show that EQ4 does not imply EQ1, EQ1b, EQ2, EQ2b, EQ3, EQ3b, EQ6, EQ6b, as illustrated by the following example.

Example 29. Suppose stable semantics, let (L, CN) be propositional logic and let

A = {({x ∧ y}, x)}, A ′ = {({x ∧ z}, x)}, R = ∅, R ′ = ∅. Output sc (F) = Output sc (F ′ ) = {x}.
The previous links between the criteria hold under all the acceptability semantics from Definition 7.As might be expected, there are more links between criteria for single-extension semantics, i.e., grounded semantics.

Theorem 30. The links between the twelve equivalence criteria under grounded semantics are summarised in Table 2.

The previous results hold for any pair of argumentation systems that are grounded on the same Tarskian logic and the same attack relations that are used by the systems. For example, in the case of Theorem 27, this result is also 'complete' in the sense that no other links exist except those depicted in Table 2. In what follows, we show that there are additional links between some criteria when the attack relations of the two systems satisfy some properties, namely those discussed by [START_REF] Gorogiannis | Instantiating abstract argumentation with classical logic arguments: Postulates and properties[END_REF]. Below we recall the ones that are important for our study.

C1 ∀a, b, c ∈ A, if Conc(a) = Conc(b) then (aRc ⇔ bRc). C1b ∀a, b, c ∈ A, if Conc(a) ≡ Conc(b) then (aRc ⇔ bRc). C2 ∀a, b, c ∈ A, if Supp(a) = Supp(b) then (cRa ⇔ cRb). C2b ∀a, b, c ∈ A, if Supp(a) ∼ = Supp(b) then (cRa ⇔ cRb).
The first two properties say that two arguments which have the same (resp. equivalent) conclusions attack the same arguments. The second two properties say that arguments which have the same (resp. equivalent) supports are attacked by the same arguments.

The following result establishes some links between the four properties.

Property 31. Let R be an attack relation.

• If R satisfies C1b then it satisfies C1. • If R satisfies C2b then it satisfies C2.
Before presenting the new links, let us first study how the equivalence relation ≈ between arguments is related to an attack relation which satisfies the two properties C1b and C2b. We show that equivalent arguments (with respect to ≈) behave in the same way with respect to attacks in the case that the attack relation satisfies these two properties.

Property 32. Let (A, R) be an argumentation system s.t. R satisfies C1b and C2b. For all a, a ′ , b, b ′ ∈ A, (a ≈ a ′ and b ≈ b ′ ) implies (aRb iff a ′ Rb ′ ).
The next result shows that equivalent arguments belong to the same extensions in an argumentation system whose attack relation satisfies C1b and C2b.

Property 33. Let (A, R) be an argumentation system s.t. R satisfies C2b. For all a, a

′ ∈ A, if a ≈ a ′ , then ∀E ∈ Ext(F), a ∈ E iff a ′ ∈ E.
An obvious consequence of this property is that equivalent arguments have the same status in any argumentation system. Property 34. Let (A, R) be an argumentation system s.t. R satisfies C1b and C2b. For all a, a ′ ∈ A, if a ≈ a ′ , then Status(a, F) = Status(a ′ , F).

We also show that two equivalent arguments which belong to two equivalent argumentation systems with respect to criterion E Q1b have the same status.

Property 35. Let F = (A, R), F ′ = (A ′ , R ′ ) be two argumentation systems built from the same logic (L, CN) such that R and R ′ satisfy C1b and C2b. If F ≡ E Q1b F ′ , then for all a ∈ A and for all a

′ ∈ A ′ , if a ≈ a ′ then Status(a, F) = Status(a ′ , F ′ ).
Finally, we show that if two argumentation systems whose attack relations satisfy C1b and C2b are equivalent with respect to E Q1b, then they are also equivalent with respect to E Q2b and E Q4b.

Theorem 36. Let F = (A, R), F ′ = (A ′ , R ′ ) be two argumentation systems built from the same logic (L, CN) such that R and R ′ satisfy C1b and C2b. If

F ≡ E Q1b F ′ , then F ≡ x F ′ with x ∈ {E Q2b, E Q4b}.

Cases of equivalent argumentation systems

We previously proposed different equivalence criteria of two argumentation systems built from the same logic. An important question now is: are there distinct argumentation systems which are equivalent with respect to those criteria?. Recall that in case of the criteria proposed by Oikarinen and Woltran (2011) (i.e., E Q1, E Q2 and E Q3), the answer is negative. Indeed, the authors have shown that when two argumentation systems do not have self-attacking arguments, they are equivalent if and only if they coincide. [START_REF] Amgoud | Bridging the gap between abstract argumentation systems and logic[END_REF] have shown that logic-based argumentation systems do not have selfattacking arguments. This means that the previous criteria are not useful in this context. In what follows, we show that their refinements make it possible to compare different systems. We focus on the criterion E Q1b since it is at the same time general like EQ1 but much more flexible (as it is syntax-independent).

We start by showing that under some reasonable conditions on the attack relation, an argumentation system built from a knowledge base has a finite number of extensions even if its set of arguments is itself infinite.

Theorem 37. Let (A, R) be an argumentation system built over . If is finite and R satisfies C2, then (A, R) has a finite number of extensions under all reviewed semantics.

We are now interested in the case of two argumentation systems that may be built from two distinct knowledge bases but use the same attack relation. For instance, both systems use the 'rebut' relation or both systems use 'assumption attack', etc. Recall that Arg(L) is the set of all arguments that can be built from a fixed logical language L using a fixed consequence operator CN. We denote by R L the attack relation which is used in the two systems with R L ⊆ Arg(L)×Arg(L). The following result shows under which conditions two systems are equivalent with respect to E Q1b.

Theorem 38. Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems s.t. A, A ′ ⊆ Arg(L) and R = R L | A , R ′ = R L | A ′ . If R L satisfies C1b and C2b and A ∼ A ′ , then F ≡ E Q1b F ′ .
The following corollary follows from the links between the criteria.

Corollary 39. Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems s.t. A, A ′ ⊆ Arg(L) and R = R L | A , R ′ = R L | A ′ . If R L satisfies C1b and C2b and A ∼ A ′ , then F ≡ x F ′ with x ∈ {E Q2b, E Q3b, E Q4b, E Q5b, E Q6b}.

Core(s) of an argumentation system

In this section we introduce a new concept: the core of an argumentation system. It is a proper subsystem of an argumentation system which considers only one argument among equivalent ones.

Notation: for an arbitrary set X , an arbitrary equivalence relation ∼ on X , and x ∈ X ,

[x] = {x ′ ∈ X |x ′ ∼ x} and X/ ∼= {[x]|x ∈ X }. For any X ⊆ L, Cncs(X ) = {x ∈ L|∃Y ⊆ X such that CN(Y ) = L and x ∈ CN(Y )}.
In other words, Cncs(X ) is the set of formulae that are drawn from consistent subsets of X .

We define a core as follows.

Definition 40 (Core of an argumentation system). Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems. F ′ is a core of F iff:

• A ′ ⊆ A; • ∀C ∈ A/ ≈, ∃!a ∈ C ∩ A ′ ; • R ′ = R| A ′ (i.e., R ′ is the restriction of R on A ′ ).
It is worth noting that an argumentation system may have several cores. The set of arguments of each of them is equivalent to the set of arguments of the original system.

Property 41. Let F = (A, R) and

F ′ = (A ′ , R ′ ) be two argumentation systems. If F ′ is a core of F, then A ∼ A ′ .
When the attack relation satisfies some intuitive properties, an argumentation system is equivalent to any of its cores.

Theorem 42. Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems s.t. R and R ′ satisfy C1b and C2b. If F ′ is a core of F, then F ≡ E Q1b F ′ .
It follows that the outputs of an argumentation system coincide with those of its cores.

Corollary 43. Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems s.t. R and R ′ satisfy C1b and C2b. If F ′ is a core of F, then:

• Sc(F) ∼ Sc(F ′ ); • Cr(F) ∼ Cr(F ′ ); • Output sc (F) ∼ = Output sc (F ′ ); • Output cr (F) ∼ = Output cr (F ′ ); • Bases(F) = Bases(F ′ ).
A core is seen as a compact version of an argumentation system. The statuses of its arguments are those computed in the original system. Moreover, it is easy to show that each argument which does not belong to a core has an equivalent argument with the same status in the original system.

Property 44. Let F = (A, R) be an argumentation system and F ′ = (A ′ , R ′ ) its core. If R satisfies C1b and C2b then:

• If a ∈ A ′ , then Status(a, F) = Status(a, F ′ ); • If a / ∈ A ′ , then Status(a, F) = Status(b, F ′ ) for some b ∈ A ′ with a ≈ b.
It is worth noticing that the cores of a given argumentation system are equivalent. This follows from the fact that the equivalence criteria (e.g., E Q1b) are equivalence relations, thus transitive. So, if F is an argumentation system and F ′ and F ′′ its cores, then from

F ≡ E Q1b F ′ and F ≡ E Q1b F ′′ , we have F ′ ≡ E Q1b F ′′ .
Property 45. Let F ′ and F ′′ be two cores of an argumentation system F = (A, R) such that R satisfies C1b and C2b. It holds that

F ′ ≡ E Q1b F ′′ .
So far, we have shown how to define a proper subsystem of an argumentation system which is able to subsequently compute all of its outputs. However, there is no guarantee that the subsystem is finite (i.e., it has a finite set of arguments). In fact, the finiteness of cores depends broadly on the logic underlying the argumentation system (i.e., (L, CN)). We show that finiteness is ensured by logics in which any consistent finite set of formulae has finitely many logically non-equivalent consequences when the knowledge base is finite. Two examples of such logics are [START_REF] Parry | Analytic implication: Its history, justification, and varieties[END_REF] and the fragment of intuitionistic logic (introduced by McKinsey and Tarski) studied by [START_REF] Mccall | A simple decision procedure for one-variable implication/negation formulae in intuitionist logic[END_REF].

Theorem 46. Let F = (A, R) be an argumentation system built over a knowledge base (i.e., A ⊆ Arg( )). If Cncs( )/ ≡ is finite, then every core of F is finite.

To sum up, under some reasonable conditions on the attack relation and the logic, any argumentation system has finite and equivalent cores.

Corollary 47. Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems s.t. R and R ′ satisfy C1b and C2b and Cncs( )/ ≡ is finite. If F ′ is a core of F, then F ′ is finite and F ≡ E Q1b F ′ .

Core(s) in propositional logic

The previous section has shown that argumentation systems which are built under some particular logics have finite cores. Propositional logic is not one of them since the set Cncs( )/ ≡ is not finite. Let us consider the following counter-example.

Example 48. Let (L, CN) be propositional logic and let = {x}. The set Cncs( ) contains the following formulae: x, x ∨ z 1 , x ∨ z 2 , x ∨ z 3 , . . . and is thus infinite.

Thus, under propositional logic, the set of all arguments that can be built from a finite knowledge base is infinite. The proof of the following property follows from the idea of the previous example.

Property 49. Let (L, CN) be propositional logic and a finite knowledge base having at least one consistent formula. The set Arg( ) is infinite.

Despite the previous properties (on Cncs( ) and Arg( )), it is possible to define finite cores for any argumentation system under propositional logic. The idea is to understand the reasons of infiniteness and try to avoid them. There are several sources of infiniteness of the set of arguments. The first one is the fact of duplicating several arguments with the same support and equivalent conclusions. For instance, the arguments {x}, x ∨ y , {x}, ¬x → y and {x}, (¬x → y) ∨ (x ∨ ¬x) are built from = {x, y} and are in some sense redundant, or equivalent with respect to the relation ≈. The case is similar for the two arguments {x}, x and {x}, x ∧ x . It is easy to see that the number of such arguments is infinite. Property 34 shows that such arguments have the same status in an argumentation system whose attack relation verifies the two properties C1b and C2b.

The second source of infiniteness of a set of arguments is due to atoms that have no occurrence within the knowledge base but occur in conclusions of arguments. For instance, the two arguments {x}, x ∨ z and {x}, x ∨ z ∨ w belong to the set Arg( ) although z and w do not occur in = {x, y}. This section shows that such arguments have no impact on the other arguments of Arg( ).

Another source of infiniteness might be an infinite knowledge base . It can contain an infinite amount of non-redundant information and in such cases it is impossible to find a finite core of the corresponding argumentation system. That is why, throughout the paper, we suppose that is finite.

In order to illustrate how to deal with the sources of infiniteness in a concrete example, the remainder of the section presents a detailed study of the case when a particular attack relation (called assumption attack) is used together with a stable semantics. In the next section, we show how some of the results can be generalised to large class of logics. Let us first introduce some notations.

Notations:Atoms( ) is the set of atoms occurring in . Arg( ) ↓ is the subset of Arg( ) that contains only arguments with conclusions based on Atoms( ). For instance, for = {x, y}, Atoms( ) = {x, y}. Thus, an argument such as ({x}, x ∨ z ∨ w) does not belong to the set Arg( ) ↓ .

We now define the attack relation we use in this section.

Definition 50 (Assumption attack). Let be a propositional knowledge base and a, b ∈ Arg( ). The argument a undermines b, denoted aR as b, iff ∃x ∈ Supp(b) s.t. Conc(a) ≡ ¬x.

It is worth noticing that this relation satisfies the two properties C1b and C2b.

Property 51. The relation R as verifies the two properties C1b and C2b. Now, note that the set Arg( ) ↓ is infinite (due to equivalent arguments). In what follows, we show that its arguments have the same status in the two systems F = (Arg( ), R) and

F ↓ = (Arg( ) ↓ , R ↓ ) (where R ↓ is of course the restriction of R to Arg( ) ↓ ).
The first result shows that arguments which use external variables (i.e., variables which are not in Atoms( )) in their conclusions can be omitted from the reasoning process.

Theorem 52. Let F = (Arg( ), R as ) be an argumentation system built over a propositional knowledge base , and F ↓ = (Arg( ) ↓ , R as↓ ) its subsystem. For all a ∈ Arg( ) ↓ , Status(a, F) = Status(a, F ↓ ) under a stable semantics.

Moreover, we show next that their status is still known. It is that of any argument in Arg( ) ↓ with the same support.

Theorem 53. Let F = (Arg( ), R as ) be an argumentation system built over a propositional knowledge base . For all a ∈ Arg( ) \ Arg( ) ↓ , under a stable semantics, Status(a, F) = Status(b, F) where b ∈ Arg( ) ↓ and Supp(a) ≈ Supp(b).

To sum up, the two previous theorems clearly show that one can use the subsystem F ↓ = (Arg( ) ↓ , R as↓ ) instead of F = (Arg( ), R as ) without losing any information. This system is still infinite due to redundant arguments. However, we prove next that the set Arg( ) ↓ is partitioned into a finite number of equivalence classes with respect to the equivalence relation ≈. This result is of great importance since it shows how it is possible to partition an infinite set of arguments into a finite number of classes. Note that each class may contain an infinite number of arguments. An example of such an infinite class is the one which contains (but is not limited to) all the arguments having {x} as a support and x, x ∧ x, . . . as conclusions. A consequence of this result is that the cores of an argumentation system which considers only the set Arg( ) ↓ of arguments are finite.

Theorem 55. Let be a propositional knowledge base and F = (A, R as ) be an argumentation system such that A ⊆ Arg( ) ↓ . Then every core of F is finite.

Since the attack relation R as satisfies the two properties C1b and C2b, then from Theorem 42, an argumentation system that does not accept external variables in its arguments is equivalent to any of its cores.

Corollary 56. Let be a propositional knowledge base and F = (A, R as ) be an argumentation system using a stable semantics such that A ⊆ Arg(

) ↓ . F ≡ E Q1b F ′ where F ′ is a core of F.
Note that no core is equivalent to the original argumentation F = (Arg( ), R as ) with respect to E Q1b. This is because the set Output(G)/ ≡ of any core G is finite while Output(F)/≡ is infinite (due to conclusions containing atoms not occurring in ). However, the next result shows that it is possible to compute the output of the original argumentation system from the output of one of its cores.

Theorem 57. Let F be an argumentation system built over a propositional knowledge base using stable semantics and let G be one of its cores.

Output sc (F) = {x ∈ L s.t. Output sc (G) ⊢ x}.
An important question now is how to choose a core. A simple solution would be to pick exactly one formula from each set of logically equivalent formulae. Since a lexicographic order on set L is usually available, we can take the first formula from that set according to that order. Instead of defining a lexicographic order, one could also choose to take the disjunctive (or conjunctive) normal form of a formula.

On the finiteness of core in other logics

The previous section presented a study of cores in a concrete example (propositional logic, assumption attack, stable semantics). In this section, we show that if the atoms not appearing in are not used in the conclusions of arguments, there is a large class of logics with finite cores. The main technical challenge is that the notion of an abstract logic defined by Tarski is too abstract -namely there is no notion of atom or variable, so it is not possible to speak of omitting atoms appearing in . Thus, we will base our result on the notion of an algebra. First, recall that an algebra is a tuple (A, ( f i ) i∈I ) where each f i is an n i -ary operation over A. The similarity type of the algebra is (n i ) i∈I .

In this section, we consider only logics satisfying the following four conditions, which we call bounded algebraic logics.

(1) The language of such a logic is a term algebra L = (F, o 1 , . . . , o n ) such that n ∈ ω and n i ∈ ω for i = 1..n (that is, the language only has finitely many logical symbols, none of them is infinite in character: there is no infinitary disjunction, no infinitary conjunction, etc.).

(2) A model of such a logic can be characterised as an homomorphism from L to an algebra whose similarity type is exactly that of L (not all such homomorphisms need be models of the logic).

(3) Completeness holds (that is, CN( ) = CN( ) iff m( ) = m( ) in all models m of (L, CN)). (4) Such a logic is to satisfy absorption laws for o 1 , . . . , o n as follows.

Absorption laws for unary logical symbols:

Let {o 1 , . . . , o m } be the set of unary operators of L. We define a prefix as a finite sequence of operators. The logic is supposed to satisfy the following condition: for every subset {o i , . . . , o k } of the set of unary operators, for every atomic formula α, for every model m of (L, CN), there exists l < ω such that for every prefix P over {o i , . . . , o k } there exists a prefix P ′ over {o 1 , . . . , o m } such that length(P ′ ) ≤ l and m(P(γ )) = m(P ′ (γ )).

The system of absorption laws which is required for such logics need not be nonredundant or optimal in any way -all that is required is that the system exists (possibly through equivalence).

Since the number of unary operators is finite, there exists K < ω which is an upper bound of the length of prefixes P ′ for different subsets of unary operators.

As an illustration, take propositional intuitionistic logic. There is only one unary operator, namely ¬. We have l = 2 since γ ≡ γ , ¬γ ≡ ¬γ , ¬¬γ ≡ ¬¬γ , ¬¬¬γ ≡ ¬γ , ¬¬¬¬γ ≡ ¬¬γ , ¬¬¬¬¬γ ≡ ¬γ , etc.

As another example, in propositional modal logic S5, such an absorption law is ⋄¬⋄γ ≡ ¬ ⋄ γ . In this case, we have l = 3.

For a formula , the sublanguage L obtained by using only non-logical symbols occurring in and the logical symbols from L is easily defined (as the sub-algebra of L generated by the non-logical symbols occurring in ). Also, since a formula is a member of the term algebra L, the notion of a sub-formula coincides with the notion of a sub-term in L.

Given a formula from L, let x 1 , . . . , x l be all the atoms occurring in it. Let F k define the set of all formulas from L in which each x j occurs at most k times and no o i occur such that n i < 2. Clearly, for every k, we have that F k is finite. Let us define F + k as the set obtained as follows: for a formula ϕ, replace every sub-formula θ in ϕ with Pθ where P ranges over all prefixes of length less or equal to K . Do this for every formula ϕ in F k .

Lemma 58. For every k, F + k is finite.

Absorption laws for n-ary logical symbols:

It is required that the logic satisfies the following condition: given a formula , there exists k < ω such that for every non-unary operator o i , for every γ 1 , . . . , γ n ∈ F + k there exists δ ∈ F + k such that for every model m of (L, CN) we have

m(o i (γ 1 , . . . , γ n )) = m(δ).
As an illustration, in propositional classical logic, such an absorption law is (β ∧γ )∨γ ≡ γ .

Please observe that, in a number of logics, if o i (γ 1 , . . . , γ n i ) is in F + k then it may happen that the corresponding absorption law is identity.

Theorem 59. For every formula α ∈ L , there exists σ ∈ F + k s.t. CN(α) = CN(σ ). We define CN L ( ) to be CN( ) ∩ L . By applying the previous theorem in view of the lemma we obtain the following result.

Corollary 60. Given a formula from L, CN L ( ) is partitioned into finitely many CN-equivalence classes.

The main theorem of this section is now a direct consequence of the previous result.

Theorem 61. Let (L, CN) be a bounded algebraic logic. Let be a finite set of formulas from L. Let F = (A, R) be an argumentation system such that A is a set of arguments whose conclusions are all in CN( ) ∩ L . Then, every core of F is finite.

Note that unlike [START_REF] Wójcicki | Theory of logical calculi: Basic theory of consequence operations[END_REF], which calls algebraic logics those systems that satisfy Tarski's finiteness axiom, we restrict the meaning of algebraic logic to those that admit an algebraic semantics in the above direct manner (excluding for instance semantics based on cylindrical algebras, as designed for predicate first-order logic). Algebraic semantics for well-known logics can be found in the literature [START_REF] Rasiowa | The mathematics of metamathematics[END_REF].

Dynamics of argument status

Several works have studied the dynamics of an argumentation system. They mainly investigate how the acceptability or status of an argument may evolve when the argumentation system is extended with new arguments. For instance, [START_REF] Amgoud | Revising option status in argument-based decision systems[END_REF] show that an argument may be sceptically accepted in a system, and becomes rejected in an extended version of the system. Similarly, an argument may be rejected or credulously accepted in a system and becomes sceptically accepted in an extended system. It has been shown that the same phenomenon occurs when arguments are removed from an argumentation system [START_REF] Bisquert | Change in argumentation systems: Exploring the interest of removing an argument[END_REF]. In what follows, we show that the notion of core is at the heart of this change in arguments' statuses.

Throughout this section, we consider a fixed Tarskian logic (L, CN) and an attack relation R(L) ⊆ Arg(L) × Arg(L) which satisfies the two properties C1b and C2b. Given an argumentation system F = (A, R) and a set E of arguments,

• F ⊕ E = (A ′ , R ′ ) with A ′ = A ∪ E and R ′ = R(L)| A ′ . • F ⊖ E = (A ′ , R ′ ) with A ′ = A \ E and R ′ = R(L)| A ′ .
Before presenting the formal results, let us introduce a new definition.

Definition 62. Let F = (A, R) and G be argumentation systems. F contains a core of G iff there exists an argumentation system

H = (A h , R h ) s.t. A h ⊆ A and R h ⊆ R and H is a core of G.
The next result shows that if an argumentation system contains a core of its complete version, then adding new arguments does not impact on the status of existing arguments.

Theorem 63. Let F = (A, R) be an argumentation system built over a knowledge base such that R satisfies C1b and C2b. If

F contains a core of G = (Arg(Base(A)), R(L)| Arg(Base(A)) ), then for all E ⊆ Arg(Base(A)), • F ≡ E Q1b F ⊕ E; • ∀a ∈ A, Status(a, F) = Status(a, F ⊕ E); • ∀e ∈ E \ A, Status(e, F ⊕ E) = Status(a, F), where a ∈ A is any argument s.t. Supp(a) ≈ Supp(e).
It is clear that the previous result holds when F is itself a core of G. The following example shows that when a system does not contain a core of the system built over its base, new arguments may change the status of the existing ones.

Example 64. Let (L, CN) be propositional logic and let the attack relation R(L) be the assumption attack relation. Let F = (A, R) be an argumentation system such that A = {a 1 = ({strad, strad → ex p}, ex p), a 2 = ({¬strad}, ¬strad)}. Recall that R = R(L)| A . thus, R = {(a 2 , a 1 )}. The argument a 2 is sceptically accepted whereas a 1 is rejected. Let e = ({strad}, strad). It is clear that e ∈ Arg(Base(A)). However, the status of each of a 1 and a 2 changes in the system F ⊕ {e}. Namely, both arguments become credulously accepted.

The previous example illustrates a situation where an argumentation system F does not contain a core of the system constructed from its base. This means that not all available information is represented in F; thus, it is not surprising that it is possible to revise the statuses of arguments. In what follows, we also provide a situation where removing arguments from F will not impact the status of arguments in F.

Theorem 65. Let F = (A, R) be an argumentation system built over a knowledge base such that R satisfies C1b and C2b and let

E ⊆ A. If F ⊖ E contains a core of G = (Arg(Base(A)), R(L)| Arg(Base(A)) ), then: • F ≡ E Q1b F ⊖ E; • ∀a ∈ A \ E, Status(a, F) ≈ Status(a, F ⊖ E).
The obvious consequence of the above result is that if F ⊖ E is itself one of the cores of G then the statuses of its arguments are not changed after removing arguments from E.

Conclusion

In this paper, we tackled the question: when are two logic-based argumentation systems equivalent? We proposed various equivalence criteria. Some of them are shown to be syntax-dependent whereas others are more flexible and take advantage of equivalences between arguments and between formulae. The links between the criteria are largely investigated. Some of the results hold for any acceptability semantics and any attack relation, while others make reasonable assumptions on the attack relations or are shown under particular semantics. The comparative study revealed that there is one particular criterion which is both flexible and general. Thus, in the second part of the paper, we only focused on this criterion. We studied under which conditions two systems are equivalent with respect to this criterion. We have shown how to move from infinite argumentation systems to finite ones and how to replace a system with a proper subsystem without losing information.

It is worth mentioning that equivalence between arguments and sets of arguments has also been studied from a computational complexity perspective [START_REF] Wooldridge | On the complexity of linking deductive and abstract argument systems[END_REF]. The authors focused on one particular argumentation system: the one that is built on propositional logic and that uses the assumption attack relation. According to this work, two arguments are logically equivalent if and only if their conclusions are logically equivalent. Thus, the two arguments a = ({y, y → x}, x) and a ′ = ({z, z → x}, x) are equivalent. Note that in our paper, these two arguments are not equivalent. We consider them not equivalent since they are based on different hypotheses. It can be the case that one of these hypotheses is attacked but not the other one. For example, the argument b = ({¬y}, ¬y) attacks a but not a ′ . This example shows that the equivalence relation considered by Wooldridge et al. is too simplistic and is not sufficient to guarantee that all information from a knowledge base is represented in an argumentation system. Wooldridge et al. also propose an equivalence criterion between sets of arguments. According to this criterion, two sets of arguments, X and Y , are equivalent if there is a bijection between them, i.e., a function f s.t. ∀x ∈ X , f (x) is equivalent with x (using their equivalence criterion between arguments). In this paper, we proposed a more flexible criterion. Let us consider the following example: let X = {({x}, x), ({x}, ¬¬x)} and Y = {({x}, x)}. According to our criterion, the two sets X and Y are equivalent while they are not equivalent with respect to the criterion used by [START_REF] Wooldridge | On the complexity of linking deductive and abstract argument systems[END_REF]. Note that our criterion allows us to reduce an infinite system to a finite one, which is impossible if using the definition demanding for a bijection between the two sets.

Notes

1. This paper is a revised and extended version of two conference papers: Amgoud and Vesic (2011) and [START_REF] Amgoud | Identifying the core of logic-based argumentation systems[END_REF]. 2. The notation Y ⊆ f X means that Y is a finite subset of X .

Property 33. Let R be an attack relation.

• If R satisfies C1b then it satisfies C1. • If R satisfies C2b then it satisfies C2.
Proof. The proof follows directly from the two following observations: first, for two formulae ϕ and ψ, it holds that ϕ = ψ implies ϕ ≡ ψ; second, for two sets of formulae X and Y , if X = Y , then X ∼ = Y .

∈ A, if a ≈ a ′ , then ∀E ∈ Ext(F ), a ∈ E iff a ′ ∈ E.
Proof. To prove this result, we use the notion of complete labelling (Caminada, 2006a). Since arguments a and a ′ have the same sets of attackers, then for every complete labelling L we have L(a) = L(a ′ ). This means that for every complete extension E, it holds that a ∈ E if and only a ′ ∈ E. The proof follows from the fact that stable, preferred and grounded extensions are also complete extensions.

Property 36. Let (A, R) be an argumentation system s.t. R satisfies C1b and C2b. For all a, a ′ ∈ A, if a ≈ a ′ , then Status(a, F ) = Status(a ′ , F ).

Proof. Let x ∈ {c, p, s, g} and denote by Ext x (F ) the set of extensions under this semantics. From Property 33, we see that for all

E i ∈ Ext x (F ) it holds that a ∈ E i if and only if a ′ ∈ E i . Consequently, • for all E i ∈ Ext x (F ), a ∈ E i if and only if for all E i ∈ Ext x (F ), a ′ ∈ E i ; • for all E i ∈ Ext x (F ), a / ∈ E i if and only if for all E i ∈ Ext x (F ), a ′ / ∈ E i .
The proof now follows directly from these two observations. Property 37. Let F = (A, R), F ′ = (A ′ , R ′ ) be two argumentation systems built from the same logic (L, CN) such that R and R ′ satisfy C1b and C2b. If F ≡ E Q1b F ′ , then for all a ∈ A and for all a ′ ∈ A ′ , if a ≈ a ′ then Status(a, F ) = Status(a ′ , F ′ ).

Proof. Let x ∈ {c, p, s, g}. If F has no extensions under semantics x, then all the arguments of F and F ′ are rejected. In the rest of the proof we study the case Ext x (F ) = ∅. Let f be the bijection from EQ1b and let us prove that for every E ∈ Ext x (F ), a ∈ E if and only if a ′ ∈ f (E).

Let E ∈ Ext x (F ) and let a ∈ E. From EQ1b, we conclude that there exists a ′′ ∈ f (E) such that a ≈ a ′′ . Since ≈ is transitive, a ′ ≈ a ′′ . Thus, from Property 33, we have that a ′ ∈ f (E).

Let us now suppose that a ′ ∈ f (E) and prove that a ∈ E. From EQ1b, there exists a ′′′ ∈ E such that a ′ ≈ a ′′′ . From the transitivity of ≈, a ′′′ ≈ a. From Property 33, a ∈ E.

Thus, we see that for every extension E of F , we have that a ∈ E if and only if a ′ ∈ f (E). From this, we can conclude that:

• a ∈ E i ∈Ext x (F ) E i iff a ′ ∈ E ′ i ∈Ext x (F ′ ) E ′ i ; • a ∈ E i ∈Ext x (F ) E i iff a ′ ∈ E ′ i ∈Ext x (F ′ ) E ′ i ; • a / ∈ E i ∈Ext x (F ) E i iff a ′ / ∈ E ′ i ∈Ext x (F ′ ) E ′ i .
In other words, if a is sceptically accepted, a ′ is sceptically accepted, if a is credulously accepted, a ′ is credulously accepted and if a is rejected then a ′ is rejected.

Property 43. Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems. If F ′ is a core of F , then A ∼ A ′ .
Proof. The property follows directly from Definition 40.

Property 46. Let F = (A, R) be an argumentation system and F ′ = (A ′ , R ′ ) its core. If R satisfies C1b and C2b then:

• If a ∈ A ′ , then Status(a, F ) = Status(a, F ′ ); • If a / ∈ A ′ , then Status(a, F ) = Status(b, F ′ ) for some b ∈ A ′ with a ≈ b.
Proof.

• Property 51. Let (L, CN) be propositional logic and a finite knowledge base having at least one consistent formula. The set Arg( ) is infinite.

Proof. Let ϕ ∈ be a consistent formula and let without loss of generality ψ 1 , ψ 2 , . . . be the atoms not appearing in ϕ. Set Arg( ) contains all the following arguments: ({ϕ}, ϕ ∨ ψ 1 ), ({ϕ}, ϕ ∨ ψ 2 ), ({ϕ}, ϕ ∨ ψ 3 ), . . .. Thus, Arg( ) is infinite.

Lemma 60. For every k, F + k is finite. Proof. Clearly, each formula from F k offers finitely many occurrences to be replaced and there are finitely many substituting strings. Therefore, each formula from F k gives rise to finitely many formulas in F + k . Since F k is finite, it then follows that so is

F + k . Lemma 68. Let (A c , R c ) be a core of F ↓ = (A ↓ = Arg( ) ↓ , R ↓ = R(L)| A ↓ )
and let A 1 be an arbitrary set which contains A c , i.e., A c ⊆ A 1 ⊆ Arg( ). We define R 1 = R| A 1 , as expected, and F 1 = (A 1 , R 1 ). Let S 1 , . . . , S n be all the maximal consistent subsets of , and let

E 1 = Arg(S 1 ) ∩ A 1 , . . . , E n = Arg(S n ) ∩ A 1 . Then, Ext(F 1 ) = {E 1 , . . . , E n }.
Proof. We will first prove that for any maximal consistent subset S i of , the set

E i = Arg(S i )∩A 1 is a stable extension of F 1 . It is easy to see that if S i is consistent then Arg(S i ) is conflict-free. Let us prove that E i attacks any argument in A 1 \ E i . Let a ′ ∈ A 1 \ E i . Since a ′ / ∈ E i , then ∃h ∈ Supp(a ′ ) s.t. h / ∈ S i .
Since Supp(a ′ ) ⊆ and S i is a maximal consistent subset of , it follows that S i ∪ {h} is inconsistent. Then, there exists a minimal set C ⊆ S i s.t. C ∪ {h} is inconsistent. Let a = (C, ¬h).

Then, since a uses only atoms from (since h ∈ ) and since

(A c , R c ) is a core of F ↓ , it follows that ∃a 1 ∈ A c s.t. a 1 ≈ 1 a. Since Supp(a 1 ) ⊆ S i then a 1 ∈ E i . Also, a 1 R 1 a ′ . Hence, E i is a stable extension of F 1 .
We will now prove that for any E ′ ∈ Ext(F 1 ), there exists a maximal consistent subset of , denoted S ′ , s.t. E ′ = Arg(S ′ ) ∩ A 1 . To show this, we will show that: 1

) Base(E ′ ) is consistent; 2) Base(E ′ ) is a maximal consistent set in ; 3) E ′ = Arg(Base(E ′ )) ∩ A 1 .
(1) Let S ′ = Base(E ′ ). Suppose that S ′ is an inconsistent set and let C ⊆ S ′ be a minimal inconsistent subset of S ′ . Let C = { f 1 , . . . , f k }, and let us construct the following argument:

a = (C \ { f 1 }, ¬ f 1 ). Since E ′ is conflict-free, then a / ∈ E ′ and ∄a 1 ∈ E ′ s.t. a 1 ≈ 1 a. Since A c ⊆ A 1 , there exists an argument a 1 ∈ A 1 s.t. a 1 ≈ 1 a. This means that a 1 ∈ A 1 \ E ′ . Since E ′ is a stable extension, E ′ must attack a 1 . Formally, ∃a ′ ∈ E ′ s.t. a ′ R 1 a 1 . So, Conc(a ′ ) ≡ ¬ f 2 or Conc(a ′ ) ≡ ¬ f 3 , . . ., or Conc(a ′ ) ≡ ¬ f k . Without loss of generality, let Conc(a ′ ) ≡ ¬ f k . Since f k ∈ S ′ , there exists at least one argument a k in E ′ s.t. f k ∈ Supp(a k ).
Consequently, E ′ is not conflict-free, since a ′ attacks at least one argument in E ′ . Contradiction. Hence, it must be that S ′ is consistent.

(2) Let S ′ = Base(E ′ ) and suppose that S ′ is not a maximal consistent set in . According to

(1), S ′ is consistent, hence ∃ f ∈ \ S ′ s.t. S ′ ∪ { f } is consistent. Thus, for the argument b = ({ f }, f ), we have that ∃b 1 ∈ A 1 \ E ′ s.t. b 1 ≈ b, but no argument in E ′ attacks b 1 .
(This is since ¬ f cannot be inferred from S ′ ; consequently, no argument can be constructed from S ′ having its conclusion logically equivalent to ¬ f .) Contradiction. Hence it must be that S ′ is a maximal consistent set.

(3) It is easy to see that for any set of arguments E ′ , we have E ′ ⊆ Arg(Base(E ′ )). Since S ′ = Base(E ′ ) is a consistent set, then the set of arguments Arg(Base(E ′ )) ∩ A 1 must be conflict-free. From the fact that E ′ is a stable extension of F 1 , we conclude that the case E ′ Arg(Base(E ′ )) ∩ A 1 is not possible (since every stable extension is a maximal conflict-free set).

We will now show that if S, S ′ are two different maximal consistent subsets of , E = Arg(S) ∩ A 1 and E ′ = Arg(S ′ ) ∩ A 1 , then E = E ′ . Without loss of generality, let f ∈ S \ S ′ . Let a f ∈ A 1 be an argument s.t. Supp(a f ) = { f } and Conc(a f ) ≡ f . Such an argument must exist since A 1 contains A c , and

(A c , R c ) is a core of F ↓ . It is clear that a ∈ E \ E ′ , which shows that E = E ′ .
Theorem 29. Let F and F ′ be two argumentation systems built on the same logic (L, CN). Table 1 summarises the dependencies (F ≡ x F ′ ) ⇒ (F ≡ x ′ F ′ ) under any of the reviewed semantics.

Proof. Throughout the proof, we use notation F = (A, R) and F ′ = (A ′ , R ′ ). We suppose any of the semantics from Definition 7.

First, note that EQ1 implies all the other criteria.

Let us now show that EQ1b implies EQ3b. Let a ∈ Cr(F ). Let us prove that ∃a ′ ∈ Cr(F ′ ) s.t. a ≈ a ′ . Since a ∈ Cr(F ) then ∃E ∈ Ext(F ) s.t. a ∈ E. Let f be a bijection from EQ1b and let E ′ = f (E). From EQ1b, E ∼ E ′ , thus ∃a ′ ∈ E ′ s.t. a ≈ a ′ . This means that ∀a ∈ Cr(F ), ∃a ′ ∈ Cr(F ′ ) such that a ≈ a ′ . To prove that ∀a ′ ∈ Cr(F ′ ), ∃a ∈ Cr(F ) such that a ≈ a ′ is similar. Thus, Cr(F ) ∼ Cr(F ′ ).

Let us now show that EQ3b implies EQ5b. Let Cr(F ) ∼ Cr(F ′ ) and let ϕ ∈ Output cr (F ). Thus, there exists a ∈ Cr(F ) such that ϕ = Conc(a). From Cr(F ) ∼ Cr(F ′ ), we conclude that there exists a ′ ∈ Cr(F ′ ) such that a ≈ a ′ . Thus, there exists ϕ ′ ∈ Output cr (F ) such that ϕ ≡ ϕ ′ . Another direction of the implication is symmetric. Thus, we conclude that EQ3b implies EQ5b.

Since EQ1b implies EQ3b and EQ3b implies EQ5b, it follows that EQ1b implies EQ5b. Let us prove that EQ1b implies EQ6b. Suppose that EQ1b hold and let f be the bijection from this criterion. Let S ∈ Bases(F ) and let E ∈ Ext(F ) be an extension such that S = Base(E). Denote E ′ = f (E) and S ′ = Base(E ′ ). Since E ∼ E ′ , it follows that S ∼ = S ′ . Thus, EQ1b implies EQ6b.

From Property 25, we see that EQ2 implies EQ2b. Let us show that EQ2 implies EQ4. Since Output sc (F ) = {Conc(a)|a ∈ Sc(F )}, we conclude that Sc(F ) = Sc(F ′ ) implies Output sc (F ) = Output sc (F ′ ). In other words, EQ2 implies EQ4.

Since EQ2 implies EQ4 and EQ4 implies EQ4b (Property 25), it follows that EQ2 implies EQ4b. Let us prove that EQ2b implies EQ4b. Let ϕ ∈ Output sc (F ). Thus, there exists a ∈ Sc(F ), such that Conc(a) = ϕ. From EQ2b it follows that there exists ϕ ′ ∈ Output sc (F ′ ) such that ϕ ≡ ϕ ′ .

Consequently, there exists a ′ ∈ Sc(F ′ ) such that Conc(a ′ ) = ϕ ′ . This means that Output sc (F ) ∼ = Output sc (F ′ ). Hence EQ2b implies EQ4b.

From Property 25, EQ3 implies EQ3b.

Let us show that EQ3 implies EQ5. Since Output cr (F ) = {Conc(a)|a ∈ Cr(F )}, it follows that Cr(F ) = Cr(F ′ ) implies Output cr (F ) = Output cr (F ′ ). Hence EQ3 implies EQ5.

Since EQ3 implies EQ5 and EQ5 implies EQ5b (Property 25), it follows that EQ3 implies EQ5b. Note that we have already seen that EQ3b implies EQ5b. That EQ4 implies EQ4b, EQ5 implies EQ5b and EQ6 implies EQ6b is shown by Property 25.

Theorem 32. The links between the twelve equivalence criteria under grounded semantics are summarised in Table 2.

Proof. Note that we only need to prove the links that do not exist in Theorem 27. Also, note that there is always exactly one extension, thus EQ1 coincides with EQ2 and EQ3. For the same reason, EQ1b coincides with EQ2b and EQ3b. EQ1b implies EQ2b since there is exactly one extension. Since EQ2b implies EQ4b in the general case, it follows that EQ1b also implies EQ4b. Since EQ2 coincides with EQ1 and EQ1 implies all the other criteria, it follows that EQ2 also implies all the other criteria. As already mentioned, EQ2b is equivalent to EQ1b. The same holds for EQ2b and EQ3b. It is also easy to see that EQ2b implies EQ5b and EQ6b (since there is exactly one extension). EQ4 coincides with EQ5 for the above-mentioned reason (that there is exactly one extension). The same applies to EQ4b and EQ5b.

Theorem 38. Let F = (A, R), F ′ = (A ′ , R ′ ) be two argumentation systems built from the same logic (L, CN), R and R ′ satisfy C1b and C2b. If F ≡ E Q1b F ′ , then F ≡ x F ′ with x ∈ {E Q2b, E Q4b}.

Proof. Suppose that the two systems are equivalent with respect to EQ1b and let us prove that EQ2b is satisfied. If Ext(F ) = ∅, then from EQ1b, Ext(F ′ ) = ∅. In this case, EQ2b trivially holds, since Sc(F ) = Sc(F ′ ) = ∅. Else, let Ext(F ) = ∅.

Let Sc(F ) = ∅ and let us prove that Sc(F ′ ) = ∅. By means of contradiction, suppose the contrary and let a ′ ∈ Sc(F ′ ). Let E ′ ∈ Ext(F ′ ). Argument a ′ is sceptically accepted, thus a ′ ∈ E ′ . Let f be a bijection from EQ1b and let us denote E = f -1 (E ′ ). From F ≡ E Q1b F ′ , we obtain E ∈ Ext(F ). Furthermore, E ∼ E ′ , and, consequently, there exists a ∈ E s.t. a ≈ a ′ . Property 35 implies that a is sceptically accepted in F , contradiction.

Let Sc(F ) = ∅ and let us prove that Sc(F ) ∼ Sc(F ′ ). Let a ∈ Sc(F ). Since F ≡ E Q1b F ′ and since a is in at least one extension, then there exists a ′ ∈ A ′ s.t. a ′ ≈ a. Furthermore, Property 35 implies that a ′ is sceptically accepted in F ′ . Thus for all a ∈ Sc(F ) there exists a ′ ∈ Sc(F ′ ) such that a ′ ≈ a. The proof that for all a ′ ∈ Sc(F ′ ) there exists a ∈ Sc(F ) such that a ≈ a ′ is similar.

Since EQ2b implies EQ4b in the general case, as shown in Theorem 27, we can conclude that F and F ′ must also be equivalent with respect to EQ4b.

Theorem 39. Let (A, R) be an argumentation system built over . If is finite and R satisfies C2, then (A, R) has a finite number of extensions under all reviewed semantics. Proof. Let x ∈ {c, p, s, g} and let S 1 , . . . , S n ⊆ be all the consistent subsets of . We will use the notation A i = {a ∈ A|Supp(a) = S i }, with i ∈ {1, . . . , n}. (Note that some of the sets in A 1 , . . . , A n may be empty, but that is not important for the proof.) Let us prove that for every E ∈ Ext x (F ), for every two arguments a, a ′ ∈ A i and a ′ , we have a ∈ E if and only if a ′ ∈ E. To prove this result, we rely on the notion of the complete labelling (Caminada, 2006a). Since a and a ′ are attacked by the same arguments, they have the same labels. Thus for every complete extension E ∈ Ext c (F ), we have a ∈ E if and only if a ′ ∈ E. Since every stable, preferred and grounded extension is a complete one, we can conclude that for every E ∈ Ext x (F ) we have that a ∈ E if and only if a ′ ∈ E. This means that for every i ∈ {1, . . . , n}, for every extension E ∈ Ext x (F ), we have that E either contains all elements of A i or none of them. Formally, ∀E ∈ Ext(F ), ∀i ∈ {1, . . . , n}, we have E ∩ A i = A i or E ∩ A i = ∅. Consequently, there are at most 2 n different extensions.

Theorem 54 .

 54 For every propositional knowledge base , it holds that |Arg( ) ↓ / ≈ | ≤ 2 n • 2 2 m , where n = | | and m = |Atoms( )|.

Property 34 .

 34 Let (A, R) be an argumentation system s.t. R satisfies C1b and C2b. For all a, a ′ , b, b ′ ∈ A, (a ≈ a ′ and b ≈ b ′ ) implies (aRb iff a ′ Rb ′ ). Proof. Let a ≈ a ′ and b ≈ b ′ and let aRb. Since Supp(b) ∼ = Supp(b ′ ) then from C2b we have aRb ′ . From C1b and Conc(a) ≡ Conc(a ′ ), we obtain a ′ Rb ′ . To show that a ′ Rb ′ implies aRb is similar.Property 35. Let (A, R) be an argumentation system s.t. R satisfies C2b. For all a, a ′

  From Theorem 42, F ≡ E Q1b F ′ . From Property 35, Status(a, F ) = Status(a, F ′ ). • From the first part of the property, Status(b, F ) = Status(b, F ′ ). Let us show that Status(a, F ) = Status(b, F ). Since a ≈ b and R satisfies C1b and C2b, then a and b are attacked by the same arguments. This means that for every complete labelling L Caminada (2006a), it holds that L(a) = L(b). Since stable, preferred and grounded extensions are complete extensions, Status(a, F ) = Status(b, F ) with respect to any of those semantics. Thus, Status(a, F ) = Status(b, F ′ ).

Theorem 40 .

 40 Let F = (A, R) and F ′ = (A ′ , R ′ ) be two argumentation systems s.t. A, A ′ ⊆ Arg(L) and R = R L | A , R ′ = R L | A ′ . If R L satisfies C1b and C2b and A ∼ A ′ , then F ≡ E Q1b F ′ .

Table 1 .

 1 Links between criteria under any of the reviewed semantics.

	EQi/EQj EQ1 EQ1b EQ2 EQ2b EQ3 EQ3b EQ4 EQ4b EQ5 EQ5b EQ6 EQ6b
	EQ1	+	+	+	+	+	+	+	+	+	+	+	+
	EQ1b		+				+				+		+
	EQ2			+	+			+	+
	EQ2b				+				+
	EQ3					+	+			+	+
	EQ3b						+				+
	EQ4							+	+
	EQ4b								+
	EQ5									+	+
	EQ5b										+
	EQ6											+	+
	EQ6b												+

Table 2 .

 2 Links between criteria under grounded semantics.

	EQi/EQj EQ1 EQ1b EQ2 EQ2b EQ3 EQ3b EQ4 EQ4b EQ5 EQ5b EQ6 EQ6b
	EQ1	+	+	+	+	+	+	+	+	+	+	+	+
	EQ1b		+		+		+		+		+		+
	EQ2	+	+	+	+	+	+	+	+	+	+	+	+
	EQ2b		+		+		+		+		+		+
	EQ3	+	+	+	+	+	+	+	+	+	+	+	+
	EQ3b		+		+		+		+		+		+
	EQ4							+	+	+	+
	EQ4b								+		+
	EQ5							+	+	+	+
	EQ5b								+		+
	EQ6											+	+
	EQ6b												+

Appendix

Property 19. Each criterion ≈ i is an equivalence relation (with i ∈ {1, 2, 3}).

Proof. The three relations are reflexive since relations ∼ =, ≡ and = are reflexive, they are symmetric since ∼ =, ≡ and = are symmetric and they are transitive since ∼ =, ≡ and = are transitive.

Property 20. Let a, a ′ ∈ Arg(L).

Proof. The claim follows from the fact that for every two sets of formulae X and Y , it holds that X = Y implies X ∼ = Y and X ≡ Y .

Property 26. For two argumentation systems F and F ′ , if F ≡ E Qi F ′ then F ≡ E Qib F ′ with i ∈ {1, . . . , 6}.

Proof. The property follows from the observations that for every pair of sets of arguments E, E ′ , we know that E = E ′ implies E ∼ E ′ and that for every pair of sets of formulae X , Y , it holds that X = Y implies X ∼ = Y . Property 27. For all i ∈ {1, . . . , 6}, the criterion E Qi (resp. E Qib) is an equivalence relation.

Proof. The result follows from the elementary properties of bijections, together with the fact that both ∼ and ∼ = are equivalence relations.

We see that the image of this function is Ext x (F ′ ) and that f is a bijection between Ext x (F ) and Ext x (F ′ ) satisfying EQ1b.

Proof. The result is obtained by applying Theorem 38 to F and F ′ .

Theorem 48. Let F = (A, R) be an argumentation system built over a knowledge base (i.e., A ⊆ Arg( )). If Cncs( )/ ≡ is finite, then every core of F is finite.

Proof. Let F ′ = (A ′ , R ′ ) be a core of F and let us prove that F ′ is finite. Since is finite, it follows that {Supp(a)|a ∈ A ′ } must be finite. If for all H ∈ {Supp(a)|a ∈ A ′ }, the set {a ∈ A ′ |Supp(a) = H } is finite, then the set A ′ is clearly finite. Else, there exists

This implies that there are infinitely many different formulae having pairwise non-equivalent conclusions in Cncs( ), formally, the set Cncs( )/ ≡ is infinite, contradiction. This means that for every

Theorem 54. Let F = (Arg( ), R as ) be an argumentation system built over a propositional knowledge base , and

Proof. Let S 1 , . . . , S n be all the maximal consistent subsets of . Since (Arg( ) ↓ , R ↓ ) and (Arg( ), R) both contain at least one core of (Arg( ) ↓ , R ↓ ) (in fact, they both contain all cores of this set), Lemma 68 implies that extensions of (Arg( ), R) are exactly Arg(S i ), and extensions of (Arg( ) ↓ , R ↓ ) are exactly Arg(S i ) ∩ Arg( ) ↓ , when 1 ≤ i ≤ n. Thus, the two frameworks have the same number of extensions and any argument of Arg( ) ↓ is in the same number of extensions in them. Consequently, its status must be the same in both frameworks. Proof. There are at most 2 n different supports of arguments. It is well known that there are at most 2 2 m logically non-equivalent Boolean functions of m variables. Thus, for any support H , there are at most 2 2 m different non-equivalent arguments, where m is the number of different atoms in .

Theorem 57. Let be a propositional knowledge base and F = (A, R as ) be an argumentation system such that A ⊆ Arg( ) ↓ . Then every core of F is finite.

Proof. Follows directly from Theorem 54 and Definition 40.

Theorem 59. Let F be an argumentation system built over a propositional knowledge base using stable semantics and let G be one of its cores.

Since a is an argument, H is consistent and no formula in H can be deduced from other formulae in H . Thus, a ′ = (H, f 1 ∧ . . . ∧ f k ) must also be an argument. Note that its conclusion only contains atoms from , thus a ′ ∈ A ′ . Consequently, there must exist an argument a g ∈ A g s.t. a g ≈ 1 a ′ . G is a core of F ′ , thus they are equivalent w.r.t. EQ1b (Theorem 42). Since equivalent arguments have the same status in equivalent frameworks (Property 35), a g is sceptically accepted in G. So,

⇐ Let f be a propositional formula that can be deduced from Output sc (G). Let S 1 , . . . , S n be all the maximal consistent subsets of . According to Lemma 68, ∃a ∈ A g s.t. Supp(a) ⊆ S 1 ∩ . . . ∩ S n and Conc(a) = f . Let us denote H = Supp(a). Obviously, H ⊢ f . Furthermore, H ⊆ S 1 ∩ . . . ∩ S n . From these two facts, we conclude that there must exist an argument a ′ ∈ Arg( ) s.t. Supp(a ′ ) ⊆ H and Conc(a ′ ) = f . From Lemma 68, a ′ is sceptically accepted in F . Thus, f ∈ Output sc (F ).

Theorem 61. For every formula α ∈ L , there exists σ ∈ F + k s.t. CN(α) = CN(σ ). Proof. By induction on the structure of formulas from L . Base step. If α is an atomic formula, then α ∈ F + k . Induction step. Induction hypothesis.Assume that for each formula λ ∈ L of depth less than n there exists µ ∈ F + k such that CN(λ) = CN(µ). Consider α ∈ L whose depth is less than n +1, i.e., α is of the form o i (γ 1 , . . . , γ n i ) where every γ h is of depth less than n. By the induction hypothesis, there exist γ

There exists an absorption law that applies here because every γ ′ h is in

Theorem 65. Theorem 63 Let F = (A, R) be an argumentation system built over a knowledge base such that R satisfies C1b and C2b. If F contains a core of G = (Arg(Base(A)), R(L)| Arg(Base(A)) ), then for all E ⊆ Arg(Base(A)),

Supp(a) ≈ Supp(e).

Proof.

We will first show that H is a core of both F and F ′ . Let us first show that H is a core of F . We will show that all conditions of Definition 40 are verified.

• We have already seen why A

Thus, H is a core of F . Let us now show that H is also a core of F ′ .

We have shown that H is a core of F and of F ′ . From Theorem 42, F ≡ E Q11 H and

Let e ∈ A ′ \ A and let a ∈ A be an argument such that Supp(a) ≈ Supp(e). Since a and e are attacked by the same arguments, they are in the same complete labellings. (Caminada, 2006a); thus they are in the same extensions. Consequently, they have the same status: Status(e, F ′ ) = Status(a, F ′ ). Since we have seen that Status(a, F ′ ) = Status(a, F ), it follows that Status(e, F ′ ) = Status(a, F ).

Theorem 66. Let F = (A, R) be an argumentation system built over a knowledge base and let E ⊆ A. If F ⊖ E contains a core of G = (Arg(Base(A)), R(L)| Arg(Base(A)) ), then:

Proof. This result is a consequence of Theorem 63.