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 for abstract dialectical frameworks

Abstract

Abstract dialectical frameworks (ADFs) have been introduced as a formalism for modeling argumentation allowing general logical satisfaction conditions and the relevant argument evaluation. Different criteria used to settle the acceptance of arguments are called semantics. Semantics of ADFs have so far mainly been defined based on the concept of admissibility. However, the notion of strongly admissible semantics studied for abstract argumentation frameworks has not yet been introduced for ADFs. In the current work we present the concept of strong admissibility of interpretations for ADFs. Further, we show that strongly admissible interpretations of ADFs form a lattice with the grounded interpretation as the maximal element. We also present algorithms to answer the following decision problems: (1) whether a given interpretation is a strongly admissible interpretation of a given ADF, and (2) whether a given argument is strongly acceptable/deniable in a given interpretation of a given ADF. In addition, we show that the strongly admissible semantics of ADFs forms a proper generalization of the strongly admissible semantics of AFs.

1.Introduction

Interest and attention in argumentation theory from researchers in the field of Artificial Intelligence (AI) has been increasing, as witnessed by the wide variety of formalisms to model argumentation and by the variety of semantics proposed to assess the acceptance of arguments [7,57]. Abstract argumentation frameworks (AFs for short) as introduced in the landmark paper by Dung [34] have gained more and more significance in the AI domain. First of all, it has been shown in [34] that AFs are useful to capture the essence of different non-monotonic formalisms. In addition, compared to other non-monotonic formalisms (which are built on top of classical logical syntax), AFs are a much simpler formalism; indeed, they are just directed graphs in which nodes present arguments and directed edges indicate attack relations among arguments. Moreover, AFs are nowadays an integral concept in several advanced argumentation-based formalisms in the sense that their semantics are defined based on a formal connection to Dung’s AFs. Finally, the simplicity of the syntax of AFs has made them an attractive modeling tool in several areas, such as multi-agent systems [44], multi-agent negotiation [3], and legal reasoning [10].

Despite the popularity and simplicity of AFs, these frameworks are used to model argumentation with simple attack relations among arguments. Thus, there exist a number of generalizations of AFs, for instance, modeling group attacks among arguments [48] or modeling preference over the arguments [9,11]. Among all generalizations of AFs, abstract dialectical frameworks (ADFs) were first introduced in [18] and further refined in [14,15,17]. They are expressive generalizations of AFs in which the logical relations among arguments can be represented. This allows researchers to express notions of support, collective attacks, and even more complicated relations. Thanks to their flexibility in formalizing relations between arguments, ADFs have recently been used in several applications; in legal reasoning [1,2,33], online dialog systems [46,47], and text exploration [19].

ADFs have been actively researched [13,16,37,5456,59]. A key question in formal argumentation is ‘How is it possible to evaluate arguments in a given formalism?’. Answering this question leads to the introduction of several types of semantics. In AFs, different semantics single out coherent subsets of arguments that “fit” together, according to specific criteria [4]. More formally, an AF semantics takes an argumentation framework as input and produces as output a collection of sets of arguments, called extensions. Thus, different semantics reflect different points of view about the acceptance or denial of arguments. Most of the semantics of AFs/ADFs are based on the concept of admissibility.

In AFs, admissibility plays an important role with respect to rationality postulates [24]. Often a new semantics is an improvement of an already existing one by introducing further restrictions on the set of accepted arguments (that are chosen together) or possible attackers. One of the main admissibility-based semantics of AFs is the grounded semantics. First, each AF has a unique grounded extension. Second, the elements of the grounded extension usually belong to other semantics of AFs. The grounded extension collects all unattacked (undoubted) arguments and each argument that can be iteratively supported by these unattacked arguments. Informally, the grounded extension accepts those arguments that no one can avoid to accept; it rejects all the arguments that no one avoid to reject; and it does not have any idea about all other arguments. Thus, no one has any doubt on the acceptance of the arguments that are in the grounded extension. Thus, answering the credulous decision problem under grounded semantics of AFs (i.e., investigating whether a queried argument is part of the grounded extension of a given AF) has a considerable importance.

It has been shown that to answer the credulous decision problem under grounded semantics, not all arguments within the grounded extension are necessary. As a remedy, another set of semantics, namely strong admissibility semantics has been introduced for AFs [8,21,25]. While the grounded extension collects all the arguments of a given AF that can be accepted without any doubt, strongly admissible extensions are subsets of the grounded extension that satisfy the same condition. Actually a strongly admissible extension explains why its arguments can be accepted without any doubt, without presenting further information of all arguments in the grounded extension. In AFs, the concept of strong admissibility semantics has first been defined in the work of Baroni and Giacomin [8], based on the notion of strong defence. Later in [21] this concept was introduced without referring to strong defence. Furthermore, in [25], Caminada and Dunne presented a labelling account of strong admissibility to answer the decision problems of AFs under grounded semantics.

The role and the relevance of strong admissibility semantics and grounded discussion games for AFs has been studied in [21,23,25]. That is, in these works it has been shown that strongly admissible extensions/labellings make a lattice with the maximum element being the grounded extension of a given AF. Therefore, the concept of strong admissibility semantics of AFs relates to grounded semantics of AFs in a similar way as the relation between admissible semantics of AFs and preferred semantics of AFs. That is, to answer the credulous decision problem of AFs under grounded semantics, it is sufficient to solve the decision problem for AFs under strongly admissible semantics, i.e., it is enough to indicate whether there exists a strongly admissible extension that contains a queried argument. Furthermore, it has been shown that the strong admissibility semantics and the corresponding discussion games may be the basis for an algorithm that can be used not only for answering the decision problem but also for human-machine interaction (cf. [12,29]). In addition, the computational complexity of strong admissibility of AFs has been analyzed [26,36].

It has been shown in [14] that each AF can be represented as an ADF; furthermore, it has been shown that ADFs provide all of Dung’s standard semantics, proposed in [34] for AFs, so there is no loss in semantic richness. By the use of general propositional formulas as argument acceptance conditions, ADFs allow for richer relations between arguments than AFs, which only allow attack. Because ADFs are at least as expressive as AFs, they can represent all important problem aspects that AFs can represent. However, some of the semantics of AFs have not yet been introduced for ADFs, namely, strongly admissible semantics. Because of the special structure of ADFs, the definition of strong admissibility semantics of AFs cannot be directly reused in ADFs. Because of the importance of the notion of strongly admissible semantics to investigate the acceptance of a queried argument under the grounded semantics, in the current work we introduce the concept of strongly admissible semantics of ADFs that satisfies/follows the same set of properties as this concept has in AFs, presented in Section 1.1. We do so not only because ADFs are generalisations of AFs, but also because ADFs are expressive enough to model a wide range of non-monotonic knowledge representation languages; furthermore, strongly admissible semantics play an important role in answering the credulous decision problem.

A main characteristic of strongly admissible semantics of ADFs is that they can be used to explain the answer to the question: ‘Why is an argument justified under grounded semantics of ADFs?’. For instance, suppose that an ADF is used to formalize a knowledge-base that presents methods to cure a disease or to make a decision in the legal domain. It is not enough to tell a patient or client that we pick a certain argument since it is presented in a semantics, but they to be convinced why this is the case. Moreover, having automated argumentation systems that can help people to make better choices is a goal of human-machine interaction [32,38]. To persuade agents to perform (or not to perform) a certain action, a user needs to have further explanation about the acceptance of arguments. To address this open problem, we previously considered grounded semantics of ADFs, since no one has any doubt on the evaluation of arguments in the grounded interpretation. Then, as a first remedy in [40], we introduced a discussion game to answer the credulous decision problem of ADFs under grounded semantics without constructing the full grounded interpretation of the given ADF. Subsequently, in the current work we propose the notion of strong admissibility semantics of ADFs. Both methods can be used to explain the truth values of arguments in the grounded interpretation. We think that grounded discussion games of ADFs and strong admissibility semantics of ADFs are two sides of the same coin. However, studying the relation between grounded discussion games, presented in [40], and the strong admissibility semantics of ADFs is beyond the scope of this work and is left for future research.

1.1.Requirements of strong admissibility semantics

As mentioned before, it is important to investigate whether a queried argument is in the grounded extension of an AF. This is mainly because each AF has a unique grounded extension and no one has any doubt on the acceptance of the arguments of the grounded extension. Furthermore, in applications it is significant not only to answer whether a queried argument is in the grounded extension but also to explain why it is so.

On the one hand, some discussion games have been presented to answer this decision problem under the grounded semantics [22,23,27,45]. That is, a queried argument belongs to the grounded extension of a given AF iff it is possible to win the associated discussion game. A web-based implementation of grounded discussion games is presented in [12]. On the other hand, the notion of strongly admissible semantics of AFs has been presented in [8,21,25]. to deal with the same issue. Furthermore, the role and the relevance of strong admissibility semantics of AFs in the Standard Grounded Game [45,53] and the Grounded Persuasion Game [27,28] has been studied in [21,25].

Similar to AFs, in ADFs the concept of grounded semantics is an important point of view on the acceptance of arguments. Each ADF has a unique grounded interpretation that presents the truth values of arguments about which no one has any doubt. Thus, it is crucial to investigate the truth value of a queried argument in the grounded interpretation of an ADF. Furthermore, it is required to explain why a queried argument has a specific truth value in the grounded interpretation. To investigate this issue in [40], the notion of discussion game for grounded semantics of ADFs has been presented. This game works locally by considering those ancestors of a certain argument that can affect the evaluation of the argument in the grounded interpretation. In this way, the grounded decision problem can be answered without constructing the full grounded interpretation. However, the notion of strongly admissible semantics has not yet been presented for ADFs to explain the reason for a truth value of a queried argument in the grounded interpretation. We show that the notion of strongly admissible semantics of ADFs presented in this work will satisfy the following conditions, which are akin to the properties of the notion of strongly admissible semantics of AFs.

  • Strong admissibility is defined in terms of strongly justified arguments.

  • Strongly justified arguments are recursively reconstructed from their strongly justified parents.

  • Each ADF has at least one strongly admissible interpretation.

  • The set of strongly admissible semantics of ADFs forms a lattice with the least element being the trivial interpretation and the maximum element being the grounded interpretation.

  • Strongly admissible semantics is used to answer whether an argument is justified in the grounded interpretation of a given ADF. This is because this notion has a close relation to the grounded semantics, in the formally precise sense that the maximal element of the lattice of strongly admissible interpretations is the grounded interpretation.

  • The notion of strongly admissible semantics of ADFs differs from the notions of admissible, conflict-free, complete and grounded semantics of ADFs.

  • The notion of strongly admissible semantics for ADFs is a proper generalization of strongly admissible semantics for AFs.

Our result leads to the presentation of an algorithm to answer the decision problem whether a given interpretation is a strongly admissible interpretation in a given ADF. In addition, since some generalizations of Dung’s AFs can be seen as special cases of ADFs, for instance, SETAFs [48], as shown in [51,52], and bipolar AFs [31,49,50], the notion of strongly admissible semantics presented for ADFs may carry over to these special cases. However, the focus of this work is to present a formal proof of clarifying the relation between strongly admissible semantics of AFs and ADFs.

This paper is structured as follows. In Section 2, we present the relevant background about AFs and ADFs. Then, in Section 3, the main contribution of our work is to introduce the concept of strongly admissible semantics for ADFs. Subsequently, we show that in each ADF, the set of strongly admissible interpretations forms a lattice with the trivial interpretation as the unique minimal element and the grounded interpretation as the unique maximal element. In Section 4 we show that the concept of strongly admissible semantics of ADFs is a generalization of the notion of strongly admissible semantics of AFs.

Section 5 presents an alternative definition for strongly admissible semantics of ADFs that is presented without referring to strongly justified arguments, when compared to the definition in Section 3. This definition also leads to a straightforward algorithm to answer the verification problem of ADFs under strongly admissible semantics. We also present an alternative definition for investigating whether a given argument is strongly justified in a given interpretation, which does not have the difficulties of the definition of strongly justified of arguments in an interpretation that is presented in Section 3. This method also leads to an algorithm to answer whether a given argument is a strongly justified argument in a given interpretation.

In Section 6, we present a finer relation between the sequence of strongly admissible extensions of a given AF and the sequence of strongly admissible interpretations constructed in the associated ADF. Finally, in Section 7, we present the conclusion of our work and we present some future research questions arising from this work.

A preliminary version of this article appeared as [41,42]. As a first addition to these previous works, we prove that strongly admissible semantics of ADFs form a generalization of strongly admissible semantics of AFs, presented in Section 4. Moreover the present paper contains new technical results including answering the verification problem under strong admissibility semantics of ADFs without considering whether all of the arguments that are presented in the given interpretation are strongly justified, reported in Section 5. In addition, in Section 5, we present a new method to investigate whether a given argument is strongly justified in a given interpretation. Further, in Section 6, we study finer relations between the sequence of strongly admissible extensions constructed based on a given extension of an AF and the sequence of strongly admissible interpretations of the associated ADF.

2.Formal background on argumentation frameworks

We assume that the reader is familiar with Dung’s abstract argumentation frameworks (AFs) [34], thus, we only briefly present the syntax of AFs. We then present the concept of strongly admissible semantics of AFs [8,21,25] and abstract dialectical frameworks (ADFs) [14,17,18].

2.1.Abstract argumentation frameworks

We start the preliminaries to our work by recalling the basic notion of Dung’s abstract argumentation frameworks (AFs). Subsequently, we introduce the extension-based definition of strong admissibility semantics of AFs due to Baroni and Giacomin [8], and the labelling-based definition of this concept due to Caminada and Dunne [25].

Definition 1

Definition 1([34]).

An abstract argumentation framework (AF) is a pair (A,R) in which A is a set of arguments and RA×A is a binary relation representing attacks among arguments.

Let F=(A,R) be a given AF. For each a,bA, the relation (a,b)R is used to represent that a is an argument attacking the argument b. An argument aA is, on the other hand, defended by a set SA of arguments (alternatively, the argument is acceptable with respect to S) (in F) if for each argument cA, it holds that if (c,a)R then there is an sS such that (s,c)R (s is called a defender of a). AF F is called a finite argumentation framework if A is a finite set of arguments. Note that in this work we assume that all AFs are finite.

Different semantics of AFs present which sets of arguments in a given AF can be jointly accepted.1 Set SA is called a conflict-free set (extension) (in F) if there are no a,bS such that (a,b)R. The characteristic function ΓF:2A2A is defined as ΓF(S)={a|a is defended by S}.

Definition 2.

Let F=(A,R) be an AF. A conflict-free set S is

  • admissible in F if SΓF(S);

  • preferred in F if S is ⊆-maximal admissible;

  • complete in F if S=ΓF(S);

  • grounded in F if S is the ⊆-least fixed point of ΓF;

  • ideal in F if it is a maximal admissible extension that is a subset of each preferred extension.

Example 1.

Let F=({a,b,c},{(a,b),(b,c)}) be an AF. In F, (a,b) means that argument a attacks b, and (b,c) means that b attacks c. Here, argument c is defended by set {a} (alternatively, c is acceptable with respect to {a}), since a attacks the attacker of c, namely b. The set of conflict-free sets of F is cf(F)={,{a},{b},{c},{a,c}}. Since ΓF2()={a,c}, the unique grounded extension of F is {a,c}. The intuition is that a is not attacked by any argument, thus no one has any doubt to accept argument a. Argument c is attacked by b, however, it is defended by a, which was accepted by everyone. Thus, {a,c} is the unique grounded extension of F.

Definition 3

Definition 3(from [8]).

Given an argumentation framework F=(A,R), aA and SA, it is said that a is strongly defended by S if and only if each attacker cA of a is attacked by some sS{a} such that s is strongly defended by S{a}.

In other words, a is strongly defended by S if for any attacker of a there exists a defender s for a in S that is not equal to a, i.e. sa, such that s is strongly defended by S{a}. In Example 1, argument c is strongly defended by set S={a,c}, since the attacker of c, namely b, is attacked by aS{c} and a is strongly defended by S{c}. Actually, a is strongly defended by S=, since a is not attacked by any argument.

Definition 4.

Given an AF (A,R) and set SA, it is said that S is a strongly admissible extension of S if every sS is strongly defended by S.

In Example 1, sets S1=, S2={a}, and S3={a,c} are strongly admissible extensions of F; all of them are subsets of the grounded extension of F. However, set S={c} is not a strongly admissible extension of F, since cS is not strongly defended by S. Because argument c is attacked by b, however, no argument in S{c} attacks b.

In [25], the concept of strongly admissible semantics of AFs is defined without having to refer to strong defence; we rephrase it in Definition 5, as follows.

Definition 5

Definition 5(from [25]).

Let F=(A,R) be an argumentation framework. We say that SA is a strongly admissible extension of F if and only if every aS is defended by some SS{a} which in its turn is a strongly admissible extension.

It is shown in [8] that strongly admissible semantics of an AF forms a lattice with the empty set as the least element and the grounded extension as the maximum element; we recall it in Theorem 1.

Theorem 1

Theorem 1(from [8]).

Let F be an AF. The set of strongly admissible semantics of F forms a lattice with the empty set as the least element and the grounded extension as the maximum element.

Theorem 1 presents a significant result that leads to the distinction between strongly admissible semantics and admissible and complete semantics of AFs. In [34] it is shown that the admissible extensions of a given AF form a semi-lattice with the empty set as the least element and the preferred extensions as its maximal elements. Furthermore, it has been shown in [34] that the complete extensions of a given AF form a semi-lattice with the grounded extension as its least element and the preferred extensions as its maximal elements. Finally, in [25] and [8], the relation between strongly admissible semantics of an AF and its admissible, conflict-free and grounded semantics is clarified; let us recall the properties in Proposition 2.

Proposition 2

Proposition 2(based on [8,25]).

Let F be an AF. The following properties hold for semantics of AF:

  • Each strongly admissible extension in F is an admissible extension and a conflict-free extension, however, the other direction does not hold.

  • Each strongly admissible extension of F is an admissible extension and it is a subset of the grounded extension of F, however, the other direction does not hold.

Proof.

Let F be an AF.

  • In Theorem 4 in [25] it has been proved that each strongly admissible extension in F is an admissible extension and a conflict-free extension. We provide a proof that the other direction does not hold, by giving a counter-example. Let F=({a,b},{(a,b),(b,a)}). Now the set S={a} is a conflict-free and admissible extension of F, however, it is not a strongly admissible extension in F. This is because there is no SS{a} that defends a against the attack of b.

  • It has been proved in [8] that the strongly admissible semantics of an AF form a lattice with the grounded extension as the maximum element. However, it does not hold that any admissible extension of a given AF that is a subset of the grounded extension is a strongly admissible extension. We provide a proof by giving a counter-example. Let F=({a,b,c},{(a,b),(b,c),(c,b)}). The grounded extension of F is {a,c}; furthermore, S={c} is an admissible extension of F. However, S is not a strongly admissible extension of F, since there is no SS{c} that defends c against the attack of b. □

The notion of an ideal extension is presented in Definition 2. In Definition 3.48 in [8], first the notion of ideal set is defined, then the notion of ideal semantics is presented; we rephrase this definition here. An admissible extension e is called ideal iff it is a subset of each preferred extension of F. The ideal extension of F is a maximal (with respect to set-inclusion) ideal set. We show that the strongly admissible extensions differ from the ideal sets and the ideal extension of a given AF.

Proposition 3.

The notion of strongly admissible semantics of AFs differs from the notion of ideal semantics of AF.

Proof.

We provide a proof by an example. Let F=({a,b},{(a,b),(b,a),(b,b)}), as depicted in Fig. 1. The unique grounded extension of F is the empty set. The set of strongly admissible extensions of F is {}. However, the set of ideal sets of F is {,{a}}. Thus, {a} is the ideal extension of F. As we see, the set of strongly admissible extensions of F is neither equal with the set of ideal sets of F nor is it equal with the ideal extension of F.  □

Fig. 1.

AF of Proposition 3.

AF of Proposition 3.

It is also possible to define the semantics of AFs in terms of argument labellings [20,30,58].

Definition 6

Definition 6([25, Definition 4]).

Let F=(A,R) be an argumentation framework. An argument labelling is a function L:A{in,out,undec}. An argument labelling is called an admissible labelling if and only if L is a total function and for each aA it holds that:

  • if L(a)=in, then for each b that attacks a it holds that L(b)=out,

  • if L(a)=out, then there exists a b that attacks a such that L(b)=in.

A labelling account of strong admissibility semantics of F is presented in [25]; we recall this definition in Definition 8, to use it in the proofs of theorems of Section 4, in order to show that strongly admissible semantics of ADFs form a generalization of strongly admissible semantics of AFs. To this end, let us first rephrase the concept of min-max numbering in Definition 7.2

Specifically, in Lemma 22 we use the notion of strongly admissible labelling of AFs, which is defined in terms of min-max numbering (Definition 8) to show that the map of each strongly admissible labelling in a given AF F is a strongly admissible interpretation of the associated ADF DF, and vice versa. That is, we show that there is a one-to-one relation between the set of strongly admissible labellings in a given AF F and the set of strongly admissible interpretations of the associated ADF DF.

Definition 7.

Let L be an admissible labelling of argumentation framework F=(A,R). A min-max numbering is a total function MML:in(L)out(L)N such that for each ain(L)out(L) it holds that:

  • if L(a)=in, then MML(a)=max({MML(b)|(b,a)R and L(b)=out})+1 (with max() defined as 0);

  • if L(a)=out, then MML(a)=min({MML(b)|(b,a)R and L(b)=in})+1 (with min() defined as ).

Theorem 4

Theorem 4([25, Theorem 6]).

Every admissible labelling has a unique min-max numbering.

Definition 8

Definition 8([25, Definition 10]).

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

Example 2.

Let F=({a,b,c,d},{(a,b),(c,d),(d,c)}). By Definition 7, admissible labelling {ain,bout,cin,dout} has a unique min-max numbering {(a:1),(b:2),(c:),(d:)}. However, this admissible labelling is not a strongly admissible labelling in F, since the MML(c)=MML(d)=. On the other hand, the admissible labelling {ain,bout,cundec,dundec} has a unique min-max numbering {(a:1),(b:2)}, since both MML(a) and MML(b) are finite, so by Definition 8, it is a strongly admissible interpretation in F.

In [6], both extension-based and labelling-based approaches of semantics of AFs are presented. Moreover, two functions are defined to map extension-based semantics of a given AF F to labelling-based semantics and vice versa, to show that each extension-based semantics of AF has a labelling-based semantics reformulation and vice versa. Namely, Ext2Lab(λ) is used to present the extension form of labelling λ of F, and Lab2Ext(e) is used to present the labelling form of the extension e of F; we recall them in Definitions 910.

Definition 9

Definition 9([6, Definition 3.6]).

Let F=(A,R) and let S be an extension of F. For aA, we write a+={b|(a,b)R} and S+={a+|aS}. If S is a conflict-free set of F, then the corresponding labelling is defined as Ext2Lab(S)={S,S+,A(SS+)}.

Function Ext2Lab(.) in Definition 9 is such that arguments of S are labelled in, elements of S+ are labelled out and all other arguments of A are labelled undec. The alternative way of presenting Ext2Lab(.) is as follows.

Ext2Lab(S)(a)=in if aS,out if aS+,undecotherwise.

Definition 10

Definition 10([6, Definition 2.7]).

Given an argumentation framework F=(A,R) and a labelling λ, the corresponding set of arguments Lab2Ext(λ) is defined as Lab2Ext(λ)=in(λ). That is, Lab2Ext(λ) is the set of all arguments that are labelled in in λ.

Proposition 5

Proposition 5([6, Proposition 3.14]).

For any argumentation framework F=(A,R), it holds that:

  • if S is a strongly admissible set of F, then Ext2Lab(S) is a strongly admissible labelling of F;

  • if λ is a strongly admissible labelling of F, then Lab2Ext(λ) is a strongly admissible set of F.

2.2.Abstract dialectical frameworks

In the current section, we briefly restate some of the key concepts of abstract dialectical frameworks that are derived from those given in [14,15,17,18].

Definition 11.

An abstract dialectical framework (ADF) is a tuple F=(A,L,C) where:

  • A is a set of arguments (statements, positions), denoted by letters;

  • LA×A is a set of links between arguments;

  • C={φa}aA is a collection of propositional formulas over arguments, called acceptance conditions.

An ADF can be represented by a graph in which nodes indicate arguments and links show the relation among arguments. Each argument a in an ADF is labelled by a propositional formula, called acceptance condition, φa over par(a) such that par(a)={b|(b,a)L}. An argument a is called an initial argument if par(a)={}. The acceptance condition of an argument clarifies under which condition the argument can be accepted [14,17,18]. Furthermore, acceptance conditions indicate the set of links implicitly. Thus, in a concrete example of ADFs, we oftentimes only define acceptance conditions explicitly and implicitly define links via the variables of the propositional formulas.

Remark.

ADF D=(A,L,C) is called a finite abstract dialectical framework if A is a finite set of arguments. Note that in this work we assume that all ADFs are finite.

Example 3.

An example of an ADF D=(A,L,C) is shown in Fig. 2, which contains four arguments, i.e., A={a,b,c,d}. Dependencies between arguments are shown by the directed edges in the associated graph, and acceptance conditions are shown as propositional formulas attached to each node. The acceptance condition of an argument clarifies the set of parents of the argument, thus, there is no need of presenting L in D explicitly. Furthermore, an acceptance condition of an argument indicates under which condition the argument can be accepted/denied. For instance, the acceptance condition of c, namely φc:¬bd, says that c depends on b and d, i.e., par(c)={b,d}, and it states that c can be accepted if b is denied and d is accepted. In this ADF, the arguments a and d are initial arguments, since par(a)=par(d)={}. The acceptance condition of a, namely φa:, says that a is always accepted and the acceptance condition of d, namely φd:, says that d is always denied.

Fig. 2.

ADF of Examples 3, 5 and 7.

ADF of Examples 3, 5 and 7.

An interpretation v (for D) is a function v:A{t,f,u} that maps arguments to one of the three truth values true (t), false (f), or undecided (u). The interpretation v is called trivial, and v is denoted by vu, if v(a)=u for each aA. Moreover, v is called a two-valued interpretation if for each aA either v(a)=t or v(a)=f.

Truth values can be ordered via the information ordering relation <i given by: u<it and u<if and no other pair of truth values are related by <i. Relation i is the reflexive and transitive closure of <i. The pair ({t,f,u},i) is a complete meet-semilattice with the meet operator i, such that tit=t and fif=f, while it returns u otherwise. The meet of two interpretations v and w is then defined as (viw)(a)=v(a)iw(a) for all aA.

Let V be the set of all interpretations for an ADF D. It is said that an interpretation v is an extension of another interpretation w, if w(a)iv(a) for each aA, denoted by wiv. Furthermore, if both viw and wiv hold, then v and w are equivalent, denoted by viw. Interpretations v and w are incomparable if neither w≰iv nor v≰iw, denoted by wiv.

For reasons of brevity, we will sometimes shorten the notion of three-valued interpretation v={a1t1,,amtm} with arguments a1,,am and truth values t1,,tm as follows: v={ai|v(ai)=t}{¬ai|v(ai)=f}. For instance, v={af,bt}={¬a,b}. Furthermore, in the current work we say that the truth value of a is presented in v, if v(a){t,f} also denoted as v(a)=t/f. Interpretations can be ordered via i with respect to their information content.

Semantics for ADFs can be defined via the characteristic operator ΓD, which maps interpretations to interpretations. Given an interpretation v (for D), the partial valuation of φa by v is v(φa)=φav=φa[b/:v(b)=t][b/:v(b)=f], for bpar(a).

Definition 12.

Let D be an ADF and let v be an interpretation of D. Applying ΓD on v leads to v such that for each aA, v is as follows:

ΓD(v)(a)=v(a)=tif φav is irrefutable (i.e., φav is a tautology),fif φav is unsatisfiable (i.e., φav is a contradiction),uotherwise.

Intuitively, the characteristic operator ΓD assigns an argument a to t (f) if the partial evaluation of the acceptance condition of a by a given interpretation is irrefutable (unsatisfiable, respectively). Note that the operator ΓD is i-monotonic, that is, when viw for interpretations v and w, then ΓD(v)iΓD(w).

Example 4.

Consider ADF D=({a,b,c,d},{φa:,φb:a¬c,φc:¬bd,φd:}) from Example 3 and the trivial interpretation vu of D. We calculate v=ΓD(vu) over all the arguments of D. Consider argument a; since φa:, it holds that φavu:, that is, φavu is irrefutable. Thus, a is assigned to t in v. However, since both of the parents of b, namely, a and c are assigned to u in vu, it holds that φbvu=φb, which is neither a tautology nor unsatisfiable. Thus, v(b)=ΓD(vu)(b)=u. By the same reason, it holds that v(c)=ΓD(vu)(c)=u. However, it holds that φdvu:, that is, φdvu is unsatisfiable. Thus, v(d)=ΓD(vu)(d)=f. Hence, v={at,bu,cu,df}.

If we apply the characteristic operator ΓD over v, then since ΓD is a monotonic operator, the truth values of a and d in ΓD(v) are equal to v(a) and v(d), respectively. Since φcv=¬b, it holds that ΓD(v)(c)=f. However, since φbv=¬c=¬c, it holds that ΓD(v)(b)=u. Thus, ΓD(v)={at,bu,cf,df}.

The semantics of ADFs, as defined by [15], are based on (collections of) three-valued interpretations and can be defined via the characteristic operator as follows.

Definition 13.

Given an ADF D, an interpretation v is:

  • conflict-free iff v(s)=t implies φsv is satisfiable and v(s)=f implies φsv is unsatisfiable;

  • admissible in D iff viΓD(v);

  • preferred in D iff v is i-maximal admissible;

  • complete in D iff v=ΓD(v);

  • the grounded interpretation of D iff v is the least fixed point of ΓD.

The set of all σ interpretations for an ADF F is denoted by σ(F), where σ{cf,adm,prf,com,grd} abbreviate the different semantics in the obvious manner. In any ADF D, it holds that prf(D)com(D)adm(D)cf(D) and grd(D)com(D).

The intuitions behind the semantics of ADFs are as follows. In ADFs an interpretation is called admissible if it does not contain any unjustifiable information. An interpretation is called preferred if it represents maximum information about arguments without losing admissibility. Thus, each admissible interpretation is contained in a preferred interpretation. That is, to answer the credulous decision problem under preferred semantics (i.e., to investigate whether there is a preferred interpretation that contains the truth value of a given argument), it is sufficient to answer the problem under admissible semantics. An interpretation is complete if it exactly contains the relevant justifiable information. Finally, an interpretation is grounded if it collects all the information that is beyond any doubt.

Example 5.

Let us consider again ADF D=({a,b,c,d},{φa:,φb:a¬c,φc:¬bd,φd:}) from Example 3. Furthermore, consider several three-valued interpretations {v0,v1,v2,v3,v,v} as shown in Table 1. We investigate whether they are part of certain semantics. Since for each i with 0i3 it holds that viiΓD(vi), it holds that each vi for i with 0i3 is an admissible interpretation of D. In general, each admissible interpretation is a conflict-free interpretation. Thus, each vi for i with 0i3 is a conflict-free interpretation of D. The interpretation v3 is a complete interpretation of D, since ΓD(v3)=v3. Furthermore, v3 is the grounded interpretation of D, since it the least fixed point of ΓD. In addition, v3 is a maximal admissible interpretation of D, therefore, v3 is a preferred interpretation of D.

Note that the interpretation v is not a(n) admissible/preferred/complete/the grounded interpretation of D, since ΓD(v)={at,bu,cf,df}, that is, v≰iΓD(v). However, v is a conflict-free interpretation of D. The truth value of b is assigned to t in v. Thus, to show that v is a conflict-free interpretation of D, it is enough to check whether φbv is satisfiable. Since φbv is indeed satisfiable, it holds that v is a conflict-free interpretation of D.

Furthermore, for v it holds that ΓD(v)={a,¬d}. Thus, since v≰iΓD(v), it holds that v is not a(n) admissible/preferred/complete/the grounded interpretation of D. To check whether v is a conflict-free interpretation, we have to check whether φdv is satisfiable. Since φdv is unsatisfiable, it holds that v is not a conflict-free interpretation of D.

Table 1

Interpretations for the ADF from Example 5

InterpretationabcdΓDPart of semantics
v0=vuuuuuΓD(vu)=v1cf,adm
v1tuufΓD(v1)=v2cf,adm
v2tuffΓD(v2)=v3cf,adm
v3ttffΓD(v3)=v3cf,adm,prf,grd,com
vutuuΓD(v)=v2cf
vuuutΓD(v)=v1

The semantics for ADFs generalize the semantics for AFs. Definition 14 presents the associated ADF for a given AF.

Definition 14.

For an AF F=(A,R), define the ADF associated with F as DF=(A,R,C) with C={φa}aA such that for each aA the acceptance condition is as follows:

φa=(b,a)R¬b

For instance, the associated ADF DF to the AF F presented in Example 1, i.e., F=({a,b,c},{(a,b),(b,c)}), is DF=(A,R,{φa:,φb:¬a,φc:¬b}). In [17, Theorem 2], it is shown that: an extension is admissible, complete, preferred, grounded for F iff it is admissible, complete, preferred, grounded for DF. The notion of an argument being acceptable and the symmetric notion of an argument being deniable in an interpretation are defined as follows.

Definition 15.

Let D=(A,L,C) be an ADF and let v be an interpretation of D.

  • An argument aA is called acceptable with respect to v if φav is irrefutable.

  • An argument aA is called deniable with respect to v if φav is unsatisfiable.

For instance, considering ADF D of Example 3, it holds that a is acceptable with respect to v={at,bu,cu,df}.

One of the main decision problems of ADFs is whether an argument is credulously acceptable (deniable) under a type of semantics, presented in Definition 16.

Definition 16.

Given an ADF D=(A,L,C), an argument aA and a semantics σ{adm,prf,com,cf,grd}. Argument a is credulously acceptable (deniable) under σ if there exists a σ interpretation v of D such that v(a)=t (v(a)=f, respectively). This reasoning task is denoted by Credσ(at/f,D).

Considering ADF of Example 3, it holds that b is credulously acceptable under σ for σ{adm,prf,com,cf,grd} in D. This is because v3, as it is shown in Table 1, is a σ-interpretation for σ{adm,prf,com,cf,grd} with v3(b)=t. However, b is not credulously deniable under σ for σ{adm,prf,com,grd} in D. The only preferred/complete/grounded interpretation of D is v3, which assigns b to t. Thus, b is not credulously deniable under σ-semantics, for σ{prf,com,grd}. Since each admissible interpretation must be equally or less informative than a preferred interpretation, b is not credulously deniable under admissible semantics of D.

Thanks to the fact that in an ADF D each preferred interpretation is a i-maximal admissible (complete) interpretation of D, it holds that the credulous decision problems under admissible, complete, and preferred semantics coincide.

In ADFs, relations between arguments can be classified into four types, reflecting the relationship of attack and/or support that exists between the arguments. These are listed in Definition 17. Further, we denote the update of an interpretation v with a truth value x{t,f,u} for an argument b by v|xb, i.e. v|xb(b)=x and v|xb(a)=v(a) for ab.

Definition 17.

Let D=(S,L,C) be an ADF. A relation (b,a)L is called

  • supporting (in D) if for every two-valued interpretation v, v(φa)=t implies v|tb(φa)=t;

  • attacking (in D) if for every two-valued interpretation v, v(φa)=f implies v|tb(φa)=f;

  • redundant (in D) if it is both attacking and supporting;

  • dependent (in D) if it is neither attacking nor supporting.

Example 6.

Consider the acceptance condition of φa:b¬c for argument a. By φa the set of parents of a is {b,c}. Thus, we clarify the type of (b,a) and (c,a). There are three satisfying two-valued interpretations, i.e., v1={bt,ct}, v2={bt,cf} and v3={bf,cf}, and one that does not satisfy the formula, i.e., v4={bf,ct}. By the definition of supporting links we have to check that whether vi(φa)=t for i with 1i3 implies vi|tb(φa)=t. Since for i with 1i3, vi(φa)=t implies vi|tb(φa)=t, it holds that (b,a) is a supporting link. Furthermore, since v4(φa)=f but v4|tb(φa)=t, link (b,a) is not an attack link.

Moreover, since v3(a)=t but v3|tc(φa)=f, it holds that (c,a) is not a support link. However, it holds that v4(φa)=f and v4|tc(φa)=f. Thus, (c,a) is only an attacking link.

As an example for a link that is both attacking and supporting, consider φa:b¬b. There are two satisfying two-valued interpretations for the formula, i.e., v1={bt} and v2={bf}. Since for i with 1i2 it holds that vi(φa)=t implies vi|tb(φa)=t, it holds that (b,a) is a supporting link. Furthermore, since there is no two-valued interpretation that does not satisfy the formula, the link (b,a) is also an attacking link. Thus, (b,a) is a redundant link in φa:b¬b.

As an example for a link that is neither an attacking nor supporting, consider φa:(¬cb)(c¬b). Let v={bf,cf} be a two-valued interpretation that satisfies the formula. However, v|tb(φa)=f. Thus, (b,a) is not a support link. Further, let v={bf,ct} be a two-valued interpretation that does not satisfy the formula. However, it holds that v|tb(φa)=t. Thus, (b,a) is not an attacking. Hence (b,a) is a dependent link.

3.The strongly admissible semantics for ADFs

In the following, we present the concept of strong admissibility semantics for ADFs. As we discussed in the introduction, we are aiming to generalize the notion of strong admissibility semantics of AFs, so that the concept of strong admissibility semantics of ADFs relates to grounded semantics of ADFs in a similar way as the concept of admissible semantics of ADFs relates to preferred semantics of ADFs. As we mentioned in the introduction, following the definition by Baroni and Giacomin [8], Caminada showed in [21,23] that strong admissibility plays a critical role in discussion games for AFs under grounded semantics [21,25]. In [40], we introduced a discussion game to answer the credulous decision problem of ADFs under grounded semantics without constructing the full grounded interpretation of the given ADF. However, the concept of strong admissibility semantics of ADFs has not been introduced in the literature so far. This was a motivation for us to present the notion of strong admissibility semantics for ADFs and study the characteristics of this concept. Similarly to the AF case, a strongly admissible interpretation of an ADF may be used not only to answer the credulous decision problem, but also to explain why an argument is justified in the grounded interpretation.

In ADFs, beside an argument being acceptable in an interpretation, there is a symmetric notion of an argument being deniable. In contrast with Definition 4, in which the concept of strong admissibility semantics of AFs is defined based on the concept of strongly defended arguments, in ADFs we define the concept of strong admissibility semantics based on the concept of strongly acceptable/deniable arguments. To this end, in Definition 18 we introduce the notion of strong justification (i.e., strongly accepted/denied) of an argument in an ADF in a given interpretation.

Note that in the following, v|P is equal to v(p) for any pP; however, it assigns all other arguments that do not belong to P to u, i.e., v|P=vu|v(p)pP.

Definition 18.

Let D=(A,L,C) be an ADF and let v be an interpretation of D. Argument a is a strongly justified argument in interpretation v with respect to set E if one of the following conditions hold:

  • v(a)=t and there exists a subset of parents of a excluding E, namely Ppar(a)E such that (a) a is acceptable with respect to v|P and (b) all pP are strongly justified in v w.r.t. set E{p}.

  • v(a)=f and there exists a subset of parents of a excluding E, namely Ppar(a)E such that (a) a is deniable with respect to v|P and (b) all pP are strongly justified in v w.r.t. set E{p}.

An argument a is strongly acceptable, respectively strongly deniable, in v if v(a)=t, resp. v(a)=f, and a is strongly justified in v with respect to set {a}. We say that an argument is strongly justified in v if it is either strongly acceptable or deniable in v.

Note that in Definition 18, the set of parents of a can be the empty set, i.e., P=. If the set P of parents of an argument is empty, then v|P=vu. In this case, a is strongly acceptable/deniable in v if φavu is irrefutable/unsatisfiable, respectively. In other words, if P=, then a is strongly acceptable/deniable in v if a is acceptable/deniable in v and v(a)=t/f. Furthermore, we say that a is not strongly justified in an interpretation v if there is no set of parents of a that satisfies the condition of Definition 18 for a.

Since the class of ADFs is a generalization of the class of AFs (see Definition 14), in the following, we informally discuss why Definition 18 can be viewed as a generalization of Definition 3 for AFs. In Section 4, we formally show that the strongly admissible semantics of ADFs is a proper generalization of strongly admissible semantics of AFs.

In the two items of Definition 18, the set P contains exactly those parents of a, excluding a, that satisfy v(a) and of which the truth value is presented in v. Definition 18 presents the same idea as Definition 3: that an argument a is strongly defended (accepted) if it can be defended by some arguments other than itself. Furthermore, each defender of a has to be strongly defended. Akin to AFs, in ADFs an argument a is strongly justifiable if its truth value is justified by some arguments other than itself, where each of those other arguments is strongly justified.

The notion of strong acceptability/deniability of arguments in a given interpretation is illustrated in Example 7.

Example 7.

Consider the ADF presented in Example 3, i.e., D=({a,b,c,d},{φa:,φb:a¬c,φc:¬bd,φd:}), depicted in Fig. 2. Let v={au,bt,cf,df}. We show that c and d are strongly justified in v and b is not strongly justified in v. Since v(c)=v(d)=f, we show that c and d are strongly deniable in v. First, since φdvu and v(d)=f, it holds that d is strongly deniable in v.

Furthermore, to show that c is strongly deniable in v, we show that c is strongly deniable in v with respect to E={c}. We choose a subset of parents of c excluding c, namely, P={d}. It is easy to check that φcv|P is unsatisfiable, i.e., φcv|Pφcv|d. Now we have to show that each pP is strongly justified in v. The only parent of c in P is d. Since dP, v(d)=f and d is also strongly deniable in v, it holds that c is strongly deniable in v.

To show that b is not strongly justified in v, since v(b)=t, we show that b is not strongly acceptable in v. Toward a contradiction, assume that b is strongly acceptable in v. Thus, we have to choose a set P of parents of b that satisfies φbv|P. Let P=par(b). Since φbv|P, there is no subset of par(b) that satisfies the conditions of Definition 18 for b. Therefore, b is not strongly acceptable in v.

Note that in Example 7, if we choose a set of parents of c equal to {b}, then we cannot show that c is strongly deniable in interpretation v. While the first condition of strong deniability holds for c, i.e., φcv|b, the second condition does not hold, i.e., b is not strongly acceptable in v, as is shown in Example 7. This shows the importance of choosing a right set of parents that satisfies the conditions of Definition 18 for a queried argument.

However, there exists an alternative definition for strongly justified of arguments, which we present in Definition 31, in which there is no need of indicating a set of parents of a queried argument. In order to prove the main result of this section, which is that the set of strongly admissible interpretations forms a lattice, we need some auxiliary results that are proven based on the current definition of an argument being strongly justified in an interpretation, i.e., Definition 18.

In Definition 19, similar to Definition 4, we introduce the concept of strong admissibility of interpretation v of a given ADF, using the notion of strong justifiability of arguments presented in v.

Definition 19.

Let D=(A,L,C) be an ADF and let v be an interpretation of D. An interpretation v is a strongly admissible interpretation if for each a such that v(a)=t/f, we have that a is a strongly justified argument in v.

The set of all strongly admissible interpretations of ADF D is denoted by sadm(D).

To clarify the notion of strongly admissible interpretations of ADFs, we continue Example 7 in Example 8.

Example 8.

Consider ADF of Example 7, i.e., D=({a,b,c,d},{φa:,φb:a¬c,φc:¬bd,φd:}), depicted in Fig. 2. Let v={au,bt,cf,df}. As was shown in Example 7, c and d are strongly deniable in v. However, b is not strongly justified in v. Thus, v is not a strongly admissible interpretation of D. However, v1={at,bu,cu,du}, v2={au,bu,cf,df}, v3={at,bt,cf,df} are strongly admissible interpretations of D. We show that b is strongly acceptable in v3. To this end, let P={a,c} be a set of parents of b. First, it holds that φbv3|P. Thus, the first condition is satisfied for b. We also have to check whether each parent of b in P is also strongly justified in v3. To this end, we show that a is strongly acceptable in v3 and c is strongly deniable in v3. The latter is obvious by the method that was presented in Example 7 to show that c is strongly deniable in v. In addition, φavu, thus, a is strongly acceptable in v3. Hence, b and a are strongly justified in v3. Thus, v3 is a strongly admissible interpretation of D. Furthermore, v3 is a unique grounded interpretation of D.

In Example 8, c is strongly deniable both in v2 and v3, however, v2 presents less information than v3. Interpretation v2 explains that c is strongly deniable in a strongly admissible interpretation, in other words, c is credulously deniable in the grounded interpretation of D, since its parent d is strongly deniable in v2. Based on the acceptance condition of c, namely φc:¬bd, this piece of information about parents of c is enough to convince a user about the truth value of c in a strongly admissible interpretation and the grounded interpretation as well. That is, to convince a user about the truth value of c in the grounded interpretation of D, there is no need of further information about the truth values of a and b in the grounded interpretation. We are interested in finding a strongly admissible interpretation with the least amount of information in which the truth value of a queried argument is satisfied.

Definition 20.

Let D be an ADF, let a be an argument and let v be a strongly admissible interpretation of D. Interpretation v is called a least witness of strong justifiability of a if the following conditions hold.

  • v(a)=t/f;

  • there is no strongly admissible interpretation v where v(a)=t/f and viv.

Note that if argument a is strongly justified in an interpretation, then there exists a strongly admissible interpretation that is a least witness of strong justifiability of a. Intuitively, the reason is that the number of arguments of a given ADF is finite, so one can guess an interpretation v and check whether it the least witness of strong justifiability of a. More formally, to find a least witness of strong justifiability of a, follow the following steps:

  • (1) Guess an interpretation v.

  • (2) Check whether v is a strongly admissible interpretation. If the answer is yes, then go to item 3, else go to item 1.

  • (3) Check whether v(a)=t/f. If the answer is yes, then go to item 4, else go to item 1.

  • (4) Pick v where v<iv and check if v(a)=t/f and v is a strongly admissible interpretation. If the answer is yes, then replace v with v and repeat this item, else pick another v and repeat this item.

  • (5) If there is no v that satisfies item 4, then v is a least witness of strong justifiability of a.

For instance, in Example 8, interpretation v2 is a least witness of strong justifiability (or deniability) of c. This is because v2 contains the truth values of c and d, and the truth value of d is the necessary and sufficient piece of information needed for denying c in the grounded interpretation.

Note that an argument may have more than one least witness of strong justification. For instance, let D=({a,b,c},{φa:,φb:ab,φc:}). Argument b is strongly acceptable in both v1={a,b} and v2={b,c}; furthermore, by Definition 20, both v1 and v2 are least witnesses of strong justifiability of b in D. We now define the maximum level of a in a least witness of strong justifiability of a; see Definition 21.

Definition 21.

Let D be an ADF, let v be a strongly admissible interpretation of D that is a least witness of strong justification of a, and let P=par(a)(vtvf). The maximum level of a with respect to a least v is a function that assigns a natural number to a, denoted by Mv, as follows:

  • if P=, then Mv(a)=1;

  • if P, then Mv(a)=max{Mv(p)|pP}+1

For instance, in Example 8, the maximum level of c with respect to the least witness v2 is 2. This is because the maximum level of d in v2 is 1. Intuitively, a least witness v of strong justification of a collects exactly the truth values of those ancestors of a that have a crucial role in the truth value of a. A maximum level of a in v presents the distance of a from an initial ancestor of a that may have an effect on the truth value of a in a strongly admissible interpretation of a given ADF. Example 9 is an instance of an ADF with a redundant link.

Example 9.

Let D=({a,b},{φa:b¬b,φb:b}) be an ADF, depicted in Fig. 3. We show that v={at,bu} is a strongly admissible interpretation of D. To this end, we show that a is strongly acceptable in v with respect to E={a}. Now let P=. It is clear that φavu is irrefutable. Thus, a is strongly acceptable in v. Furthermore, v is a least witness of strong acceptability of a and by Definition 21, the maximum level of a in v is 1.

Fig. 3.

ADF of Examples 9.

ADF of Examples 9.

Example 10 presents the associated ADF DF to the AF F presented in Example 2.

Example 10.

Consider AF F=({a,b,c,d},{(a,b),(c,d),(d,c)}) and the associated ADF DF=({a,b,c,d},{φa:,φb:¬a,φc:¬d,φd:¬c}). The set of all strongly admissible interpretations of DF is as follows: sadm(DF)={{},{a},{a,¬b}}. For instance, interpretation v={a,¬b} is a strongly admissible interpretation of DF. To substantiate our claim, we show that a is strongly acceptable in v and b is strongly deniable in v. The former one is clear, since φavu. For the latter one, let P={a} be a set of parents of b. First, it holds that φbv|a; second, a is strongly acceptable in v. Thus, b is strongly deniable in v. Hence, v is a strongly admissible interpretation of D. Furthermore, v is a least witness of strong deniability of b and the maximum level of b in v is 2.

Lemma 6 shows that if v is a least witness of strong justification of a, then the maximum level of a in v is finite in a given ADF.

Lemma 6.

Let D be an ADF, let a be an argument, and let v be a strongly admissible interpretation of D that is a least witness of strong justification of a. It holds that a has a finite maximum level in v.

Proof.

Toward a contradiction, assume that a is an argument with infinite maximum level in v. Therefore, by Definition 21, the set of parents of a, namely P with φav|P, is a non-empty set. Further, there exists an argument p in P{a} with infinite maximum level. By the same reason, p has a parent with infinite maximum level that is neither equal to a nor p, and so on. Thus, a has an infinite number of ancestors. This contradicts the assumption that D is a finite ADF. Thus, the assumption that a has an infinite maximum level is wrong. □

Corollary 7 is a direct result of Lemma 6 together with the second item of Definition 21.

Corollary 7.

Let D be an ADF, let a be an argument, and let v be a strongly admissible interpretation of D that is a least witness of strong justification of a. Let the maximum level of a in v be m, and let P=par(a)(vtvf), then the maximum level of each parent of a, i.e., each pP, in v is less than m.

Lemma 8 presents the monotonic characteristic of strongly justified arguments, i.e., if a is strongly justifiable in v and viv, then a is strongly justifiable in v.

Lemma 8.

Let D be an ADF. If aA is strongly justifiable in interpretation v of D and viv, then a is also strongly justifiable in v.

Proof.

We show the lemma for the case that a is strongly acceptable in v; the proof method for the case that a is strongly deniable in v is similar. Assume that v is also a least witness of strong justification of a. We complete the proof by induction on the maximum level of argument a in v.

Base case: let a be an argument of the maximum level 1 that is strongly acceptable with respect to v. Therefore, φavu. Thus, a is clearly strongly acceptable with respect to v.

Induction hypothesis: Assume that the property holds for each argument of the maximum level j with 1j<i in v, i.e., if a is an argument with the maximum level j in v, then a is strongly justified in v.

Inductive step: We show that this property also holds for arguments of level i. That is, if a is an argument with the maximum level i in v, then a is strongly acceptable in v. Let a be an argument of the maximum level i. Since a is strongly acceptable in v, by Lemma 8, the maximum level i of a is a finite number. Since a is strongly acceptable in v, there exists a set of parents P of a excluding a where a is acceptable with respect to v|P and all pP are strongly justified in v. Since viv, it holds that Pvtvf. Thus, it holds that a is acceptable with respect to v|P. We have to show that each pP is strongly justified in v. By Corollary 7, the maximum level of each pP is at most i1 in v. Thus, by induction hypothesis, p is strongly justified in v. Therefore, the second condition of strong acceptability of a in v also holds. Thus, a is strongly acceptable in v. □

A sequence of interpretations for a given ADF D, each member of which is strongly admissible, is presented in Lemma 9. In Lemma 10, it is shown that the maximum element of this sequence is the grounded interpretation of D.

Lemma 9.

Let D be an ADF, let v0=vu and let vi=ΓD(vi1) for i>0. For each 0i it holds that:

  • viivi+1;

  • vi is strongly admissible interpretation of D.

Proof.

  • The first item holds because the characteristic operator is a monotonic function.

  • We show by induction on i that each vi is a strongly admissible interpretation.

    Base case: For i=0, it is clear that v0=vu is a strongly admissible interpretation.

    Induction hypothesis: Assume that each vj for j with 0j<i is a strongly admissible interpretation.

    Inductive step: We show that vi is a strongly admissible interpretation. Let a be an argument that is assigned to either t or f in vi. We show that a is strongly justifiable in vi. If at/fvi1, then there is nothing to prove, since by the induction hypothesis vi1 is a strongly admissible interpretation. Thus, a is strongly justified in vi1, and since vi1ivi, by Lemma 8, a is strongly justifiable in vi.

    Assume that atvi and auvi1. We show that a is strongly acceptable in vi. For the case that afvi, the proof follows a similar method. Since vi(a)=t, we can conclude that φavi1 is irrefutable. Let P be a subset of parents of a the truth value of which appears in vi1 and φavi1|P. Otherwise, φavi1 cannot be irrefutable. Assume that P{}, otherwise, there is nothing to prove. Let pP. Since pt/fvi1 for each pP, p is strongly justifiable in vi by the induction hypothesis. Thus, by Lemma 8, p is strongly justifiable in vi. Thus, both conditions of Definition 18 hold for a in vi. Therefore, for an arbitrary argument a, if vi(a)=t/f, then it holds that a is strongly justifiable in vi. Thus, vi is a strongly admissible interpretation. Hence, every interpretation in the sequence vu,ΓD(vu), is a strongly admissible interpretation. □

Lemma 10.

Let D be an ADF.

  • D has at least one strongly admissible interpretation.

  • The least strong admissible interpretation of D, with respect to the i ordering, is the trivial interpretation.

  • The maximal strongly admissible interpretation in the sequence of interpretations as in Lemma 9, with respect to the i ordering, is the unique grounded interpretation of D.

Proof.

  • The first and the second item of the lemma are clear by Lemma 9, which says that vu is a strongly admissible interpretation.

  • By definition, the grounded interpretation of D is the least fixed-point of the characteristic operator. By Lemma 9, each element of the sequence ΓDn(vu), for n with n>0, is a strongly admissible interpretation. Since the number of arguments is finite, this sequence has a limit; that is, there exists an m with m>0 where ΓDm(vu)=ΓDm+1(vu). Therefore, the limit of this sequence, namely ΓDm(vu), which is the grounded interpretation of D, is also a strongly admissible interpretation. Note that the nth power of ΓD is defined inductively, that is, ΓDn=ΓD(ΓDn1). □

In Theorem 11, we show that each strongly admissible interpretation is an admissible interpretation as well as conflict-free. However, the other direction of the following theorem does not work.

Theorem 11.

Let D=(A,L,C) be an ADF and let v be a strongly admissible interpretation of D. Then the following hold:

  • v is an admissible interpretation of D.

  • v is a conflict-free interpretation of D.

Proof.

  • Let v be a strongly admissible interpretation of D. We show that v is an admissible interpretation. Toward a contradiction, assume that v is not an admissible interpretation, that is, v≰iΓ(D)(v). Therefore, there exists an a such that v(a)=t/f but ΓD(v)(a)t/f. By the assumption, v is a strongly admissible interpretation. That is, if v(a)=t/f, then a is strongly acceptable/deniable in v. Thus, there exists a subset of parents P of a such that a is acceptable with respect to v|P if v(a)=t, and a is deniable with respect to v|P if v(a)=f. However, φav|P implies that φav is irrefutable and φav|P implies that φav is unsatisfiable. The former implies that if v(a)=t, then ΓD(v)(a)=t; the latter one implies that if v(a)=f, then ΓD(v)(a)=f. This contradicts the assumption that there exists an a such that v(a)=t/f and ΓD(v)(a)t/f. Thus, the assumption that v is not an admissible interpretation is wrong. Hence, if v is a strongly admissible interpretation, then it is also an admissible interpretation.

  • If v is a strongly admissible interpretation, then by the first item of this theorem, it is an admissible interpretation. By the fact that in ADFs every admissible interpretation is a conflict-free interpretation, based on the definition of conflict-freeness (presented in Definition 13), we conclude that v is a conflict-free interpretation, as well. □

Example 11 indicates the distinction between the notion of strong admissibility semantics of ADFs and the notions of admissible and conflict-free semantics of ADFs.

Example 11.

let D=({a,b},{φa:¬ba,φb:¬a}) be a given ADF. The interpretation v={af,bt} is an admissible interpretation of D. However, a is not strongly deniable, nor is b strongly acceptable in v. Thus, v is not a strongly admissible interpretation of D. Furthermore, v={au,bt} is a conflict-free interpretation of D that is neither an admissible nor a strongly admissible interpretation. The only strongly admissible interpretation of D, which is also the grounded interpretation of D, is the trivial interpretation.

3.1.The strongly admissible interpretations of an ADF form a lattice

Although the sequence of interpretations presented in Lemma 9 produces a sequence of strongly admissible interpretations of a given ADF D, this sequence does not contain all of the strongly admissible interpretations of D. For instance, in ADF D=({a,b,c,d},{φa:,φb:a¬c,φc:¬bd,φd:}), presented in Example 7, it holds that v={au,bu,cf,df} is a strongly admissible interpretation of D. However, v is not equal to any of the elements of the sequence vu,ΓD(vu), (for D), as in Lemma 9. In this section we show that the strongly admissible interpretations of an ADF form a lattice.

Theorem 12 indicates that any strongly admissible interpretation of an ADF D is bounded by an element of the sequence of strongly admissible interpretations presented in Lemma 9.

Theorem 12.

Let D be an ADF, let w be an interpretation of D, and let vi for 0i be the sequence of interpretations presented in Lemma 9. If w is a strongly admissible interpretation of D, then there exists the least m0 such that wivm.

Proof.

Assume that w is a strongly admissible interpretation of D. Let S={a1,,an} be the set of arguments the truth values of which appear in w, i.e., S=wtwf. For each i with 1in, it holds that ai is strongly justified in w. Thus, for each ai there is a least witness of strong justification, namely wi where wiiw. Let mi be the maximum level of ai in mi and let m be the greatest of mi’s, i.e., m=max{mi|mi is the maximum level of ai in wi}. We claim that wivm. To prove our claim, we show that if ait/fw, then ait/fvm. We show our claim by induction on the maximum level of arguments.

Base case: Let a be a strongly justified argument in w with the maximum level of 1 in a wi. We show that at/fvm, i.e., a is a strongly justified argument in vm. Since the maximum level of a in a wi is 1, Definition 21 implies that P=. Thus, φavu/, that is, ΓD(v0)(a)=t/f. Hence, at/fv1. Since the set of vi as in Lemma 9 forms a sequence of interpretations, it holds that at/fvm, for m1.

Induction hypothesis: Suppose that for all j with 1jk<m and any a being a strongly justified argument in w with the maximum level of j in a wi, it holds that at/fvj (and also at/fvm, for mj).

Induction step: Let a be a strongly justified argument in w with the maximum level of k+1 in a wi. We show that at/fvk+1 (and also at/fvm, for mk+1). By Lemma 6 the maximum level of a in a wi (i.e., k+1) is a finite number, thus, there exists a non-empty set Ppar(a) such that φaw|P/. Since p, with pP, is a parent of a, by Definition 18, p is also a strongly justified argument in w. Thus, by Corollary 7 the maximum level of each p is strictly less than the maximum level of a i.e. the maximum level of p in a wi is at most k. Then, by the induction hypothesis, pt/fvk, for each pP. Therefore, φaw|Pφavk|P. Further, φavk|Pφavk because vk|Pivk and ΓD is a monotonic function. Therefore, at/fvk+1 (and also at/fvm for mk+1). That is, there exists an m0, such that wivm.

Further, we have to show that the natural number m assumed in the beginning of the proof is the least natural number that satisfies the condition of the theorem. Toward a contradiction assume that there exists an m<m such that wivm. By our assumption the greatest maximum level of an argument of S, namely a is m in a wi. Thus, either ΓDm(v0)(a)=u, or there exists ppar(a)S such that vm(p)=u. In both cases it holds that, w≰ivm. That is, m is the least natural number that satisfies the condition of the theorem, i.e, wivm and there is not m<m such that wivm. □

To show that the set of strongly admissible interpretations of a given ADF form a lattice, first, in Theorem 15 we show that every two strongly admissible interpretations of D have a unique supremum. To this end, we first introduce the notion of join of two strongly admissible interpretations; see Definition 22.

Definition 22.

Let D be an ADF and let v and w be two strongly admissible interpretations of D. The join viw is defined as

viw(a)=v(a)if at/fv,w(a)if at/fw,uotherwise.

Proposition 13.

The join of two strongly admissible interpretations of D is a well-defined function.

Proof.

Let D be an ADF and let v and w be two strongly admissible interpretations of D. We show that the join operator is a well-defined function. That is, we have to show that there is no a that has two different values via (viw)(a). Toward a contradiction, assume that there is an a that has two different outputs via (viw)(a). That is, a is assigned to t in one of the interpretations and to f in another one. For instance, v(a)=t and w(a)=f. By Theorem 12, there exist the least natural numbers k and m such that vivk and wivm, respectively. Since vivk and v(a)=t, atvk. Furthermore, since wivm and w(a)=f, afvm. That is, vk≰ivm and vm≰ivk. This is a contradiction by Lemma 9, which says that either vkivm or vmivk, because vk and vm are elements of the sequence of interpretations presented in Lemma 9. Thus, the assumption that there exists a that is acceptable in a strongly admissible interpretation of D but that is deniable in another strongly admissible of D is wrong. Thus, viw is a well-defined function. □

Lemma 14 presents that the join of two strongly admissible interpretations of a given ADF is also a strongly admissible interpretation of that ADF.

Lemma 14.

Let D be an ADF and let v and w be strongly admissible interpretations of D. Then viw is also a strongly admissible interpretation of D.

Proof.

Toward a contradiction, assume that viw is not a strongly admissible interpretation of D. Thus, there exists an a such that at/fviw but it is not strongly justifiable in viw. By Definition 22, either at/fv or at/fw. Since v and w are strongly admissible interpretations, a is strongly justifiable in v or w. Since viviw and wiviw, by Lemma 8, a is strongly justifiable in viw. This contradicts the assumption that a is not strongly justifiable in viw. Thus, the assumption that viw is not a strongly admissible interpretation was wrong. That is, the join of two strongly admissible interpretations of D is a strongly admissible interpretation of D.  □

Theorem 15.

Let D be an ADF. Every two strongly admissible interpretations of D have a unique supremum.

Proof.

Let D be an ADF and let v and w be two strongly admissible interpretations of D. We show that viw is a supremum of v and w. By Definition 22, viw is an upper bound of v and w. By Lemma 14, viw is a strongly admissible interpretation of D. It remains to show that viw is a least upper bound of v and w. Toward a contradiction, assume that viw is not the least upper bound of v and w. That is, there exists a strongly admissible interpretation w of D such that viw, wiw and w<iviw. Thus there exists a with auw and at/fviw. However, at/fviw implies that either at/fv or at/fw. That is, either v≰iw or w≰iw. This contradicts the assumption that w is the least upper bound of v and w. Thus, the assumption that viw is not the least upper bound of v and w was wrong. □

Subsequently, to show that the set of strongly admissible interpretations of ADF D form a lattice, in Theorem 17 we show that every two strongly admissible interpretations of D have an infimum. To this end, in Definition 23, we present the concept of the maximum strongly admissible interpretation contained in an interpretation of D.

Definition 23.

Let D be an ADF and let v be an interpretation of D. Interpretation w is called a unique maximum strongly admissible interpretation contained in v with respect to i ordering if the following conditions hold:

  • w is a strongly admissible interpretation of D such that wiv;

  • If wiv, then there is no strongly admissible interpretation w of D such that w<iwiv.

Lemma 16.

Let D be an ADF and let v be an interpretation of D. Then there exists a unique maximum strongly admissible interpretation contained in v, with respect to the i ordering.

Proof.

Each interpretation of D has at least as much information as the trivial interpretation. Thus, each v of D has at least as much information as vu, which is a strongly admissible interpretation. Since the number of arguments of D is finite, there exists at least one maximal strongly admissible interpretation of D (with respect to the i ordering), let us call it w, contained in a given interpretation v. We show that this w is unique. Toward a contradiction, assume that there are two maximal strongly admissible interpretations that satisfy the condition of the lemma, namely w and w. By Lemma 14, wiw is a strongly admissible interpretation of D. Since wiv and wiv, it also holds that wiwiv. However, wiwiw, wiwiw and wiwiv together with the assumption that w and w are maximal strongly admissible interpretations contained in v lead to wiwiw and wiwiw. That is, wiw. Thus, the maximum strongly admissible interpretation which is contained in v is unique. □

Theorem 17.

Let D be an ADF. Every two strongly admissible interpretations of D have a unique infimum.

Proof.

Let D be an ADF and let v and v be two strongly admissible interpretations of D. Let w=viv. By Lemma 16, there exists a unique maximum strongly admissible interpretation w with wiw. That is, w is a lower bound of v and v. It remains to show that w is the greatest lower bound of v and v. Toward a contradiction, assume that there exists a w that is the greatest lower bound of v and v. That is, wiv and wiv. Then by the definition, wi(viv=w). By the assumption, w is the maximum strongly admissible interpretation that is less or equal to w, thus, wiw. Thus, w is an infimum of v and v. □

Theorem 18.

Let D be an ADF. The strongly admissible interpretations of D form a lattice with respect to the i-ordering, with the least element vu and the top element grd(D).

Proof.

We have to show that each pair of strongly admissible interpretations of D has a supremum and an infimum. Theorem 15 shows the former one and Theorem 17 indicates the latter one. Thus, the strongly admissible interpretations of D form a lattice with respect to the i-ordering. In Lemma 10, it is shown that vu is the least strongly admissible interpretation and the grounded interpretation of D is the largest strongly admissible interpretation of the sequence of the interpretations presented in Lemma 9. This fact, together with Theorem 12, shows that the grounded interpretation D is the greatest element of this lattice. It is trivial that vu is the least element of this lattice. □

Corollary 19.

The maximal strongly admissible interpretation of ADF D, with respect to the i ordering, is the unique grounded interpretation of D.

The set of strongly admissible interpretations of ADF D=({a,b,c,d},{φa:,φb:a¬c,φc:¬bd,φd:}) given in Example 7 form a lattice, depicted in Fig. 4. The top element of this lattice is the grounded interpretation of D {at,bt,cf,df}={a,b,¬c,¬d}.

Fig. 4.

Complete lattice of the strongly admissible interpretations of the ADF of Example 7.

Complete lattice of the strongly admissible interpretations of the ADF of Example 7.

4.Strong admissibility for ADFs generalizes strong admissibility for AFs

In this section we show that the concept of strong admissibility semantics for ADFs is a proper generalization of the concept of strong admissiblity semantics for AFs [25]. The technical proofs of Propositions 20 and 21 and Lemma 22 are available in the Appendix.

Given an AF F=(A,R) and its corresponding ADF DF=(A,R,C) (see Definition 14), the set of all possible conflict-free extensions of F is denoted by E and the set of all possible conflict-free interpretations of DF is denoted by V. The functions Ext2IntF and Int2ExtDF in Definitions 2425, are modifications of the labelling functions as given in [6], which we recalled in Definitions 910. Function Ext2IntF(S) represents the interpretation associated with a given extension S in F, and function Int2ExtDF(v) indicates the extension associated with a given interpretation v of DF.

Definition 24.

Let F=(A,R) be an AF, and let S be an extension of F. The truth value assigned to each argument aA by the three-valued interpretation vS associated with S is given by Ext2IntF:EV as follows.

Ext2IntF(S)(a)=t if aS,f if bA such that (b,a)R and bS,uotherwise.

Proposition 20.

Let F=(A,R) be an AF, let DF be its associated ADF, and let S be a conflict-free extension of F. Then Ext2IntF(S) is well-defined.

Note that in Definition 24, the basic condition that S has to be a conflict-free extension is a necessary condition for Ext2IntF(S) being well-defined. For instance, let F=({a,b},{(a,b)}). Set S={a,b} is an extension of F. However, S does not satisfy the conflict-free property. On the other hand, Ext2IntF(S)={at,bt,bf}. In other words, the correspondence between extensions and interpretations via Ext2IntF(.) is well-defined for conflict-free sets of arguments. This is the reason why we restrict E and V to the set of all conflict-free extensions of F and the set of all conflict-free interpretations of DF, respectively. By Theorem 4 in [25], every strongly admissible extension of an AF is a conflict-free extension. Thus, if S is a strongly admissible extension of AF F, then, by Proposition 20, Ext2IntF(S) is well-defined.

So extensions of F can be represented as interpretations of DF. Also an interpretation of DF can be represented as an extension via the following function.

Definition 25.

Let DF=(A,R,C) be the ADF associated with AF F, and let v be an interpretation of DF, that is, vV. The associated extension Sv of v is obtained via application of Int2ExtDF:VE on v, as follows:

Int2ExtDF(v)={aA|atv}

To present the correspondence between strongly admissible extensions of F and strongly admissible interpretations of the associated DF, we first present the correspondence between strongly admissible labellings of F and strongly admissible interpretations of the associated DF in Lemma 22. To this end, we define two functions, Lab2Int and Int2Lab to indicate the correspondence between labellings and interpretations in Definitions 26 and 27. Note that L denotes the set of labellings of AF F.

Definition 26.

The function Lab2Int(·):LV maps three-valued labellings to three-valued interpretations such that

  • Lab2Int(λ)(a)=t iff λ(a)=in,

  • Lab2Int(λ)(a)=f iff λ(a)=out, and

  • Lab2Int(λ)(a)=u iff λ(a)=undec.

Definition 27.

The function Int2Lab(·):VL maps three-valued interpretations to three-valued labellings such that

  • Int2Lab(v)(a)=in iff v(a)=t;

  • Int2Lab(v)(a)=out iff v(a)=f;

  • Int2Lab(v)(a)=undec iff v(a)=u.

In Proposition 21 we show that Int2Lab is the inverse of Lab2Int.

Proposition 21.

Lab2Int(Int2Lab(.))=idV and Int2Lab(Lab2Int(.))=idL.

Lemma 22.

For any argument framework F=(A,R) and its associated ADF DF, the following properties hold:

  • if λ is a strongly admissible labelling of F, then Lab2Int(λ) is a strongly admissible interpretation of DF;

  • if v is a strongly admissible interpretation of DF, then Int2Lab(v) is a strongly admissible labelling of F.

Theorem 23 is a direct result of Propositions 521, and Lemma 22. It presents the correspondence between strongly admissible extensions of F and strongly admissible interpretations of the associated DF.

Theorem 23.

For any argument framework F=(A,R) and its associated ADF DF, the following properties hold:

  • If S is a strongly admissible extension of F, then Ext2IntF(S) is a strongly admissible interpretation of DF;

  • If v is a strongly admissible interpretation of DF, then Int2ExtDF(v) is a strongly admissible extension of F.

Proof.

  • It is enough to show that Ext2IntF(S)=Lab2Int(Ext2Lab(S)).

    (1) Let a be an argument such that aS. By Definition 24, aS if and only if atExt2IntF(S). In other words, aS if and only if Ext2Lab(S)(a)=in if and only if Lab2Int(Ext2Lab(S)(a))=t. (2) Let a be an argument such that aS and there exists a parent of a, namely pa, with paS. By Definition 24, aS and paS if and only if afExt2IntF(S). In other words, aS and paS if and only if Ext2Lab(S)(a)=out if and only if Lab2Int(Ext2Lab(S)(a))=f.

    Thus, Ext2IntF(S)=Lab2Int(Ext2Lab(S)). Hence, by Proposition 5, if S is a strongly admissible extension of F, then λ=Ext2Lab(S) is a strongly admissible labelling of F. Furthermore, by Lemma 22, if λ is a strongly admissible labelling of F, then Lab2Int(λ) is a strongly admissible interpretation of DF. That is, Ext2IntF(S) is a strongly admissible interpretation of DF.

  • By the similar method as the one presented in the proof of the previous item, we have Int2ExtDF(v)=Lab2Ext(Int2Lab(v)). By Lemma 22, if v is a strongly admissible interpretation of DF, then λ=Int2Lab(v) is a strongly admissible labelling of F. By Proposition 5, if λ is a strongly admissible labelling of F, then Lab2Ext(λ) is a strongly admissible extension of F. Hence, Int2ExtDF(v) is a strongly admissible extension of F. □

We have already shown that the projection of a strongly admissible extension/labelling of AF F via Ext2IntF(.)/Lab2Int(.) is a strongly admissible interpretation of the associated DF. The commutative diagrams in Fig. 5 show the relation between strong admissibility semantics of AF F and strong admissibility semantics of its associated ADF DF. In the following, the set of strongly admissible extensions of F, the set of strongly admissible labellings of F, and the set of strongly admissible interpretations of DF are denoted by sadm(F), sadmL(F), and sadm(DF), respectively.

Fig. 5.

The left diagram shows that strong admissibility semantics of F project to strong admissibility semantics of DF, via Ext2IntF. The right diagram shows that strong admissibility semantics of DF project to strong admissibility semantics of F, via Int2ExtDF.

The left diagram shows that strong admissibility semantics of F project to strong admissibility semantics of DF, via Ext2IntF. The right diagram shows that strong admissibility semantics of DF project to strong admissibility semantics of F, via Int2ExtDF.

The direct result of Theorem 23 is that the strong admissibility semantics of ADFs form a proper generalization of strong admissibility semantics of AFs, as presented in Corollary 24.

Corollary 24.

Let F be an AF and let DF be its associated ADF. An extension S is a strongly admissible semantics of F if and only if v=Ext2IntF(S) is a strongly admissible interpretation of DF.

However, Corollary 24 does not claim that there is a one-to-one relation between the set of strong admissibility extensions of F and the set of strong admissibility interpretations of DF. In other words, for the strong admissibility semantics, neither Ext2IntF(.) nor Int2ExtDF(.) is a bijective function. The reason is that for the strong admissibility semantics, the function Ext2IntF is not a surjective function and function Int2ExtDF is not an injective function, as clarified in Example 12.3

Example 12.

Let F=({a,b,c,d},{(a,b),(b,c),(c,d)}). The associated ADF of F is DF=({a,b,c,d},{(a,b),(b,c),(c,d)},{φa:,φb:¬a,φc:¬b,φd:¬c}). The interpretation {at,bf,ct,du} is a strongly admissible interpretation of DF, but it is not a projection of any strongly admissible extension of F via Ext2IntF. Thus, Ext2IntF is not a surjective function. Furthermore, both of the strongly admissible interpretations of DF, namely, v1={at,bf,ct,du} and v2={at,bf,ct,df}, are mapped to the strongly admissible extension {a,c} via Int2ExtDF. Thus, DF is not an injective function. In other words, we did not claim that Ext2IntF is an inverse of Int2ExtDF for strongly admissible semantics. For instance, in this example Ext2IntF(Int2ExtDF(v1))=v2.

Although Int2Ext(.) is not an injective function, by the second item of Theorem 23, function Int2Ext(.) maps any strongly admissible interpretation of DF to a strongly admissible extension of F. That is, Int2Ext(.) may map an element of sadm(DF) to an element of sadm(F). On the other hand, it is possible that there exists an element of sadm(DF) that is not an image of any element of sadm(F) by Ext2Int(.), since Ext2Int(.) is not a surjective function. However, the image of any element of sadm(F) by Ext2Int(.) is a strongly admissible interpretation of DF, by the first item of Theorem 23. These results together lead to Corollary 25.

Corollary 25.

The concept of strong admissibility semantics of ADFs is a generalization of the concept of strong admissibility semantics of AFs.

5.Algorithm for strong admissibility semantics of ADFs

Definition 19 says that an interpretation v is strongly admissible in a given ADF D if and only if for each argument a that is presented in v, i.e., v(a)=t/f, we have that a is a strongly justified argument in v. In the following, we present an alternative method to answer the verification problem under strong admissibility semantics of ADFs. In this method of investigating whether the given interpretation v is a strongly admissible interpretation of D, there is no need to check whether each argument is strongly justified in v. The results of this section lead to algorithms to answer the following decision problems.

  • (1) The verification problem: whether a given interpretation is a strongly admissible interpretation of a given ADF.

  • (2) The strong justification problem: whether a given argument a is a strongly justified argument in a given interpretation.

To this end, we introduce ΓD,v a variant of the characteristic operator restricted to a given interpretation v, presented in Definition 28.

Definition 28.

Let D=(A,L,C) be a given ADF and let v,w be interpretations of D. Let ΓD,v(w)=ΓD(w)iv where ΓD,vn(w)=ΓD,v(ΓD,vn1(w)) for n with n1. Note that ΓD,v0(w)=w. We call the collection of the interpretations of ΓD,vn(vu) for n1, the set of interpretations constructed based on v in D.

In Lemma 26, we show that each interpretation in the set of interpretations constructed based on v is a strongly admissible interpretation.

Lemma 26.

Let D=(A,L,C) be a given ADF and let v be an interpretation of D. Let ΓD,vn(vu) be the sequence of interpretations constructed based on v, as in Definition 28. For each i with i0 it holds that;

  • ΓD,vi(vu)iΓD,vi+1(vu);

  • ΓD,vi(vu) is a strongly admissible interpretation of D;

  • if ΓD,vi(vu)(a)=t/f, then a is strongly justifiable in ΓD,vi(vu).

Proof.

  • We show the first item by induction on i.

    Base case: By Definition 28, for i=0 it holds that ΓD,v0(vu)=vu and it is clear that vuiΓD,v1(vu).

    Induction hypothesis: Suppose that ΓD,vj(vu)iΓD,vj+1(vu) for each j with 0j<i.

    Inductive step: We show that this property holds for j=i, i.e., ΓD,vi(vu)iΓD,vi+1(vu). From the fact that the characteristic operator is monotonic together with the induction hypothesis, it follows that ΓD(ΓD,vj(vu))iΓD(ΓD,vj+1(vu)), for j with 0j<i. Thus, ΓD(ΓD,vi1(vu))iΓD(ΓD,vi(vu)) and further, ΓD(ΓD,vi1(vu))iviΓD(ΓD,vi(vu))iv. That is, ΓD,vi(vu)iΓD,vi+1(vu).

  • We show the second item by induction on i.

    Base case: For i=0 it is clear that ΓD,v0(vu)=vu is a strongly admissible interpretation of D.

    Induction hypothesis: Suppose that for each j with 0j<i it holds that ΓD,vj(vu) is a strongly admissible interpretation of D.

    Inductive step: We prove that ΓD,vi(vu) is also a strongly admissible interpretation of D. To this end, we show that if the truth value of a is presented in ΓD,vi(vu), then a is a strongly justified argument in ΓD,vi(vu). We assume that ΓD,vi(vu)(a)=t and ΓD,vi1(vu)(a)=u, otherwise if the truth value of a is presented in ΓD,vi1(vu), then a is strongly acceptable in ΓD,vi1(vu) and there is nothing to prove (because by induction hypothesis ΓD,vi1(vu) is a strongly admissible interpretation of D). We show that a is strongly acceptable in ΓD,vi(vu). For the case that ΓD,vi(vu)(a)=f the proof follows a similar method. Since ΓD,vi(vu)(a)=t, we can conclude that ΓD(ΓD,vi1(vu))=t, that is, the evaluation of φa under ΓD,vi1(vu) is irrefutable. Thus, there exists a non-empty subset of parents of a, namely P such that the truth value of each pP is presented in ΓD,vi1(vu). Since by induction hypothesis ΓD,vi1(vu) is strongly admissible if the truth value of an argument is presented in ΓD,vi1(vu), then that argument is strongly justified in ΓD,vi1(vu). That is, each pP is also strongly justified in ΓD,vi1(vu). This satisfies the conditions of Definition 18. Thus, every interpretation in the sequence ΓD,vi(vu) for i with i0 is a strongly admissible interpretation.

  • Toward a contradiction, assume that there exists an i and an argument a such that ΓD,vi(vu)(a)=t/f but a is not a strongly justified argument in ΓD,vi(vu). Thus, by Definition 19, ΓD,vi(vu) is not a strongly admissible interpretation of D. This contradicts the second item of the current lemma, in which we showed that for each i with i0, it holds that ΓD,vi(vu) is a strongly admissible interpretation of D. Thus the assumption that there exists an argument a such that ΓD,vi(vu)(a)=t/f but a is not a strongly justified argument in ΓD,vi(vu) was wrong. Thus, if ΓD,vi(vu)(a)=t/f, then a is a strongly justified argument in ΓD,vi(vu). □

Remark.

the sequence of interpretations ΓD,vi(vu) as Definition 28, is named the sequence of strongly admissible interpretations constructed based on v in D.

Proposition 27 presents that for each interpretation v the sequence of interpretations constructed based on v is a finite sequence and therefore has a limit.

Proposition 27.

Let D be an ADF and let v be an interpretation of D. Let ΓD,vi(vu) (for i0) be the sequence of strongly admissible interpretations constructed based on v in D. Then there is an m with m0 such that ΓD,vm(vu)iΓD,vm+1(vu).

Proof.

Let vu,ΓD,v1(vu), be the sequence of strongly admissible interpretations constructed based on v in D. Since ΓD,vi(vu)iΓD,vi+1(vu) for i0, by the first item of Lemma 26, and the number of arguments of D is finite, the sequence vu,ΓD,v1(vu), has to stop. That is, there exists m0 such that ΓD,vm(vu)iΓD,vm+1(vu). □

Definition 29.

Let D be an ADF and let v be an interpretation of D. Let ΓD,vi(vu) (for i0) be the sequence of strongly admissible interpretations constructed based on v in D. Consider an m with m0 such that ΓD,vm(vu)iΓD,vm+1(vu). Then, w=ΓD,vm(vu) is called the limit of the sequence of ΓD,vi(vu) (for i0) which is the least fixed-point of ΓD,v.

Theorem 28 proposes the necessary and sufficient condition for an interpretation being a strongly admissible interpretation.

Theorem 28.

Let D be an ADF and let v be an interpretation of D. Let ΓD,vi(vu) (for i0) be the sequence of strongly admissible interpretations constructed based on v in D. Interpretation v is a strongly admissible interpretation if and only if v is the limit of the sequence of ΓD,vi(vu) (for i0), (i.e., there exists an m such that viΓD,vm(vu)).

Proof.

‘→’ Assume that v is a strongly admissible interpretation of D. By Proposition 27, there exists an m (m0) such that ΓD,vm(vu)iΓD,vm+1(vu). We show that viΓD,vm(vu).

  • By the definition of the constructed sequence of interpretations based on v in Definition 28 it is clear that ΓD,vi(vu)iv for i0. Therefore, ΓD,vm(vu)iv.

  • It remains to show that viΓD,vm(vu). Toward a contradiction assume that v≰iΓD,vm(vu). This means that there exists a such that at/fv, but at/fΓD,vm(vu). Since v is a strongly admissible interpretation, a is a strongly justified argument in v. Thus, by Definition 18, there exists a non-empty subset of parents of a, namely P such that the truth value of each pP is presented in v, such that P satisfies the condition of Definition 18 for a. This means that each pP is also a strongly justified argument in v. Note that if P= the fact that a is strongly justified in v implies that at/fΓD,v1(vu), i.e., at/fΓD,vm(vu). Thus, P has to be a non-empty set to satisfy the assumption that at/fΓD,vm(vu).

    If the truth value of arguments of P are presented in ΓD,vm(vu), then there exists a j with 0jm such that the truth value of arguments of P are also presented in ΓD,vj(vu). If so, it holds that at/fΓD,vj+1(vu). This contradicts the assumption that at/fΓD,vm(vu).

    Hence, there exists pP such that the truth value of p is not presented in ΓD,vm(vu). The fact that p is a strongly justified argument in v implies that there exists a non-empty subset of parents of p, namely P1 such that the truth value of elements of P1 are presented in v, such that P1 satisfies the condition of Definition 18 for p. Using the same method of reasoning for p, we conclude that there exists a parent of p, namely p1 such that the truth value of p1 is not presented in ΓD,vm(vu).

    Following the same method of reasoning, we find that there exists a sequence of ancestors of a, namely p,p1, such that the truth value of none of them is presented in ΓD,vm(vu). Since the number of arguments of A is finite, the sequence p,p1, cannot be an infinite sequence. If the sequence p,p1, is finite, then for some i, Pi=. If Pi=, then by Definition 18, φpi1vu is irrefutable/unsatisfiable. This means that pi1t/fΓD,v1(vu). This contradicts the assumption that the truth values of arguments of sequence p,p1, are not presented in ΓD,vm(vu). Thus, the assumption that at/fΓD,vm(vu) is wrong. Hence, viΓD,vm(vu).

  • ‘←’ Assume that viΓD,vm(vu). We show that v is a strongly admissible interpretation. Lemma 26 says that each ΓD,vi(vu), for i0, is a strongly admissible interpretation of D. Thus, ΓD,vm(vu) is a strongly admissible interpretation of D. As viΓD,vm(vu) it follows that v is a strongly admissible interpretation of D. □

Based on the above observations, one can characterise a strongly admissible interpretation v as the least fixed point of the corresponding operator ΓD,v. That is, we can verify an interpretation by computing this sequence of strongly admissible interpretations. By Theorem 28, to investigate whether interpretation v is a strongly admissible there is no need of indicating whether each argument which is presented in v is a strongly justified argument in v. That is, there is no need of following Definition 18 to answer the verification problem for strong admissibility semantics of ADFs. That is, by Theorem 28, it is enough to investigate whether viΓD,vm(vu), where ΓD,vi(vu) (i0) is a sequence of strongly admissible interpretations constructed based on v in D. Example 13 illustrates the role of Theorem 28 and the sequence of strongly admissible interpretations constructed based on a given interpretation.

Example 13.

Consider the ADF given in Example 7, i.e., D=({a,b,c,d},{φa:,φb:a¬c,φc:¬bd,φd:}). To investigate whether interpretation v={at,bu,cf,df} is a strongly admissible interpretation, we follow the method presented in Theorem 28 by constructing the sequence of strongly admissible interpretations constructed based on v, as in Definition 28. That is, we investigate whether there exists an m such that viΓD,vm(vu). The sequence of strongly admissible interpretations constructed based on v is as follows.

v1=ΓD,v(vu)=ΓD(vu)iv={a,¬d}i{a,¬c,¬d}={a,¬d},v2=ΓD,v2(vu)=ΓD,v(v1)=ΓD(v1)iv={a,¬c,¬d}i{a,¬c,¬d}={a,¬c,¬d}
Since v is the limit of the sequence v1,v2, i.e., viΓD,v2(vu), (i.e., v is a least fixed point of ΓD,v), interpretation v is a strongly admissible interpretation of D.

On the other hand, we investigate that v={at,bt,cu,du} is not a strongly admissible interpretation of D. The sequence of interpretation constructed based on v are as follow.

v1=ΓD(vu)iv={a,¬d}i{a,b}={a},v2=ΓD(v1)iv={a,¬d}i{a,b}={a}.
Thus, the sequence of interpretations constructed based on v leads to v2={a}, which is not equal to v, i.e., viv2 (that is, v is not a least fixed point of ΓD,v). Hence, v is not a strongly admissible interpretation of D. The reason is that the truth value of b is presented in v, however, with a similar reason as was presented in Example 7, it is easy to show that b is not strongly acceptable in v.

Lemma 26 and Theorem 28 lead us to present an algorithm to answer the decision problem of whether interpretation v is a strongly admissible interpretation, presented in Algorithm 1.

Algorithm 1

Algorithm to decide whether v is a strongly admissible interpretation of D

Algorithm to decide whether v is a strongly admissible interpretation of D

The results of this section lead to an alternative definition for strongly admissible semantics of ADFs, presented in Definition 30.

Definition 30.

Let D be an ADF and let v be an interpretation of D. Let ΓD,vi(vu) (for i0) be the sequence of strongly admissible interpretations constructed based on v in D. Interpretation v is a strongly admissible interpretation if v is the limit of the sequence of ΓD,vi(vu) (for i0), (i.e., if there exists an m such that viΓD,vm(vu)).

In the current section we presented an alternative definition (i.e., Definition 30) of strongly admissible interpretations of a given ADF in which there is no need to investigate that all the arguments the truth values of which are presented in a given interpretation are strongly justifiable. If a given interpretation v is a strongly admissible interpretation of D, then it is clear that a is strongly acceptable in v if v(a)=t and it is strongly deniable in v if v(a)=f. In contrast, when v is not strongly admissible, it may contain some arguments that are strongly justifiable in v. For instance, in Example 13, a is strongly acceptable in v, however, v is not a strongly admissible interpretation of D, because b is not strongly acceptable in v. Algorithm 2 presents a method to answer whether an argument is strongly justifiable in a given interpretation. Note that in this method, presented in Definition 31, in contrast with Definition 18 there is no need to find a set of ancestors of a given argument to answer the decision problem. Theorem 29 shows why the method presented in Algorithm 2 and Definition 31 works to answer the decision problem whether an argument is strongly justifiable in a given interpretation.

Theorem 29.

Let D be an ADF and let v be an interpretation of D. Let ΓD,vi(vu) (for i0) be the sequence of strongly admissible interpretations constructed based on v in D. Assume that v is the limit of the sequence of ΓD,vi(vu) (for i0). It holds that v(a)=t/f if and only if a is a strongly justified argument in v.

Proof.

First, we assume that v(a)=t/f; and we show that a is a strongly justified argument in v. Since v is the limit of the sequence ΓD,vi(vu) (for i0), there exists an m with m0 where v=ΓD,vm(vu). By the third item of Lemma 26, if ΓD,vm(vu)(a)=t/f, then a is a strongly justified argument of ΓD,vm(vu), i.e., a is a strongly justified argument of v. Thus, if v(a)=t/f, since viv, by Lemma 8 it holds that a is a strongly justified argument of v.

Second, we assume that a is a strongly justified argument in v; we show that v(a)=t/f. Since a is a strongly justified argument in v, there exists a least witness of strong justifiability of a, namely wa. We claim that if the maximum level of a in wa is i (i.e., Mwa(a)=i), then ΓD,vi(vu)(a)=t/f. We show this claim by induction on the maximum level of a.

Base case: If a is a strongly justified argument in v and Mwa(a)=1 in a wa, then we show that ΓD,v1(vu)(a)=t/f. If Mwa(a)=1, then φavu/, i.e., at/fΓD(vu). Since v(a)=t/f, it holds that ΓD,v1(vu)(a)=t/f.

Induction hypothesis: For all j with for 0j<i, if a is a strongly justified argument in v and the maximum level of a in a wa is j, then ΓD,vj(vu)(a)=t/f.

Inductive step: If a is a strongly justified argument in v and the maximum level of a in a wa is i, then ΓD,vi(vu)(a)=t/f. Let P be a set of parents of a that satisfies the conditions of Definition 18 for a, that is, φav|P/, where each pP is a strongly justified in v. By Corollary 7, the level of each parent of a in the wa is at most i1. For each pP, since v(p)=t/f and the maximum level of p in wa is at most i1, by the induction hypothesis, we have ΓD,vi1(vu)(p)=t/f. Hence, ΓD,vi(vu)(a)=t/f.

Algorithm 2

Algorithm to decide whether a is a strongly justified argument in v

Algorithm to decide whether a is a strongly justified argument in v

Thus, if a is a strongly justified argument in v and the maximum level of a in a wa is i, then ΓD,vi(vu)(a)=t/f. Since v is the limit of the sequence of ΓD,vi(vu), it holds that v(a)=t/f.  □

Theorem 29 leads to present an alternative definition of strong acceptability/deniability of arguments, presented in Definition 31, in which to answer whether a given argument is a strongly justified argument in a given interpretation there is no need to find a proper set P of parents of the argument in question to satisfy the conditions of Definition 18.

Definition 31.

Let D be an ADF and let v be an interpretation of D. Let ΓD,vi(vu) (for i0) be the sequence of strongly admissible interpretations constructed based on v in D. Assume that v is the limit of the sequence of ΓD,vi(vu) (for i0). Argument a, with v(a)=t/f, is a strongly justified argument in v if v(a)=v(a).

6.Sequence of strongly admissible extensions for AFs and ADFs

In Section 4 we showed that the concept of strongly admissible semantics of ADFs forms a generalization of the concept of strongly admissible semantics of AFs. Furthermore, we indicated that there is no one-to-one relation between the set of strongly admissible extensions of AF F and the set of strongly admissible interpretations of the associated ADF DF. In this section we clarify the relation between the sequence of strongly admissible extensions of a given AF F and the sequence of strongly admissible interpretations of the associated ADF DF.

In Lemma 26, we constructed a sequence of strongly admissible interpretations ΓD,vi(vu) (for i0) based on a given interpretation v in an ADF. In Theorem 28, we proved that v is a strongly admissible interpretation of a given ADF if and only if v is the limite of the sequence ΓD,vi(vu) (for i0). There is a similar method to indicate whether a given extension is a strongly admissible extension of a given AF, presented in [25]. In the following, we first represent the necessary notations from [25]. Then we investigate the relation between the sequence of extensions presented in [25] for an AF and the sequence of interpretations for the associated ADF presented in the current work.

In [25, Lemma 2], it is presented that, in a given AF F, for an arbitrary extension S of ΓF, each extension in the sequence H0=, Hi+1=ΓF(Hi)S is a strongly admissible extension of F. We recall this lemma in Lemma 30. Note that in the following, ΓF(.) is the characteristic function of AFs, as it is defined in Section 2.1.

Lemma 30

Lemma 30([25, Lemma 2]).

Let F=(A,R) and let SA. Let H0= and Hi+1=ΓF(Hi)S (i0). For each i>0 it holds that

  • HiHi+1;

  • Hi is strongly admissible;

  • Hi strongly defends each of its arguments.

Let S be a strongly admissible extension of F and let v=Ext2IntF(S). The main goal of the rest of this section is to show the exact relation between the sequence of strongly admissible extensions of F, namely Hi as in Lemma 30, and the sequence of the strongly admissible interpretations of DF, namely ΓD,vi(vu), as in Definition 28. In Theorem 1 of [25], it was shown that S is a strongly admissible extension of F if and only if S=i=0Hi; we rephrase it in Theorem 31.

Theorem 31

Theorem 31([25, Theorem 1]).

Let F=(A,R), let SA and let Hi (i0) be as in Lemma 30. S is strongly admissible iff S=i=0Hi.

Since the number of arguments of F is finite and HiHi+1, we conclude that there exists j0 such that S=Hj iff S is a strongly admissible extension of F. It is easy to check that Ext2IntF is a monotonic function over Hi, that is, if HiHj, then Ext2IntF(Hi)iExt2IntF(Hj). Before presenting the formal relation between the sequence of strongly admissible extensions of F (in the sense of Theorem 31) and the sequence of strongly admissible interpretations of DF (in the sense of Theorem 28), we clarify this relation by an example, in Example 14.

Example 14.

Consider F=({a,b,c,d},{(a,b),(b,c),(c,d)}) and extension S={a,c}. We show that S is a strongly admissible extension of F via Theorem 31. That is, we construct the sequence of extensions Hi and we show that S=i=0Hi. Furthermore, in the right-hand column we show the associated interpretation to each extension via Definition 24.

H0={}Ext2Int(H0)={au,bu,cu,du}H1=ΓF(H0)S={a}{a,c}={a}Ext2Int(H1)={at,bf,cu,du}H2=ΓF(H1)S={a,c}{a,c}={a,c}Ext2Int(H2)={at,bf,ct,df}
Since S=H2, i.e., S is a unique fixed point of i=0Hi, it is a strongly admissible extension of F. The interpretation associated with S in DF via Definition 24 is Ext2Int(S)=v={at,bf,ct,df}. By Theorem 23, we already know that v is a strongly admissible interpretation of DF. In other words, we illustrate that v is a strongly admissible interpretation of DF via Definition 30. To this end, we construct the sequence of strongly admissible interpretations ΓD,vi(vu) based on v. It is expected that there is a one-to-one relation between Ext2Int(Hi) and the elements of the sequence of ΓD,vi(vu) in Definition 30.
v0=vuv1=ΓDF(v0)v={at,bu,cu,du}v={at,bu,cu,du}v2=ΓDF(v1)v={at,bf,cu,du}v={at,bf,cu,du}v3=ΓDF(v2)v={at,bf,ct,du}v={at,bf,ct,du}v4=ΓDF(v3)v={at,bf,ct,df}v={at,bf,ct,df}
In fact, by Theorem 28, it holds that v is a strongly admissible interpretation of DF, since viΓDF,v4(vu). However, the guess that each ΓDF,vi(vu), for i0, is equal to Ext2Int(Hi) was wrong. Since as we can see, on the one hand, Ext2Int(H1) contains the truth value of initial arguments that are in S and the arguments that are attacked by H1, i.e., the children of arguments of H1. On the other hand, ΓDF,v1(vu) contains the truth values of initial arguments that are presented in v and do not contain the truth values of children of initial arguments presented in v. In other words, ΓDF(v1) produces the truth values of children of initial arguments presented in v1. That is, v2=ΓDF(v1)iv contains the truth values of initial arguments and their children that are presented in v. Thus, it seems that, for i0, it holds that each Ext2Int(Hi) is equal to v2i. For instance, in the current example Ext2Int(H1)=v2 and Ext2Int(H2)=v4. Further, in this example the projection of each strongly admissible extension of F via Ext2Int(.) is a strongly admissible interpretation of DF. However, for instance, v1 is not a projection of any strongly admissible extension. This shows that Ext2Int(.) is not a surjective function, as presented earlier in Example 12.

Theorem 32.

Let F be an AF and let DF be its associated ADF. Let S be a strongly admissible extension of F and let Hi be as in Lemma 30. Let Ext2Int(S)=v and let vi=ΓD,vi(vu) be the sequence of interpretations as in Definition 28. Then it holds that Ext2Int(Hi)=v2i, for each i0.

Proof.

For i0, we show that Ext2Int(Hi)=v2i by induction on i.

Base case: It is obvious that Ext2Int(H0)=vu=v0.

Induction hypothesis: assume that Ext2IntF(Hj)=v2j for each j with 0j<i.

Inductive step: we have to show that Ext2IntF(Hi)=v2i. To show the inductive step, we show that axExt2IntF(Hi) if and only if axv2i, for x{t,f}.

  • (1) First we show that atExt2IntF(Hi) if and only if atv2i. We claim that atExt2IntF(Hi) if and only if atv2i1. Assume that atExt2IntF(Hi), i.e., aHi. Since Hi=ΓF(Hi1)S, it holds that aΓF(Hi1) and aS. Relation aΓF(Hi1) implies that a is defended by Hi1. Thus, for each p such that (p,a)R, there exists a defender of a, namely cp, such that (cp,p)R, cpHi1 and since Hi1 is a strongly admissible extension, cpa. Since defender cp belongs to Hi1, it holds that cptExt2IntF(Hi1) and each parent of a is assigned to f in Ext2IntF(Hi1). By the induction hypothesis, Ext2IntF(Hi1)=v2(i1)=v2i2. That is, for each p such that (p,a)R, it holds that pfv2i2. Thus, φav2i2, that is, atΓDF(v2i2). Since atExt2IntF(S), it holds that atΓDF(v2i2)iv. Thus, atv2i1.

    We have already shown that if atExt2IntF(Hi), then atv2i1. Since all the relations are equivalence relations, the other direction works as well. That is, if atv2i1 then atExt2IntF(Hi). Thus, atExt2IntF(Hi) iff atv2i1. We use this equation in the proof of the next item. Further, since the characteristic function is a monotonic function, atv2i1 implies that atΓDF(v2i1). Hence, atExt2IntF(Hi) if and only if at(ΓDF(v2i1)iv)=v2i.

  • (2) We show that afExt2IntF(Hi) if and only if afv2i. Assume that afExt2IntF(Hi). By the definition of the Ext2IntF function, there exists a parent of a, namely p, such that pHi, i.e., ptExt2IntF(Hi). As shown in the first item, ptExt2IntF(Hi) if and only if ptv2i1. Thus, φav2i1. Hence, afΓDF(v2i1). On the other hand, afExt2IntF(Hi) implies that afExt2IntF(S), since Ext2IntF(Hi)=Ext2IntF(F(Hi1))Ext2IntF(S). That is, af(ΓDF(v2i1)iv)=v2i. Thus, if afExt2IntF(Hi), then afv2i. Since all the relations are equivalence relations, afExt2IntF(Hi) if and only if afv2i.

To conclude, Ext2IntF(Hi)=v2i, for i0. □

In Section 4, we showed that an extension is a strongly admissible extension of AF F if and only if Ext2IntF(S) is a strongly admissible interpretation of the associated ADF DF. Thus, the map of each Hi via Ext2IntF(.), such that Hi is as in Lemma 30, is a strongly admissible interpretation of DF. However, by Theorem 32, ΓD,vj(vu) as in Lemma 26 is a map of an Hi if and only if j is an even number, i.e., Ext2IntF(Hi)=ΓD,v2i(vu), for i with i0.

7.Conclusion

In this work we have defined the concept of strong admissibility semantics for ADFs, based on the concept of strongly justified arguments. From a theoretical perspective, in Section 3, we observe that the strongly admissible interpretations of a given ADF form a lattice with the trivial interpretation as the unique minimal element and the grounded interpretation as the unique maximal element. Furthermore, in Section 4 we prove that the concept of strong admissibility semantics of ADFs forms a proper generalization of the concept of strong admissibility semantics of AFs [8,21].

In addition, in Section 5 we present an alternative definition for an interpretation being strongly admissible without checking whether all the arguments that are presented in that interpretation are strongly justified. This leads to Algorithm 1 to answer the verification problem under strong admissibility semantics of ADFs. Moreover, based on the new definition of strongly admissible interpretations of ADFs, we present an alternative definition for an argument being strongly justified in a given interpretation, in which there is no need to find a set of arguments that satisfies the conditions of Definition 18, for a given argument. This definition leads to Algorithm 2, to answer the decision problem whether a given argument is a strongly justified argument in a given interpretation.

In Section 6, we indicate further relations between the sequence of strongly admissible extensions of an AF F and the sequence of strongly admissible interpretations of the associated ADF DF. That is, we show that there is no one-to-one relation between the sequence of strongly admissible extensions constructed based on a strongly admissible extension S of a given AF F and the sequence of strongly admissible interpretations constructed based on Ext2Int(S) of the associated ADF DF.

It is a possible topic of future research to show that the notion of strong admissibility semantics of ADFs can be reused for those generalizations of AFs that can be represented in ADFs, namely SETAFs [48] and bipolar AFs [31].

In addition, we proved that each grounded interpretation is the unique maximal element of the lattice of strongly admissible interpretations. Thus, it seems that the concept of strong admissibility can play a significant role in the dialectical proof procedures that we have introduced for grounded semantics in [40]. The idea of the grounded discussion games presented in [40] is that a discussion game can serve as an explanation why a particular argument should be accepted/denied in the grounded interpretation of a given ADF.

Since the grounded semantics is the unique maximal element of the lattice constructed by strongly admissible interpretations, the concept of strong admissibility is related to grounded semantics in a similar way as the concept of admissibility is related to preferred semantics. That is, to answer the credulous decision problem of an ADF under the grounded semantics, there is no need to construct the full grounded interpretation of the given ADF. Instead, it is enough to construct a strongly admissible interpretation of the given ADF that satisfies the decision problem. In other words, answering the credulous decision problem of ADFs under the grounded semantics is equivalent to answering the same decision problem under the strong admissibility semantics. Similarly, to answer the credulous decision problem of ADFs under preferred semantics, it is enough to investigate whether there exists an admissible interpretation in order to solve the decision problem. We used this method in preferred discussion games in [39] to answer the credulous decision problem of ADFs under preferred semantics.

On the other hand, the grounded discussion game (GDG) presented in [40] was defined over ADFs without any redundant links, to answer whether a given argument is credulously justifiable under the grounded semantics of an ADF. However, the concept of strongly admissible semantics is presented for all kinds of ADFs. Thus, we will investigate whether the concept of strongly admissible semantics is at the basis of the proof procedures of the grounded discussion games for ADFs without any redundant links.

Intuitively, it seems that the grounded discussion game and a strongly admissible interpretation are two sides of the same coin to investigate whether a queried argument is credulously justified in the grounded interpretation of an ADF. Moreover, both methods can be used to explain ‘why is an argument credulously justified in the grounded interpretation?’ Thus, a motivation for future work is to study the relation between these two approaches.

In addition, another possible question that can be answered using the concept of strongly admissible semantics of ADFs is whether a grounded discussion game contains the least possible amount of information about the truth values of ancestors of the argument in question to answer the credulous decision problem under grounded semantics; in other words, whether the grounded discussion game presents the shortest explanation that answers the credulous decision problem under strongly admissible/grounded semantics for a given argument in an ADF. This question is interesting, since specifically when the proponent wins the game, we are eager to know whether the proponent presents the least possible amount of information to convince the opponent about the truth of their initial claim, i.e., acceptance/denial of an argument in the grounded interpretation.

Computational complexity results of different semantics of AFs and ADFs are presented in [35,43,49,56]. Computational complexity of strongly admissible semantics of AFs is studied in [36]. Further, in [26], the computational complexity of identifying strongly admissible labellings with bounded or minimal size is studied. As a future work, it would be interesting to clarify the computational complexity of investigating: (1) whether a given interpretation is a strongly admissible interpretation, (2) whether a given argument is credulously/skeptically justifiable under the strongly semantics of a given ADFs.

Notes

1 The reader interested in several types of semantics of AFs is referred to [5,34].

2 Caminada and Dunne [25] describe the intuition behind the min-max number of an argument as follows: ‘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.’

3 In [6,25], it is shown that Ext2Lab is not a surjective function and function Lab2Ext is not an injective function, for strong admissibility semantics of a given AF.

Acknowledgements

The authors would like to thank Martin Caminada and Stefan Woltran for their recommendations for presenting and investigating the notion of strongly admissible semantics for ADFs. This research is supported by the Center of Data Science & Systems Complexity (DSSC) Doctoral Programme, at the University of Groningen.

Appendices

Appendix

AppendixFull proofs

Proof of Proposition 20.

  • (1) Assume that aS. We show that a is only assigned to t in Ext2IntF(S). By Definition 24, it definitely holds that atExt2IntF(S), thus auExt2IntF(S). We show that a cannot assign to f in Ext2IntF(S). Toward a contradiction, assume that afExt2IntF(S). That is, by Definition 24, there exists a parent pa of a such that paS. However, this means that S contains conflicting arguments, i.e., a and pa with (pa,a)R. Thus, S is not a conflict-free extension. This contradicts the assumption that S is a conflict-free extension of F. Thus, the assumption that afExt2IntF(S) is wrong.

  • (2) Assume that aS. We show that either afExt2IntF(S) or auExt2IntF(S), but not both. Either at least one parent of a belongs to S or none of them belong to S. By Definition 24, it is straightforward that if aS and a parent of a belongs to S, then afExt2IntF(S). In other words, if aS and none of the parents of a belong to S, then auExt2IntF(S). That is, if aS, then either afExt2IntF or auExt2IntF(S) but not both.

Thus, if S is a conflict-free extension, then Ext2IntF(S) is well-defined. □

Proof of Proposition 21.

We show that Lab2Int and Int2Lab are bijective functions. To this end, we show that Lab2Int is a surjective and injective function. Let λ be a labelling. We define interpretation vλ as follows:

vλ(a)=tif λ(a)=in;fif λ(a)=out;uif λ(a)=undec
By Definition 26, it holds that Lab2Int(λ)=vλ. Thus, Lab2Int(.) is a surjective function.

Toward a contradiction, assume that Lab2Int(.) is not an injective function. That is, there are λ1,λ2L such that Lab2Int(λ1)=Lab2Int(λ2), and λ1λ2. That is, there exists a such that λ1(a)λ2(a). Thus, by Definition 26, Lab2Int(λ1)(a)Lab2Int(λ2)(a), i.e., Lab2Int(λ1)Lab2Int(λ2). This contradicts our assumption. Thus, the assumption that Lab2Int(.) is not an injective function was wrong.

Thus, Lab2Int is a bijective function. With a similar method we have that Int2Lab(.) is a bijective function. Thus, Lab2Int and Int2Lab have inverse functions.

Let v be an interpretation. We show that Lab2Int(Int2Lab(v))=v. (1) If atv, then by Definition 27, Int2Lab(v)(a)=in. Then, by definition 26, Lab2Int(Int2Lab(a))=t. (2) If afv, then by Definition 27, Int2Lab(v)(a)=out. Then, by Definition 26, Lab2Int(Int2Lab(a))=f. (3) If auv, then by Definition 27, Int2Lab(v)(a)=undec. Then, by Definition 26, Lab2Int(Int2Lab(a))=u. Thus, Lab2Int(Int2Lab(v))=v. Hence, Lab2Int(Int2Lab(.))=idV. With the same method it is easy to show that, Int2Lab(Lab2Int(.))=idL. Thus, Lab2Int(.) is the inverse of Int2Lab(.). □

Proof of Lemma 22.

  • Assume that λ is a strongly admissible labelling of F. Let v=Lab2Int(λ). By Definition 8, a strongly admissible labelling λ of F is an admissible labelling whose min-max numbering yields natural numbers only. We show that v is a strongly admissible interpretation of DF. To this end, we show that if ain/outλ, then a is a strongly justified argument in v. We show this by induction on the min-max numbering of arguments.

    Base case: If ain/outλ and the min-max numbering of a is 1, then we show that a is a strongly justified in v. If the min-max numbering a is 1, then a is an initial argument of F and DF. That is, φavu. Thus, a is strongly acceptable in v.

    Induction hypothesis: For all j with 0j<i, if ain/outλ and the min-max numbering a is j, then a is a strongly justified argument in v.

    Inductive step: We show that if ain/outλ and the min-max numbering a is i, then a is a strongly justified argument in v.

    • (1) Assume that ainλ and min-max numbering a is i. Since λ is a strongly admissible labelling of F, it is also an admissible labelling of F. Thus, ainλ implies that any attacker of a, namely pa is labelled out in λ. That is, by Definition 26, each attacker of a is assigned to f in v, i.e., pafv. Thus, φav=((b,a)R¬b)v. By Definition 7 (min-max numbering) and since λ is a strongly admissible labelling of F, for each attacker pa, it holds that MML(pa)<MML(a) (otherwise, MML does not yield natural numbers). Since MML(pa)<i and λ(pa)=out, by the induction hypothesis, each pa is strongly deniable in v. This implies that the conditions of Definition 18 are satisfied for a. Thus, a is strongly acceptable in v.

    • (2) By the similar proof method one can check when aoutλ, then a is strongly deniable in v.

    Thus, v is a strongly admissible interpretation of DF.

  • Let v be a strongly admissible interpretation of DF. Let λ=Int2Lab(v). We show that λ is a strongly admissible labelling of F. To this end, we show that λ is an admissible labelling whose min-max numbering yields natural numbers only.

    • (1) Since by Theorem 11 each strongly admissible interpretation is an admissible interpretation, v is an admissible interpretation. Thus, λ=Int2Lab(v) is an admissible labelling of F.

    • (2) To complete the proof, we show that min-max numbering of λ leads to natural numbers only. For each a with at/f, let va be a least witness of strong admissibility of a (as Definition 20), where vaiv. We show that the maximum level of a in a least va is equal to the min-max numbering of a in λ.

      (a) Assume that atv (i.e., ainλ). Thus, by the acceptance condition of a and since each AF does not have any redundant links, for each parent pa of a it holds that pafv (i.e., paoutλ). Thus, all parents of a are assigned to f in va. By Definition 21, the maximum level of a in va, i.e., Mv(a) is the maximum level of pa plus 1 such that pa has the maximum level among the parents of a in va. This is exactly equal to MML(a) in λ. (b) Assume that afv (i.e., aoutλ). Thus, by the acceptance condition of a and Definition 18 and since AF does not contain any redundant or dependent links, there exists a parent pa of a such that patva. Thus, the maximum level of a in va is Mva(a)=max{Mva(pa)|papar(a)vat}+1. Since va is a least interpretation that satisfies the conditions of Definition 18 for a and vaiv, it holds that Mva(pa)Mv(p), where ppar(a)v, viv, and vsadm(DF), that is pa has the minimum level among the parents of a in any interpretation v. That is, the maximum level of a in va is equal to MML(a) in λ.

      Thus, for each a with at/fv the maximum level of a in va is equal to MML(a) in λ. Furthermore, by Lemma 6, each a has a finite maximum level in va. Thus, λ is a strongly admissible labelling of F. □

References

[1] 

L. Al-Abdulkarim, K. Atkinson and T.J.M. Bench-Capon, Abstract dialectical frameworks for legal reasoning, in: Legal Knowledge and Information Systems JURIX, Frontiers in Artificial Intelligence and Applications, Vol. 271, IOS Press, Amsterdam, 2014, pp. 61–70.

[2] 

L. Al-Abdulkarim, K. Atkinson and T.J.M. Bench-Capon, A methodology for designing systems to reason with legal cases using abstract dialectical frameworks, Artificial Intelligence and Law 24(1) (2016), 1–49. doi:10.1007/s10506-016-9178-1.

[3] 

L. Amgoud, Y. Dimopoulos and P. Moraitis, A unified and general framework for argumentation-based negotiation, in: Proceedings of the 6th International Joint Conference on Autonomous Agents and Multiagent Systems, 2007, pp. 1–8.

[4] 

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

[5] 

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

[6] 

P. Baroni, M. Caminada and M. Giacomin, Abstract argumentation frameworks and their semantics, Handbook of Formal Argumentation 1 (2018), 157–234.

[7] 

P. Baroni, D.M. Gabbay, M. Giacomin and L. van der Torre, Handbook of Formal Argumentation, College Publications, London, 2018.

[8] 

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.

[9] 

T. Bench-Capon and K. Atkinson, Abstract argumentation and values, in: Argumentation in Artificial Intelligence, Springer, 2009, pp. 45–64. doi:10.1007/978-0-387-98197-0_3.

[10] 

T.J. Bench-Capon and P.E. Dunne, Argumentation in AI and law: Editors’ introduction, Artificial Intelligence and Law 13(1) (2005), 1–8. doi:10.1007/s10506-006-9007-z.

[11] 

T.J.M. Bench-Capon, Persuasion in practical argument using value-based argumentation frameworks, Journal of Logic and Computation 13(3) (2003), 429–448. doi:10.1093/logcom/13.3.429.

[12] 

R. Booth, M. Caminada and B. Marshall, DISCO: A web-based implementation of discussion games for grounded and preferred semantics, in: Proceedings of Computational Models of Argument COMMA, S. Modgil, K. Budzynska and J. Lawrence, eds, IOS Press, Amsterdam, 2018, pp. 453–454.

[13] 

G. Brewka, P.E. Dunne and S. Woltran, Relating the semantics of abstract dialectical frameworks and standard AFs, in: Twenty-Second International Joint Conference on Artificial Intelligence, Citeseer, 2011.

[14] 

G. Brewka, S. Ellmauthaler, H. Strass, J.P. Wallner and S. Woltran, Abstract dialectical frameworks. An overview, IFCoLog Journal of Logics and their Applications (FLAP) 4(8) (2017).

[15] 

G. Brewka, S. Ellmauthaler, H. Strass, J.P. Wallner and S. Woltran, Abstract dialectical frameworks: An overview, in: Handbook of Formal Argumentation, P. Baroni, D. Gabbay, M. Giacomin and L. van der Torre, eds, College Publications, 2018, pp. 237–285, Chapter 5.

[16] 

G. Brewka and T.F. Gordon, Carneades and abstract dialectical frameworks: A reconstruction, in: Proceedings of the 2010 Conference on Computational Models of Argument: Proceedings of COMMA 2010, 2010, pp. 3–12.

[17] 

G. Brewka, H. Strass, S. Ellmauthaler, J.P. Wallner and S. Woltran, Abstract dialectical frameworks revisited, in: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI 2013), 2013, pp. 803–809.

[18] 

G. Brewka and S. Woltran, Abstract dialectical frameworks, in: Proceedings of the Twelfth International Conference on the Principles of Knowledge Representation and Reasoning (KR 2010), 2010, pp. 102–111.

[19] 

E. Cabrio and S. Villata, Abstract dialectical frameworks for text exploration, in: Proceedings of the 8th International Conference on Agents and Artificial Intelligence (ICAART (2), SCITEPRESS-Science and Technology, Publications, Lda, 2016, pp. 85–95.

[20] 

M. Caminada, On the issue of reinstatement in argumentation, in: JELIA, Lecture Notes in Computer Science, Vol. 4160, Springer, 2006, pp. 111–123.

[21] 

M. Caminada, Strong admissibility revisited, in: Proceedings of Computational Models of Argument COMMA, Frontiers in Artificial Intelligence and Applications, Vol. 266, IOS Press, 2014, pp. 197–208.

[22] 

M. Caminada, A discussion game for grounded semantics, in: International Workshop on Theory and Applications of Formal Argumentation, Springer, 2015, pp. 59–73. doi:10.1007/978-3-319-28460-6_4.

[23] 

M. Caminada, Argumentation semantics as formal discussion, in: Handbook of Formal Argumentation, P. Baroni, D. Gabbay, M. Giacomin and L. van der Torre, eds, 2018, pp. 487–518.

[24] 

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

[25] 

M. Caminada and P.E. Dunne, Strong admissibility revisited: Theory and applications, Argument & Computation 10(3) (2019), 277–300.

[26] 

M. Caminada and P.E. Dunne, Minimal strong admissibility: A complexity analysis, in: Proceedings of Computational Models of Argument COMMA, Frontiers in Artificial Intelligence and Applications, Vol. 326, IOS Press, 2020, pp. 135–146.

[27] 

M. Caminada and M. Podlaszewski, Grounded semantics as persuasion dialogue, in: Proceedings of Computational Models of Argument COMMA, Frontiers in Artificial Intelligence and Applications, Vol. 245, IOS Press, 2012, pp. 478–485.

[28] 

M. Caminada and M. Podlaszewski, User-computer persuasion dialogue for grounded semantics, in: Proceedings of BNAIC, 2012, pp. 343–344.

[29] 

M. Caminada and S. Uebis, An implementation of argument-based discussion using ASPIC-, in: Proceedings of the 2020 Conference on Computational Models of Argument: Proceedings of COMMA, Frontiers in Artificial Intelligence and Applications, Vol. 326, IOS Press, Amsterdam, 2020, pp. 455–456.

[30] 

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

[31] 

C. Cayrol and M. Lagasquie-Schiex, On the acceptability of arguments in bipolar argumentation frameworks, in: ECSQARU, Lecture Notes in Computer Science, Vol. 3571, Springer, 2005, pp. 378–389.

[32] 

L.A. Chalaguine and A. Hunter, A persuasive chatbot using a crowd-sourced argument graph and concerns, in: COMMA, Frontiers in Artificial Intelligence and Applications, Vol. 326, IOS Press, 2020, pp. 9–20.

[33] 

J. Collenette, K. Atkinson and T.J.M. Bench-Capon, An explainable approach to deducing outcomes in European court of human rights cases using ADFs, in: Proceedings of Computational Models of Argument COMMA 2020, Frontiers in Artificial Intelligence and Applications, Vol. 326, IOS Press, 2020, pp. 21–32.

[34] 

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.

[35] 

W. Dvořák and P. Dunne, Computational problems in formal argumentation and their complexity, FLAP 4 (2017).

[36] 

W. Dvořák and J.P. Wallner, Computing strongly admissible sets, in: Proceedings of Computational Models of Argument COMMA 2020, IOS Press, 2020, pp. 179–190.

[37] 

S. Ellmauthaler, Abstract dialectical frameworks: Properties, complexity, and implementation, PhD thesis, Vienna University of Technology, 2012.

[38] 

A. Hunter, Towards a framework for computational persuasion with applications in behaviour change, Argument & Computation 9(1) (2018), 15–40.

[39] 

A. Keshavarzi Zafarghandi, R. Verbrugge and B. Verheij, Discussion games for preferred semantics of abstract dialectical frameworks, in: European Conference on Symbolic and Quantitative Approaches with Uncertainty, G. Kern-Isberner and Z. Ognjanovic, eds, Springer, Berlin, 2019, pp. 62–73. doi:10.1007/978-3-030-29765-7_6.

[40] 

A. Keshavarzi Zafarghandi, R. Verbrugge and B. Verheij, A discussion game for the grounded semantics of abstract dialectical frameworks, in: Proceedings of Computational Models of Argument COMMA, Frontiers in Artificial Intelligence and Applications, IOS Press, 2020.

[41] 

A. Keshavarzi Zafarghandi, R. Verbrugge and B. Verheij, Strong admissibility for abstract dialectical frameworks, in: The 36th ACM/SIGAPP Symposium on Applied Computing SAC ’21, 2021.

[42] 

A. Keshavarzi Zafarghandi, R. Verbrugge and B. Verheij, Strong admissibility for abstract dialectical frameworks, 2020, CoRR arXiv:2012.05997.

[43] 

T. Linsbichler, M. Maratea, A. Niskanen, J.P. Wallner and S. Woltran, Novel algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving, in: IJCAI, ijcai.org, 2018, pp. 1905–1911.

[44] 

P. McBurney, S. Parsons and I. Rahwan (eds), Argumentation in Multi-Agent Systems – 8th International Workshop, ArgMAS 2011, Revised Selected Papers, Taipei, Taiwan, May 3, 2011, Lecture Notes in Computer Science, Vol. 7543, Springer, 2012.

[45] 

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

[46] 

D. Neugebauer, Generating defeasible knowledge bases from real-world argumentations using D-BAS, in: Proceedings of the 1st Workshop on Advances in Argumentation in Artificial Intelligence Co-Loc