You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Strong admissibility revisited: Theory and applications

Abstract

In the current paper, we re-examine the concept of strong admissibility, as was originally introduced by Baroni and Giacomin. We examine the formal properties of strong admissibility, both in its extension-based and in its labelling-based form, and analyse the computational complexity of the relevant decision problems. Moreover, we show that strong admissibility plays a vital role in discussion-based proof procedures for grounded semantics. In particular it allows one to compare the performance of alternative dialectical proof procedures for grounded semantics, and obtain some remarkable differences between the Standard Grounded Game and the Grounded Discussion Game.

1.Introduction

Admissibility is generally seen as one of the cornerstones of abstract argumentation theory [19], as it is the basis of various argumentation semantics [1]. Not only does admissibility appeal to common intuitions [5], it is also one of the key requirements for obtaining a consistent outcome of instantiated argumentation formalisms [13,22,25].

Slightly less well-known is the principle of strong admissibility, which was originally introduced in [3]. The original aim of strong admissibility was to characterise the unique properties of the grounded extension. It turns out, however, that the concept is also useful for comparing the characteristics of the different dialectical proof procedures that have been stated in the literature. In particular, the Standard Grounded Game [21,26] and the Grounded Discussion Game [11] prove membership of the grounded extension essentially by constructing a strongly admissible labelling where the argument in question is labelled in. However, as we will see, the Grounded Discussion Game is able to do so in a more efficient way, requiring a number of steps that is linearly related to the in/out-size of the strongly admissible labelling,1 whereas the Standard Grounded Game can require a number of steps that is exponentially related to the in/out-size of the strongly admissible labelling.

The remaining part of the current paper is structured as follows. First, in Section 2 we briefly summarise some of the key concepts of abstract argumentation theory, both in its extension and in its labelling based form. In Section 3, we then discuss the extension based version of strong admissibility and examine its formal properties. In Section 4 we introduce the labelling based version of strong admissibility and show how it relates to its extension based version. In Section 5 we examine the computational complexity of some of the decision problems related to strong admissibility. In Section 6 we then re-examine the Standard Grounded Game, and the Grounded Persuasion Game, and show that strong admissibility plays a vital role in describing the relative efficiency of these games. In Section 7 we then round off with a discussion of our results and some open research issues.2

2.Formal preliminaries

In the current section, we briefly restate some of the key concepts of abstract argumentation theory, in both its extension based and labelling based form.

Definition 1.

An argumentation framework is a pair (Ar,att) where Ar is a finite set of entities, called arguments, whose internal structure can be left unspecified, and att a binary relation on Ar. For any A,BAr we say that A attacks B iff (A,B)att.

Definition 2.

Let (Ar,att) be an argumentation framework, AAr and ArgsAr. We define A+ as {BArA attacks B}, A as {BArB attacks A}, Args+ as {A+AArgs}, and Args as {AAArgs}. Args is said to be conflict-free iff ArgsArgs+=. Args is said to defend A iff AArgs+. The characteristic function F:2Ar2Ar is defined as F(Args)={AArgs defends A}.

Definition 3.

Let (Ar,att) be an argumentation framework. ArgsAr is said to be:

  • an admissible set iff Args is conflict-free and ArgsF(Args)

  • a complete extension iff Args is conflict-free and Args=F(Args)

  • a grounded extension iff Args is the smallest (w.r.t. ⊆) complete extension

  • a preferred extension iff Args is a maximal (w.r.t. ⊆) complete extension

If Args is a conflict-free set, then its down-admissible set (written as Args) is defined as the (unique) biggest (w.r.t. ⊆) admissible subset of Args.3

The above definitions essentially follow the extension based approach of [19].4 It is also possible to define the key argumentation concepts in terms of argument labellings [8 ,15].

Definition 4.

Let (Ar,att) be an argumentation framework. An argument labelling is a partial function Lab:Ar{in,out,undec}. An argument labelling is called an admissible labelling iff Lab is a total function and for each AAr it holds that:

  • if Lab(A)=in then for each B that attacks A it holds that Lab(B)=out

  • if Lab(A)=out then there exists a B that attacks A such that Lab(B)=in

Lab is called a complete labelling iff it is an admissible labelling and for each AAr it also holds that:
  • if Lab(A)=undec then there is a B that attacks A such that Lab(B)=undec, and for each B that attacks A such that Lab(B)undec it holds that Lab(B)=out

As a labelling is essentially a function, we sometimes write it as a set of pairs. Also, if Lab is a labelling, we write in(Lab) for {AArLab(A)=in}, out(Lab) for {AArLab(A)=out} and undec(Lab) for {AArLab(A)=undec}. As a labelling is also a partition of the arguments into sets of in-labelled arguments, out-labelled arguments and undec-labelled arguments, we sometimes write it as a triplet (in(Lab),out(Lab),undec(Lab)).

Definition 5

Definition 5([16]).

Let Lab and Lab be argument labellings of argumentation framework (Ar,att). We say that LabLab iff in(Lab)in(Lab) and out(Lab)out(Lab). LabLab is defined as (in(Lab)in(Lab),out(Lab)out(Lab),Ar((in(Lab)in(Lab))(out(Lab)out(Lab)))). LabLab is defined as ((in(Lab)out(Lab))(in(Lab)out(Lab)),(out(Lab)in(Lab))(out(Lab)in(Lab)),(in(Lab)out(Lab)(out(Lab)in(Lab))(undec(Lab)undec(Lab)))).

We say that Lab1 is a sublabelling of Lab2 (or alternatively, that Lab2 is a superlabelling of Lab2) iff Lab1Lab2. If Lab is a total labelling (i.e. a total function), then its down-admissible labelling [16] (written as Lab) is defined as the (unique) biggest (w.r.t. ⊑) admissible sublabelling of Lab.

Definition 6.

Let Lab be a complete labelling of argumentation framework (Ar,att). Lab is said to be

  • a grounded labelling iff Lab is the (unique) smallest (w.r.t. ⊑) complete labelling

  • a preferred labelling iff Lab is a maximal (w.r.t. ⊑) complete labelling

Given an argumentation framework (Ar,att) we define two functions Args2Lab and Lab2Args (to translate a conflict-free set of arguments to an argument labelling, and to translate an argument labelling to a set of arguments, respectively) such that Args2Lab(Args)=(Args,Args+,Ar(ArgsArgs+)) and Lab2Args(Lab)=in(Lab). It has been proven [15] that if Args is an admissible set (resp. a complete, grounded or preferred extension) then Args2Lab(Args) is an admissible labelling (resp. a complete, grounded or preferred labelling), and that if Lab is an admissible labelling (resp. a complete, grounded or preferred labelling) then Lab2Args(Lab) is an admissible set (resp. a complete, grounded or preferred extension). Moreover, when the domain and range of Args2Lab and Lab2Args are restricted to complete extensions and complete labellings they become injective functions and each other’s reverses, which implies that the complete extensions (resp. the grounded extension and the preferred extensions) and the complete labellings (resp. the grounded labelling and the preferred labellings) are one-to-one related [15].

3.Strongly admissible sets

The concept of strong admissibility was first introduced by Baroni and Giacomin [3], using the notion of strong defence.

Definition 7

Definition 7([3]).

Let (Ar,att) be an argumentation framework, AAr and ArgsAr be a set of arguments. A is strongly defended by Args iff each attacker BAr of A is attacked by some CArgs{A} such that C is strongly defended by Args{A}.

Baroni and Giacomin say that a set Args satisfies the strong admissibility property iff it strongly defends each of its arguments [3]. However, it is also possible to define strong admissibility without having to refer to strong defence.

Definition 8.

Let (Ar,att) be an argumentation framework. ArgsAr is strongly admissible iff every AArgs is defended by some ArgsArgs{A} which in its turn is again strongly admissible.

To illustrate the concept of strong admissibility, consider the argumentation framework of Fig. 1. Here, the strongly admissible sets are , {A}, {A,C}, {A,C,F}, {D}, {A,D}, {A,C,D}, {D,F}, {A,D,F} and {A,C,D,F}, the latter also being the grounded extension. As an example, the set {A,C,F} is strongly admissible as A is defended by , C is defended by {A} and F is defended by {A,C}, each of which is a strongly admissible subset of {A,C,F} not containing the argument it defends. Please notice that although the set {A,F} defends argument C in {A,C,F}, it is in its turn not strongly admissible (unlike {A}). Hence the requirement in Definition 8 for Args to be a subset of Args{A}. We also observe that although {C,H} is an admissible set, it is not a strongly admissible set, since no subset of {C,H}{H} defends H.

Fig. 1.

An example of an argumentation framework.

An example of an argumentation framework.

It can be proved that a set is strongly admissible (in the sense of Definition 8) iff it strongly defends each of its arguments (in the sense of Definition 7). In order to do so, we need the following two lemmas.

Lemma 1.

Let AAr and Args1,Args2Ar such that AArgs1 and Args1Args2. If A is strongly defended by Args1 then A is also strongly defended by Args2.

Proof.

By induction over the number of arguments in Args2. Let i=|Args2|.

basis

For i=1 it holds that |Args2|=1, which together with AArgs1 and Args1Args2 implies that Args1=Args2={A}. From Args1=Args2 it trivially holds that if A is strongly defended by Args1 then A is also strongly defended by Args2.

step

Suppose the lemma holds for some i1. We now prove it also holds for i+1. Let A be strongly defended by Args1. We need to prove that A is also strongly defended by Args2 with |Args2|=i+1. According to Definition 7 this would be the case if each attacker BAr of A is attacked by some CArgs2{A} such that C is strongly defended by Args2{A}. The fact that A is strongly defended by Args1 means that each attacker BAr of A is attacked by some CArgs1{A}. From the fact that Args1Args2 it follows that Args1{A}Args2{A} so CArgs2{A}. We now need to prove that C is strongly defended by Args2{A}. From the fact that |Args2{A}|=i we can apply the induction hypothesis to obtain that if C is strongly defended by Args1{A} (which it is) C is also strongly defended by Args2{A}. □

Lemma 2.

Let ArgsAr. Let H0= and Hi+1=F(Hi)Args (i0). For each i0 it holds that

  • (1) HiHi+1

  • (2) Hi is strongly admissible

  • (3) Hi strongly defends each of its arguments

Proof.

  • (1) Proof by induction over i.

    basis

    For i=0 it holds that HiHi+1 because H0=H1.

    step

    Suppose that for some i0 it holds that HiHi+1. From the fact that F is a monotonic function, it follows that F(Hi)F(Hi+1), from which it follows that F(Hi)ArgsF(Hi+1)Args. That is, Hi+1Hi+2.

  • (2) Proof by induction over i.

    basis

    For i=0 it holds that Hi=H0= which is trivially strongly admissible.

    step

    Suppose that for each i0 it holds that each Hj (ji) is strongly admissible. We now prove that Hi+1 is also strongly admissible. Let AHi+1. That is, AF(Hi)Args. Let j be the smallest number such that AHj (this implies that ji+1 and AHj1). The fact that AHj means that AF(Hj1)Args, so A is defended by Hj1. From point 1 above, it follows that Hj1Hi+1, which together with the fact that AHj1 implies that Hj1Hi+1{A}. This, together with the fact that Hj1 is strongly admissible (induction hypothesis), means the conditions of Definition 8 (take Hj1 for Args) are satisfied.

  • (3) Proof by induction over i.

    basis

    For i=0 it holds that Hi=H0= which trivially strongly defends each of its arguments.

    step

    Suppose that for some i0 it holds that each Hj (ji) strongly defends each of its arguments. We now prove that Hi+1 also strongly defends each of its arguments. Let AHi+1. Let j be the smallest number such that AHj (this implies that ji+1 and AHj1). From AHj it follows that AF(Hj1)Args, so each attacker B of A is attacked by some CHj1 such that C is strongly defended by Hj1 (induction hypothesis). From point 1 above, it follows that Hj1Hi+1, which together with AHj1 implies that Hj1Hi+1{A}. So from the fact that each attacker B of A is attacked by some CHj1 such that C is strongly defended by Hj1, it follows that each attacker B of A is attacked by some CHi+1 (as Hj1Hi+1) such that C is strongly defended by Hi+1{A} (Lemma 1, together with Hj1Hi+1{A}). □

Theorem 1.

Let ArgsAr and let Hi (i0) be as in Lemma 2. Args is strongly admissible iff i=0Hi=Args.

Proof.

“⇒”:

Suppose Args is strongly admissible. We need to show that

  • (1) i=0HiArgs. This follows directly from the definition of H0 and Hi+1.

  • (2) Argsi=0Hi. Let Args1=Args. Suppose towards a contradiction that Args1i=0Hi.

    This means there is an A1Args1 such that A1i=0Hi. The fact that Args1 is strongly admissible implies that A1 is defended by some Args2Args1{A1} which in its turn is again strongly admissible. Can it be the case that Args2i=0Hi? If so, there must be an i such that Args2Hi. But as Args2 defends A1, it would follow that A1F(Hi), which together with the fact that A1Args implies that A1F(Hi)Args, so A1Hi+1 so A1i=0Hi. Contradiction. So Args2i=0Hi.

    This means there is an A2Args2 such that A2i=0Hi. The fact that Args2 is strongly admissible implies that A2 is defended by some Args3Args2{A2} which in its turn is again strongly admissible. Can it be the case that Args3i=0Hi? If so, there must be an i such that Args3Hi. But as Args3 defends A2, it would follow that A2F(Hi) which together with the fact that A2Args implies that A2F(Hi)Args, so A2Hi+1 so A2i=0Hi. Contradiction. So Args3i=1Hi.

    Using similar reasoning as in the above two paragraphs, we observe that there exists a sequence Args1,Args2,,Argsn and a sequence A1,A2,,An where

    • (a) for each j{1n1} Argsj+1Argsj (because Argsj+1Argsj{Aj})

    • (b) for each j{1n} Argsji=0Hi

    • (c) Args1=Args

    • (d) Argsn= (because Args1=Args is finite, and we lose at least one argument when going from Argsj to Argsj+1 as shown in point 2a)

    From 2b and 2d it follows that Argsn=i=0Hi. Contradiction. Therefore Argsi=0Hi.

“⇐”:

Suppose i=0Hi=Args. Lemma 2 states that each Hi (i0) is strongly admissible. Therefore i=0Hi is also strongly admissible. As i=0Hi=Args it directly follows that Args is strongly admissible. □

Theorem 2.

Let ArgsAr and let Hi (i1) be as in Lemma 2. Args strongly defends each of its arguments iff i=0Hi=Args.

Proof.

“⇒”:

Suppose Args strongly defends each of its arguments. We need to show that

  • (1) i=0HiArgs. This follows directly from the definition of H0 and Hi+1.

  • (2) Argsi=0Hi. Suppose towards a contradiction that Argsi=0Hi. This means there is an A1Args such that A1i=0Hi. As Args strongly defends each of its arguments, Args strongly defends A1.

    The fact that Args strongly defends A1 means that each attacker B1 of A1 is attacked by some A2Args{A1} such that A2 is strongly defended by Args{A1}. If each such A2 were an element of i=0Hi (so of some Hj) then A1 would be defended by Hj, so A1Hj+1, so A1i=0Hi. Therefore, A2i=0Hi for at least one A2Args{A1}.

    The fact that Args{A1} strongly defends A2 means that each attacker B2 of A2 is attacked by some A3Args{A1,A2} such that A3 is strongly defended by Args{A1,A2}. If each such A3 were an element of i=0Hi (so of some Hj) then A2 would be defended by Hj, so A2Hj+1, so A2i=0Hi. Therefore, A3i=0Hi for at least one A3Args{A1,A2}.

    Using similar reasoning as in the above two paragraphs, one can identify an infinite sequence of different arguments A1,A2,A3, such that for each Ai (i1) it holds that AiArgs{A1Ai1}. However, since Args contains only a finite number of arguments, this cannot be the case. Contradiction.

“⇐”:

Suppose that i=0Hi=Args. Lemma 2 states that each Hi (i0) strongly defends each of its arguments. Therefore i=0Hi strongly defends each of its arguments. As i=0Hi=Args it directly follows that Args strongly defends each of its arguments. □

Theorem 3.

Let (Ar,att) be an argumentation framework and ArgsAr. Args is a strongly admissible set (in the sense of Definition 8) iff each AArgs is strongly defended by Args (in the sense of Definition 7).

Proof.

This follows directly from Theorem 1 and Theorem 2. □

Now that the equivalence between the two ways of defining strongly admissible sets has been proven, the next step is to examine some of the formal properties of strong admissibility. We start with conflict-freeness and admissibility.

Theorem 4.

Let (Ar,att) be an argumentation framework and let ArgsAr be a strongly admissible set. It holds that:

  • Args is conflict-free

  • Args is admissible

Proof.

Conflict-freeness follows from [3, Proposition 51], together with Theorem 3. Admissibility follows from conflict-freeness, together with the fact that every strongly admissible set defends each of its arguments. □

Baroni and Giacomin prove that the grounded extension is the unique biggest (w.r.t. ⊆) strongly admissible set [3].5 However, it can additionally be proved that the strongly admissible sets form a lattice, of which the grounded extension is the top element and the empty set is the bottom element. To do so, we need two lemmas.

Lemma 3.

If Args1 and Args2 are strongly admissible sets, then Args1Args2 is also a strongly admissible set.

Proof.

Let Args1 and Args2 be strongly admissible sets. Let AArgs1Args2. If AArgs1 then A is defended by some Args1Args1{A} which in its turn is strongly admissible. If AArgs2 then A is defended by some Args2Args2{A} which in its turn is strongly admissible. In both cases, we have that A is defended by some Args(Args1Args2){A} which in its turn is strongly admissible. Therefore, Args1Args2 is a strongly admissible set in the sense of Definition 8. □

Lemma 4.

Each admissible set has a unique biggest (w.r.t.) strongly admissible subset.

Proof.

We first observe that each admissible set Args has at least one strongly admissible subset: the empty set. As we consider only finite argumentation frameworks, this implies that there exists at least one maximal (w.r.t. ⊆) strongly admissible subset of Args. We now proceed to show that this maximal strongly admissible subset is unique. Let Args1 and Args2 be maximal strongly admissible subsets of Args. Now consider Args1Args2. From Lemma 3 it follows that this is again a strongly admissible set. From the fact that Args1 and Args2 are maximal strongly admissible subsets, it follows that if Args1Args1Args2 then Args1=Args1Args2, and that if Args2Args1Args2 then Args2=Args1Args2, so we obtain that Args1=Args1Args2 and Args2=Args1Args2 so Args1=Args2. □

If Args is an admissible set, we write Args for its biggest (w.r.t. ⊆) strongly admissible subset.

It turns out that the strongly admissible sets of an argumentation framework form a lattice.6

Theorem 5.

Let (Ar,att) be an argumentation framework. The strongly admissible sets of this framework form a lattice (w.r.t.).

Proof.

We need to prove that each two strongly admissible sets have a supremum (a least upper bound) and a infimum (a greatest lower bound).

supremum

Let Args1 and Args2 be two strongly admissible sets. From Lemma 3 it follows that Args1Args2 is again a strongly admissible set. Since, by definition, Args1Args1Args2 and Args2Args1Args2, it follows that Args1Args2 is an upper bound. Moreover, it is also a least upper bound, since any proper subset of Args1Args2 will not be a superset of Args1 and Args2.

infimum

Let Args1 and Args2 be two strongly admissible sets. Let Args3 be Args1Args2. From the fact that Args3 is conflict-free, it follows that it has a (unique) biggest admissible subset, which we will refer to as Args3. From Lemma 4 it follows that Args3 has a (unique) biggest strongly admissible subset, which we will refer to as Args3. We now prove that Args3 is an infimum of Args1 and Args2.

lower bound

From the fact that Args3Args3Args3=Args1Args2 it follows that Args3Args1 and Args3Args2.

greatest lower bound

Let Args3 be a strongly admissible admissible set such that Args3Args1 and Args3Args2. Then, by definition, Args3Args3. Since Args3 is admissible, it follows that Args3Args3 (since Args3 is the biggest admissible subset of Args3). Since Args3 is a strongly admissible subset of Args3 it follows that Args3Args3 (since Args3 is the biggest strongly admissible subset of Args3). □

Fig. 2.

The strongly admissible sets of the argumentation framework of Fig. 1.

The strongly admissible sets of the argumentation framework of Fig. 1.
Fig. 3.

The complete extensions of the argumentation framework of Fig. 1.

The complete extensions of the argumentation framework of Fig. 1.

In essence, if Args1 and Args2 are strongly admissible sets, then Args1Args2 is their supremum, and (Args1Args2) is their infimum. By forming a lattice, with the empty set as its bottom element and the grounded extension as its top element, the strongly admissible sets differ from the admissible sets, which form a semi-lattice with the empty set as its bottom element, and the preferred extensions as its top elements [19]. It also distinguishes the strongly admissible sets from the complete extensions, which form a semi-lattice with the grounded extension as its bottom element and the preferred extensions as its top elements [19].

As an example, a Hasse diagram of the strongly admissible sets of the argumentation framerwork of Fig. 1 is shown in Fig. 2. Notice that (as specified by Theorem 5) the strongly admissible sets form a lattice with the empty set as its bottom element and the grounded extension as its top element. A Hasse diagram of the complete extensions of the argumentation framework of Fig. 1 is shown in Fig. 3. Notice that (as indicated in [19]) the complete extensions form a semi-lattice with the grounded extension as its bottom element and the preferred extensions as its top elements.

4.Strongly admissible labellings

Argument labellings [8,15] have become a popular approach for purposes such as argumentation algorithms [9,21,23], argument-based judgment aggregation [16,17] and issues of measuring distance of opinion [6]. In the current section, we develop a labelling account of strong admissibility, which will subsequently be used to analyse some of the existing discussion games for grounded semantics.

To define a strongly admissible labelling, we first have to introduce the concept of a min–max numbering.7

Definition 9.

Let Lab be an admissible labelling of argumentation framework (Ar,att). A min–max numbering is a total function MMLab:in(Lab)out(Lab)N{} such that for each Ain(Lab)out(Lab) it holds that:

  • if Lab(A)=in then MMLab(A)=max({MMLab(B)B attacks A and Lab(B)=out})+1 (with max() defined as 0)

  • if Lab(A)=out then MMLab(A)=min({MMLab(B)B attacks A and Lab(B)=in})+1 (with min() defined as )

To illustrate the concept of a min–max numbering, consider again the argumentation framework of Fig. 1. Here, the admissible labelling Lab1=({A,C,F,G},{B,E,H},{D}) has min–max numbering {(A:1),(B:2),(C:3),(E:4),(F:5),(G:),(H:)}, and the admissible labelling Lab2=({A,C,D,F},{B,E},{G,H}) has min–max numbering {(A:1),(B:2),(C:3),(D:1),(E:2),(F:3)}.

Theorem 6.

Every admissible labelling has a unique min–max numbering.

Proof.

Let Lab be an admissible labelling, and let Args=Lab2Args(Lab). Now consider the sequence H0,H1,H2, as defined in Lemma 2. For each Ain(Lab) we define MMLab(A) as

2i1, where i is the lowest number such that AHiif i=0Hi contains Aif i=0Hi does not contain A
For each Aout(Lab) we define MMLab(A) as
2i, where i is the lowest number such that Hi attacks Aif i=0Hi attacks Aif i=0Hi does not attack A
We first prove that MMLab is a correct min–max numbering. For this, we need to prove the following two properties from Definition 9:
  • if Lab(A)=in then MMLab(A)=max({MMLab(B)B attacks A and Lab(B)=out})+1

    Let AAr such that Lab(A)=in. We distinguish two cases:

    • (1) Ai=0Hi

      In that case, MMLab(A)=2i1, where i is the lowest number such that AHi. We first observe that i1 (otherwise AHi=H0=). In case i=1 it holds that AF(H0)Args, so A is defended by so A does not have any attackers, so max(MMLab(B)B attacks A and Lab(B)=out})+1=0+1=1, which is indeed equal to 2i1 for i=1. In the remaining part of this proof we will therefore focus on the case where i2. In that case AF(Hi1)Args so A is defended by Hi1, which means that each B that attacks A is attacked by some CHi1, so Hi1 attacks B. As B is labelled out (as Lab is an admissible labelling) from the fact that Hi1 attacks B it follows that each out labelled attacker of A has a min–max number of at most 2(i1). However, the fact that AHi1 (as i is the lowest number such that AHi) implies that there exists at least one out labelled attacker of A with min–max number of exactly 2(i1). Therefore max({MMLab(B)B attacks A and Lab(B)=out})+1=2(i1)+1=2i1 so A is numbered correctly.

    • (2) Ai=0Hi

      In that case, MMLab(A)=. From the fact that Ai=0Hi it follows that AHi for any i1, which means that AF(Hi1)Args. As AArgs, it follows that AF(Hi1) for any i1. This means that there exists a B that attacks A and is not attacked by Hi1 (for any i). So B is not attacked by i=0Hi. It also holds that B is labelled out, as Lab is an admissible labelling. Hence, B is numbered . Therefore max({MMLab(B)B attacks A and Lab(B)=out})+1=+1= so A is numbered correctly.

  • if Lab(A)=out then MMLab(A)=min({MMLab(A)B attacks A and Lab(B)=in})+1

    Let AAr such that Lab(A)=out. We distinguish two cases:

    • (1) i=0Hi attacks A

      In that case, MMLab(A)=2i, where i is the lowest number such that Hi attacks A. We first observe that i1 (otherwise i=0 so Hi=H0= which would not be able to attack A). The fact that Hi attacks A means that there is some BHi that attacks A such that Lab(B)=in (as BArgs because Hi=F(Hi1)Args). From this, it follows that the min–max number of B is at most 2i1. The fact that Hi1 does not attack A (as i is the lowest number such that Hi attacks A) means there is no BHi1 that attacks A such that Lab(B)=in. Therefore, it follows that no in labelled attacker of A can have a min–max number of 2(i1)1=2i3 or lower, which together with the fact that the min–max number of any in labelled argument has to be odd means that any in labelled attacker of A has to be at least 2i1. This implies that the min–max number of B is precisely 2i1. We have therefore obtained that there is at least one in labelled attacker of A that is numbered 2i1, and that every in labelled attacker of A is numbered at least 2i1. Therefore, MMLab(A)=min({MMLab(A)B attacks A and Lab(B)=in})+1=(2i1)+1=2i so A is numbered correctly.

    • (2) i=0Hi does not attack A

      In that case, MMLab(A)=. From the fact that i=0Hi does not attack A it follows that for each attacker B of A it holds that Bi=0Hi. This implies that each in labelled attacker B of A has a min–max number of . Also, A has at least one such in labelled attacker (as Lab is an admissible labelling). Therefore MMLab(A)=min({MMLab(A)B attacks A and Lab(B)=in})+1= so A is numbered correctly.

Now that we have proved that each admissible labelling has a min–max numbering, the next thing to prove is that this min–max numbering is unique. Let MMLab1 and MMLab2 be two min–max numberings of the same admissible labelling Lab. We now prove, by strong induction over i1, that for each AAr, MMLab1=i iff MMLab2=i.

basis

i=1

“⇒”: Let MMLab1=1. This can only be the case if A is labelled in and does not have any attackers. This means that MMLab2 is also 1.

“⇐”: Similar to “⇒”.

step

Suppose that for each j{1i} it holds that MMLab1(A)=j iff MMLab2(A)=j.

“⇒”: Let MMLab1(A)=i+1. We distinguish two cases:

  • (1) Lab(A)=in. In that case, i+1=MMLab1(A)=max({MMLab1(B)B attacks A and Lab(B)=out})+1 so i=max({MMLab1(B)B attacks A and Lab(B)=out}). This implies that for each out labelled attacker B of A, it holds that MMLab1(B) is at most i. Hence, we can apply the induction hypothesis and infer that MMLab2(B)=MMLab1(B). Therefore, MMLab2(A)=max{MMLab2B attacks A and Lab(B)=out})+1=max{MMLab1B attacks A and Lab(B)=out}+1=i+1.

  • (2) Lab(A)=out. In that case i+1=MMLab1(A)=min({MMLab1(B)B attacks A and Lab(B)=in})+1 so i=min{MMLab1(B)B attacks A and Lab(B)=in}). This means there is at least one in labelled B that attacks A such that MMLab1(B)=i. From the induction hypothesis we infer that MMLab2(B)=i. Furthermore, for each j<i the induction hypothesis tells us that MMLab1(C)=j iff MMLab2(C)=j. Therefore, from the fact that no in labelled attacker of A is numbered less than i by MMLab1 it follows that also no in labelled attacker of A is numbered less than i by MMLab2. Therefore, MMLab2(A)=min({MMLab2(B)B attacks A and Lab(B)=in})+1=min{MMLab1(B)B attacks A and Lab(B)=in})+1=i+1.

“⇐”: Similar to “⇒”.

From the thus proved fact that for each 11, MMLab1(A)=i iff MMLab2(A)=i, together with the fact that each min–max number has to be in (N{0}){} it follows that also MMLab1(A)= iff MMLab2(A)=. Hence, we have that for each AAr, MMLab1(A)=MMLab2(A), so MMLab1=MMLab2. □

Using the concept of a min–max numbering, we can proceed to define the concept of a strongly admissible labelling.

Definition 10.

A strongly admissible labelling is an admissible labelling whose min–max numbering yields natural numbers only (so no argument is numbered ).

From Definition 10 it directly follows that every strongly admissible labelling is also an admissible labelling. Also, there exists a clear connection between strongly admissible labellings and strongly admissible sets, as one can be converted into the other.

Theorem 7.

Let (Ar,att) be an argumentation framework.

  • for every strongly admissible set ArgsAr, it holds that Args2Lab(Args) is a strongly admissible labelling

  • for every strongly admissible labelling Lab, it holds that Lab2Args(Lab) is a strongly admissible set

Proof.

  • Let Args be a strongly admissible set. This means that i=0Hi=Args. The procedure specified in the proof of Theorem 6 makes sure that every argument in Hi (i0) is numbered with a natural number (note: each such argument is labelled in). As i=0Hi=Args it follows that each argument in Args (that is, each in labelled argument) is numbered with a natural number. It then follows (from Definition 9) that also each out labelled argument is numbered with a natural number. This means that no argument is numbered , thus satisfying the condition of Definition 10.

  • Let Lab be a strongly admissible labelling. This means that each in or out labelled argument is numbered with a natural number. As the min–max number of Lab can be constructed using the procedure explained in the proof of Theorem 6, the fact that each in labelled argument A is assigned a natural number means that for each AArgs there is an i such that AHi. This means that Argsi=0Hi. This, together with the fact that HiArgs for each i0, implies that Args=i=0Hi which means that Args is a strongly admissible set. □

Please notice that strongly admissible labellings and strongly admissible sets are not one-to-one related; instead, they are many-to-one related. As an example, in the argumentation framework of Fig. 1 the strongly admissible set {A,C} is related to two strongly admissible labellings: ({A,C},{B,E},{D,F,G,H}) and ({A,C},{B},{D,E,F,G,H}).

The fact that strongly admissible sets and strongly admissibe labellings are not one-to-one related unfortunately means that some of the results for strongly admissible sets (for instance Theorem 5) do not automatically carry over to strongly admissible labellings. Instead, they need to be proved separately.

Lemma 5.

If Lab1 and Lab2 are strongly admissible labellings, then Lab1Lab2 is also a strongly admissible labelling.

Proof.

Let Args1=Lab2Args(Lab1) and Args2=Lab2Args(Lab2). From Theorem 7 it then follows that Args1 and Args2 are strongly admissible sets, hence (Lemma 3) Args1Args2 is also a strongly admissible set. Let Lab3=Args2Lab(Args1Args2). From Theorem 7 it follows that Lab3 is a strongly admissible labelling. Let MMLab3 be the min–max numbering of this strongly admissible labelling. How does Lab3 compare with Lab3=Lab1Lab2? We start with making the following thee observations.

  • Lab3 is an admissible labelling.

    This is because Lab3 is a strongly admissible labelling.

  • Lab3 is an admissible labelling.

    From the fact that Args1Args2 is a strongly admissible set, it follows that Args1Args2 is conflict-free, so Args1 and Args2 do not attack each other. This implies that in(Lab1)out(Lab2)= and in(Lab2)out(Lab1)=, which means that Lab1Lab2=(in(Lab1)in(Lab2),out(Lab1)out(Lab2),undec(Lab1)undec(Lab2)). That is, we obtain that in(Lab3)=in(Lab1)in(Lab2) and that out(Lab3)=out(Lab1)out(Lab2). Hence, each argument that is labelled in by Lab3 has all its attackers labelled out by Lab3 (this folows from the fact that Lab1 and Lab2 are admissible labellings) and each argument that is labelled out by Lab3 has an attacker that is labelled in by Lab3 (which again follows from the fact that Lab1 and Lab2 are admissible labellings). This means that Lab3 is an admissible labelling.

  • in(Lab3)=in(Lab3).

    In the previous point, it was observed that in(Lab3)=in(Lab1)in(Lab2). As we have that in(Lab1)=Args1 (as Args1=Lab2Args(Lab1)) and in(Lab2)=Args2 (as Args2=Lab2Args(Lab2)) it holds that in(Lab3)=Args1Args2 (as in(Lab3)=in(Lab1)in(Lab2) as observed in the previous point). As in(Lab3)=Args1Args2 (as Lab3=Args2Lab(Args1Args2)) we obtain that in(Lab3)=in(Lab3).

We define the min–max numbering MMLab3 of Lab3 such that MMLab3(A)=MMLab3(A) for each Ain(Lab3)out(Lab3). We now prove that MMLab3 is a correct min–max numbering. For this, we need to show two things:
  • if Lab3(A)=in then MMLab3(A)=max({MMLab3(B)B attacks A and Lab3(B)=out})+1

    As Lab3 and Lab3 are both admissible labellings, it holds that all attackers of an in labelled argument are labelled out. This implies that argument A, which is labelled in by Lab3 and is therefore also labelled in by Lab3 (as in(Lab3)=in(Lab3)) has the same out labelled attackers in both Lab3 and Lab3. As the out labelled attackers of A are numbered the same by MMLab3 as by MMLab3 we have that {MMLab3(B)B attacks A and Lab3(B)=out}={MMLab3(B)B attacks A and Lab3(B)=out}. This, together with the fact that MMLab3(A)=max({MMLab3(B)B attacks A and Lab3(B)=out})+1 (as MMLab3 is a correct min–max numbering) and the fact that MMLab3(A)=MMLab3(A) implies that MMLab3(A)=max({MMLab3(B)B attacks A and Lab3(B)=out})+1.

  • if Lab3(A)=out then MMLab3(A)=min({MMLab3(B)B attacks A and Lab3(B)=in})+1

    As in(Lab3)=in(Lab3) it holds that the out labelled argument A has the same in labelled attackers in both Lab3 and Lab3. As the in labelled attackers of A are numbered the same by MMLab3 as by MMLab3 we have that {MMLab3(B)B attacks A and Lab3(B)=in}={MMLab3(B)B attacks A and Lab3(B)=in}. This, together with the fact that MMLab3(A)=min({MMLab3(B)B attacks A and Lab3(B)=in})+1 (as MMLab3 is a correct min–max numbering) and the fact that MMLab3(A)=MMLab3(A) implies that MMLab3(A)=min({MMLab3(B)B attacks A and Lab3(B)=in})+1.

Hence, we have established that MMLab3 is a correct min–max numbering of Lab3, one that numbers each argument that is labelled in or out by Lab3 the same as MMLab3. As MMLab3 does not number any argument with (as Lab3 is a strongly admissible labelling) it follows that MMLab3 also does not number any argument with . Hence, Lab3 is a strongly admissible labelling. □

Lemma 6.

Each admissible labelling Lab has a unique biggest (w.r.t.) strongly admissible sublabelling.

Proof.

Similar to the proof of Lemma 4, but with Args, Args1 and Args2 replaced by Lab, Lab1 and Lab2, with ⊆ and ∩ replaced by ⊑ and ⊓ and Lemma 3 replaced by Lemma 5. □

If Lab is an admissible labelling, then we write Lab for its biggest (w.r.t. ⊑) strongly admissible sublabelling.

Theorem 8.

Let (Ar,att) be an argumentation framework. The strongly admissible labellings of this framework form a lattice (w.r.t.).

Proof.

Similar to the proof of Theorem 5, with Args1, Args2, Args3, Args3, Args3 and Args3 replaced by Lab1, Lab2, Lab3, Lab3, Lab3 and Lab3, ⊆, ∪ and ∩ replaced by ⊑, ⊔ and ⊓, and Lemma 4 replaced by Lemma 6. ⊆ replaced by ⊑, ∪ replaced by ⊔ and ∩ replaced by ⊓. □

5.Computational complexity

Regarding the issue of computational complexity, one can distinguish the standard decision problems of credulous acceptance, sceptical acceptance and verification.

The formal statement of these decision problems (which are defined for any extension based argumentation semantics σ) is presented in Table 1. In this, we use σ to described an arbitrary semantics, e.g. any of the cases given in Definition 3, although our principal interest will be the case of σ being the class of strongly-admissible sets; Eσ for the set of all subsets of arguments within a framework that satisfy the criteria given by σ, e.g. Eadm(Ar,att) is the set of all admissible sets in the framework Ar,att.

Table 1

Decision problems in argumentation semantics

ProblemInstanceQuestionFormal statement
caAr,att, xArIs x credulously accepted?SAr:xS and SEσ(Ar,att)?
saAr,att, xArIs x sceptically accepted?SAr:SEσ(Ar,att)xS?
verAr,att SArDoes S satisfy the criteria of σ?SEσ(Ar,att)?

The credulous acceptance problem for strong admissibility reduces to deciding if the given argument, x, is in the grounded extension, as the grounded extension is the (unique) biggest (w.r.t. ⊆) strongly admissible set [3]. Hence, the credulous acceptance problem of strong admissibility is of polynomial complexity.

As for sceptical acceptance, the issue is to determine whether a particular argument is in every strongly admissible set. However, as the empty set is always strongly admissible, this decision problem is trivial as the answer is always negative.

The verification problem is more interesting in that it is not simply a matter of testing if S is a subset of the grounded extension, i.e. although S being such a subset is a necessary condition for strong-admissibility it is not a sufficient condition. In determining if a set S is strongly admissible one could use Algorithm 1.

Algorithm 1

Verification of Args as a strongly admissible set

Verification of Args as a strongly admissible set

The correctness of Algorithm 1 follows from Theorem 1 and Lemma 2. To see this, notice that the algorithm accumulates a subset of Ar (in Argsi) stopping when there is no change to the existing subset (i.e. that forming Argsi1) and using the final set to compare with the candidate subset Args. The set(s) Argi are formed by the adding the intersection of the characteristic function of Hi with the set, Args, being tested. This set, Hi starts (i=0) from the empty set. Overall the process of computing successive subsets Hi and the concomitant changes to Argsi mimics exactly the stages applied in the proof of Theorem 1 using the result of Lemma 2 as support.

As we only consider finite argumentation frameworks, the algorithm is guaranteed to terminate.

The maximal number of loop iterations is of the order |Ar| because at each iteration there will be at least one argument added (this must be the case for otherwise we would have Argsi=Argsi1 resulting in the loop terminating at line 8) until the loop terminates. As for the set operations of union and intersection, it holds that S1S2 and S1S2 each require the order of |S1|+|S2| operations, provided that appropriate data structures are being used. For the above algorithm, this would be |F(Hi)|+|Args|+|Argsi|+|Hi+1|, so no more than 4·|Ar| for each loop iteration. As there are no more than |Ar| loop iterations, this implies the maximal number of steps for doing the set operations is in the order of |Ar|·|Ar|.

As for determining the number of operations of the F-operator, the easiest way to do this is to consider the total number of operations, throughout all loop iterations. Calculating F(S) can be done basically by removing the arguments of S+ from the argumentation framework (together with the attacks from and to S+) and then examining which arguments have no attackers (this is one standard approach used in computing the grounded extension). Point 1 of Lemma 2 implies that this can be done in an iterative way when it comes to calculating each Hi+1. As no more than |att| edges can be removed from the graph, there can be at most |att| edges relevant to any Hi. Note that the maximum number of attacks that could be present in any framework satisfies |att||Ar|·|Ar|, so it holds that the number of operations is at most |Ar|·|Ar| for computing the outcome of the characteristic functions. This, together with the number of operations required for computing the union and intersection (which is also |Ar|·|Ar|) means the total number of required operations is in the order of |Ar|·|Ar|, so of polynomial complexity.

As an aside, please notice that in order to simplify the above discussion, we have formulated Algorithm 1 in a way that is closely aligned to Lemma 2 and Theorem 1. However, it can be observed that for every i it holds that Argsi=Hi (this is because of point 1 of Lemma 2). Hence, it would be possible to do away with Argsi in the above algorithm, and only use Hi instead. We observe that this does not affect the overall complexity of the algorithm, which remains in the order of |Ar|·|Ar|.

6.Strong admissibility and argument games

Now that some of the formal properties of strong admissibility have been examined, the next step is to study some of its applications. In particular, it turns out that strong admissibility is one of the corner stones of the discussion games for grounded semantics.

6.1.The standard grounded game

As far as we are know, the Standard Grounded Game [7,21,26] was the first dialectical proof procedure to determine whether a particular argument is in the grounded extension.

Definition 11.

A discussion in the Standard Grounded Game is a finite sequence [A1,,An] (n1) of arguments (sometimes called moves), of which the odd moves are called P-moves (Proponent moves) and the even moves are called O-moves (Opponent moves), such that:

  • (1) every O-move is an attacker of the preceding P-move (that is, every Ai where i is even and 2in attacks Ai1)

  • (2) every P-move except the first one is an attacker of the preceding O-move (that is, every Ai where i is odd and 3in attacks Ai1)

  • (3) P-moves are not repeated (that is, for every odd i,j{1,,n} it holds that if ij then AiAj)

A discussion is called terminated iff there is no An+1 such that [A1,,An,An+1] is a discussion. A terminated discussion is said to be won by the player making the last move.

An argument tree is a tree of which each node (n) is labelled with an argument (Arg(n)). The level of a node is the number of nodes in the path to the root.

Definition 12.

A winning strategy of the Standard Grounded Game for argument A is an argument tree, where the root is labelled with A, such that

  • (1) for each path from the root (nroot) to a leaf node (nleaf) it holds that the arguments on this path form a terminated discussion won by P

  • (2) for each node at odd level nP it holds that {Arg(nchild)nchild is a child of nP}={BB attacks Arg(nP)} and the number of children of nP is equal to the number of attackers of Arg(nP)

  • (3) each node of even level nO has precisely one child nchild, and Arg(nchild) attacks Arg(nO)

The soundness and completeness of the Standard Grounded Game depends on the presence of a winning strategy. That is, an argument A is in the grounded extension iff there exists a winning strategy for A. Interesting enough, it turns out that such a winning strategy defines a strongly admissible set containing A.

Theorem 9.

The set of all proponent moves in a winning strategy of the Standard Grounded Game is strongly admissible.

Proof.

We prove this by induction over the depth (i) of the winning strategy game tree.

basis

i=0. In that case, the winning strategy consists of a single argument (say, A). This means that A has no attackers. Hence, {A} is a strongly admissible set.

step

Suppose that every winning strategy of depth less or equal than i has its proponent moves constituting a strongly admissible set. We need to prove that also every winning strategy of depth i+2 has its proponent moves constituting a strongly admissible set. Let WS be a winning strategy of depth i+2. Let A be the argument at the root of the tree. Let WS1,,WSn be the subtrees whose roots are at distance 2 of the root of WS. The induction hypothesis states that for each of these subtrees (WSj), their set of proponent moves Argsj constitutes a strongly admissible set. Therefore (by Lemma 3) the set Args=j=1nArgsj is strongly admissible. Also, AArgs (this is because the proponent is not allowed to repeat his moves). Let B be an arbitrary argument in Args (the set of all proponent moves in the winning strategy). We distinguish two cases:

  • (1) BArgs. Then, since Args is a strongly admissible set, there exists an ArgsArgs{B} that defends B and is itself strongly admissible. Since ArgsArgs, it also holds that ArgsArgs{B}.

  • (2) BArgs. Then B=A (the root of the tree WS). The structure of the WS tree is such that B is defended by the roots of WS1,,WSn. So B is defended by the strongly admissible set Args. Also BArgs, so ArgsArgs{B}, therefore satisfying Definition 8. □

It can also be observed that a winning strategy defines a strongly admissible labelling.

Theorem 10.

Let ArgsP be the set of proponent moves and ArgsO be the set of opponent moves of a particular winning strategy given an argumentation framework (Ar,att). It holds that (ArgsP,ArgsO,Ar(ArgsPArgsO)) is a strongly admissible labelling.

Proof.

Given that ArgsP is strongly admissible (Theorem 9) it then follows from Theorem 7 that LabPP+=(ArgsP,ArgsP+,Ar(ArgsPArgsP+)) is a strongly admissible labelling. Now consider LabPO=(ArgsP,ArgsO,Ar(ArgsPArgsO)). Notice that ArgsPArgsP+, otherwise ArgsP would not be an admissible set. Also, from the structure of a winning strategy (with the Opponent playing all possible attackers of each Proponent move as its children) it follows that ArgsO=ArgsP. Hence, ArgsOArgsP+. LabPO has the same min–max numbering as LabPP+ (minus the arguments that are no longer out in LabPO, since out(LabPO)out(LabPP+), as ArgsOArgsP+). This is because the out-labelled arguments in ArgsP+ArgsO do not influence the min–max numbers of the in-labelled arguments in ArgsP. It then follows that the min–max numbers of the out-labelled arguments in LabPO also stay the same. Hence, the min–max numbering of LabPO is essentially a restricted version (with a smaller domain) of the min–max numbering of LabPP+. So from the fact that LabPP+ is a strongly admissible labelling (not yielding ) it directly follows that LabPO is a strongly admissible labelling (not yielding ). □

Hence, given a winning strategy of the Standard Grounded Game, the set of all proponent moves and the set of all opponent moves essentially define a strongly admissible labelling.

6.2.The grounded discussion game

Like the Standard Grounded Game, the Grounded Discussion Game [11] is a proof procedure to determine whether a particular argument is a member of the grounded extension. The game has two players (proponent and opponent) and is based on four different moves, each of which has an argument as a parameter.

HTB(A)

(“A has to be the case”)

With this move, the proponent claims that argument A has to be labelled in by every complete labelling (and hence also has to be labelled in by the grounded labelling).

CB(B)

(“B can be the case, or at least cannot be ruled out”)

With this move, the opponent claims that argument B does not have to be labelled out by every complete labelling. That is, the opponent claims there exists at least one complete labelling where B is labelled in or undec, and that B is therefore not labelled out by the grounded labelling.

CONCEDE(A)

(“Fair enough, I agree that A has to be the case”)

With this move, the opponent indicates that he now agrees with the proponent (who previously did a HTB(A) move) that A has to be the case (labelled in by every complete labelling, including the grounded labelling).

RETRACT(B)

(“Fair enough, I give up that B can be the case”)

With this move, the opponent indicates that he no longer beliefs that argument B can be in or undec. That is, the opponent acknowledges that B has to be labelled out by every complete labelling, including the grounded labelling.

One of the key ideas of the discussion game is that the proponent has burden of proof. He has to establish the acceptance of the main argument. The opponent merely has to cast sufficient doubts. Also, the proponent has to make sure that the discussion does not go around in circles.

The game starts with the proponent uttering a HTB statement. After each HTB statement (either the first one or a subsequent one) the opponent utters a sequence of one or more CB, CONCEDE and RETRACT statements, after which the proponent again utters an HTB statement, etc. In the argumentation framework of Fig. 1 the discussion could go as follows.

aac-10-aac190463-e001.jpg

In the above discussion, C is called the main argument (the argument the discussion starts with). The discussion ends with the main argument being conceded by the opponent, which means the proponent wins the discussion.

As an example of a discussion that is lost by the proponent, it can be illustrative to examine what happens if, still in the argumentation framework of Fig. 1, the proponent claims that B has to be the case.

aac-10-aac190463-e002.jpg
After the second move, the discussion is terminated, as the proponent cannot move anymore, since A does not have any attackers. This brings us to the precise preconditions of the discussion moves.

HTB(A)

This is either the first move, or the previous move was CB(B), where A attacks B, and no CONCEDE or RETRACT move is applicable.

CB(A)

A is an attacker of the last HTB(B) statement that is not yet conceded, the directly preceding move was not a CB statement, argument A has not yet been retracted, and no CONCEDE or RETRACT move is applicable.

CONCEDE(A)

There has been a HTB(A) statement in the past, of which every attacker has been retracted, and CONCEDE(A) has not yet been moved.

RETRACT(A)

There has been a CB(A) statement in the past, of which there exists an attacker that has been conceded, and RETRACT(A) has not yet been moved.

Apart from the preconditions mentioned above, all four statements also have the additional precondition that no HTB-CB repeats have occurred. That is, there should be no argument for which HTB has been uttered more than once, CB has been uttered more than once, or both HTB and CB have been uttered. In the first and second case, the discussion is going around in circles (which the proponent has to prevent, since he has burden of proof). In the third case, the proponent has been contradicting himself, as his statements are not conflict-free. In each of these three cases, the discussion comes to an end with no move being applicable anymore.

The above conditions are made formal in the following definition.

Definition 13.

Let (Ar,att) be an argumentation framework. A grounded discussion is a sequence of discussion moves constructed by applying the following principles.

BASIS (HTB)

If AAr then [HTB(A)] is a grounded discussion.

STEP (HTB)

If [M1,,Mn] (n1) is a grounded discussion without HTB-CB repeats,8 and no CONCEDE or RETRACT move is applicable,9 and Mn=CB(A) and B is an attacker of A then [M1,,Mn,HTB(B)] is also a grounded discussion.

STEP (CB)

If [M1,,Mn] (n1) is a grounded discussion without HTB-CB repeats, and no CONCEDE or RETRACT move is applicable, and Mn is not a CB move, and there is a move Mi=HTB(A) (i{1n}) such that the discussion does not contain CONCEDE(A), and for each move Mj=HTB(A) (j>i) the discussion contains a move CONCEDE(A), and B is an attacker of A such that the discussion does not contain a move RETRACT(B), then [M1,,Mn,CB(B)] is a grounded discussion.

STEP (CONCEDE)

If [M1,,Mn] (n1) is a grounded discussion without HTB-CB repeats, and CONCEDE(B) is applicable then [M1,,Mn,CONCEDE(B)] is a grounded discussion.

STEP (RETRACT)

If [M1,,Mn] (n1) is a grounded discussion without HTB-CB repeats, and RETRACT(B) is applicable then [M1,,Mn,RETRACT(B)] is a grounded discussion.

It can be observed that the preconditions of the moves are such that a proponent move (HTB) can never be applicable at the same moment as an opponent move (CB, CONCEDE or RETRACT). That is, proponent and opponent essentially take turns in which each proponent turn consists of a single HTB statement, and every opponent turn consists of a sequence of CONCEDE, RETRACT and CB moves.

Definition 14.

A grounded discussion [M1,M2,,Mn] is called terminated iff there exists no move Mn+1 such that [M1,M2,,Mn,Mn+1] is a grounded discussion. A terminated grounded discussion (with M1 being HTB(A) for some AAr) is won by the proponent iff the discussion contains CONCEDE(A), otherwise it is won by the opponent.

To illustrate why the discussion has to be terminated after the occurrence of a HTB-CB repeat, consider the following discussion in the argumentation framework of Fig. 1.

aac-10-aac190463-e003.jpg

After the third move, an HTB-CB repeat occurs and the discussion is terminated (opponent wins). Hence, termination after a HTB-CB repeat is necessary to prevent the discussion from going on perpetually.

It has been proved [11,12] that the Grounded Discussion Game is a sound and complete proof procedure for determining whether an argument is in the grounded extension. More specifically,

(soundness)

if a discussion for a particular argument has been won by the proponent, then the argument is in the grounded extension, and

(completeness)

if an argument is in the grounded extension, then the proponent is able to win the game for the argument (that is, the proponent has a winning strategy)

As for the first point (soundness) it can be observed that if one would label the arguments of CONCEDE moves in, the arguments of RETRACT moves out and all other arguments undec, the result is a strongly admissible labelling at each state of the discussion game. If this game is ultimately won by the proponent, then the main argument has been CONCEDEd. Hence, the result is a strongly admissible labelling where the main argument is labelled in. This means the main argument is in the grounded extension.

As for the second point (completeness) it can be observed that the grounded labelling, together with its associated min–max numbering, serves as a roadmap that allows the proponent to win the game. In essence, the proponent does this by using only in labelled arguments to select the HTB moves, and to select the in labelled argument with a lowest min–max number whenever there is a choice. We refer to [11,12] for details.

6.3.The Standard Grounded Game (SGG) vs. the Grounded Discussion Game (GDG)

So far, we have seen that both the SGG and the GPG show membership of the grounded extension essentially by building a strongly admissible labelling where the argument in question is labelled in.10 This raises the question of how many steps each of these games requires for doing so. Consider the argumentation framework of Fig. 4 (top left). The winning strategy of the SGG is in the same figure (top right). Now consider what would happen if one would start to extend the argumentation framework by duplicating the middle part. That is, suppose we have arguments B1,,Bn and C1,,Cn (with n being an odd number), as well as arguments A and D. Suppose that for every i{1,,n1} Bi+1 attacks Bi, and Ci+1 attacks Ci, and that for each even i{2,,n1} Bi+1 attacks Ci, and Ci+1 attacks Bi, and that B1 and C1 attack A, and that D attacks Bn and Cn. In that case, the branches in the SGG winning strategy would split at every O-move. So for n=3 (as is the case in Fig. 4) the number of branches is four, for n=5 it is eight, etc. In general, the number of branches in the SGG winning strategy is 2(n+1)/2, with the number of nodes in the SGG winning strategy being 1+2i=1(n+1)/22i. Hence, the number of steps needed in a winning strategy of the SGG can be exponential in relation to the in/out-size11 of the strongly admissible labelling that the SGG winning strategy is constructing.12

Fig. 4.

The Standard Grounded Game (SGG) versus the Grounded Discussion Game (GDG).

The Standard Grounded Game (SGG) versus the Grounded Discussion Game (GDG).

As for the Grounded Discussion Game, the situation is different. It can be proven [11,12] that the proponent always has a strategy for the game that results in the total number of moves being 2·|in(Lab)|+2·|out(Lab)| where Lab the strongly admissible labelling that is built up during the discussion game. This labelling is such that in(Lab) consists of all arguments that have been subject to a CONCEDE move and out(Lab) consists of all arguments that have been subject to a RETRACT move. An example of a game that results from such a strategy is provided in Fig. 4.

Overall, we observe that both the Standard Grounded Game and the Grounded Discussion Game prove that an argument is in the grounded extension by building a strongly admissible labelling around it. However, where the Standard Grounded Game can require a number of moves that is exponential in relation to the in/out-size of the strongly admissible labelling, the Grounded Discussion game requires a number of moves that is always linear in relation to the in/out-size of the strongly admissible labelling.

7.Discussion and future research

In the current paper, we have re-examined the concept of strong admissibility, from both theoretical and practical perspectives. From theoretical perspective, we have observed that the strongly admissible sets form a lattice with the empty set as bottom element and the grounded extension as top element. Also, we have developed the concept of a strongly admissible labelling, and shown how it relates to the concept of a strongly admissible set. From practical perspective, we have examined how strongly admissible labellings lie at the basis of both the Standard Grounded Game [21] and the Grounded Discussion Game [11,12]. Although both essentially construct a strongly admissible labelling around the argument in question, the Grounded Discussion Game does so using a linear number of steps, whereas the Standard Grounded Game can require an exponential number of steps.

An alternative definition of a strongly admissible set is given by Baumann et al. [4]. Basically, the idea is that a set of Args is strongly admissible iff there are finitely many and pairwise disjoint sets A1,,An such that (1) Args=i=1nAi, (2) A1F(), and (3) i=1jAi defends Aj+1 (1j<n). Baumann et al. [4] prove that their definition is equivalent with Definition 8 of the current paper (which first appeared in [10]). One particular issue with their definition is that they do not specify how to actually obtain the sequence A1,,An. However, we observe that it is fairly easy to convert the sequence H0,H1,H2, as specified in Lemma 2 to a corresponding sequence A1,,An. This can be done by first identifying n to be the lowest number such that Hn=Hn+1 (which implies that Hm=Hn for each mn) and then taking A1=H1 and Ai+i=Hi+1Hi (1i<n).

The idea of numbering arguments (such as is done in a min–max numbering) can be traced back to the work of Pollock [24], who gives an iterative procedure (basically for computing the grounded extension, as is explained by Dung [19]) in which arguments become in and out at different levels during the algorithm [24, Algorithm 2]. It has to be mentioned, however, that Pollock’s algorithm (the ideas of which have also been applied in [2]) computes the entire grounded extension (in a way that is similar to what is done in [21]) and is not applicable to the concept of a strongly admissible set (or labelling) in general.

One of the things to be examined in the future is how the concept of strong admissibility can be useful in identifying the shortest discussion that shows an argument (A) is in the grounded extension. For instance, we conjecture that for each minimal (w.r.t. ⊑) strongly admissible labelling that labels A in, there exists a discussion under the Grounded Persuasion Game for argument A that builds precisely this labelling. However, there can be more than one such labelling. For argument F in Fig. 1, for instance, both ({A,C,F},{B,E},{D,G,H}) and ({D,F},{E},{A,B,C,G,H}) are minimal (w.r.t. ⊑) strongly admissible labellings that label F in, but the in/out-size of the second labelling is smaller than that of the first labelling, thus yielding a shorter discussion. How to precisely obtain such a strongly admissible labelling with minimal size is a topic for further investigation.

Finally there are a number of questions that would merit further consideration with respect to complexity issues. For example, although the canonical decision problems (credulous and sceptical acceptance, verification) for the strong admissibility semantics are tractable having polynomial-time sequential algorithms, it seems unlikely that verification would have efficient parallel algorithms. The notion of “efficient parallel algorithm” being one that can be realised using a logarithmic depth Boolean combinational circuit. A formal demonstration that such is indeed the case would be achieved by showing the verification problem to be p-complete. In view of the supporting technical detail that would be required in exploring this question we have not pursued it in the current article.

A question of some considerable interest whose status is far from clear concerns the following: given two argumentation frameworks (Ar,att1) and (Ar,att2) (that is with identical arguments but not necessarily identical attacks), do their strongly admissible sets coincide? That is, is the case that Esa(Ar,att1)=Esa(Ar,att2)? Alternatively we could examine if |Esa(Ar,att1)|=|Esa(Ar,att2)|. It is worth noting that the “equivalence by set equality” is only one such definition, but there are alternatives: we could also ask about the existence of a relabelling of arguments so that the two frameworks become identical. It is worth noting two further aspects of this question: firstly, unlike previously studied and superficially similar problems, e.g. coincidence of stable and preferred semantics from [20] the question involves more than a single framework (although given an appropriate semantics, σ, the question Eσ(Ar,att)=Esa(Ar,att) may also be non-trivial: while some instances, e.g. preferred semantics, reduce to known cases since Epr(Ar,att)=Esa(Ar,att) if and only if Epr(Ar,att)={} others are less so). A second point is the how much “obvious” necessary conditions can be exploited, e.g. “in order for Esa(Ar,att1)=Esa(Ar,att2) to hold the number of unattacked arguments in each must be equal” (otherwise there will be different single argument strongly admissible sets in the two). While conditions such as these suggest a natural way of progressing from single to two to k argument set comparisons, there is potentially an exponential increase in the number of sets being compared as the process continues. Such further algorithmic and complexity issues are the topic of continuing work.

Notes

1 With the in/out-size of a labelling Lab, we mean |in(Lab)out(Lab)|.

2 This paper is an extended and thoroughly revised version of work that was presented at COMMA 2014 [10] and TAFA 2015 [11]. In particular, we have rewritten some of the previously unpublished proofs (of Theorem 1, Theorem 2, Theorem 3, Theorem 6 and Theorem 7) to take advantage of a new technical result (Lemma 2). Moreover, we have added results on computational complexity (Section 5) and we have decided to include the Grounded Discussion Game [11] instead of the outdated Grounded Discussion Game [18].

3 The well-definedness of the down-admissible set follows from [16], where this concept is defined in its labellings form, together with the equivalence between extensions and labellings [15].

4 In [19] a preferred extension is defined as a maximal admissible set, instead of as a maximal complete extension, but it can be shown that these are equivalent.

5 Hence, each strongly admissible set is an admissible set that is contained in the grounded extension. The converse, however, does not hold. For instance, in Fig. 1, {F} is an admissible set that is contained in the grounded extension, but it is not a strongly admissible set.

6 We recall that a lattice is a partial order such that each two elements have both a greatest lower bound and a least upper bound. For an ordering to be a semi-lattice only one of these two conditions needs to be met.

7 The intuition behind the min–max number of an argument is that of the game-theoretic length of the path (consisting of alternately in and out labelled arguments) from the argument back to an unattacked ancestor argument. The player selecting the in labelled arguments aims to make the path as short as possible whereas the player selecting the out labelled arguments aims to make the path as long as possible.

8 We say that there is a HTB-CB repeat iff i,j{1,,n}AAr:(Mi=HTB(A)Mi=CB(A))(Mj=HTB(A)Mj=CB(A))ij.

9 A move CONCEDE(B) is applicable iff the discussion contains a move HTB(A) and for every attacker A of B the discussion contains a move RETRACT(B), and the discussion does not already contain a move CONCEDE(B). A move RETRACT(B) is applicable iff the discussion contains a move CB(B) and there is an attacker A of B such that the discussion contains a move CONCEDE(A), and the discussion does not already contain a move RETRACT(B).

10 Similarly, it can be observed that for instance the credulous preferred game [14,27] shows membership of a preferred extension essentially by building an admissible labelling around the argument in question.

11 We recall that with the in/out-size of a labelling Lab we mean |in(Lab)out(Lab)|.

12 We thank Mikołaj Podlaszewski for this example.

Acknowledgements

We would like to thank Ringo Baumann and the anonymous reviewers for their useful comments.

References

[1] 

P. Baroni, M.W.A. Caminada and M. Giacomin, An introduction to argumentation semantics, Knowledge Engineering Review 26(4) (2011), 365–410. doi:10.1017/S0269888911000166.

[2] 

P. Baroni and M. Giacomin, Self-stabilizing defeat status computation: Dealing with conflict management in multi-agent systems, Artificial Intellligence 165 (2005), 187–259. doi:10.1016/j.artint.2005.02.003.

[3] 

P. Baroni and M. Giacomin, On principle-based evaluation of extension-based argumentation semantics, Artificial Intelligence 171(10–15) (2007), 675–700. doi:10.1016/j.artint.2007.04.004.

[4] 

R. Baumann, T. Linsbichler and S. Woltran, Verifiability of argumentation semantics, in: Computational Models of Argument; Proceedings of COMMA 2016, P. Baroni, T.F. Gordon, T. Scheffler and M. Stede, eds, 2016, pp. 83–94.

[5] 

T.J.M. Bench-Capon, Dilemmas and paradoxes: Cycles in argumentation frameworks, Journal of Logic and Computation (2014).

[6] 

R. Booth, M.W.A. Caminada, M. Podlaszewski and I. Rahwan, Quantifying disagreement in argument-based reasoning, in: Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems, 2012.

[7] 

M.W.A. Caminada, For the sake of the Argument. Explorations into argument-based reasoning, PhD thesis, Vrije Universiteit Amsterdam, 2004.

[8] 

M.W.A. Caminada, On the issue of reinstatement in argumentation, in: Logics in Artificial Intelligence; 10th European Conference, JELIA 2006, M. Fischer, W. van der Hoek, B. Konev and A. Lisitsa, eds, LNAI, Vol. 4160, Springer, 2006, pp. 111–123.

[9] 

M.W.A. Caminada, An algorithm for computing semi-stable semantics, in: Proceedings of the 9th European Conference on Symbolic and Quantitalive Approaches to Reasoning with Uncertainty (ECSQARU 2007), Springer Lecture Notes in AI, Springer Verlag, Berlin, 2007, pp. 222–234. doi:10.1007/978-3-540-75256-1_22.

[10] 

M.W.A. Caminada, Strong admissibility revisited, in: Computational Models of Argument, Proceedings of COMMA 2014, S. Parsons, N. Oren, C. Reed and F. Cerutti, eds, IOS Press, 2014, pp. 197–208.

[11] 

M.W.A. Caminada, A discussion game for grounded semantics, in: Theory and Applications of Formal Argumentation (Proceedings TAFA 2015), E. Black, S. Modgil and N. Oren, eds, Springer, 2015, pp. 59–73. doi:10.1007/978-3-319-28460-6_4.

[12] 

M.W.A. Caminada, A Discussion Protocol for Grounded Semantics (proofs), Technical Report, University of Aberdeen, 2015.

[13] 

M.W.A. Caminada and L. Amgoud, On the evaluation of argumentation formalisms, Artificial Intelligence 171(5–6) (2007), 286–310. doi:10.1016/j.artint.2007.02.003.

[14] 

M.W.A. Caminada, W. Dvořák and S. Vesic, Preferred semantics as Socratic discussion, Journal of Logic and Computation 26 (2014), 1257–1292. doi:10.1093/logcom/exu005.

[15] 

M.W.A. Caminada and D.M. Gabbay, A logical account of formal argumentation, Studia Logica 93(2–3) (2009), 109–145, Special issue: New ideas in argumentation theory. doi:10.1007/s11225-009-9218-x.

[16] 

M.W.A. Caminada and G. Pigozzi, On judgment aggregation in abstract argumentation, Autonomous Agents and Multi-Agent Systems 22(1) (2011), 64–102. doi:10.1007/s10458-009-9116-7.

[17] 

M.W.A. Caminada, G. Pigozzi and M. Podlaszewski, Manipulation in group argument evaluation, in: Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence, T. Walsh, ed., 2011, pp. 121–126.

[18] 

M.W.A. Caminada and M. Podlaszewski, Grounded semantics as persuasion dialogue, in: Computational Models of Argument – Proceedings of COMMA 2012, B. Verheij, S. Szeider and S. Woltran, eds, 2012, pp. 478–485.

[19] 

P.M. Dung, On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games, Artificial Intelligence 77 (1995), 321–357. doi:10.1016/0004-3702(94)00041-X.

[20] 

P.E. Dunne and T.J.M. Bench-Capon, Coherence in finite argument systems, Artificial Intelligence 141(1–2) (2002), 187–203. doi:10.1016/S0004-3702(02)00261-8.

[21] 

S. Modgil and M.W.A. Caminada, Proof theories and algorithms for abstract argumentation frameworks, in: Argumentation in Artificial Intelligence, I. Rahwan and G.R. Simari, eds, Springer, 2009, pp. 105–129. doi:10.1007/978-0-387-98197-0_6.

[22] 

S. Modgil and H. Prakken, A general account of argumentation with preferences, Artificial Intellligence 195 (2013), 361–397. doi:10.1016/j.artint.2012.10.008.

[23] 

S. Nofal, K. Atkinson and P.E. Dunne, Algorithms for decision problems in argumentation systems under preferred semantics, Artificial Intelligence 207 (2014), 23–51. doi:10.1016/j.artint.2013.11.001.

[24] 

J.L. Pollock, How to reason defeasibly, Artificial Intelligence 57 (1992), 1–42. doi:10.1016/0004-3702(92)90103-5.

[25] 

H. Prakken, An abstract framework for argumentation with structured arguments, Argument and Computation 1(2) (2010), 93–124. doi:10.1080/19462160903564592.

[26] 

H. Prakken and G. Sartor, Argument-based extended logic programming with defeasible priorities, Journal of Applied Non-Classical Logics 7 (1997), 25–75. doi:10.1080/11663081.1997.10510900.

[27] 

G.A.W. Vreeswijk and H. Prakken, Credulous and sceptical argument games for preferred semantics, in: Proceedings of the 7th European Workshop on Logic for Artificial Intelligence (JELIA-00), Springer Lecture Notes in AI, Springer Verlag, Berlin, 2000, pp. 239–253. doi:10.1007/3-540-40006-0_17.