Logical theories and abstract argumentation: A survey of existing works

Abstract

In 1995, in his seminal paper introducing the abstract argumentation framework, Dung has also established the first relationship between this framework and a logical framework (in this case: logic programming). Since that time, a lot of work have pursued this path, proposing different definitions, uses and exhibiting distinct relationships between argumentation and logic. In this paper, we present a survey of existing works about this topic and more especially those that address the following question: “How logic has been used for capturing various aspects or parts of Dung’s argumentation”. This survey covers many different approaches but is not intended to be totally exhaustive due to the huge quantity of papers in this scope. Moreover, due to the fact that each approach has its own specificities, sometimes antagonistic with the other approaches, and is also justified by its own context of definition or use, the aim of this survey is not to identify one approach as being better than another.

Keywords

Abstract argumentation logics

1. Introduction

Argumentation has become an essential paradigm for Knowledge Representation and, especially, for reasoning from contradictory information [2,54] and for formalizing the exchange of arguments between agents in, e.g., negotiation [3]. Two main classes of approaches exist in computational argumentation: structured argumentation and abstract argumentation. The difference between these classes is on their starting point: works corresponding to the first class are about building arguments and identifying their relationships, whereas works in the second class consider that a collection of arguments interacting with each other is given [54], thereby disregarding the topic of building altogether. Because of these “abstract inputs”, abstract frameworks have greatly eased the modelling and study of argumentation, allowing to focus, in particular, on the different ways for determining “acceptable” sets of arguments called extensions.

The relationship between abstract argumentation and logic has actually been exploited right from the start, in the seminal article [54] introducing abstract argumentation where Dung establishes a formal equivalence between argumentation frameworks and logic programs. Since this work, this relationship has been the theme of intensive research, and several correspondences between abstract argumentation and different logical theories have been established. The number of works in this topic is so huge that there is a critical need to clarify the links between all these works and that is the main aim of our paper.

So, this article is a survey about abstract argumentation papers that have a strong emphasis on logic. Two categories of approaches can be identified: (1) approaches taking advantage of logic to capture various aspects of abstract argumentation; (2) approaches embedding “logical structures” into abstract argumentation.1

¹
For instance, an encoding of logic programs under the form of argumentation frameworks, or the creation of an argumentation framework using logical knowledge bases (see for instance, papers as [14]).

For this paper, considering that this survey is published on the occasion of the 25 years of Dung’s approach, we have chosen to discuss only works related to category (1) for the following reason: this a well-delimited category whereas the second one is less clearly defined; in particular, one can found in the second category some approaches also related to the structured argumentation and not only to the abstract argumentation.

Focussing on the many papers that provide an answer to the question “How can logic be used for achieving abstract argumentation?”, we attempt to follow the same pattern for each work reviewed:2

Note that, even if we tried to give an uniform presentation of the different approaches, some of them will be sometimes over-represented, either because of the huge number of publications concerning them, or because of the need of some additional explanations (examples have been added in order to illustrate some complex notions used in the presented approaches).

Since at the heart of these works is a correspondence between argumentation frameworks and logical formulae (or sets thereof), we first identify the entry points of the correspondence. Indeed, while the main input is usually an argumentation graph, some approaches handle an extended argumentation graph, be it bipolar, recursive, weighted, with collective interactions, and so on. There may also be extra inputs, for instance, special requirements and constraints, a distinguished subset of the arguments in the graph, a given argumentative semantics.

Second, the aim of the approach reviewed is explicited, whether is it to provide a logical encoding of an argumentation graph, or to answer a question such as “is this subset of the arguments a preferred extension of the argumentation graph?”.

Third, we have a look at the type of logic employed in the work reviewed. Propositional logic is the most widely used, either as such or extended to Quantified Boolean Formulae, but some approaches resort to (possibly many-sorted) predicate logic, modal logics, as well as constructive logics (including intuitionistic logic) either directly or through a theoretical account of logic programming.

Fourth, we list the auxiliary items involved in the approach at hand, e.g., labellings, signed atoms.

Fifth, we deal with the question: Has the work reviewed been implemented?

In addition, the main topic in each case is of course about the role of logic in the work reviewed.

We now present the content of our survey in more detail. Section 2 gives the necessary background about abstract argumentation [6,28,31,54,81]. Then the presented works are split over several sections, as follows.

Section 3 is devoted to a single approach, Abstract Dialectical Frameworks (see for instance [21]), a general formalism for representing complex dependence links between arguments. In our terminology, the input consists of a dependence graph (nodes represent arguments and edges represent dependence links) together with an acceptance condition (in the form of a logical formula) attached to each node and the outputs are the logical models of the acceptance conditions, permitting to retrieve labellings and extensions.

The approaches reviewed in Section 4 aim at giving a logical theory (in propositional logic) that encodes an argumentation graph [30,33,52,67]. Multiple approaches are reviewed, that mainly vary on the logic used for the encoding: propositional logic, either pure or extended in a number of alternative ways (sorted language, modal-like language). Additional properties may map models to extensions according to a given semantics.

Section 5 reports on two approaches whose aim is to express properties over a given argumentation graph, so that these properties can be used to characterize appropriate labellings of the graph [4,49,50]. Thus, the input consists of an argumentation graph (or an abstract dialectical framework, see Section 3) together with an extension-based semantics σ. The main feature of both approaches is that the output is a Quantified Boolean Formula whose models coincide with the σ-extensions of the graph (i.e., using names of the nodes of the graph as propositional atoms, the models of the formula are exactly the σ-extensions of the graph).

Section 6 is mainly devoted to an approach called YALLA [55],3

YALLA: Yet Another Logic Language for Argumentation.

whose language permits not only to express an argumentation framework by means of specific formulae of first-order logic but also to express properties of update operators in dynamic argumentation. As an aside, a distinctive feature of YALLA is that a reference universe of argumentation is assumed, which makes it possible to capture cases of incomplete knowledge. The second approach reported in the same section proposes a propositional logic to specify and to check requirements in argumentation graphs [93]. The input consists of an argumentation graph together with constraints (such as: argument a or argument b is acceptable) and the outputs are formulae encoding the graph and the constraints, so that the models of the formulae capture properties of the argumentation graph.

In Section 7 are reviewed two approaches, [11,12] and [59], that, given an extension-based semantics σ, produce a formula $Φ_{σ}$ whose satisfiability answers the σ-extension problem for the input (usually, an argumentation graph and a candidate subset of the arguments): given a candidate S, is S an extension according to the semantics σ?

The purpose of the two approaches reviewed in Section 8, [25,36], is to encode labelling-based semantics by means of a set of logical formulae (these express the different constraints associated with a particular kind of labelling). Thus, the input is an argumentation graph together with a labelling-based semantics s and the output is a logical theory characterizing the labelling-based semantics s (depending on s, it can be that the logic needed is second-order).

The purpose of the works reviewed in Section 9 is to associate a logic program with an argumentation graph in such a way that logic programming semantics, applied to the logic program, capture argumentative semantics. In this research line, many works exist from the seminal work presented by Dung [54]: for instance, [24,26,61,83,84,89]. So, this section describes different mappings which allow to transform an argumentation graph into a logic program, all of them offering different characterizations of argumentative semantics in terms of logic programming semantics.

Section 10 reviews three methods for expressing abstract argumentation in modal logic [25,70,93], two of them taking as input an argumentation graph together with a labelling (the third method regards argumentative semantics as primitives of the language) while the output consists of modal formulae expressing the distinctive properties of a given argumentative semantics.

Section 11 deals with approaches resorting to a constructive logic (either intuitionistic or Nelson’s), where constructive negation is used to represent an attack in argumentation graphs and the models of the resulting formulae characterize the argumentative extensions of the input graph [63,68].

Lastly, Section 12 is an attempt to wrap all this up with proposing tentative conclusions suggested by the comparisons discussed throughout Sections 3–11.

Disclaimer.

We have adopted (or at least attempted to) a single procedure to present all the works reviewed in our survey, in order to make it easier for the reader to compare these works. Please note that, in the last section, we go through the same example treated in turn by all approaches in order to better illustrate the behaviour of each of them. However, it is not our aim to assess them in any way, and we are definitely not to claim that such and such approach is better than another approach.

Moreover, despite the apparent similarity in the approaches (they are all based on logic and all attempt to capture Dung’s argumentation model), it would be a formidable task to provide a comparative evaluation.

Finally, we make no claim for exhaustiveness. Some articles on the very topic of the survey may have gone unnoticed from us, others have been left out because we felt them having more emphasis on another topic or still other reasons. Of course, omitting to cite or to discuss these articles bears no quality assessment whatsoever on our behalf.

2. Abstract argumentation: Definitions and notations

2.1. Argumentation frameworks

According to [54], an abstract argumentation framework consists of a set of arguments together with a binary relation between arguments.

Def. 1 (AF [54]).

An argumentation framework (AF) is a pair $(A, R)$ where $A$ is a set4

⁴
Generally assumed to be finite.

of abstract arguments and

R \subseteq A \times A

is a binary relation on

A

, called the attack relation:

(a, b) \in R

means that a attacks b (a is the source of the interaction and b is the target).

An AF can be represented by a directed graph, called argumentation graph,5

⁵

We will often use “argumentation graph” in place of “argumentation framework”.

with vertices as arguments and edges as attacks.

Ex. 2.1.1.

The AF defined by $A = {a, b, c, d}$ and $R = {(a, b), (b, c), (d, b)}$ can be represented by the following graph (arguments are given in a circle, and attacks are denoted by simple arrows):

Many extensions of this framework have been proposed. For instance, bipolar abstract frameworks have been introduced first in [71,91]. They include a second relation between arguments, the support relation, that is a positive interaction (in contrast to the attack relation that is a negative one). In [31], the support relation is left general so that the bipolar framework keeps a high level of abstraction.

Def. 2 (BAF [31]).

A bipolar argumentation framework (BAF) is a triple $(A, R_{att}, R_{\sup})$ where $A$ is a set of abstract arguments, $R_{att} \subseteq A \times A$ (resp. $R_{\sup} \subseteq A \times A$ ) is a binary relation on $A$ , called the attack (resp. support) relation.

A BAF can still be represented by a directed graph with vertices as arguments and two kinds of edges (attacks denoted by simple arrows and supports denoted by double arrows).

Ex. 2.1.2.
Consider the following BAF with only one support.

However, there is no single interpretation of the support, and a number of researchers proposed specialized variants of the support relation (deductive support [17], necessary support [79,80], evidential support [81,82]). These proposals have been developed quite independently, based on different intuitions and with different formalizations. In [32], is presented a comparative study in order to restate these proposals in a common setting, the bipolar argumentation framework (see also [41] for another survey).

For instance, evidential support is based on the intuition that every argument must be supported by some chain of supports rooted in special arguments called prima-facie. Considering a BAF with an evidential understanding of the support leads to Evidence-Based Argumentation Frameworks (EBAF) which can be defined as follows [29]:6
⁶
The first definition of EBAF was given in [81] then modified in [87].

Def. 3 (EBAF).

An Evidence-Based Argumentation Framework (EBAF) is a 4-tuple $(A, R, E, P)$ where $A$ is a set of arguments, $R \subseteq 2^{A} ∖ {\emptyset} \times A$ is the attack relation, $E \subseteq 2^{A} ∖ {\emptyset} \times A$ is the support relation, and $P \subseteq A$ is the set of distinguished prima-facie arguments.

Another extension of AF is the higher-order AF with the idea of encompassing attacks to attacks in abstract argumentation frameworks (see [8] in the context of an extended framework handling argument strengths and their propagation). Then, higher-order attacks have been considered for representing preferences between arguments (second-order attacks in [76]), or for modelling situations where an attack might be defeated by an argument, without contesting the acceptability of the source of the attack [7]. Attacks to attacks and supports have been first considered in [64] with higher level networks, then in [92]; and more generally, in [42] an Attack–Support Argumentation Framework is proposed which allows for nested attacks and supports, i.e. attacks and supports whose targets can be other attacks or supports, at any level. Different names are given to these higher-order AF, depending on the kind of interaction that is handled: AFRA or RAF (with only attacks), ASAF or REBAF (with attacks and supports, necessary supports for ASAF and evidential supports for REBAF).

For instance, the definition of a RAF is as follows.

Def. 4 (RAF [28]).

A recursive argumentation framework (RAF) is a tuple $⟨ A, R, s, t ⟩$ where $A$ is a finite and non-empty set of arguments, $R$ is a finite set disjunct from $A$ representing attack names, s is a function from $R$ to $A$ mapping each interaction to its source, and t is a function from $R$ to $(A \cup R)$ mapping each interaction to its target.

Note that an AF can be viewed as a particular RAF with t being a mapping from $R$ to $A$ .

A RAF can also be represented graphically.

Ex. 2.1.3.
The RAF in which an attack named α (with $s (α) = a$ and $t (α) = b \in A$ ) being the target of an attack β (with $s (β) = c$ ) can be represented by:

(arguments are in a circle and attack names are in a square)

Still other extensions exist such as frameworks with collective interactions (SETAF: the source of interaction can be a set of arguments and not only one argument, as in EBAF or REBAF) and frameworks with weights over arguments or interactions.
2.2. Acceptability semantics

Case of AF. Acceptability semantics can be defined in terms of extensions [54] following basic requirements:

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

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

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

Stability expresses the fact that each argument that does not belong to the extension is attacked by the extension.

Standard AF semantics are defined as follows:

Def. 5 (Extension-based semantics [54]).

Given $(A, R)$ and $S \subseteq A$ .

S is conflict-free iff $(a, b) \notin R$ for all $a, b \in S$ .

$a \in A$ is acceptable w.r.t. S (or equivalently S defends a) iff for each $b \in A$ with $(b, a) \in R$ , there is $c \in S$ with $(c, b) \in R$ .

The characteristic function of $(A, R)$ is defined by: $F (S) = {a \in A such that a is acceptable w.r.t. S}$ .

S is admissible iff S is conflict-free and $S \subseteq F (S)$ .

S is a complete extension of $(A, R)$ iff it is conflict-free and a fixed point of $F$ .

S is the grounded extension of $(A, R)$ iff it is the minimal (w.r.t. ⊆) fixed point7

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

F

S is a preferred extension of $(A, R)$ iff it is a maximal (w.r.t. ⊆) complete extension.

S is a stable extension of $(A, R)$ iff it is conflict-free and for each $a \notin S$ , there is $b \in S$ with $(b, a) \in R$ .

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

Ex.

2.1.1 (cont’d) In this example, the set ${a, c, d}$ is the grounded, complete, preferred and stable extension.

Acceptability semantics can also be defined in terms of labellings, as in [6], for instance.

Def. 6 (Labelling [6]).

Let $(A, R)$ be an AF. A labelling for $(A, R)$ is a total function $ℓ : A \to {in, out, und}$ .

Let $ℓ$ be a labelling of $(A, R)$ .

An $in$ -labelled argument is said to be legally $in$ iff all its attackers are labelled $out$ .

An $out$ -labelled argument is said to be legally $out$ iff at least one of its attackers is labelled $in$ .

An $und$ -labelled argument is said to be legally $und$ iff it doesn’t have an attacker that is labelled $in$ and not all its attackers are labelled $out$ .

Standard labelling-based semantics are defined as follows:

Def. 7 (Labelling-based semantics [6]).

Let $ℓ$ be a labelling for $(A, R)$ .

$ℓ$ is an admissible labelling iff each $in$ -labelled argument is legally $in$ and each $out$ -labelled argument is legally $out$ .

$ℓ$ is a complete labelling iff each $in$ -labelled argument is legally $in$ , each $out$ -labelled argument is legally $out$ , and each $und$ -labelled argument is legally $und$ .

$ℓ$ is the grounded labelling iff it is the complete labelling that minimizes (w.r.t. ⊆) the set of $in$ -labelled arguments.

$ℓ$ is a preferred labelling iff it is a complete labelling of $(A, R)$ that maximizes (w.r.t. ⊆) the set of $in$ -labelled arguments.

$ℓ$ is a stable labelling iff it is a complete labelling with no $und$ -labelled argument.

Alternative characterizations of complete labellings can be found in [25]. Let us recall them as they will be used in the remainder of this document:

Prop. 1 (Characterizing complete labellings).

Let $ℓ$ be a labelling for $(A, R)$ .

$ℓ$ is a complete labelling iff for each argument a, it holds that:

If a is $in$ -labelled, then all its attackers are $out$ -labelled

If a is $out$ -labelled, then it has at least one attacker that is $in$ -labelled

If a is $und$ -labelled, then it has at least one attacker that is not $out$ -labelled and it does not have an attacker that is $in$ -labelled

$ℓ$ is a complete labelling iff for each argument a, it holds that:

a is $in$ -labelled iff all its attackers are $out$ -labelled

a is $out$ -labelled iff it has at least one attacker that is $in$ -labelled.

Case of extended AF (BAF, RAF). The associated semantics are very often defined using a flattening process: the extended AF is turned into an AF, then the AF semantics are applied (see for instance [7]). In recent works (see for instance [29]), semantics for extended AF have been defined directly.

3. ADF (Abstract Dialectical Frameworks)

The aim of the ADF approach is the definition of a general framework for representing complex dependence links between arguments (these links impact the acceptability of the arguments). It is rather a theoretical approach but several implementations have been proposed. This approach has been introduced many years ago and one of the more recent synthetic paper about ADF is [21].

The input consists of a dependence graph (nodes are arguments, statements or positions and edges are dependence links) together with an acceptance condition attached to each node. This condition can be a propositional formula8

⁸
In ADF, this condition is generally a propositional formula, but there also exist some works on ADF that specify acceptance conditions as Boolean functions that may be represented in different ways. In this survey, we only consider the case where acceptance conditions are propositional formulae.

expressing the way the status of the argument is impacted by the status of its parents in the graph. Following the acceptance conditions, one can encode an AF, a BAF (with different meanings for the support relation), a framework with sets of attacking arguments (SETAF). One can also encode an AF with higher-order interactions through the addition of meta-arguments representing interactions.

The outputs are the interpretations of the set of acceptance conditions. These interpretations allow to retrieve some labellings and extensions.

In this approach, the logic is used for encoding and interpretating the dependence links.

3.1. Main definitions

An ADF is a directed graph defined as follows:

Def. 8.
An abstract dialectical framework (ADF) is a tuple $D = (S, L, C)$ where S is a finite set of nodes, $L \subseteq S \times S$ is a set of links, and $C = {φ_{s} | s \in S}$ is a set of propositional formulae (acceptance conditions). Each $φ_{s} \in C$ is built over the set $par (s) = {a \in S | (a, s) \in L}$ (i.e. $par (s)$ is the set of the parents of s).

So the status of an argument depends on the status of its parents in the graph following the acceptance condition attached to the argument. The ideas are the following ones:
First, the status “accepted” (resp. “rejected”, “unknown”) of an argument is related to its assignment with the truth value t (resp. f, u).9
⁹
t for true, f for false and u for unknown.

Second, let s be an argument, let $par (s)$ be the set of the parents of s in the dependence graph, let $φ_{s}$ be the acceptance condition associated with s and consider $R \subseteq par (s)$ . $φ_{s} (R)$ denotes the truth value of $φ_{s}$ using the truth value of the elements of R. Then $φ_{s} (R)$ is used for determining the status of s: if $φ_{s} (R) = t$ (resp. f, u) then s is accepted (resp. rejected, unknown).

Note that the dependence links can be extracted from the acceptance conditions. So in general the ADF is defined only with the set of arguments and their acceptance conditions: $D = (S, {φ_{s} | s \in S})$ .

ADF semantics. In terms of semantics, two operators can be defined, one for two-values semantics and another one for three-valued semantics. The idea behind these operators is the following one: starting from a given interpretation, the use of the operator allows to browse the set of possible interpretations (two-valued or three-valued) taking into account the impact of acceptance conditions on the interpretations. The aim is to find a fixed point if it exists (it is always the case for three-valued operators).
Def. 9 (Two-valued operator).

Let $D = (S, {φ_{s} | s \in S})$ be an ADF. The two-valued operator $G_{D}$ takes a two-valued interpretation v of each argument and returns a two-valued interpretation $v^{'}$ mapping each argument s to the truth value that is obtained by evaluating its acceptance condition $φ_{s}$ with v.

Thus, for v a two-valued interpretation, $G_{D} (v) = v^{'}$ where for $s \in S$ , $v^{'} (s) = v (φ_{s})$ .

In the case of a three-valued operator, the idea is similar. However, due to the existence of the third value (u for unknown) a specific technique must be used:

Def. 10 (Three-valued operator).

Let $D = (S, {φ_{s} | s \in S})$ be an ADF. The three-valued operator $Γ_{D}$ takes a three-valued interpretation v of each argument and returns a three-valued interpretation $v^{'}$ corresponding to the consensus truth value for the acceptance condition where this consensus takes into account all possible two-valued interpretations w that extend the input interpretation v.

Then semantics for interpretations can be defined using either a two-valued operator or a three-valued operator and a preordering between interpretations. Two preorderings can be defined:

Def. 11 (Preordering $⩽_{t}$ on two-valued interpretations).

Let $(S, {φ_{s} | s \in S})$ be an ADF. Let $v_{1}$ and $v_{2}$ be two-valued interpretations. $v_{1} ⩽_{t} v_{2}$ if and only if $\forall s \in S$ , $v_{1} (s) = t \Rightarrow v_{2} (s) = t$ .

Def. 12 (Preordering $⩽_{i}$ on three-valued interpretations).

Let $(S, {φ_{s} | s \in S})$ be an ADF. Let $v_{1}$ and $v_{2}$ be three-valued interpretations. $v_{1} ⩽_{i} v_{2}$ if and only if $\forall s \in S$ , $v_{1} (s) \in {t, f} \Rightarrow v_{2} (s) = v_{1} (s)$ .

Some semantics can be defined as follows:10

¹⁰
The definition for the stable models is not given here but can be found in [21] (a model being an interpretation v such that $\forall s \in S$ , $v (s) = v (φ_{s})$ ).

Def. 13.

Let $D = (S, {φ_{s} | s \in S})$ be an ADF. Let v be a three-valued interpretation.

v is complete for D iff $v = Γ_{D} (v)$ .

v is admissible for D iff $v ⩽_{i} Γ_{D} (v)$ .

v is preferred for D iff v is $⩽_{i}$ -maximal admissible.

v is grounded for D iff v is the $⩽_{i}$ -least fixed point of $Γ_{D}$ .

Note that the well-known relationships between AF semantics also hold for ADF semantics:

Prop. 2.

Let $D = (S, {φ_{s} | s \in S})$ be an ADF.

Each stable model of D is a two-valued model of D.

Each two-valued model of D is a preferred interpretation of D.

Each preferred interpretation of D is complete.

Each complete interpretation of D is admissible for D.

The grounded interpretation of D is complete. 11

¹¹

Note that the grounded interpretation is unique.

ADF as a modelling tool. An ADF can be used for modelling variants of abstract argumentation frameworks such as AF, BAF, RAF. A significant survey can be found in [85,86].

Case of AF: Let $(A, R)$ be an AF, its associated ADF is defined by the pair $(A, {φ_{a} | a \in A})$ with $φ_{a} = ⋀_{b \in A, (b, a) \in R} \neg b$ . Each Dung’s semantics can be retrieved using ADF semantics.

Case of AF with annotated links and/or preferences: An ADF can be used for expressing the impact of annotated links representing qualitative or quantitative preferences and/or preorderings between arguments.

First, consider the case of a weighted AF (i.e. an AF with numerical weights attached to each interaction representing quantitative preferences).

A positive (resp. negative) value on a link means that this link is a support (resp. attack) link;

A link is said “active” if its source node is accepted;

A node will be accepted if the sum of the weights of all the active links pointing to it is positive (strategy sum-of-weights – sow).

Example 3.2.6 given in the next section illustrates the above ideas.

Qualitative preference can be handled in a similar way, particularly for the input arguments. Note also that these kinds of annotated links can be used for expressing richer interactions such as, for instance, those used in legal reasoning (notions of “valid”, “strong”, “credible” and “weak” arguments and principles of “scintilla of evidence”, “preponderance of evidence”).

Case of BAF: An annotated AF can be used for modelling a BAF (particularly the qualitative version with + on the support links and − on the attack links). Nevertheless, as different meanings exist for the support, several encodings can be defined (see Ex. 2.1.2 in the next section).

Case of AFRA, RAF: In an ADF, no recursive link exists. So in order to represent an AFRA or a RAF with an ADF, flattening techniques must be used (for instance, the one described in [7] for translating an AFRA into an AF). See Ex. 2.1.3 in the next section.

3.2. Some examples

The previous ADF definitions are illustrated on the following examples (most of them are issued from [21]).

Ex. 3.2.1.
Consider the ADF represented by:

Intuitively, $φ_{a}$ states that a should be accepted. Condition $φ_{b}$ expresses a kind of self-support for b. $φ_{c}$ says that c will be accepted if both a and b are accepted whereas $φ_{d}$ says that d is attacked by b. Note that strictly speaking, the attack from b to d is represented by the assertion “If b is accepted then d is not accepted” or equivalently “If d is accepted then b is not accepted”, which is a necessary condition for the acceptance of d. It is worth noticed that such statements refer, implicitly, to argumentation semantics. The converse condition which writes “If b is not accepted then d is accepted” expresses a kind of reinstatement. So, at least for the attack links, the acceptance condition is a necessary and sufficient condition.

The mechanism used for the two-valued operator is illustrated by Fig. 3 (given at the end of this paper) that represents the evolution of interpretations by the operator $G_{D}$ (nodes = interpretations and edges = the relation between two interpretations defined by the operator).

Consider for instance $v = {a \mapsto t, b \mapsto t, c \mapsto t, d \mapsto t}$ . For each acceptance condition, it can be seen how the operator produces the updated interpretation $v^{'}$ :
$φ_{a} = ⊤$ : so $v^{'} (a) = t$ (v has no impact since a has no parent in the ADF);

$φ_{b} = b$ : so $v^{'} (b) = v (b) = t$ (v has an impact since b is its own parent);

$φ_{c} = a \land b$ : so $v^{'} (c) = v (a) \land v (b) = t$ (v has an impact since a and b are the parents of c);

$φ_{d} = \neg b$ : so $v^{'} (d) = \neg v (b) = f$ (v has an impact since b is the parent of d).

So, the operator applied to $v = {a \mapsto t, b \mapsto t, c \mapsto t, d \mapsto t}$ produces the interpretation $G_{D} (v) = v^{'} = {a \mapsto t, b \mapsto t, c \mapsto t, d \mapsto f}$ .

Consider now $v^{'} = {a \mapsto t, b \mapsto t, c \mapsto t, d \mapsto f}$ and, using the same way, compute the interpretation $G_{D} (v^{'}) = v^{″}$ . It is easy to see that $v^{″}$ is exactly $v^{'}$ . So $v^{'}$ is a fixed point for the operator $G_{D}$ . Note that, in this example, there exist 2 fixed points (each fixed point being by definition a two-valued model).

This example also illustrates the preordering $⩽_{t}$ , see Fig. 4 (given at the end of this paper). Note that the set of two-valued interpretations over $⩽_{t}$ consists of a complete lattice (the top element of the lattice is at the top of the figure and the bottom element is at the bottom of the figure).

Unfortunately, due to the important number of three-valued interpretations of this example ( $3^{4} = 81$ three-valued interpretations), we do not represent the $⩽_{i}$ preordering and the corresponding complete meet-lattice in a figure. Nevertheless, some interesting three-valued interpretations can be identified:
$v_{0} = {a \mapsto t, b \mapsto u, c \mapsto u, d \mapsto u}$ ,

$v_{1} = {a \mapsto t, b \mapsto t, c \mapsto t, d \mapsto f}$ that is also a two-valued interpretation and a fixed point of $G_{D}$ (so a two-valued model),

$v_{2} = {a \mapsto t, b \mapsto f, c \mapsto f, d \mapsto t}$ that is also a two-valued interpretation and a fixed point of $G_{D}$ (so a two-valued model),

$v = {a \mapsto t, b \mapsto f, c \mapsto f, d \mapsto u}$ .

Following Def. 13, $v_{0}$ , $v_{1}$ and $v_{2}$ are complete (they are the only fixed points of $Γ_{D}$ ). Moreover $v_{1}$ and $v_{2}$ are preferred and $v_{0}$ is grounded. It can be shown that v is admissible.12
¹²
Moreover, $v_{2}$ is also the stable model of the ADF.

The next example illustrates the three-valued operator and the $⩽_{i}$ preordering.
Ex. 3.2.2.
Consider the ADF represented by:

Figure 5 (given at the end of this paper) represents the evolution of interpretations by the three-valued operator $Γ_{D}$ for the ADF (nodes = interpretations and edges = the relation between two interpretations defined by the operator).

First, consider $v = {a \mapsto u, b \mapsto f, c \mapsto t}$ . The two possible two-valued interpretations that extend v are: $w_{1} = {a \mapsto t, b \mapsto f, c \mapsto t}$ and $w_{2} = {a \mapsto f, b \mapsto f, c \mapsto t}$ . Consider now each acceptance condition and let us see how the operator produces the updated interpretation $v^{'}$ :
With $w_{1}$ :

$φ_{a} = ⊥$ : so $w_{1}^{'} (a) = f$ ( $w_{1}$ has no impact since a has no parent in the ADF);

$φ_{b} = a \lor b \lor \neg c$ : so $w_{1}^{'} (b) = t$ ( $w_{1}$ has an impact since b as three parents – a, b and c –);

$φ_{c} = \neg a \lor \neg b$ : so $w_{1}^{'} (c) = t$ ( $w_{1}$ has an impact since c as two parents – a and b –);

With $w_{2}$ :

$φ_{a} = ⊥$ : so $w_{2}^{'} (a) = f$ ( $w_{2}$ has no impact since a has no parent in the ADF);

$φ_{b} = a \lor b \lor \neg c$ : so $w_{2}^{'} (b) = f$ ( $w_{2}$ has an impact since b as three parents – a, b and c –);

$φ_{c} = \neg a \lor \neg b$ : so $w_{2}^{'} (c) = t$ ( $w_{2}$ has an impact since c as two parents – a and b –);
Then, using $w_{1}^{'}$ and $w_{2}^{'}$ , one can compute the consensus truth value for each argument: $v^{'} (a) = f$ (since $w_{1}^{'} (a) = w_{2}^{'} (a) = f$ ), $v^{'} (b) = u$ (since $w_{1}^{'} (b) \neq w_{2}^{'} (b)$ ), $v^{'} (c) = t$ (since $w_{1}^{'} (c) = w_{2}^{'} (c) = t$ ).

Another example of this process can be given with the interpretation $v^{'} = {a \mapsto f, b \mapsto u, c \mapsto t}$ . The two possible two-valued interpretations that extend $v^{'}$ are: $w_{1}^{'} = {a \mapsto f, b \mapsto t, c \mapsto t}$ and $w_{2}^{'} = {a \mapsto f, b \mapsto f, c \mapsto t}$ .

With $w_{1}^{'}$ , we obtain $w_{1}^{″} (a) = f$ , $w_{1}^{″} (b) = t$ and $w_{1}^{″} (c) = t$ .

With $w_{2}^{'}$ , we obtain $w_{2}^{″} (a) = f$ , $w_{2}^{″} (b) = f$ , $w_{2}^{″} (c) = t$ .

Then, using $w_{1}^{″}$ and $w_{2}^{″}$ , the consensus truth value for each argument is $v^{″} (a) = f$ , $v^{″} (b) = u$ , $v^{″} (c) = t$ . This three-valued interpretation is one of the three fixed points of this example.

In this example, the preordering $⩽_{i}$ is given by Fig. 6 (given at the end of this paper). Note that the set of three-valued interpretations over $⩽_{i}$ consists of a complete meet-lattice (the top elements of the meet-lattice are at the top of the figure and the bottom element is at the bottom of the figure).

Here are some interesting three-valued interpretations:
$v_{0} = {a \mapsto f, b \mapsto u, c \mapsto t}$ ,

$v_{1} = {a \mapsto f, b \mapsto t, c \mapsto t}$ (that is also a two-valued model),

$v_{2} = {a \mapsto f, b \mapsto f, c \mapsto t}$ (that is also a two-valued model).

$v_{0}$ , $v_{1}$ and $v_{2}$ are complete (they are the only fixed points of $Γ_{D}$ ), $v_{1}$ and $v_{2}$ are preferred and $v_{0}$ is grounded.

The following examples illustrate the use of ADF as a modelling tool.
Ex. 3.2.3.
The sequence of two attacks can be translated into the following ADF:

Applying the $G_{D}$ or the $Γ_{D}$ operators gives only one fixed point: $v = {a \mapsto t, b \mapsto f, c \mapsto t}$ . That corresponds to the complete, preferred and grounded extension.
Ex. 3.2.4.
Two attacks to the same argument can be translated into the following ADF:
Ex. 3.2.5.
An even-length cycle of attacks can be translated into the following ADF:

Applying the $Γ_{D}$ operator gives three fixed points: $v_{0} = {a \mapsto u, b \mapsto u}$ , $v_{1} = {a \mapsto t, b \mapsto f}$ and $v_{2} = {a \mapsto f, b \mapsto t}$ . That corresponds to the complete extensions, $v_{0}$ being the grounded one and $v_{1}$ , $v_{2}$ being the preferred ones.
Ex. 3.2.6.
The following graph represents a weighted AF.

Considering that the set ${a, c}$ is the subset of the input arguments that are accepted (so even if b is an input argument it is not considered as accepted), this weighted AF by an ADF can be turned into the following ADF:
Ex.
2.1.2 (cont’d) Consider a BAF with only one support from a to b. Following [21], the encoding of a support could be done using a positive link between a and b in the corresponding ADF. Nevertheless, in order to find the best encoding of the BAF into an ADS, we must identify the direction of this link and the acceptance conditions. These elements will depend on the meaning of the used support (indeed, recall that several meanings exist for the support relation in the literature); in this example, we are interested in the deductive and necessary supports. Moreover, in an ADF, it is important to note that the acceptance condition can be viewed as a sufficient and necessary condition.

Let consider the following possible encoding: a positive link from a to b with $φ_{b} = a$ and $φ_{a} = ⊤$ . So, in this case, $φ_{b}$ corresponds to the two following conditions: “if a is accepted then b is accepted” (that is the sufficient condition), and “a is accepted if b is accepted” (that is the necessary condition).

Consider now that the support is a deductive one. Then the meaning of this support in argumentation semantics can be described by the following assertion (the target of the support is impacted by its source): $\begin{array}{l} “if a is accepted then b is accepted”. \end{array}$

With the proposed encoding, the sufficient condition given by $φ_{b}$ encodes exactly the deductive meaning of the support but the necessary condition issued from $φ_{b}$ gives an additional constraint and we can easily see that this additional constraint corresponds to the necessary meaning of the support.

Indeed, the meaning of the necessary support from a to b in argumentation semantics can be described by the following assertion (the target of a support impacts its source): $\begin{array}{l} “ a is accepted if b is accepted”. \end{array}$

The same problem appears when we try to represent a necessary support from a to b or when we use another encoding changing the direction of the link and the acceptance condition (a positive link from b to a with $φ_{a} = b$ and $φ_{b} = ⊤$ ). In each case, we obtain a formula that encodes both the deductive meaning of the support (“if a is accepted then b is accepted”) and the necessary meaning of the support (“a is accepted if b is accepted”). Even if there is a difference between the two ADFs (the formula is attached either to b – deductive support –, or to a – necessary support –), when there is no other interaction from, or to, these two arguments, the acceptance conditions do not allow to distinguish between the two meanings of the supports in argumentation semantics.

A synthesis of the above remarks is given in the following table. Let us consider a support from a to b, denoted by the pair $(a, b)$ :

in ADF Sufficient condition of $φ_{b} = a$ Necessary condition of $φ_{b} = a$ Sufficient condition of $φ_{a} = b$ Necessary condition of $φ_{a} = b$

in BAF Deductive meaning of $(a, b)$ Necessary meaning of $(a, b)$ Necessary meaning of $(a, b)$ Deductive meaning of $(a, b)$

In conclusion, as the acceptance condition in an ADF reads as a necessary and sufficient condition, and without another mechanism (specific interpretations for instance), it seems difficult to capture a support which is not both necessary and deductive in argumentation semantics.
Ex.
2.1.3 (cont’d) Consider the RAF with an attack named α (from a to b) attacked by another attack named β whose source is c.

Using the flattening technique, this RAF can be turned into the following AF (the RAF is translated into an AF by the addition of new arguments, one for each attack, and the definition of a new set of attacks; for more details, see for instance [7]):

This AF can be in turn represented by the following ADF:
3.3. Some implementations

Several implementations have been proposed for ADF (see [22,23]). Here are some of them:13

¹³
This list is not exhaustive. For instance, the reader can also refer to YADF [19] or to k++ADF [75].

DIAMOND

(DIAlectictal MOdels eNcoDing) is based on Answer Set Programming (ASP). DIAMOND translates an ADF into an ASP program whose stable models correspond to models of the ADF with respect to several semantics (i.e. admissible, complete, stable, grounded).

QADF

is a system for solving reasoning problems on ADF using Quantified Boolean Formulae (QBF).14

¹⁴

These formulae are a generalization of the propositional formulae in which both existential quantifiers and universal quantifiers can be applied to each variable.

Given an ADF and a reasoning problem as input, QADF returns the encoding of the reasoning problem as a QBF for that ADF. Then, a subsequent QBF solver solves the reasoning task.

UNREAL

(Uniform Account of Realizability in Abstract Argumentation) is a system based on ASP for deciding realizability of a given set of interpretations. It supports AFs, ADFs, the subclass of bipolar ADFs (BADFs), and frameworks with sets of attacking arguments (SETAFs). For each of these formalisms, realizability can be tested for the standard semantics, namely admissible, complete, preferred and two-valued models (stable semantics for (SET)AFs). In words, given a set of interpretations V, a formalism F and a semantics σ, UNREAL computes all knowledge bases K of type F having $σ (K) = V$ . Optionally, the output can be converted into the format readable by ASPARTIX (see Section 9.3) or DIAMOND.

GrappaVis

is a Java tool for specifying and evaluating GRAPPA and ADF instances (GRAPPA being a semantical framework for graph-based argument processing − GRAPPA = GRaph-based Argument Processing based on Patterns of Acceptance). GrappaVis is a graphical tool for specifying GRAPPA and ADF-instances, evaluating them and visualizing the results of the evaluation. GrappaVis itself is a JAVA-application based on the JGraphX framework and therefore provides intuitive tools to draw GRAPPA / ADF instances. For the evaluation it makes use of two different types of ASP encodings.

3.4. Related works

As shown before, the ADF approach is able to encompass several approaches of abstract argumentation. The main difficulty rests in the choice of the right acceptance conditions appropriate to a given framework.

The idea to attach an acceptance condition to an AF has also been used in [43]. In this approach, a constrained argumentation framework (CAF) has been defined as an AF associated with an acceptance condition that is a propositional formula. As in ADF, this propositional formula is defined over a vocabulary built on the set of arguments. Nevertheless there exist important differences between a CAF and an ADF:

the graph used in [43] is a standard argumentation graph (links encode attacks) and not a dependence graph,

there is a unique acceptance condition in [43] and not one attached to each argument,

In [43] are defined new semantics by combining standard semantics with the satisfaction of the acceptance condition.

The following example illustrates this approach.

Ex. 3.4.1.
Consider the CAF built with the following AF and the propositional formula $C = a \land \neg e$ :

There are 2 preferred extensions ${a}$ and ${b, d}$ for the AF.

Then taking into account the acceptance condition C, only the first one can be considered as an extension for the CAF.
4. Translation of AF into propositional logic

The approaches reviewed in this section aim at giving a logical theory (in propositional logic) that encodes an AF. That is, for each of these approaches, the input is an AF and the output is a theory in propositional logic. They are theoretical approaches, but the output theories supplemented with formulae capturing a given argumentation semantics, can be fed into a SAT solver. In these approaches, the logic (propositional logic, either pure or extended in a number of alternative ways: sorted language, modal-like language) is used to encode the AF. Additional properties may map models to extensions according to a given semantics.

4.1. The syntactic sugar way

The simplest approach for encoding an AF consists of introducing special propositional atoms in the language in order to denote the edges of the argumentation graph ( ${Att}_{a, b}$ in [52], $r_{a, b}$ in [56]15

¹⁵
See also Section 6. In the YALLA language, a specific predicate has been introduced for encoding an attack between sets of arguments: $x ⊳ y$ .

). These special atoms are considered as always true.

The description needs not include propositional atoms of the form ${Arg}_{a}$ (or the like) that would explicitly list the nodes of the argumentation graph.

4.2. The approach by Cayrol et al.

This approach has been presented in several papers [30,33,34]. The definitions presented here are those given in the more recent paper [33].

In the case of an AF, the atoms are of the form $Acc (a)$ and $Nacc (a)$ . For a node a of the argumentation graph, $Acc (a)$ expresses the status of being accepted, whereas $Nacc (a)$ expresses that a cannot be accepted (implicitly: with regard to a given argumentation semantics). Note that the meaning of $Nacc (a)$ is stronger than “a is not accepted”.

The theory generated by [33] consists of the following axioms:

For every $a R b$ in the input AF $\begin{matrix} (Acc (a) \to Nacc (b)) \end{matrix}$

For every argument b in the input AF $\begin{matrix} (Nacc (b) \to \neg Acc (b)) \end{matrix}$

Such formulae express (by transitivity of material implication) conflict-freeness of extension-based semantics: $Acc (a) \to \neg Acc (b)$ whenever $a R b$ . Such formulae also express that if an argument cannot be accepted then it is not accepted: $Nacc (b) \to \neg Acc (b)$ , or, equivalently, $\neg (Acc (b) \land Nacc (b))$ .

In the case of RAFs, the authors use a two-sorted logic with equality. There are $\arg$ a sort for arguments and $att$ a sort for attacks. In addition to $Acc (a)$ and $Nacc (a)$ as above, the language also admits atoms of the form $Val (e)$ for attack names in the input RAF (intuitively, $Val (e)$ means that the attack named e is valid in the input RAF with regard to a given argumentation semantics). Lastly, two function symbols s and t can be applied to objects of the sort $att$ to capture source and target of the attack. The target can be either of sort $\arg$ or of sort $att$ and the source can only be of sort $\arg$ (as the source of an attack in a RAF is restricted to a single argument, see Definition 4, in Section 2).

The generated theory is bigger than for AFs. First, there are the following conflict-freeness axioms: $\begin{array}{l} \forall e : att, ((Val (e) \land Acc (s (e))) \to \neg Val (t (e))) if t (e) is of sort att \\ \forall e : att, ((Val (e) \land Acc (s (e))) \to Nacc (t (e))) if t (e) is of sort \arg \end{array}$ and the coherence axiom as above: $\begin{matrix} \forall a : \arg, Nacc (a) \to \neg Acc (a) \end{matrix}$

Of course, the generated theory includes RAF-dependent axioms (assuming the arguments of the input RAF are $a_{1}, \dots, a_{n}$ and the attack names are $e_{1}, \dots, e_{m}$ ) as follows: $\begin{array}{l} s (e) = x \land t (e) = y for every edge e from x to y \\ \forall a : \arg, a = a_{1} \lor \dots \lor a = a_{n} \\ \forall e : att, e = e_{1} \lor \dots \lor e = e_{m} \\ \neg (a_{i} = a_{j}) \land \neg (e_{i} = e_{j}) i \neq j \end{array}$

Additional formulae are introduced for encoding the different principles that govern argumentation semantics. There are formulae for capturing the defence principle, the reinstatement principle and the stability principle. Then extensions under a given semantics (admissible, complete, preferred, grounded, or stable semantics) can be characterized by models of logical theories obtained by combining some of these formulae. See an example in Section 12.2.

4.3. The approach by Gabbay and Gabbay

In [67], for every AF, a theory is generated with the axiom: $\begin{matrix} N a \to \neg a, for all a \in A, \end{matrix}$ where $N a$ is a special propositional atom with the same reading as $Nacc (a)$ in the Cayrol–Fariñas–Lagasquie approach. Also, a is to play here the same role as $Acc (a)$ in the Cayrol–Fariñas–Lagasquie approach.

Similarly, a conflict-freeness axiom is needed: $\begin{matrix} a \to N b, for all a and b such that a R b . \end{matrix}$

The theory generated by [67] consists of four kinds of formulae:

${x | \neg \exists y (y R x)}$

${y \leftrightarrow ⋀_{z \in R^{-} (y)} N z}$ for each argument y16

¹⁶
If y is unattacked then this formula is equivalent to $y \leftrightarrow ⊤$ as the conjunction of an empty set of formulae is always true.

${z \to N y | (z R y)}$

${(⋀_{z \in R^{-} (y)} \neg z \land ⋁_{z \in R^{-} (y)} \neg N z) \to \neg y \land \neg N y}$ for each argument y17

¹⁷

If y is unattacked then the formula $⋁_{z \in R^{-} (y)} \neg N z$ is equivalent to ⊥ as the disjunction of an empty set of formulae is always false.

The complete extensions correspond to the models of the above theory. See an example in Section 12.2.

Note that the above formulae fail to provide a modular encoding of some principles of argumentation semantics such as for instance the defence or the reinstatement principles (so, it is not so easy to characterize, e.g., admissibility). This is a difference with the Cayrol–Fariñas–Lagasquie approach.

An additional axiom is introduced for characterizing stable semantics: $\begin{matrix} a \lor N a, for all a . \end{matrix}$

The corresponding stability axiom given in [33] is: $\begin{matrix} \neg Acc (a) \to \underset{b \in R^{-} (a)}{⋁} Acc (b) \end{matrix}$

Both [30] and [67] prove that the models of the respective theory coincide with the extensions of the AF (the list of semantics dealt with in [30] is longer).

4.4. Some implementations

The approach of [30,33,34] has been implemented in Grafix, a Java software for representing graphically argumentation frameworks with higher-order interactions (see [35]).

5. QBF-formalization of AF

The aim of both approaches [4,50] reviewed in this section is to express properties over a given AF, so that these properties can be used to characterize extensions of the AF. Thus, the input consists of an AF (or an ADF [49]) together with an extension-based semantics. The output is a quantified Boolean formula (QBF)18

¹⁸
These formulae are a generalization of the propositional formulae in which both existential quantifiers and universal quantifiers can be applied to each variable. With this formalism, one can ask whether a quantified sentential form over a set of Boolean variables is true or false. An example of QBF formula: $\forall x \exists y \exists z ((x \lor z) \land y)$ .

whose models coincide with the extensions of the AF (i.e., using names of the nodes of the argumentation graph as propositional atoms, the models of the formula are exactly the extensions of the AF). The definitions are formulated in terms of labellings over the AF, and translated in a logical language (QBF). The translation is shown to establish a one-to-one correspondence (i.e., a bijection) between the extensions of the AF and the models of the resulting quantified Boolean formula. The logic is used to encode the AF (nodes of the argumentation graph are injectively mapped to propositional atoms and edges are injectively mapped to special propositional atoms that are taken to be always true), with quantification serving to express minimality/maximality w.r.t. a property (e.g., there exists no complete labelling larger than the current labelling). The propositional atoms denoting nodes are duplicated, with a plus version and a minus version (e.g., for a node of name a, the language at hand includes

a^{\oplus}

and

a^{⊖}

). These signed atoms are used to encode the truth values t, f, u according to the labels as assigned (e.g., if a is assigned u by the current labelling then this is captured by letting both

a^{\oplus}

and

a^{⊖}

to be false). A general constraint rules out the possibility for

a^{\oplus}

and

a^{⊖}

to be both true.

These are theoretical approaches but implementations are afoot using QBF solvers, and indeed such an implementation is QADF, due to Diller, Wallner & Woltran [50].

5.1. Main definitions

We first describe the approach due to Arieli and Caminada [4,5].

Let us recall that a labelling $ℓ$ for an AF $(A, R)$ , is a total function $ℓ$ : $A \to {in, out, und}$ . We consider complete labellings, characterized by the following conditions (see Section 2.2):

For each argument a,

If a is $in$ -labelled, then all its attackers are $out$ -labelled;

If a is $out$ -labelled, then it has at least one attacker that is $in$ -labelled;

If a is $und$ -labelled, then it has at least one attacker that is not $out$ -labelled and it does not have an attacker that is $in$ -labelled.

The assignments of truth values to (name of) nodes are captured syntactically, that is, through formulae. This is done as follows:

Def. 14.
For an unsigned atom a and unsigned formulae ϕ, ψ, define the following signed formulae: $\begin{matrix} τ^{+} (a) = a^{\oplus} & τ^{-} (a) = a^{⊖} \\ τ^{+} (\neg ϕ) = τ^{-} (ϕ) & τ^{-} (\neg ϕ) = τ^{+} (ϕ) \\ τ^{+} (ϕ \to ψ) = \neg τ^{-} (ϕ) \lor τ^{+} (ψ) & τ^{-} (ϕ \to ψ) = τ^{+} (ϕ) \land τ^{-} (ψ) \end{matrix}$

The encoding then expands to
Def. 15.
For an unsigned formula ϕ: $\begin{array}{l} val (ϕ, t) = τ^{+} (ϕ) \land \neg τ^{-} (ϕ) \\ val (ϕ, f) = \neg τ^{+} (ϕ) \land τ^{-} (ϕ) \\ val (ϕ, u) = \neg τ^{+} (ϕ) \land \neg τ^{-} (ϕ) \end{array}$

The main definition is:19
¹⁹
$att (y, x)$ means that $(y, x) \in R$ .

Def. 16.
Let $AF = (A, R)$ and $x \in A$ . Define $\begin{matrix} {LAB}_{AF} (x) = \{\begin{matrix} val (x, t) \to ⋀_{y \in A} (att (y, x) \to val (y, f)) \\ val (x, f) \to ⋁_{y \in A} (att (y, x) \land val (y, t)) \\ val (x, u) \to (\begin{matrix} (\neg ⋀_{y \in A} (att (y, x) \to val (y, f))) \\ \land (\neg ⋁_{y \in A} (att (y, x) \land val (y, t))) \end{matrix}) \end{matrix}\} \end{matrix}$

The role of ${LAB}_{AF} (x)$ is to ensure that the three conditions for a complete labelling are satisfied, for x ranging over all arguments of AF. Then, the formula characterizing complete labellings over $AF = (A, R)$ is: $\begin{matrix} CMP (AF) = ⋃_{a \in A} {LAB}_{AF} (a) \cup {\neg (a^{\oplus} \land a^{⊖})} \end{matrix}$

Also, stable extensions can be captured: $\begin{matrix} STB (AF) = CMP (AF) \cup {a^{\oplus} \lor a^{⊖} | a \in A} \end{matrix}$

Quantified Boolean formulae enter the picture as minimization or maximization is required. For an AF such that $A = {a_{1}, \dots, a_{n}}$ , an example is: $\begin{array}{l} \forall x_{1}^{\oplus} x_{1}^{⊖} \dots x_{n}^{\oplus} x_{n}^{⊖} \\ [CMP (AF) [x_{1}, \dots, x_{n}] \to (\begin{matrix} (⋀_{a_{i} \in A} (val (x_{i}, t) \to val (a_{i}, t))) \\ \to (⋀_{a_{i} \in A} (val (a_{i}, t) \to val (x_{i}, t))) \end{matrix})] \end{array}$

This formula can be read as follows. Considering a current labelling $a_{1}, \dots, a_{n}$ for the n arguments in $A$ , look at all labellings $x_{1}, \dots, x_{n}$ so that if one of them satisfies $CMP (AF)$ and is smaller than the current labelling (this is what $⋀_{a_{i} \in A} (val (x_{i}, t) \to val (a_{i}, t))$ expresses) then the current labelling must be in fact the same as this labelling. In other words, any model of this formula and of $CMP (AF) [a_{1}, \dots, a_{n}]$ defines a minimal complete extension, so that (according to well-known results in abstract argumentation) it defines the grounded extension.
5.2. An example

Ex.
3.4.1 (cont’d)

The corresponding theory is:20
²⁰
This set of rules is partitioned in 3 subsets: rules for assigning to each argument the value t, then f, then u.

$\begin{array}{l} \begin{array}{l} val (a, t) \to val (b, f) \\ val (b, t) \to val (a, f) \\ val (c, t) \to (val (b, f) \land val (e, f)) \\ val (d, t) \to val (c, f) \\ val (e, t) \to val (d, f) \end{array} \\ \begin{array}{l} val (a, f) \to val (b, t) \\ val (b, f) \to val (a, t) \\ val (c, f) \to (val (b, t) \lor val (e, t)) \\ val (d, f) \to val (c, t) \\ val (e, f) \to val (d, t) \end{array} \\ \begin{array}{l} val (a, u) \to (\neg val (b, f) \land \neg val (b, t)) \\ val (b, u) \to (\neg val (a, f) \land \neg val (a, t)) \\ val (c, u) \to (\neg (val (b, f) \land val (e, f)) \land \neg (val (b, t) \lor val (e, t))) \\ val (d, u) \to (\neg val (c, f) \land \neg val (c, t)) \\ val (e, u) \to (\neg val (d, f) \land \neg val (d, t)) \end{array} \end{array}$

In the signed language, $\begin{array}{l} \begin{array}{l} (a^{\oplus} \land \neg a^{⊖}) \to (b^{⊖} \land \neg b^{\oplus}) \\ (b^{\oplus} \land \neg b^{⊖}) \to (a^{⊖} \land \neg a^{\oplus}) \\ (c^{\oplus} \land \neg c^{⊖}) \to ((b^{⊖} \land \neg b^{\oplus}) \land (e^{⊖} \land \neg e^{\oplus})) \\ (d^{\oplus} \land \neg d^{⊖}) \to (c^{⊖} \land \neg c^{\oplus}) \\ (e^{\oplus} \land \neg e^{⊖}) \to (d^{⊖} \land \neg d^{\oplus}) \end{array} \\ \begin{array}{l} (a^{⊖} \land \neg a^{\oplus}) \to (b^{\oplus} \land \neg b^{⊖}) \\ (b^{⊖} \land \neg b^{\oplus}) \to (a^{\oplus} \land \neg a^{⊖}) \\ (c^{⊖} \land \neg c^{\oplus}) \to ((b^{\oplus} \land \neg b^{⊖}) \lor (e^{\oplus} \land \neg e^{⊖})) \\ (d^{⊖} \land \neg d^{\oplus}) \to (c^{\oplus} \land \neg c^{⊖}) \\ (e^{⊖} \land \neg e^{\oplus}) \to (d^{\oplus} \land \neg d^{⊖}) \end{array} \\ \begin{array}{l} (\neg a^{\oplus} \land \neg a^{⊖}) \to (\neg (b^{⊖} \land \neg b^{\oplus}) \land \neg (b^{\oplus} \land \neg b^{⊖})) \\ (\neg b^{\oplus} \land \neg b^{⊖}) \to (\neg (a^{⊖} \land \neg a^{\oplus}) \land \neg (a^{\oplus} \land \neg a^{⊖})) \\ ((\neg c^{\oplus} \land \neg c^{⊖}) \to [\neg ((b^{⊖} \land \neg b^{\oplus}) \land (e^{⊖} \land \neg e^{\oplus})) \land \neg ((b^{\oplus} \land \neg b^{⊖}) \lor (e^{\oplus} \land \neg e^{⊖}))] \\ \neg d^{\oplus} \land \neg d^{⊖}) \to (\neg (c^{⊖} \land \neg c^{\oplus}) \land \neg (c^{\oplus} \land \neg c^{⊖})) \\ (\neg e^{\oplus} \land \neg e^{⊖}) \to (\neg (d^{⊖} \land \neg d^{\oplus}) \land \neg (d^{\oplus} \land \neg d^{⊖})) \end{array} \\ \begin{array}{l} \neg (a^{\oplus} \land a^{⊖}) \land \neg (b^{\oplus} \land b^{⊖}) \land \neg (c^{\oplus} \land c^{⊖}) \land \neg (d^{\oplus} \land d^{⊖}) \land \neg (e^{\oplus} \land e^{⊖}) \end{array} \end{array}$
5.3. A QBF approach for ADF

The QBF-based formalization due to Diller, Wallner and Woltran [49,50] concerns ADFs.

This approach also uses a signed language, with the same atoms as given in Def. 14, namely $a^{\oplus}$ and $a^{⊖}$ for every $a \in A$ (interestingly, the notation for these atoms is the same in both approaches).

The same constraint (see $CMP (AF)$ above) ruling out a contradictory assignment of truth values is enforced, i.e., for every $a \in A$ : $\begin{matrix} \neg (a^{\oplus} \land a^{⊖}) \end{matrix}$

The main difference with the approach due to Arieli and Caminada is that the existence of the acceptance condition $φ_{a}$ in ADF is addressed by Boolean quantification, even prior to any minimization/maximization:21

²¹
The quantification ensures ranging over all interpretations: conjunction over all $a \in A$ fails to bind other propositional atoms that presumably occur in $φ_{a}$ .

\begin{array}{l} \forall x_{1}^{\oplus} x_{1}^{⊖} \dots x_{n}^{\oplus} x_{n}^{⊖} \\ [\underset{a \in A}{⋀} ((a^{\oplus} \to a) \land (a^{⊖} \to \neg a)) \to \underset{a \in A}{⋀} ((a^{\oplus} \to φ_{a}) \land (a^{⊖} \to \neg φ_{a}))] \end{array}

This formula expresses that the current labelling is admissible. It can then be used to obtain a formula $CMP$ for complete labellings, again using Boolean quantification. In turn, Boolean quantification over $CMP$ can be used to obtain, e.g., a formula characterizing the grounded extension.

5.4. Implementation

The QBF approach has been implemented in the form of the QADF system (see the description in Section 3.3).

6. Dedicated languages for abstract argumentation

6.1. YALLA (Yet Another Logic Language for Argumentation)

The aim of this approach is the definition of a first-order logical theory capable of describing an AF and its standard semantics. In the basic language YALLA, an AF is described by specific axioms of the theory and formulae are interpreted by argumentation graphs. A variant of the basic language called ${YALLA}_{U}$ has been defined for describing AFs built on a given universe U. Such a universe is supposed to specify exactly what arguments and interactions are possible w.r.t. the studied case.

It is a theoretical approach (no implementation yet) introduced in order to express the properties of update operators in dynamic argumentation. Moreover, ${YALLA}_{U}$ enables to express incomplete knowledge about an AF, and to describe a set of AFs by one formula (each model of this formula corresponding to a particular AF).

6.1.1. Main definitions

[55] has proposed a framework for handling change in argumentation (addition or removal of arguments or attacks). All the definitions are related to a specific AF, called universe, setting the set of possible arguments together with their interactions. This universe is supposed to be finite and is denoted by the pair $(A_{U}, R_{U})$ . For instance, if the domain is a knowledge base then $A_{U}$ and $R_{U}$ are the set of all arguments and interactions that may be built from the formulae of the base. In the following example issued from [55], it is assumed that $A_{U}$ and $R_{U}$ are explicitly provided:

Ex. 6.1.1.
During a trial concerning a defendant (Mr. X), several arguments can be involved to determine his guilt. The set of arguments $A_{U}$ and the graphical representation of the relation $R_{U}$ are given below.

$a_{0}$ Mr. X is not guilty of premeditated murder of Mrs. X, his wife.

$a_{1}$ Mr. X is guilty of premeditated murder of Mrs. X.

$a_{2}$ The defendant has an alibi, his business associate has solemnly sworn that he met him at the time of the murder.

$a_{3}$ The close working business relationships between Mr. X and his associate induce suspicions about his testimony.

$a_{4}$ Mr. X loves his wife so deeply that he asked her to marry him twice. A man who loves his wife cannot be her killer.

$a_{5}$ Mr. X has a reputation for being promiscuous.

$a_{6}$ The defendant had no interest to kill his wife, since he was not the beneficiary of the huge life insurance she contracted.

$a_{7}$ The defendant is a man known to be venal and his “love” for a very rich woman could be only lure of profit.

In [55], an AF is defined w.r.t. to a given universe $(A_{U}, R_{U})$ , so the definition differs slightly from the definition of [54] in the sense that arguments and interactions must be built according to the universe.
Def. 17.
An AF on $(A_{U}, R_{U})$ is a pair $(A, R)$ where
$A \subseteq A_{U}$ and

$R \subseteq R_{U} \cap (A \times A)$ .
The set of AFs that can be built on the universe $(A_{U}, R_{U})$ is denoted by $Γ_{U}$ .

An example of AF on the universe $(A_{U}, R_{U})$ described in Ex. 6.1.1 could be:
Ex. 6.1.2.
The prosecutor is trying to make accepted the guilt of Mr. X. She is not omniscient and knows only a subset of the arguments of the universe presented in Example 6.1.1 (a subset that is not necessarily shared with other agents). Moreover, her knowledge being based on the universe, any argument or attack that does not appear in the universe cannot appear in her graph. Here is her AF ( ${AF}_{Pro}$ ):

[55] has proposed a first-order logical theory capable of describing abstract AFs built on a given finite universe $(A_{U}, R_{U})$ , where $A_{U} = {a_{1}, a_{2}, \dots, a_{k}}$ with k being the cardinal of $A_{U}$ . The signature of the associated language ${YALLA}_{U}$ is defined as follows:22
²²
For each function or predicate symbol, the arity is indicated by an exponent attached to the symbol.

Def. 18 (Signature).

$Σ_{U} = (V_{const}, V_{f}, V_{P})$ where the set of constants $V_{const} = {c_{⊥}, c_{1}, \dots, c_{p}}$ with $p = 2^{k} - 1$ , the set of functions $V_{f} = {{union}^{2}}$ and the set of predicates $V_{P} = {{on}^{1}, ⊳^{2}, \subseteq^{2}}$ .

As the logical theory has been built for describing AFs on a given universe, terms and formulae of the language ${YALLA}_{U}$ will be interpreted on AFs built on this universe. Formally, the semantics of ${YALLA}_{U}$ is defined thanks to a structure over $Σ_{U}$ , on which terms and formulae will be interpreted. So a structure is associated with an AF built on the universe $(A_{U}, R_{U})$ and its domain is $D = 2^{A_{U}}$ , which is not empty.

Def. 19 (Structure).

A structure $M$ over the signature $Σ_{U}$ , associated with $(A, R)$ , is a pair $(D, I)$ where $D = 2^{A_{U}}$ is the domain of the structure and $I$ is an interpretation function associating:

a unique element of $D$ to each constant symbol $c_{i}$ (in particular the empty set is associated with the constant symbol $c_{⊥}$ ),

the binary set theoretic union operator (function from $D^{2}$ to $D$ ) to the function symbol $union$ ,

the characterization of the subsets of $A$ to the predicate symbol $on$ : $on (S)$ if and only if $S \subseteq A$ ,

the binary set theoretic inclusion relation (binary relation on $D^{2}$ ) to the predicate symbol ⊆,

the binary relation of attack between sets of arguments induced by $R$ , and defined by $S_{1} R S_{2}$ if and only if $S_{1} \subseteq A$ , $S_{2} \subseteq A$ and $\exists x_{1} \in S_{1}$ , $\exists x_{2} \in S_{2}$ , such that $x_{1} R x_{2}$ , to the predicate symbol ⊳.

Among the formulae that can be built on the signature $Σ_{U}$ , we find the specific axioms of the theory, that will allow to describe AFs on the universe:

Let x, y, z be variables of ${YALLA}_{U}$ ,

Axioms for set inclusion

$\forall x$ $(c_{⊥} \subseteq x)$

$\forall x$ $(x \subseteq x)$

$\forall x, y, z$ $((x \subseteq y \land y \subseteq z) ⟹ x \subseteq z)$

Axioms for set operators

$\forall x, y$ $(x \subseteq union (x, y))$

$\forall x, y$ $(y \subseteq union (x, y))$

$\forall x, y, z$ $(((x \subseteq z) \land (y \subseteq z)) ⟹ (union (x, y) \subseteq z))$

Axioms combining set operators and attack relation

$\forall x, y, z$ $(((x ⊳ y) \land (x \subseteq z)) ⟹ (z ⊳ y))$

$\forall x, y, z$ $(((x ⊳ y) \land (y \subseteq z)) ⟹ (x ⊳ z))$

$\forall x, y, z$ $((union (x, y) ⊳ z) ⟹ ((x ⊳ z) \lor (y ⊳ z)))$

$\forall x, y, z$ $((x ⊳ union (y, z)) ⟹ ((x ⊳ y) \lor (x ⊳ z)))$

Axioms for the predicate $on$

$on (c_{⊥})$

$\forall x, y$ $((on (x) \land (y \subseteq x)) ⟹ on (y))$

$\forall x, y$ $((on (x) \land on (y)) ⟹ on (union (x, y)))$

$\forall x, y$ $((x ⊳ y) ⟹ (on (x) \land on (y)))$

An AF belonging to $Γ_{U}$ can be described by its characteristic formula in the language ${YALLA}_{U}$ .

Def. 20 (Formula describing an AF).

Let the function $Φ_{U}$ be defined as follows: $\begin{matrix} Φ_{U} : a Γ_{U} \to & {YALLA}_{U} \\ (A, R) \mapsto & on (A) \land \\ \underset{x \in A_{U} ∖ A}{⋀} \neg on ({x}) \land \\ \underset{(x, y) \in R}{⋀} ({x} ⊳ {y}) \land \\ \underset{(x, y) \in R_{U} ∖ R}{⋀} \neg ({x} ⊳ {y}) \end{matrix}$

$Φ_{U} (A, R)$ is called the characteristic formula of $(A, R)$ .23

²³
When t denotes a term of ${YALLA}_{U}$ , t is identified with the subset of $A_{U}$ which interprets t. It is the case for ${x}$ for instance.

Note that $(A, R)$ determines the unique structure (Def. 19) which is a model of $Φ_{U} (A, R)$ .

Some additional notations are used for encoding the argumentation semantics: let $t_{1}$ and $t_{2}$ be terms of ${YALLA}_{U}$ , $\begin{array}{l} t_{1} = t_{2} \overset{def}{\equiv} (t_{1} \subseteq t_{2}) \land (t_{2} \subseteq t_{1}), \\ t_{1} \neq t_{2} \overset{def}{\equiv} \neg (t_{1} = t_{2}), \\ singl (t_{1}) \overset{def}{\equiv} (t_{1} \neq c_{⊥}) \land \forall t_{2} (((t_{2} \neq c_{⊥}) \land (t_{2} \subseteq t_{1})) ⟹ (t_{1} \subseteq t_{2})) . \end{array}$ The following property obviously holds: $(A, R) ⊧ singl (t)$ if and only if the term t is interpreted by a singleton of $A$ .

Then the principles used in argumentation semantics can be encoded in terms of ${YALLA}_{U}$ formulae:

Prop. 3.

Let $A_{U}$ be a set of arguments and $(A, R)$ be an AF such that $A \subseteq A_{U}$ and $R \subseteq A \times A$ . Let t, $t_{1}$ , $t_{2}$ , $t_{3}$ be terms of ${YALLA}_{U}$ .

t is conflict-free in $(A, R)$ if and only if $(A, R) ⊧ on (t) \land (\neg (t ⊳ t))$ . The latter formula is denoted by $F (t)$ .

$t_{1}$ defends each element of $t_{2}$ in $(A, R)$ if and only if $(A, R) ⊧ (\forall t_{3} ((singl (t_{3}) \land (t_{3} ⊳ t_{2})) ⟹ (t_{1} ⊳ t_{3})))$ . The latter formula is denoted by .

t is admissible in $(A, R)$ if and only if . The latter formula is denoted by $A (t)$ .

t is a complete extension of $(A, R)$ if and only if . The latter formula is denoted by $C (t)$ .

t is the grounded extension of $(A, R)$ if and only if $(A, R) ⊧ (C (t) \land \forall t_{2} (C (t_{2}) ⟹ (t \subseteq t_{2})))$ . The latter formula is denoted by $G (t)$ .

t is a stable extension of $(A, R)$ if and only if $(A, R) ⊧ (F (t) \land \forall t_{2} ((singl (t_{2}) \land \neg (t_{2} \subseteq t)) ⟹ (t ⊳ t_{2})))$ . The latter formula is denoted by $S (t)$ .

t is a preferred extension of $(A, R)$ if and only if $(A, R) ⊧ (A (t) \land \forall t_{2} (((t_{2} \neq t) \land (t \subseteq t_{2})) ⟹ \neg A (t_{2})))$ . The latter formula is denoted by $P (t)$ .

Due to the finite size of a universe, each ${YALLA}_{U}$ formula can be viewed as a propositional formula and the satisfiability problem of a ${YALLA}_{U}$ base is a NP-complete problem.

In [55] ${YALLA}_{U}$ is used for expressing update in argumentation dynamics. For instance, in the case of a debate, classical update amounts to consider a formula φ in ${YALLA}_{U}$ representing a current state of knowledge about exchanged arguments (i.e., it may encompass several possible AFs), and a new piece of information α stating that the debate has evolved in such a way that α now holds (i.e., the current state of the debate is inside a set of AFs satisfying α). Updating φ by α gives a formula $φ ◇ α$ that represents the set of AFs corresponding to an evolution of the debate where a change has been done imposing α. Nevertheless, an AF can only evolve by an allowed operation made by an agent (according to the agent’s own AF and her target). That means that some transitions are not allowed. So the update operators in argumentation dynamics must take into account these constraints: let $T$ be a set of authorized transitions, an update operator is a mapping from ${YALLA}_{U} \times {YALLA}_{U}$ to ${YALLA}_{U}$ which associates with any formula φ and any formula α a formula, denoted by $φ ♢_{T} α$ satisfying $T$ . In [55], a general update operator is defined following this idea. Then refinements are proposed in order to give a logical translation of previous characterizations proposed in [15,27].

6.1.2. Some examples

Ex.
3.2.4 (cont’d) Let us consider the AF given in Ex. 3.2.4 as the universe ( $A_{U} = {a, b, c}$ , $R_{U} = {(a, b), (c, b)}$ ). Let $(A_{1}, R_{1})$ and $(A_{2}, R_{2})$ be the two AFs built the universe $(A_{U}, R_{U})$ defined by: $A_{1} = {a, b, c}$ , $R_{1} = {(a, b)}$ , $A_{2} = {a, b}$ , $R_{2} = {(a, b)}$ .

Fig. 1.
An example of argumentation graphs built on a universe.

Let $φ_{1}$ be the formula $on ({a, b, c}) \land ({a} ⊳ {b})$ and $φ_{2}$ be the formula $on ({a, b}) \land ({a} ⊳ {b})$ .

We have $(A_{1}, R_{1}) ⊧ φ_{1}$ , $(A_{1}, R_{1}) ⊧ φ_{2}$ , $(A_{2}, R_{2}) ⊧ φ_{2}$ . However $(A_{2}, R_{2})$ is not a model of $φ_{1}$ , as ${a, b, c}$ is not a subset of $A_{2}$ .

Moreover, following Definition 20, we have:24
²⁴
Note that the absence of an attack is expressed only if this attack is in the universe: $\neg ({c} ⊳ {b})$ is in $Φ_{U} (A_{1}, R_{1})$ as c attacks b in U, whereas $\neg ({b} ⊳ {a})$ is not in $Φ_{U} (A_{1}, R_{1})$ as b does not attack a in U.

$\begin{array}{l} Φ_{U} (A_{1}, R_{1}) = on ({a, b, c}) \land ({a} ⊳ {b}) \land \neg ({c} ⊳ {b}) \\ Φ_{U} (A_{2}, R_{2}) = on ({a, b}) \land \neg (on ({c})) \land ({a} ⊳ {b}) \land \neg ({c} ⊳ {b}) \end{array}$

More complex assertions can be expressed in ${YALLA}_{U}$ , such as, for instance, the fact that b does not belong to the grounded extension of $(A_{1}, R_{1})$ : $\begin{matrix} Φ_{U} (A_{1}, R_{1}) \land ∄ t (G (t) \land ({b} \subseteq t)) \end{matrix}$

${YALLA}_{U}$ also enables the expression of incomplete knowledge held by an agent about AFs built on the universe, as shown by the following example:
Ex.
6.1.1 (cont’d) Let us consider the universe $(A_{U}, R_{U})$ given in the trial example. Assume that Agent ${Ag}_{a}$ has only a partial knowledge about the AF built by Agent ${Ag}_{b}$ . Indeed, ${Ag}_{a}$ hesitates between two possible situations for ${Ag}_{b}$ ’s AF, namely $(A_{1}, R_{1})$ and $(A_{2}, R_{2})$ given in Fig. 2. So Agent ${Ag}_{a}$ has a doubt about the existence of $a_{7}$ and of the attacks from $a_{7}$ to $a_{4}$ and from $a_{2}$ to $a_{1}$ .

Fig. 2.
Two possible cases for the argumentation graph of Agent ${Ag}_{b}$ .

The knowledge held by ${Ag}_{a}$ can be expressed by the following ${YALLA}_{U}$ formula: $\begin{array}{rcl} φ & = & on ({a_{0}, a_{1}, a_{2}, a_{4}}) \land \\ \neg (on ({a_{3}})) \land \neg (on ({a_{5}})) \land \neg (on ({a_{6}})) \land \\ ({a_{4}} ⊳ {a_{1}}) \land ({a_{1}} ⊳ {a_{0}}) \land \\ \neg ({a_{0}} ⊳ {a_{1}}) \land \neg ({a_{3}} ⊳ {a_{2}}) \land \neg ({a_{5}} ⊳ {a_{4}}) \land \\ \neg ({a_{6}} ⊳ {a_{1}}) \land \\ (\begin{matrix} (on ({a_{7}}) \land ({a_{7}} ⊳ {a_{4}}) \land ({a_{2}} ⊳ {a_{1}})) \\ \lor \\ (\neg (on ({a_{7}})) \land \neg ({a_{7}} ⊳ {a_{4}}) \land \neg ({a_{2}} ⊳ {a_{1}})) \end{matrix}) \end{array}$

φ is satisfied by only two structures which correspond to $(A_{1}, R_{1})$ and $(A_{2}, R_{2})$ .

Note that $φ \equiv Φ_{U} (A_{1}, R_{1}) \lor Φ_{U} (A_{2}, R_{2})$ .
6.1.3. Related works

Other works propose dedicated logical languages for dealing with dynamics in argumentation frameworks. See for instance [18,44,45,48,51,52]. Moreover, it is worth noticed that a survey has been done in the context of dynamics in argumentation frameworks, see [53].

6.2. The approach by Villata et al.

In [93] is proposed a propositional logic of argumentation to specify and verify requirements in AFs. Note that a modal variant of this logic has been proposed (see Section 10).

The input consists of an AF together with requirements to be satisfied. The outputs are formulae encoding the framework and formulae encoding the requirements. Examples of such requirements are: “Argument a attacks argument b”; “argument a defends argument b”; “argument a or argument b is acceptable”; “if argument a is accepted (in an extension) then argument b is accepted too (in the same extension) and argument c is not accepted”.

The basic ideas of the logic for specification and verification are close to the ideas of YALLA. A model of the logic represents an AF, and such a model satisfies formulae representing the fact that arguments attack or defend each other, or whether sets of arguments are extensions. Moreover the models are built on a given universe of arguments.

Atoms of the language represent sets of arguments. The attack relation is explicitly encoded by a new logical connective ⊳. The formula $p ⊳ q$ is interpreted in $(A, R)$ as “there is an argument in p that attacks an argument in q”, where p, q denote subsets of $A$ . There is also a logical connective for defence, which can be defined in terms of the attack connective, as follows: $\begin{matrix} a ⊘ b \equiv \underset{c \subseteq A}{⋀} ((c ⊳ b) \to (a ⊳ c)) \end{matrix}$

The above connectives allow the specification of requirements related to the structure of an AF.

In order to specify requirements related to the semantics, new kinds of formulae are considered such as $F (p)$ , $A (p)$ , or $G (p)$ for instance. The formula $F (p)$ (resp. $A (p)$ , $G (p)$ ) is interpreted in $(A, R)$ as “the set of arguments of $A$ denoted by p is conflict-free (resp. admissible, the grounded extension) in $(A, R)$ ”. The semantics are thus considered as primitives of the language.

Note that all the verifications need a model-theoretic approach, as the logic has not been axiomatized. So the verifications have to be made at the AF level.

7. Encoding of extension-based semantics

In this section are reviewed two approaches that, given an extension-based semantics σ, produce a formula $Φ_{σ}$ whose satisfiability answers the σ-extension problem for the input (usually, an AF and a candidate subset of the arguments). The role of the logic (it is propositional logic) is to specify the semantics but there is no encoding of the graph itself as it is done by the approaches presented in Section 4. Both approaches are theoretical as well as practical: implementations exist.

7.1. The approach by Besnard and Doutre

The original proposal is [11], extended in [12]. Independently, an equivalent proposal is [94].

The idea is as follows. Let σ be an extension-based semantics, $(A, R)$ be an AF and S be a subset of $A$ . A formula $Φ (σ, S)$ is produced which is satisfiable iff S is a σ-extension of the AF (“Satisfiability approach”). A semantics being defined by a set of principles, a formula associated with each principle is produced, then composing these formulae results in the formula $Φ (σ, S)$ .

Logic is used for specifying the principles of the semantics and the produced formula is parametrized by S (and by σ of course).

7.1.1. Description of the approach

For a given $(A, R)$ , a set of propositional symbols $a, b, c, \dots$ is introduced to represent the elements of $A$ . For simplicity, the same symbol is used, i.e., a is regarded as a propositional symbol whenever $a \in A$ . An argumentative semantics σ can then be mapped to a propositional formula (dependent on a subset S of $A$ ) that happens to be satisfiable iff S is a σ-extension of $(A, R)$ .

Such a formula is constructed in view of the interpretation for a propositional symbol a: a is true means that a is in the extension.

Also, the usual conditions underlying admissibility in extension-based semantics are captured: Conflict-free

$\begin{matrix} \underset{a R b}{⋀} (a \to \neg b) \end{matrix}$

Admissible

$\begin{matrix} \underset{b R a}{⋀} \underset{c R b}{⋁} c \end{matrix}$

Complete

$\begin{matrix} (\underset{b R a}{⋀} \underset{c R b}{⋁} c) \to a \end{matrix}$

and so on …

General test:. $S \subseteq A$ is a σ-extension of $(A, R)$ iff the formula below is satisfiable: $\begin{matrix} \underset{a \in S}{⋀} a \land \underset{a \in A ∖ S}{⋀} \neg a \land Φ_{σ} \end{matrix}$

In the above formula, $Φ_{σ}$ captures the conditions expressing that S is a σ-extension of $(A, R)$ .

For example, in the formula enabling to determine whether S is a stable extension of $(A, R)$ there is: $\begin{matrix} Φ_{s} = \underset{a \in A}{⋀} (a \leftrightarrow \underset{b R a}{⋀} \neg b) . \end{matrix}$ As to the case of complete extensions, $\begin{matrix} Φ_{c} = \underset{a \in A}{⋀} [(a \to \underset{a R b}{⋀} \neg b) \land (a \leftrightarrow \underset{b R a}{⋀} \underset{c R b}{⋁} c)] . \end{matrix}$

7.1.2. Some implementations

Besnard and Doutre’s approach has been used in many different implementations. Here we focus on four examples.

In [12 ,13] and thanks to the project SESAME (see [10]), an implementation has been proposed under the form of a software allowing the definition of semantics with logical formulae (aggregation of formulae, each of them representing a requirement that must be respected by the set of arguments candidate, such as conflict-freeness, or defence).

In [95], the encoding proposed by Besnard and Doutre in [11] is extended in order to take into account the semi-stable semantics. Then two extensions of SAT are used, the minimal correction sets (MCS) and the backbone (BB): consider a CNF propositional formula Φ, the MCS problem consists in the computation of the minimal sets of clauses issued from Φ such that, after their removal, Φ becomes satisfiable; the BB problem consists in identifying the litterals that are true in each model of Φ. The idea of this paper is to establish links between the MCS and BB problems and the computation of semi-stable, eager and ideal extensions.

In [72], the encoding proposed by Besnard and Doutre in [11] is used in two different ways. First, it is used directly in a SAT solver for computing the semantics that are in the first level of the polynomial hierarchy. Secondly, it is extended with some weights for computing the semantics that are in the second or more level of the polynomial hierarchy (with a flavour of constraints programming techniques) then used in a Partial Max-SAT solver (the Partial Max-SAT problem is an optimisation problem that consists in satisfying the more possible clauses of a given formula with respect to the weights given to each clause). These algorithms have been implemented in a software called CoQuiAAS.

In [74], the encoding proposed by Besnard and Doutre in [11] is extended for the computation of three new problems: find an extension that is maximal in terms of cardinality, repair a set of arguments in order to transform it into an extension, and adjust an extension such that it contains (or not) a given argument. Each of these new problems is encoded in logic and solved either by an iteration of SAT solver calls, or by a Max-SAT solver call.

7.2. The CEGARTIX approach

In [59], a specific encoding of some extension-based semantics is proposed, using two propositional symbols for each argument (for an argument a, the symbols are $x_{a}$ and $y_{a}$ ). For instance, the formula corresponding to the complete semantics is the following one:

For a given $(A, R)$ , $\begin{array}{rcl} Φ_{c} & = & \underset{(a, b) \in R}{⋀} (\neg x_{a} \lor \neg x_{b}) \land \underset{(b, a) \in R}{⋀} (x_{a} \to \underset{(c, b) \in R}{⋁} x_{c}) \land \\ \underset{b \in A}{⋀} (y_{b} \leftrightarrow (x_{b} \lor \underset{(c, b) \in R}{⋁} x_{c})) \land \underset{a \in A}{⋀} ((\underset{(b, a) \in R}{⋀} y_{b}) \to y_{a}) \end{array}$

As it is said in [59]: “The first line declares the conditions for admissible sets following the definition: any admissible set must be (i) conflict free and (ii) each argument in the set must be defended by the set. The second line declares (i) the value of auxiliary atoms $y_{a}$ ( $y_{a}$ is true iff either $x_{a}$ is true or some $x_{b}$ is true where b attacks a in the AF), and that (ii) each argument a defended by the extension is contained in the extension.”

Here is a small illustration to give some insight into the intuition behind the items $x_{a}$ and $y_{a}$ ; let us prove that the end of the second line of $Φ_{c}$ implies that each argument defended by the conflict-free extension is contained in the extension:

a is defended by the extension is encoded by $(⋀_{(b, a) \in R} ⋁_{(c, b) \in R} x_{c}) \to x_{a}$ .

Let us assume that: $\forall b$ s.t. $(b, a) \in R$ , $⋁_{(c, b) \in R} x_{c}$ .

By definition of $y_{b}$ (first part of the second line of $Φ_{c}$ ), we have that: $\forall b$ s.t. $(b, a) \in R$ $y_{b}$ .

From the end of the second line of $Φ_{c}$ , we can deduce $y_{a}$ , that is by definition, $x_{a} \lor ⋁_{b R a} x_{b}$ .

Moreover, from the first part of the first line of $Φ_{c}$ (conflict-free requirement), we have that $x_{a} \to \neg (⋁_{(b, a) \in R} x_{b})$ .

So we obtain $x_{a}$ .

Models of $Φ_{c}$ characterize the complete extensions of $(A, R)$ in the sense that $x_{a}$ is true in a model I ( $x_{a} \in I$ ) iff the argument a is in the extension characterized by I.

Then this encoding is used in a software called CEGARTIX (see [58,60]) that computes skeptical and credulous acceptance under given semantics. It is based on NP-oracles (basically the MiniSAT solver).

8. Encoding of labelling-based semantics

The purpose of the works reviewed in this section is to encode labelling-based semantics25

²⁵
Various definitions have been recalled in Section 2 and Section 5.

by a set of logical formulae. These formulae express the different constraints associated with a kind of labelling (complete, grounded, stable, preferred). One of the approaches has led to implemented systems for computing semantics.

8.1. The approach by Caminada and Gabbay

In [25], metalevel approaches are proposed for talking about argumentation. A metalevel approach describes an argumentation framework from “above”, using another language and logic. The metalevel language can be classical logic or modal logic. The case of modal logic will be presented in Section 10. Here, we focus on the metalevel approach that uses classical logic for encoding argument labellings.

The logical language includes the equality predicate (“=”), a binary predicate R and the three unary predicates $Q_{0}$ , $Q_{1}$ and $Q_{?}$ .

Intuitively, given an AF denoted by $(A, R)$ , and a labelling $ℓ$ , an interpretation of the language can be obtained: $A$ is taken as the domain, the predicate R is interpreted by the attack relation $R$ of the AF and $ℓ$ is used to get the interpretation of the predicates $Q_{0}$ , $Q_{1}$ and $Q_{?}$ as follows: $a \in Q_{0}$ iff $ℓ$ labels a as $out$ , $a \in Q_{1}$ iff $ℓ$ labels a as $in$ ; $a \in Q_{?}$ iff $ℓ$ labels a as $und$ .

Let us consider the following classical theory denoted by $Δ (R, Q_{0}, Q_{1}, Q_{?})$ (or Δ for short):

$\forall x (Q_{0} (x) \lor Q_{1} (x) \lor Q_{?} (x))$

$\neg \exists x (Q_{i} (x) \land Q_{j} (x))$ for $i \neq j$ , $i, j \in {0, 1, ?}$

$\forall y (\forall x (x R y \to Q_{0} (x)) \to Q_{1} (y))$

$\forall y (\exists x (x R y \land Q_{1} (x)) \to Q_{0} (y))$

$\forall y (\forall x (x R y \to (Q_{0} (x) \lor Q_{?} (x))) \land \exists x (x R y \land Q_{?} (x)) \to Q_{?} (y))$

Any model of the above theory Δ with domain D defines an argumentation framework $(A, R)$ with $A = D$ , $R = R$ and a complete labelling $ℓ$ defined from the elements satisfying the predicates $Q_{0}$ , $Q_{1}$ and $Q_{?}$ .

Then other labellings can be characterized as particular models of Δ. For instance, the grounded labelling is obtained with a model that minimizes $Q_{1}$ , whereas the preferred labellings are obtained with models that maximize $Q_{1}$ . Note that second-order formulae are needed in order to express the concept “ $Q_{1}$ is minimal” or “ $Q_{1}$ is maximal”. That leads to the circumscription technique.26

²⁶
An example of the use of circumscription in order to solve AF reasoning problems is described in [1].

In short, standard circumscription gives the minimal relation(s) that enjoy a given set of properties (e.g., circumscribing

\forall x y

R (x, y) \lor R (y, x)

gives all total antisymmetric relations over the domain). Maximization is obtained dually (although this is usually not called circumscription).

When dealing with a specific AF, additional axioms are needed. They use “=” and constant names for denoting the arguments. Let $Θ (AF)$ denote the set of axioms describing $AF = (A, R)$ :

$\forall x$ $(⋁_{a \in A} x = a)$

$⋀_{a, b \in A, a \neq b} a \neq b$

$⋀_{(a, b) \in R} a R b$

Let

Δ (AF) = Δ \cup Θ (AF)

. It can be shown that characterizing some of the labellings is easier, since for a given AF, the set of arguments is finite. For instance, the grounded labelling of AF can be characterized as the set of x such that

Δ (AF) ⊢ Q_{1} (x)

. Moreover, as the set of arguments is finite, circumscription becomes first-order.

8.2. The approach by Cerutti et al.

In [36], three propositional symbols are defined for each argument: $I_{a}$ , $O_{a}$ and $U_{a}$ meaning that the value of a in the labelling is respectively $in$ , $out$ or $und$ . Moreover, for each value of the labelling, two formulae are given for expressing the necessary and the sufficient conditions corresponding to the assignment of this value. For instance, considering an AF denoted by $(A, R)$ , we have for the value $in$ : $\begin{array}{l} (\underset{b | (b, a) \in R}{⋁} \neg O_{b}) \lor I_{a} (sufficient condition for I_{a}) \\ \underset{b | (b, a) \in R}{⋀} (O_{b} \lor \neg I_{a}) (necessary condition for I_{a}) \end{array}$

Other formulae are defined for expressing some constraints about labellings. For instance, the fact that “an argument has one and only one value in a labelling” is expressed by the formula: $\begin{matrix} \underset{a \in A}{⋀} ((I_{a} \lor O_{a} \lor U_{a}) \land (\neg I_{a} \lor \neg O_{a}) \land (\neg I_{a} \lor \neg U_{a}) \land (\neg U_{a} \lor \neg O_{a})) \end{matrix}$ or the fact that “unattacked arguments must be $in$ ” is encoded by: $\begin{matrix} \underset{a | ∄ b, (b, a) \in R}{⋀} I_{a} \end{matrix}$

Several combinations of these formulae are proposed in order to encode complete labellings.

Note that in the case of a finite AF, the encodings of complete labellings proposed in [36] and [25] can be matched, owing to the equivalence between the alternative definitions of complete labellings provided in [25] (see Section 2.2).

8.3. Some implementations

At least three systems have been developed using the approach proposed in [36].

In [36], an algorithm using a SAT solver is proposed for computing the preferred semantics. This algorithm is called PrefSAT.

In [37], a system called ArgSemSAT is proposed including PrefSAT for computing the preferred semantics. It also includes an approach proposed by the same authors using a decomposition of the argumentation graph in its strong connected components (SCC) and the computation of the preferred extensions by a propagation process across these SCCs with a call to a SAT solver for each SCC.

In [9], a software called LabSAT allows the computation of extensions for several semantics (complete, stable, preferred, grounded) and also the resolution of the credulous and skeptical acceptance problems. It uses the encoding proposed in [36].

Moreover, due to the ICCMA competition [16], many other solvers have been developed. See for instance [38–40,62,77] (once again this list is not exhaustive).

9. Argumentation frameworks and logic programming

The close connection between AF semantics and Logic Programming (LP) semantics goes back to Dung’s work [54]. Dung introduced a transformation from LP to AF, and showed that stable models (resp. the well-founded model) of a logic program correspond to stable extensions (resp. the grounded extension) of the associated AF. These results have been extended by connections between LP 3-valued stable models (resp. regular models) and complete (resp. preferred) extensions [24,96]. Roughly speaking, the purpose of these works is to provide an argumentative semantics for logic programs. So following our choice presented in Section 1, these works are out of the scope of this survey.

In the same paper [54], Dung also introduced a converse transformation from AF to LP, and showed that stable extensions (resp. the grounded extension) of an AF can be obtained as stable models (resp. the well-founded model) of the associated logic program. These results have been extended to relate other AF semantics to LP semantics [24,26,61,83,84,89]. In that case, the purpose is rather to apply computational techniques of Logic Programming to argumentation and so matches with the topic we are interested in. In this context, note that the relationship between argumentation and logic programming has been the subject of intensive research. Currently, there are different mappings which allow to transform an AF into a logic program, all of them offering different characterizations of argumentation semantics in terms of LP semantics. A summary of these characterizations can be found in [83] with all the associated references. Moreover, some works have also considered the issue of using ASP-solvers to compute the extensions of AFs under different semantics [47,61,69,90].

In the following, we first consider some works relating a (simple) AF and Logic Programs. Then we consider generalizations to enriched argumentation frameworks (BAF, RAF). The works reviewed in this section can be distinguished according to the following features:

AF semantics can be encoded under the form of extension-based semantics as in [54,84], or under the form of labelling-based semantics (as for instance in [24,89]).

Different semantics of AF correspond to different semantics of a same logic program as in [24,54] or different semantics of AF are all characterized by the single 2-valued stable model semantics of different transformed programs as in [89].

Note that all the logic programs that we consider below are normal logic programs, that is logic programs whose rules may contain weak negation (i.e. negation as failure, with the symbol $not$ ) but not strong negation (i.e. the classical negation of classical logic), and where the head of each rule is a single atom. From now, normal logic programs will be called logic programs. Atoms of the form $not a$ will be called weak atoms and the weak part of a rule consists in the set of its weak atoms.

9.1. From an AF to a logic program

The input is an AF. The output consists of a logic program P together with the characterization of some of the standard argumentation semantics (at least the grounded semantics and the stable semantics) using the models of P (two-valued or three-valued models depending on the considered approach).

The logical formalism enables to encode attacks. Moreover, depending of the approaches, the concept of attack is encoded in an explicit way (as for instance in [26,54,84]) or in an implicit way (as for instance in [24]).

Two kinds of work can be distinguished. The first kind lies in the spirit of Dung’s work and concerns works using two-valued models for LP semantics. The second kind of works uses three-valued models for LP semantics.

Towards logic programs under 2-valued semantics. Let us start by the initial approach of [54]. Given an AF $(A, R)$ , the associated logic program consists of three parts:

The rules describing the attacks in $R$ : ${attack (x, y) \leftarrow | (x, y) \in R}$ .

The rules defining acceptability: $acc (x) \leftarrow not d (x)$ .

The rules defining defeat: $d (x) \leftarrow attack (y, x), acc (y)$

where

acc (x)

stands for “the argument x is acceptable” and

d (x)

stands for “the argument x is defeated”.

The approaches described in [26,83,84] propose an alternative transformation considering not only attackers but also defenders. The common idea is to encode attack in an explicit way through a literal $def (x)$ meaning “x cannot belong to an admissible set”. So the logic program P contains rules that define $def (x)$ given the attackers of x.

The characteristic features of these approaches are:

The logic program includes weak negation (i.e. negation as failure, with the symbol $not$ ).

The encoding captures both conflict-freeness and admissibility principles.

The predicate $def$ is used. $def (x)$ means “x is defeated” or equivalently “x cannot belong to an admissible set”.

The logic program P contains two parts P⁻ and P⁺: P⁻ encodes conflict-freeness and P⁺ encodes admissibility.

P⁻ contains rules of the form $def (x) \leftarrow not def (y)$ if y attacks x. So, P⁻ defines $def (x)$ given the attackers of x.

P⁺ contains rules of the form $def (x) \leftarrow def (z_{1}), \dots, def (z_{n})$ if $z_{1}, \dots, z_{n}$ are all the attackers of some y attacker of x. Such a rule defines $def (x)$ given the defenders of x against y.

Then, acceptability can be encoded through the predicate $acc$ , where $acc (x)$ means “x can be considered as accepted”, with the rule $acc (x) \leftarrow not def (x)$ .

There are correspondences between standard argumentation semantics (grounded, stable, preferred, complete) and two-valued models of the logic program (well-founded, stable, p-stable, supported models).

Note that acceptability is defined by default. That is close to the reinstatement principle. In particular, if an argument x is not attacked, it does not appear as the head of any rule, so x will be accepted.

Ex.
3.2.3 (cont’d) We consider here the AF corresponding to a sequence of two attacks (a attacks b that in turn attacks c). The associated logic program is: $\begin{array}{l} def (b) \leftarrow not def (a) \\ def (c) \leftarrow not def (b) \\ def (b) \leftarrow ⊤ \\ def (c) \leftarrow def (a) \\ acc (x) \leftarrow not def (x) (x being a variable) \end{array}$
Ex.
3.2.4 (cont’d) We consider here the AF corresponding to an argument attacked by two other arguments (a and c attack b). The associated logic program is: $\begin{array}{l} def (b) \leftarrow not def (a) \\ def (b) \leftarrow not def (c) \\ def (b) \leftarrow ⊤ \\ acc (x) \leftarrow not def (x) (x being a variable) \end{array}$
Ex. 9.1.1.
Consider the following AF:

The associated logic program is: $\begin{array}{l} def (b) \leftarrow not def (a) \\ def (a) \leftarrow not def (b) \\ def (c) \leftarrow not def (a) \\ def (b) \leftarrow def (b) \\ def (a) \leftarrow def (a) \\ def (c) \leftarrow def (b) \\ acc (x) \leftarrow not def (x) (x being a variable) \end{array}$
Ex.
3.4.1 (cont’d) The associated logic program is: $\begin{array}{l} def (a) \leftarrow not def (b) \\ def (b) \leftarrow not def (a) \\ def (c) \leftarrow not def (b) \\ def (c) \leftarrow not def (e) \\ def (d) \leftarrow not def (c) \\ def (e) \leftarrow not def (d) \\ def (a) \leftarrow def (a) \\ def (b) \leftarrow def (b) \\ def (c) \leftarrow def (a) \\ def (c) \leftarrow def (d) \\ def (d) \leftarrow def (b), def (e) \\ def (e) \leftarrow def (c) \\ acc (x) \leftarrow not def (x) (x being a variable) \end{array}$ The unique stable model is ${def (a), def (c), def (e), acc (b), acc (d)}$ . That characterizes the unique stable extension of the AF ${b, d}$ .

The approach of [89] is rather different in the sense that it proposes several transformations of an AF in different logic programs, each one encoding a labelling-based semantics. These semantics are all characterized by the single 2-valued stable model semantics.

Given an AF, each logic program consists of two parts:

the rules encoding admissibility, which will belong to all the different programs,

the rules specific to each semantics.

For instance, let us give the program representing the grounded semantics. The first part contains rules defined as follows:27
²⁷
Note that the rules with an empty head represent constraints.

$in (x) \leftarrow out (y_{1}), \dots, out (y_{n})$ , where $y_{1}, \dots, y_{n}$ are all the attackers of x.

$out (x) \leftarrow in (y)$ for each y attacker of x.

$\leftarrow in (x), not out (y)$ for each y attacker of x.

$\leftarrow out (x), not in (y_{1}), \dots, not in (y_{n})$ , where $y_{1}, \dots, y_{n}$ are all the attackers of x.

The part specific to the grounded semantics contains rules of the form: $und (x) \leftarrow not in (x), not out (x)$ .
Ex.
3.2.3 (cont’d) The associated logic program under the grounded semantics is:

The unique stable model is ${in (a), out (b), in (c)}$ .
Ex.
3.2.4 (cont’d) The associated logic program under the grounded semantics is:

The unique stable model is ${in (a), out (b), in (c)}$ .
Ex.
9.1.1 (cont’d) The associated logic program under the grounded semantics is:

The unique stable model is ${und (a), und (b), und (c)}$ .

Towards logic programs under 3-valued semantics. Let us consider the approach described in [24]. The idea is to encode attack in an implicit way, that is as a rule of the logic program, without any additional predicate. Each argument generates a rule with the name of the argument as its head and the name of the attackers in the weak part of its body. The characteristic features of this approach are:
No predicate is needed.

Each argument becomes an atom of the program P.

The logic program includes weak negation (i.e. negation as failure, with the symbol $not$ ).

The logic program contains rules of the form $x \leftarrow not y_{1}, \dots, not y_{n}$ , where $y_{1}, \dots, y_{n}$ are all the attackers of x.

The logic program is a simple program, that is a program with at most one rule with head x for each argument x. Moreover for each rule of the program the body only contains weak atoms (atoms of the form $not a$ ).

There are correspondences between standard argumentation semantics (complete, stable, grounded, preferred) and three-valued models (3-valued stable, 2-valued stable, well-founded, regular) of the logic program.
Ex.
3.2.3 (cont’d) The associated logic program is: $\begin{array}{l} b \leftarrow not a \\ c \leftarrow not b \\ a \leftarrow \end{array}$
Ex.
3.2.4 (cont’d) The associated logic program is: $\begin{array}{l} b \leftarrow not a, not c \\ a \leftarrow \\ c \leftarrow \end{array}$
Ex.
9.1.1 (cont’d) The associated logic program is: $\begin{array}{l} b \leftarrow not a \\ a \leftarrow not b \\ c \leftarrow not a \end{array}$ This logic program has three 3-valued stable models: $(\emptyset, \emptyset)$ , $({a}, {b, c})$ , $({b, c}, {a})$ corresponding respectively to the three complete extensions of the AF: ∅, ${a}$ and ${b, c}$ .
Ex.
3.4.1 (cont’d) The associated logic program is: $\begin{array}{l} b \leftarrow not a \\ a \leftarrow not b \\ c \leftarrow not b, not e \\ d \leftarrow not c \\ e \leftarrow not d \end{array}$
Ex. 9.1.2.
Consider the following AF:

The associated logic program is: $\begin{array}{l} a \leftarrow not a, not b \\ b \leftarrow not b, not a, not c \\ c \leftarrow not d \\ d \leftarrow not c \end{array}$

9.2. Generalizations to enriched frameworks

Now we consider generalizations to enriched argumentation frameworks: a framework accounting for both attack and support interactions, called AFN, and a framework accounting for higher-order interactions.

9.2.1. AFNs and logic programs

Let us briefly review the work done by F. Nouioua (unpublished report, private communication). That work examines the connections between an Argumentation Framework with Necessities (AFN) and logic programs under three-valued semantics. Both directions are considered but following our choice we discuss only the case when an AFN is encoded into a logic program.

An AFN [78] is a kind of BAF, where the support is collective and is interpreted as a “necessary support”: Given E a non-empty set of arguments and a an argument, E is a “necessary support” for a means that the acceptance of a requires the acceptance of at least one argument of E. Note that in AFN semantics, acyclicity of the support relation is required among accepted arguments. In other words, in a given extension, support for each argument is provided by at least one of its necessary arguments and there is no risk of deadlock due to necessity cycles.

An AFN is encoded into a logic program as follows:

For each argument a, an atom a and a rule $r_{a}$ of head a are created.

For each set of arguments E that necessary supports an argument, an atom e is created.

The body of the rule $r_{a}$ contains all the weak atoms $not b_{i}$ , with $b_{i}$ attacks a, and all the strong atoms $e_{j}$ , with $E_{j}$ supports a.

For each support E, there is a rule $e \leftarrow x$ for each $x \in E$ .

There are correspondences between AFN labelling-based semantics and three-valued semantics of the program which is obtained.

Ex. 9.2.1.
Consider the following AFN:

The associated logic program is: $\begin{array}{l} a \leftarrow not b \\ b \leftarrow not a \\ c \leftarrow e_{1}, not e \\ d \leftarrow not c \\ e \leftarrow not d \\ f \leftarrow e_{2}, not e \\ g \leftarrow not g \\ e_{1} \leftarrow b \\ e_{2} \leftarrow g \end{array}$ This program has three 3-valued stable models: $(\emptyset, \emptyset)$ , $({b, e_{1}}, {a})$ , $({a, d}, {b, c, e, e_{1}})$ corresponding respectively to the three complete labellings of the AFN.

9.2.2. Argumentation frameworks with higher level attacks and logic programs by Gabbay

In [65] higher level extended argumentation frameworks are considered, where attacks on other attacks are allowed, at any level. A translation from a higher level framework into a logic program is suggested, as follows:

The atoms of the logic program are all the arguments and all the attacks.

For each e, argument or attack, if e is not attacked, the rule $e \leftarrow$ is created.

Assume that e is attacked by the arguments $a_{1}, \dots, a_{k}$ through the attacks named $α_{1}, \dots, α_{k}$ . Assume that each $α_{i}$ is itself attacked by the arguments $b_{i}^{1}, \dots, b_{i}^{k (i)}$ through the attacks named $β_{i}^{1}, \dots, β_{i}^{k (i)}$ . Then the following formula is created: $e \leftarrow ⋀_{i = 1, k} (not a_{i} \lor ⋁_{j = 1, k (i)} (β_{i}^{j} \land b_{i}^{j}))$ .

The above formula must be turned into several clauses in order to get a normal logic program.

Gabbay, in [65], proposes to define the semantics of a higher level extended argumentation framework through known semantics for logic programs, using the above transformation.

However, to the best of our knowledge, this way was not pursued by the author. Instead, Gabbay in [66] proposes to give up the logic programming approach for defining the semantics of higher level argumentation frameworks. Indeed, the new approach consists in rewriting higher level attacks as frameworks with a special kind of collective attacks (called joint attacks).

Note that another connection could be considered between another variant of higher level extended argumentation frameworks, called REBAF, and logic programs (private communication by J. Fandinno). A REBAF [29] is a generalization of AF that allows the representation of both recursive attacks and evidential supports. It is also a generalization of EBAF (see Section 2) with attacks and supports targeting other attacks or supports. Nevertheless, this connection is not in the scope of this survey since this is the encoding of a logic program into a REBAF and, up to now, the other direction (from a REBAF to a logic program) has not been considered.

9.3. Some implementations

Some implementations using logic programming have been proposed. The first one uses a translation of an AF into a logic program. The other ones do not propose a translation of an AF into a logic program but use logic programming for computational issues. ASPARTIX

(Answer Set Programming Argumentation Reasoning Tool) supports reasoning in AFs using the ASP formalism (see [57] for the description of the tool and many references).

The core of ASPARTIX handles AFs. It provides encodings for computing extensions or performing credulous/skeptical reasoning in AFs. A broad range of argumentation semantics is dealt with.

ASPARTIX also handles several other frameworks built on top of AFs, including for instance AFs augmented with preferences (PAFs), BAFs, AFRAs, SETAFs (AFs where attacks are carried by sets of arguments).

[ 46 ]

presents dialectical proofs for the credulous acceptance problem in constrained argumentation frameworks (CAF, see Section 3.4). A CAF is a generalization of AF that allows additional constraint on arguments to be taken into account in the definition of admissible sets of arguments. A dialectical proof is formalized by a dialogue between two players, the proponent and the opponent. Dialectical proofs are computed by an ASP program which consists of facts encoding a CAF and rules encoding what a dialectical proof is (that is the legal-move function of the dialogue). The models of the logic program correspond to the dialectical proofs of the CAF (see [73] for the description of the ASP solver ASPeRiX and its application to the credulous acceptance problem in a CAF).

[ 88 ]

proposes a Boolean algebra to encode acceptability semantics for AFs. A subset of arguments is represented by a Boolean vector and the attack relation is represented by a Boolean matrix. Then series of Boolean operations on vectors and matrices are introduced so that acceptability semantics (namely the admissible, stable and complete semantics) can be encoded by Boolean constraints. These constraints are translated into logic programs and solved using a Constraint Logic Programming over Boolean variables (CLPB) system, which is an instance of the general CLP scheme that extends logic programming with reasoning over Boolean domains. The implementation uses SWI-Prolog, a Prolog system equipped with a CLPB system. Experiments have been conducted, with a comparison with the approach using the solver ArgSemSAT [37] (see Section 8.3).

10. Argumentation frameworks and modal logic

As outlined in [25], there exist several methods for expressing argumentation in modal logic, among which the object-level approach and the meta-level approach. Roughly speaking, in the object-level approach, an AF and its logical translation share the same language (each argument becomes a logical atom), whereas a meta-level approach talks about an AF from “above”, using another language and logic (for instance a modal logic).

We first recall some modal logic background. Then, we present three examples of meta-level approaches. In the first two, the input consists of an AF together with a labelling. The output consists of modal formulae that express the characteristic properties of complete and stable semantics.

Finally, we briefly present an object-level approach.

10.1. Modal logic preliminaries

The modal logic K is a propositional system with the modal operator □ (and its dual ♢), the usual logical connectives, the symbols ⊤, ⊥ and atomic propositions $q_{1}, q_{2}, \dots$ .

Models for K have the form $(S, R, h)$ where $S \neq \emptyset$ is the set of possible worlds, $R \subseteq (S \times S)$ , and h is the assignment function giving for each atomic proposition q a subset $h (q)$ of S.

Satisfaction is defined as follows:

$t ⊨ q$ iff $t \in h (q)$

$t ⊨ (A \land B), (\neg A), (A \lor B), (A \to B)$ as usual

$t ⊨ (□ A)$ iff for all s such that $t R s$ , $s ⊨ A$

A holds in $(S, R, h)$ iff for all $t \in S$ , $t ⊨ A$

The system K can be axiomatized as follows:

propositional tautologies

$□ (A \to B) \to (□ A \to □ B)$

If $⊨ A$ then $⊨ □ A$

10.2. The approach by Grossi

In [70] a well-known modal logic (the extension of K with universal modality) is used to formalize basic notions of argumentation theory.

Let $AF = (A, R)$ . $AF$ is viewed as a modal frame, where the set of possible worlds is the set of arguments $A$ and the accessibility relation is the inverse of the attack relation (intuitively the “being attacked” relation).

An assignment I on $(A, R)$ is a function from a set of propositional atoms to the subsets of arguments.28

²⁸
That is, the codomain of I is the powerset of $A$ .

The fact that an argument a belongs to

I (p)

can be interpreted as “argument a has property p”.

An argumentation model has the form $(AF, I)$ where I is an assignment on $AF$ . As an example of assignment, we find the labellings: A labelling function $ℓ$ on $A$ can be viewed as an assignment on the propositional symbols $1, 0, ?$ (intuitively $in, out, und$ ).

The following statements are interesting in argumentation theory:

“argument a is attacked by the set of arguments E”;

“argument a is defended by the set of arguments E”;

“the set of arguments E attacks an attacker of argument a”.

In order to express these statements, two modal operators are used:

$⟨ \leftarrow ⟩$ whose intuitive reading is “there exists an argument attacking the current one such that”, and

$⟨ \forall ⟩$ whose intuitive reading is “there exists an argument such that”.

As usual, there are also the dual operators $[\leftarrow]$ and $[\forall]$ .

The semantics is as follows: In a given model $(AF, I)$ :

$a ⊨ ⟨ \leftarrow ⟩ ϕ$ iff there exists s such that s attacks a in $AF$ and $s ⊨ ϕ$ .

$a ⊨ ⟨ \forall ⟩ ϕ$ iff there exists s such that $s ⊨ ϕ$ .

Consider for instance the particular case of a labelling. Let a be an argument. $a ⊨ ⟨ \leftarrow ⟩ 1$ reads “there exists at least one attacker of a labelled $in$ ”.

Given an argumentation model $(AF, I)$ , the statement “argument a is attacked by an argument in the set of arguments of $A$ that satisfy the property ϕ” can be encoded as $a ⊨ ⟨ \leftarrow ⟩ ϕ$ . As $s ⊨ ϕ$ reads “s belongs to the set of arguments in $A$ that satisfy ϕ”, it follows that $a ⊨ ⟨ \leftarrow ⟩ ϕ$ encodes the statement “argument a is attacked by the set of arguments in $A$ that satisfy ϕ”. Similarly, the statement $a ⊨ ⟨ \leftarrow ⟩ ⟨ \leftarrow ⟩ ϕ$ encodes the statement “argument a is defended by the set of arguments in $A$ that satisfy ϕ”.

The modal logic that is obtained is an extension of the modal logic K, denoted by $K^{\forall}$ . It enables to capture basic principles of argumentation semantics, as for instance:

$[\forall] (ϕ \to [\leftarrow] \neg ϕ)$ encodes that $⟦ ϕ ⟧$ 29

²⁹

$⟦ ϕ ⟧$ denotes the set of arguments in $AF$ that satisfy ϕ.

is conflict-free.

$[\forall] (ϕ \to [\leftarrow] ⟨ \leftarrow ⟩ ψ)$ encodes that $⟦ ϕ ⟧$ is acceptable w.r.t. $⟦ ψ ⟧$ .

$[\forall] (ϕ \leftrightarrow [\leftarrow] \neg ϕ)$ encodes that $⟦ ϕ ⟧$ is stable.

Consider the particular case of a labelling. A labelling $ℓ$ is a complete labelling for $AF$ iff the model $(AF, ℓ)$ satisfies the following formula: $\begin{matrix} [\forall] ((1 \leftrightarrow [\leftarrow] 0) \land (0 \leftrightarrow ⟨ \leftarrow ⟩ 1) \land Label) \end{matrix}$ where $Label$ is the formula $(1 \land \neg 0 \land \neg ?) \lor (\neg 1 \land 0 \land \neg ?) \lor (\neg 1 \land \neg 0 \land ?)$ , meaning that each argument can get at most one label. See an example given in Section 12.2.

Then model-checking can be used in order to determine whether a given formula is conflict-free, admissible, stable.

Furthermore, Grossi, in [70], presents a game-theoretic proof procedure based on model-checking games for the logic $K^{\forall}$ . In such a game, a proponent tries to prove that $a ⊨ ϕ$ holds in a given model $(AF, I)$ while an opponent tries to disprove it.

Note that an additional modal machinery including a least fixed point operator is needed to capture the notion of grounded extension.

10.3. The meta-level approach of Caminada and Gabbay

The meta-level approach of [25] is close to the approach of [70]. It can be summarized as follows. Given $AF = (A, R)$ ,

Arguments are viewed as possible worlds; so $AF$ becomes a modal frame for the modal logic K.

The attack relation becomes the accessibility relation.

A labelling becomes an assignment of three propositional atoms $q_{0}$ , $q_{1}$ , $q_{?}$ .

More precisely, given $ℓ$ a labelling on $AF$ , the associated assignment I is defined as follows: $\begin{array}{l} t \in I (q_{0}) (or t ⊨ q_{0}) iff ℓ (t) = out; \\ t \in I (q_{1}) (or t ⊨ q_{1}) iff ℓ (t) = in; \\ t \in I (q_{?}) (or t ⊨ q_{?}) iff ℓ (t) = und . \end{array}$

The modality □ means “being attacked by”, namely $a ⊨ □ ϕ$ iff for all s such that s attacks a in $AF$ , $s ⊨ ϕ$ . As usual, ♢ denotes the dual modality.

Note that the modality □ corresponds to the modality $[\leftarrow]$ of [70]. However there is no modality corresponding to $[\forall]$ .

Complete labellings can be characterized with a set of axioms including for instance: $\begin{array}{l} □ q_{0} \to q_{1} (if all attackers of t are out then t is in) \\ ♢ q_{1} \to q_{0} (if t is attacked by an argument which is in then t is out) . \end{array}$

Then, stable and complete extensions are characterized by the following equations. Let E be a propositional letter denoting a set of arguments (see an example given in Section 12.2).

E is stable iff $E = □ \neg E$ .

E is a complete extension iff $E = □ (\neg E \land ♢ E)$ .

The extensions can be obtained as fixed point solutions for the above equations.

10.4. The modal setting of Villata et al.

The purpose of the work reported in [93] is to define a logic for specifying and verifying requirements for AFs. A propositional variant has been presented in Section 6. Here we consider the modal variant, which allows the expression that some semantics admit multiple extensions and also the expression of properties of the attack relation (such as irreflexivity, or symmetry for instance).

The main difference with the modal approaches of [25] and [70] is that these works describe semantics in the modal language, whereas [93] considers semantics as primitives of the language.

The approach of [93] presents the following features:

Sets of arguments are viewed as possible worlds.

The attack relation is interpreted as an accessibility relation among worlds. That implies that the attack relation represents a collective attack (a set of arguments taken together may attack another set of arguments).

There are two modal operators: $□_{1}$ and $□_{2}$ . The modality $□_{1}$ means “attacks”, namely $p ⊨ □_{1} ϕ$ iff for all q such that p attacks q in the AF, $q ⊨ ϕ$ . $□_{2}$ is a universal modality (as $[\forall]$ in [70]).

As in the propositional variant, primitives of the modal language (such as $F (p)$ , $A (p)$ ) represent semantics. Moreover, in order to abbreviate formulae, a connective for collective attack is defined as follows: $p ⊳ q \equiv □_{2} (p \to □_{1} \neg q)$ .

The modal logic that is obtained enables to express characterizations such as:

For any pair $(p, q)$ of sets of arguments such that p attacks q, they cannot be subsets of a conflict-free extension: $□_{2} (p ⊳ q) \to F (\neg p \lor \neg q)$

The grounded semantics admits a single extension: $⊨ (G (p) \land G (q)) \to □_{2} (p \leftrightarrow q)$

10.5. The object-level approach of Caminada and Gabbay

The object-level approach of [25] can be summarized as follows. Given $AF = (A, R)$ ,

Arguments are viewed as atomic propositions in the modal provability logic ${LN}_{3}$ .

The content of $AF$ is represented by a formula $M (AF)$ of the logic ${LN}_{3}$ .

The possible world models of $M (AF)$ are in one-to-one correspondence with the labellings of $AF$ .

The modal formula $M (AF)$ is as follows: $\begin{array}{l} M (AF) = (\begin{matrix} (G ((□ ⊥) \lor (⋀_{y has attackers y_{i}} (y \leftrightarrow ⋀_{i} ♢ \neg y_{i})))) \\ ⋀ \\ (⋀_{x is not attacked} G x) \end{matrix}) \end{array}$ where $G A$ stands for $A \land □ A$ .

The provability logic ${LN}_{3}$ has the following axioms and rules:

axioms and rules of modal logic K

$♢ A \to ♢ (A \land □ \neg A)$

$□ A \to □ □ A$

$(♢ A \land ♢ B) \to ♢ (A \land B) \lor ♢ (A \land ♢ B) \lor ♢ (B \land ♢ A)$

$□ □ □ ⊥$

11. Translation of an AF into intuitionistic logic

The translation of an AF into an intuitionistic logic theory has been first considered in [68]. The idea is to use intuitionistic negation to model an attack. The intuitionistic models of the obtained theory characterize the complete extensions.

More recently, [63] presents a translation of an AF into Nelson’s constructive logic, an extension of intuitionistic logic including the notion of strong negation as a means to deal with constructive falsity. This logic allows to capture an AF under the stable semantics, at the object level, in the sense that arguments in AF become atoms in the corresponding logical theory and interactions between arguments are expressed by logical connectives. Moreover the translation allows to deal with enriched argumentation frameworks such as frameworks with collective attacks, and frameworks with attacks and evidential supports.

11.1. Background about intuitionistic logic

Let us recall that:

Intuitionistic implication $ϕ_{1} \to ϕ_{2}$ can be understood as a means to construct a proof of the truth of $ϕ_{2}$ in terms of a proof of the truth of $ϕ_{1}$ .

Strong negation $\sim ϕ$ can be understood as the existence of a proof of the falsity of ϕ.

Intuitionistic negation is defined as $\neg ϕ \equiv (ϕ \to ⊥)$ . It can be understood as a means to obtain a proof of a contradiction from a proof of the truth of ϕ (or roughly speaking as “there cannot be a proof of the truth of ϕ”).

Then, a new implication connective, ⇒, allows the formalization of the “non contradictory” inference principle (NC): “no belief can be held based on contradictory evidence”. $\begin{matrix} ϕ_{1} \Rightarrow ϕ_{2} \equiv (\neg \sim ϕ_{1} \land ϕ_{1}) \to ϕ_{2} \end{matrix}$

Intuitively, $ϕ_{1} \Rightarrow ϕ_{2}$ can be understood as a means to construct a proof of the truth of $ϕ_{2}$ given a proof of the truth of $ϕ_{1}$ and the fact that there cannot be a proof of its falsity (or in other words given a “consistent” proof of $ϕ_{1}$ ).

11.2. Abstract argumentation and intuitionistic logic

In [63], intuitionistic logic is used for translating an AF or an EBAF.

Translation of an AF. The translation presented in [63] relies on the following intuition: under the constructive logic point of view, an attack is a “means to construct a proof of the falsity of the attacked argument based on the acceptability of the attacker”. Moreover, the acceptability of ϕ is identified with having a consistent proof of it (i.e. there is a proof of the truth of ϕ and there cannot be a proof of the falsity of ϕ).

Then the above intuition of the notion of attack is formalized by a new connective: $\begin{matrix} ϕ_{1} ⇝ ϕ_{2} \equiv ϕ_{1} \Rightarrow \sim ϕ_{2} \end{matrix}$

In other words, $ϕ_{1} ⇝ ϕ_{2}$ says that the acceptability of $ϕ_{1}$ allows to construct a proof of the falsity of $ϕ_{2}$ , and a proof of the falsity of $ϕ_{2}$ is identified with $ϕ_{2}$ being defeated.

Given $AF = (A, R)$ , the associated theory in constructive logic is: $\begin{matrix} C (AF) \equiv A \cup {a ⇝ b | (a, b) \in R} \end{matrix}$ [63] proves that there is a one-to-one correspondence between the stable extensions of AF and the equilibrium models of the theory $C (AF)$ , where the equilibrium models of a theory are a particular selection of constructive logic models of this theory.

Regarding how other extension-based semantics could be characterized in constructive logic is an open topic.

Translation of evidential argumentation frameworks. In the case of an argumentation framework with collective attacks and evidential supports (EBAF) the translation uses the connectives ⋀, ⇝ and ⇒.

Let $EBAF = (A, R, E, P)$ . Recall that the attack relation $R$ is a subset of $2^{A} ∖ \emptyset \times A$ , the support relation $E$ is a subset of $2^{A} ∖ \emptyset \times A$ , and $P \subseteq A$ is the set of distinguished prima-facie arguments (see Section 2.1).

Using the notation $⋀ B$ that denotes “the conjunction of the elements of B”, the associated theory in constructive logic is: $\begin{matrix} C (EBAF) \equiv P \cup {⋀ B ⇝ b | (B, b) \in R} \cup {⋀ B \Rightarrow b | (B, b) \in E} \end{matrix}$

Note that the support from the set of arguments B to an argument b is translated by the formula $⋀ B \Rightarrow b$ which says that the acceptability of B enables to construct a proof of the truth of b.

As for the case of an AF, in [63] it is proved that there is a one-to-one correspondence between the stable extensions of an EBAF (defined in [29]) and the equilibrium models of the theory $C (EBAF)$ .

12. Analysis and conclusion

In this section, we first compare the reviewed approaches according to several criteria. Then, we illustrate the associated encodings on an example. And finally we will conclude this survey.

12.1. Comparison criteria

Recall that our initial choice was to identify and to compare approaches that “use logic for doing argumentation”.30

³⁰
The other direction could be the object of another survey that would cover the relationship between logical frameworks and formal argumentation, including structured argumentation.

At least four criteria can be used:

The first comparison criterion is about the input taken into account by the different approaches. In each case, the input consists at least of a graph. Except in the ADF approach, this graph usually represents an AF. Moreover, in some approaches, the AF is extended into either a bipolar AF, or a recursive AF, or an AF with collective interactions, or with weighted arguments/interactions, or with preferences, or built on a given universe.

In some approaches, an additional input is needed: either constraints or requirements that must be satisfied by the output or “candidates” that must be studied in order to satisfy some properties. Table 1 synthetizes all these cases.

Table 1

The first comparison criterion: the input

Input graph	Approaches
Case of an input graph that represents an AF
Dung	[4,5,11,12,24–26,30,36,43,49,50,52,54,55,59,65,67,70,83,84,89,93]
Bipolar	[63]
Recursive	[34,65]
Weighted	none
With preference	[56]
With collective interactions	[55,63]
On a universe	[55]
Case of an input graph that does not represent an AF
Dependence graph	ADF approach [20,21]

Other input	Approaches
Acceptance conditions	∙ (on each argument) ADF approach [20,21]: depending on the chosen acceptance conditions, the dependence graph can represent any type of AF, from Dung AFs to AFs with collective interactions
	∙ (on the AF) Constrained AF [43]: the acceptance condition is used only for removing some extensions
Requirements	On the AF or the semantics [93]: the requirements are used for constraining the structure of the AF or the resulting labellings
Candidates	Are these candidates actual extensions or labellings for the given semantics? [11,12,25,36,59,70]

The second criterion is about the aim of the approaches that use logic for doing argumentation and is related to the produced output. Two kinds of aim can be encountered:

Either the aim is to obtain a logical encoding of the input AF; in this case, the output is a set of formulae;

Or the aim is to encode argumentative semantics; in this case, the output is a set of logical formulae whose models correspond to extensions or labellings for a given argumentation semantics possibly with additional constraints; sometimes, it is also possible to check whether some “candidates” are actual extensions or labellings for a given semantics.

It is worth noting that if an approach covers the first aim, it also covers at least part of the second one. Indeed, it is very difficult to encode an argumentation graph without taking into account the meaning attached to the notion of attack (at least the notion of conflict-freeness). Table 2 synthetizes the aims of the reviewed approaches.

Table 2

The second comparison criterion: the aim

Aim		Approaches
Translation of an AF		[24,26,30,34,52,55,56,67,84]
Encoding of semantics	Case of extension-based semantics	[11,12,24–26,30,34,52,54–56,59,63,65,67,78,83,84,89,93]
Encoding of semantics	Case of labelling-based semantics	[4,5,25,25,36,49,50,70]

The third criterion is about logic. Several logics are encountered: propositional logic, first-order logic, QBF formalism, logic programming, modal logic, intuitionistic logic. Table 3 synthetizes the different cases.

Note that the complexity of the chosen logic must be taken into account: it is more or less difficult to compute models and to establish the link between these models and the output that must be produced. This point is related to the next criterion.

Table 3

The third comparison criterion: the used logic

Used logics	Approaches
Propositional	[11,12,20,21,43,52,56,59,67]
First-order (with finite domains)	[25,30,34,36,55,93]
QBF	[4,5,49,50]
Logic programming	[24,26,54,65,78,83,84,89]
Modal	[25,70,93]
Intuitionistic	[63]

The fourth criterion is about the existence of implementations: some approaches are yet to be implemented, whereas some others have led to different implementations, some of them being used in the ICCMA competition (see for instance [72]). Table 4 synthetizes all these implementations.

Table 4

The fourth comparison criterion: the implementations

Some existing implementations	Approaches
None	[25,43,55,63,67,70,93]
DIAMOND, UNREAL, GrappaVis	[20,21]
GRAFIX	[30,34]
SESAME, CoQuiAAS	[11–13,72,74,95]
CEGARTIX	[59]
QADF	[20,21,49,50]
PrefSAT, ArgSemSAT	[36,37]
LabSAT	[9,9]
ASPARTIX, ASPeRiX, ASP-solvers	[24,26,46,54,61,69,83,84,88,89]

12.2. An illustrating example

The following example illustrates the different encodings that can be obtained.

Ex.
2.1.1 (cont’d) The AF is a simple Dung’s framework that has only one complete extension: ${a, d, c}$ .

With ADF approach (translation of the AF into a dependence graph):
See Section 3. The AF is encoded by the following dependence formulae: $\begin{array}{l} φ_{a} = ⊤, φ_{b} = \neg a \land \neg d, φ_{c} = \neg b, φ_{d} = ⊤ . \end{array}$

The language is propositional with the vocabulary $V = {a, b, c, d}$ . Then, using the ADF machinery (the computation of the fixed points of the $Γ_{D}$ operator) a 3-valued model is produced, which corresponds to the complete extension ${a, d, c}$ .
Translation of the AF into a logical base:
Several approaches exist, each of them including an encoding of semantics.

[ 30 , 33 , 34 ]:
See Section 4.2. The vocabulary is defined as follows: $\begin{array}{l} V = {Acc (a), NAcc (a), Acc (b), NAcc (b), Acc (c), NAcc (c), Acc (d), NAcc (d)} . \end{array}$ Note that it is a first-order approach whose term models are finite so it is equivalent to a propositional approach.

The AF is encoded by the set of formulae: $\begin{array}{l} Σ = & {Acc (a) \to NAcc (b), Acc (d) \to NAcc (b), \\ Acc (b) \to NAcc (c), \\ NAcc (a) \to \neg Acc (a), NAcc (b) \to \neg Acc (b), \\ NAcc (c) \to \neg Acc (c), NAcc (d) \to \neg Acc (d)} . \end{array}$

The different requirements of the standard semantics are also logically encoded. For instance, for the complete semantics, the defence and the reinstatement principles are respectively encoded by: $\begin{array}{l} Σ_{d} = {\neg Acc (b), Acc (c) \to (Acc (a) \lor Acc (d))} \\ Σ_{r} = {Acc (a), Acc (d), Acc (a) \to Acc (c), Acc (d) \to Acc (c)} . \end{array}$

Then, the models of $Σ \cup Σ_{d} \cup Σ_{r}$ characterize the complete extensions (here there is only one model corresponding to the unique complete extension ${a, d, c}$ ).
[ 67 ]:
See Section 4.3. The language is propositional with the vocabulary $V = {a, b, c, d, N a, N b, N c, N d}$ . The AF and some requirements corresponding to the semantics are logically encoded. However, the logical encoding mixes the part issued from the input AF and the part issued from the encoding of semantics. Moreover, it is not possible to identify the part issued from each principle in the logical encoding of a semantics. For the considered AF, the resulting base is:31
³¹
Without trivial formulae such as, for instance, $(⊤ \land ⊥) \to (\neg a \land \neg N a)$ .

$\begin{array}{l} {N a \to \neg a, N b \to \neg b, N c \to \neg c, N d \to \neg d, \\ a, d, a \to N b, d \to N b, b \to N c, \\ a \leftrightarrow ⊤, d \leftrightarrow ⊤, b \leftrightarrow (N a \land N d), c \leftrightarrow N b, \\ (\neg a \land \neg d \land (\neg N a \lor \neg N d)) \to (\neg b \land \neg N b), \\ (\neg b \land \neg N b) \to (\neg c \land \neg N c)} . \end{array}$

The models of this base characterize the complete extensions (here there is only one model corresponding to the unique complete extension ${a, d, c}$ ).
[ 55 ]:
See Section 6.1. The language is first-order. Considering that the input AF is also the universe, the encoding produces the formula Φ: $\begin{array}{l} (on ({a, b, c, d})) \land ({a} ⊳ {b}) \land ({d} ⊳ {b}) \land ({b} ⊳ {c}) . \end{array}$

Then, considering a set of arguments t, one can check whether t is an extension for the given semantics. For instance, t is a complete extension if the following formula is a tautology:

[ 26 , 83 , 84 ]:
See Section 9.1. The approach uses logic programming. The AF is encoded by the following logic program: $\begin{array}{l} def (b) \leftarrow not def (a) \\ def (b) \leftarrow not def (d) \\ def (c) \leftarrow not def (b) \\ def (c) \leftarrow def (a), def (d) \\ def (b) \leftarrow ⊤ \\ acc (a) \leftarrow not def (a) \\ acc (b) \leftarrow not def (b) \\ acc (c) \leftarrow not def (c) \\ acc (d) \leftarrow not def (d) \end{array}$

The complete extensions are characterized by the supported models of the logic program. Here, there is only one supported model ( ${acc (a), acc (c), acc (d), def (b)}$ ) corresponding to the unique complete extension ( ${a, c, d}$ ).
[ 24 ]:
See Section 9.1. The approach also uses logic programming, with propositional symbols. The AF is encoded by the following logic program: $\begin{array}{l} b \leftarrow not a, not d \\ c \leftarrow not b \\ a \leftarrow \\ d \leftarrow \end{array}$

There are correspondences between 3-valued models of the logic program and argumentation semantics. For instance, the complete extensions of the AF are characterized by the 3-valued stable models of the associated logic program.
[ 63 ]:
See Section 11. The logic is equilibrium logic, with the vocabulary $V = {a, b, c, d}$ . The AF is encoded by the base: $\begin{array}{l} a \\ b \\ c \\ d \\ a ⇝ b \\ d ⇝ b \\ b ⇝ c \end{array}$

However, only the stable semantics has been characterized in terms of equilibrium models.

Encoding of semantics
The approaches presented above allow the characterization of some semantics, given the logical encoding of the AF. Some other approaches give a characterization of semantics without encoding the input AF. They try to identify and to encode some principles governing the input semantics. In some cases, the produced formulae can be instantiated on a given AF, particularly in order to compute the extensions/labellings, or to check whether a given set of arguments is an extension (or whether a given labelling is correct w.r.t. the input semantics).

[ 11 ]:
See Section 7.1. The language is propositional with the vocabulary $V = {a, b, c, d}$ . For the considered AF, the complete extensions are characterized by the following formula Φ: $\begin{array}{l} [(a \to \neg b) \land (a \leftrightarrow ⊤)] \land \\ [(d \to \neg b) \land (d \leftrightarrow ⊤)] \land \\ [(b \to \neg c) \land (b \leftrightarrow ⊥)] \land \\ [(c \to ⊤) \land (c \leftrightarrow (a \lor d))] \end{array}$

Then, given a set of arguments S, it can be checked whether S is a complete extension.
[ 59 ]:
See Section 7.2. The language is propositional with the vocabulary $V = {x_{a}, y_{a}, x_{b}, y_{b}, x_{c}, y_{c}, x_{d}, y_{d}}$ . For the considered AF, the complete extensions are characterized by the following formula Φ: $\begin{array}{l} [(\neg x_{a} \lor \neg x_{b}) \land (\neg x_{d} \lor \neg x_{b}) \land (\neg x_{b} \lor \neg x_{c})] \land \\ [(\neg x_{b}) \land (x_{c} \to (x_{a} \lor x_{d}))] \land \\ [(y_{a} \leftrightarrow x_{a}) \land (y_{d} \leftrightarrow x_{d})] \land \\ [y_{b} \leftrightarrow (x_{b} \lor x_{a} \lor x_{d})] \land \\ [y_{c} \leftrightarrow (x_{c} \lor x_{b})] \land \\ [y_{a} \land y_{d} \land ((y_{a} \land y_{d}) \to y_{b})] \land \\ [y_{b} \to y_{c}] \end{array}$

Models of Φ characterize the complete extensions of the AF ( $x_{i}$ is true in the model iff the argument i belongs to the extension).
[ 4 , 5 ]:
See Section 5. The logic uses quantified Boolean formulae (QBF formalism). The formulae can be instantiated on a given AF. For the considered AF, the complete labellings are characterized by the following formula: $\begin{array}{l} [val (a, t) \land \neg val (a, f) \land \neg val (a, u)] \land \\ [val (d, t) \land \neg val (d, f) \land \neg val (d, u)] \land \\ [val (b, t) \to (val (a, f) \land val (d, f))] \land \\ [val (b, f) \to (val (a, t) \lor val (d, t))] \land \\ [val (b, u) \to (\begin{matrix} \neg (val (a, f) \land val (d, f)) \\ \land (\neg (val (a, t) \lor val (d, t))) \end{matrix})] \land \\ [val (c, t) \to val (b, f)] \land \\ [val (c, f) \to val (b, t)] \land \\ [val (c, u) \to (\neg val (b, f) \land \neg val (b, t))] \land \\ [\neg (a^{\oplus} \land a^{⊖})] \land \\ [\neg (b^{\oplus} \land b^{⊖})] \land \\ [\neg (c^{\oplus} \land c^{⊖})] \land \\ [\neg (d^{\oplus} \land d^{⊖})] \end{array}$
[ 25 ] with first-order logic:
See Section 8.1. For the considered AF, the complete labellings are characterized by the following formula: $\begin{array}{l} [Q_{0} (a) \lor Q_{1} (a) \lor Q_{?} (a)] \land \\ [Q_{0} (b) \lor Q_{1} (b) \lor Q_{?} (b)] \land \\ [Q_{0} (c) \lor Q_{1} (c) \lor Q_{?} (c)] \land \\ [Q_{0} (d) \lor Q_{1} (d) \lor Q_{?} (d)] \land \\ [\neg (Q_{0} (a) \land Q_{1} (a)) \land \neg (Q_{0} (a) \land Q_{?} (a)) \land \neg (Q_{?} (a) \land Q_{1} (a))] \land \\ [\neg (Q_{0} (b) \land Q_{1} (b)) \land \neg (Q_{0} (b) \land Q_{?} (b)) \land \neg (Q_{?} (b) \land Q_{1} (b))] \land \\ [\neg (Q_{0} (c) \land Q_{1} (c)) \land \neg (Q_{0} (c) \land Q_{?} (c)) \land \neg (Q_{?} (c) \land Q_{1} (c))] \land \\ [\neg (Q_{0} (d) \land Q_{1} (d)) \land \neg (Q_{0} (d) \land Q_{?} (d)) \land \neg (Q_{?} (d) \land Q_{1} (d))] \land \\ [(Q_{0} (a) \to Q_{1} (b)) \land (Q_{0} (d) \to Q_{1} (b)) \land Q_{1} (a) \land Q_{1} (d)] \land \\ [Q_{0} (b) \to Q_{1} (c)] \land \\ [((Q_{1} (a) \lor Q_{1} (d)) \to Q_{0} (b)) \land (Q_{1} (b) \to Q_{0} (c))] \land \\ [((Q_{0} (b) \lor Q_{?} (b)) \land Q_{?} (b)) \to Q_{?} (c)] \land \\ [(\begin{matrix} (Q_{0} (a) \lor Q_{?} (a)) \\ \land (Q_{0} (d) \lor Q_{?} (d)) \\ \land (Q_{?} (a) \lor Q_{?} (d)) \end{matrix}) \to Q_{?} (b)] \end{array}$
[ 25 ] with modal logic:
See Section 10.3. The modal formula characterizing the complete extensions is quite simple. The difficulty lies in computational issues. $\begin{array}{l} E is a complete extension iff E = □ (\neg E \land ♢ E) \end{array}$
[ 70 ]:
See Section 10.2. The logic is a modal logic. The modal formula characterizing the complete extensions is the following one: $\begin{array}{l} [\forall] (\begin{matrix} (1 \leftrightarrow [\leftarrow] 0) \\ \land (0 \leftrightarrow ⟨ \leftarrow ⟩ 1) \\ \land [(1 \land \neg 0 \land \neg ?) \lor (\neg 1 \land 0 \land \neg ?) \lor (\neg 1 \land \neg 0 \land ?)] \end{matrix}) \end{array}$

Here again, the difficulty lies in computational issues.

12.3. Conclusion

Considering that this survey is published on the occasion of the 25 years of Dung’s approach, we have chosen to discuss approaches that relate logical theories and abstract argumentation in a specific sense: “How logic has been used for capturing various aspects or parts of Dung’s argumentation”. In view of the numerous proposals on the topic, it seemed to us of interest to look at them in the same place (this paper) and in a common way (whereas authors often introduce their approaches with some bias, no matter how sensible and well-taken). So, the presentation of each approach has been designed in order to answer the same set of questions: What is the aim? What are the “inputs” and the “outputs”? What is the type of the logic used? Do implementations exist?

In Section 12.1, we have given some criteria/traits/features/properties to get comparisons [similarities and differences] out of the answers to these questions; then in Section 12.2, a same example has been used in order to illustrate the behaviour of the presented approaches. The number and the diversity of these approaches are so huge that this comparison is limited but we still believe it has some value. Indeed, each presented approach has its own specificities, sometimes antagonistic with the other approaches, but also justified by its own context of definition or use. And we think that it is difficult and perhaps impossible to give here a more precise evaluation.

Nevertheless, some “use cases” could be proposed for which an approach makes a better choice that another one.

A first example of “use cases” could be: when your “input” is an AF (only simple attacks between arguments) and we are only interested in a very efficient computation of extensions, an encoding using [11,12] coupled with a SAT solver could be a good choice (note that some of the best solvers of the ICCMA competition do this choice [16]).

Fig. 3.

ADF approach, Example 3.2.1: set of two-valued interpretations and $G_{D}$ operator.

Fig. 4.

ADF approach, Example 3.2.1: the complete lattice built from the set of two-valued interpretations and the $⩽_{t}$ preordering.

Fig. 5.

ADF approach, Example 3.2.2: set of three-valued interpretations and $Γ_{D}$ operator.

Fig. 6.

ADF approach, Example 3.2.2: the complete meet-lattice built from the set of three-valued interpretations and the $⩽_{i}$ preordering.

Another example of “use cases” could be: your “input” is an argumentation framework with several enrichments such as weighting functions, and we want to compute labellings. Obviously the approach defined in [11,12] cannot be used whereas an encoding by an ADF [21] coupled with one of the ADF solvers (and there are many ADF solvers) could be a better choice.

But if your input is an argumentation framework with recursive interactions, perhaps it would be better to use an encoding of this framework using the approach proposed in [33] coupled with a SAT solver in order to obtain the extensions.

Another point of view could be the size of the logical knowledge base corresponding to the encoded framework: clearly the encoding in propositional logic proposed in [59] is lengthy compared to the encoding in modal logic proposed by [70].

On another hand, expressiveness can also be taken into account since it differs depending on the approach under consideration. An example can be found when we compare the YALLA approach for instance with the encoding proposed in [33]: both use a first-order language, but YALLA is also able to reason about extensions, and not only about argument acceptance (for each semantics, there is a first-order formula in YALLA expressing that a subset of arguments is an extension under this semantics).

And of course, in a computational point of view, an existing and efficient implementation could offer a preponderant advantage. For instance, this is generally the case of approaches using propositional logic [11,59] compared to those using modal logic [25,70].

All previous “use cases” clearly show the multiplicity of points of view and that leads us to conclude that one cannot obtain a definite answer to the question of what approach is best.

Footnotes

Acknowledgements

This work has been supported by the Centre International de Mathématiques et d’Informatique de Toulouse (CIMI) through contract ANR-11-LABEX-0040-CIMI within the program ANR-11-IDEX-0002-02. Moreover, the authors wish to thank Sylvie Doutre and Luis Fariñas del Cerro for the fruitful exchanges and discussions.

References

Alviano, Argumentation reasoning via circumscription with Pyglaf, Fundamenta Informaticae167(1–2) (2019), 1–30. doi:10.3233/FI-2019-1808.

Amgoud and

Cayrol, A reasoning model based on the production of acceptable arguments, Annals of Mathematics and Artificial Intelligence34 (2002), 197–216. doi:10.1023/A:1014490210693.

Amgoud,

Maudet and

Parsons, Modelling dialogues using argumentation, in: Proc. of ICMAS, 2000, pp. 31–38.

Arieli and

Caminada, A general QBF-based formalization of abstract argumentation theory, in: Proceedings of the 4th Conference on Computational Models of Argument (COMMA’2012),

Verheij,

Szeider and

Woltran, eds, Frontiers in Artificial Intelligence and Applications, Vol. 245, IOS Press, Vienna, Austria, 2012, pp. 105–116.

Arieli and

M.W.A.

Caminada, A QBF-based formalization of abstract argumentation semantics, J. Applied Logic11(2) (2013), 229–252. doi:10.1016/j.jal.2013.03.009.

Baroni,

Caminada and

Giacomin, An introduction to argumentation semantics, Knowledge Eng. Review26(4) (2011), 365–410. doi:10.1017/S0269888911000166.

Baroni,

Cerutti,

Giacomin and

Guida, AFRA: Argumentation framework with recursive attacks, International Journal of Approximate Reasoning52 (2011), 19–37. doi:10.1016/j.ijar.2010.05.004.

Barringer,

D.M.

Gabbay and

Woods, Temporal dynamics of support and attack networks: From argumentation to zoology, in: Mechanizing Mathematical Reasoning,

Hutter and

Stephan, eds, LNAI, Vol. 2605, Springer-Verlag, 2005, pp. 59–98. doi:10.1007/978-3-540-32254-2_5.

Beierle,

Brons and

Potyka, A software system using a SAT solver for reasoning under complete, stable, preferred, and grounded argumentation semantics, in: KI 2015: Advances in Artificial Intelligence – 38th Annual German Conference on AI, Proceedings, Dresden, Germany, September 21–25, 2015, 2015, pp. 241–248.

10.

Besnard,

Boudou,

Doutre, Van Hieu Ho and

Longin, The SESAME website, https://www.irit.fr/SESAME/.

11.

Besnard and

Doutre, Checking the acceptability of a set of arguments, in: 10th International Workshop on Non-Monotonic Reasoning (NMR’04),

J.P.

Delgrande and

Schaub, eds, Whistler, Canada, 2004, pp. 59–64.

12.

Besnard,

Doutre and

Herzig, Encoding argument graphs in logic (regular paper), in: International Conference on Information Processing and Management of Uncertainty in Knowledge-Based Systems (IPMU), Montpellier, France, 15/07/2014–19/07/2014,

Laurent,

Strauss,

Bouchon-Meunier and

R.R.

Yager, eds, Communications in Computer and Information Science, Vol. 443, Springer, http://www.springerlink.com , 2014, pp. 345–354.

13.

Besnard,

Doutre,

V.H.

Ho and

Longin, SESAME – a system for specifying semantics in abstract argumentation (regular paper), in: International Workshop on Systems and Algorithms for Formal Argumentation (SAFA), Potsdam, Germany, 13/09/2016,

Thimm,

Cerutti,

Strass and

Vallati, eds, CEUR Workshop Proceedings, Vol. 1672, http://CEUR-WS.org , 2016, pp. 40–51.

14.

Besnard and

Hunter, A logic-based theory of deductive arguments, Artificial Intelligence128(1–2) (2001), 203–235. doi:10.1016/S0004-3702(01)00071-6.

15.

Bisquert,

Cayrol,

Dupin de Saint-Cyr Bannay and

M.-C.

Lagasquie-Schiex, Characterizing change in abstract argumentation systems, in: Trends in Belief Revision and Argumentation Dynamics,

Fermé,

Gabbay and

Simari, eds, Studies in Logic, Vol. 48, College Publications, http://www.collegepublications.co.uk/ , 2013, pp. 75–102.

16.

Bistarelli,

Santini,

Kotthoff,

Mantadelis and

Taticchi, Int. competition on computational models of argumentation, 2019, https://www.iccma2019.dmi.unipg.it/.

17.

Boella,

D.M.

Gabbay,

van der Torre and

Villata, Support in abstract argumentation, in: Proceeding of the 2010 Conference on Computational Models of Argument: Proceedings of COMMA 2010, IOS Press, Amsterdam, The Netherlands, 2010, pp. 111–122.

18.

Booth,

Kaci,

Rienstra and

van der Torre, A logical theory about dynamics in abstract argumentation, in: Scalable Uncertainty Management,

Liu,

V.S.

Subrahmanian and

Wijsen, eds, Lecture Notes in Computer Science, Vol. 8078, Springer, Berlin, Heidelberg, 2013, pp. 148–161. doi:10.1007/978-3-642-40381-1_12.

19.

Brewka,

Diller,

Heissenberger,

Linsbichler and

Woltran, Solving advanced argumentation problems with answer-set programming, in: Proc. of AAAI, 2017, pp. 1077–1083.

20.

Brewka,

Ellmauthaler,

Strass,

J.P.

Wallner and

Woltran, Abstract Dialectical Frameworks. An overview, The IfCoLog Journal of Logics and Their Applications4(8) (2017), 2263–2318.

21.

Brewka,

Ellmauthaler,

Strass,

J.P.

Wallner and

Woltran, Abstract Dialectical Frameworks, in: Handbook of Formal Argumentation,

Baroni,

Gabbay,

Giacomin and

van der Torre, eds, College Publications, 2018, pp. 237–286, Chapter 5.

22.

Brewka and

Woltran, The ADF project website, http://www.dbai.tuwien.ac.at/research/project/adf/.

23.

Brewka and

Woltran, The GRAPPA project website, http://www.dbai.tuwien.ac.at/proj/grappa/.

24.

Caminada,

Sá,

Alcântara and

Dvorák, On the equivalence between logic programming semantics and argumentation semantics, Int. J. Approx. Reasoning58 (2015), 87–111. doi:10.1016/j.ijar.2014.12.004.

25.

M.W.A.

Caminada and

D.M.

Gabbay, A logical account of formal argumentation, Studia Logica93(2–3) (2009), 109–145. doi:10.1007/s11225-009-9218-x.

26.

J.L.

Carballido,

J.C.

Nieves and

Osorio, Inferring preferred extensions by pstable semantics, Inteligencia Artificial, Revista Iberoamericana de Inteligencia Artificial13(41) (2009), 38–53.

27.

Cayrol,

Dupin de Saint-Cyr Bannay and

M.-C.

Lagasquie-Schiex, Change in abstract argumentation frameworks: Adding an argument, Journal of Artificial Intelligence Research38 (2010), 49–84. doi:10.1613/jair.2965.

28.

Cayrol,

Fandinno,

Fariñas del Cerro and

M.-C.

Lagasquie-Schiex, Valid attacks in argumentation frameworks with recursive attacks, in: Proc. of Thirteenth International Symposium on Commonsense Reasoning, CEUR Workshop Proceedings, Vol. 2052, 2017.

29.

Cayrol,

Fandinno,

Fariñas del Cerro and

M.-C.

Lagasquie-Schiex, Argumentation frameworks with recursive attacks and evidence-based support, in: Proc. of Tenth International Symposium on Foundations of Information and Knowledge Systems (FoIKS),

Ferrarotti and

Woltran, eds, LNCS, Vol. 10833, Springer-Verlag, 2018, pp. 150–169. doi:10.1007/978-3-319-90050-6_9.

30.

Cayrol,

Fariñas del Cerro and

M.-C.

Lagasquie-Schiex, Logical encodings of interactions in an argumentation graph with recursive attacks, Technical report, RR-2017-08-FR, IRIT, 2017.

31.

Cayrol and

M.-C.

Lagasquie-Schiex, Gradual valuation for bipolar argumentation frameworks, in: Proc. of the Eighth European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU),

Godo, ed., LNAI, Vol. 3571, Springer-Verlag, Barcelona, Spain, 2005, pp. 366–377.

32.

Cayrol and

M.-C.

Lagasquie-Schiex, Bipolarity in argumentation graphs: Towards a better understanding, International Journal of Approximate Reasoning54(7) (2013), 876–899. doi:10.1016/j.ijar.2013.03.001.

33.

Cayrol and

M.-C.

Lagasquie-Schiex, Logical encoding of argumentation frameworks with higher-order attacks, in: Proc. of the 30th International Conference on Tools with Artificial Intelligence (ICTAI), IEEE, 2018.

34.

Cayrol and

M.-C.

Lagasquie-Schiex, Acceptability semantics in recursive argumentation frameworks: Logical encoding and computation, Rapport de recherche, IRIT/RR-2018-02-FR, IRIT, Université Paul Sabatier, Toulouse, 2018.

35.

Cayrol and

M.-C.

Lagasquie-Schiex, The Grafix website, http://www.irit.fr/grafix.

36.

Cerutti,

P.E.

Dunne,

Giacomin and

Vallati, Computing preferred extensions in abstract argumentation: A SAT-based approach, in: Theory and Applications of Formal Argumentation, TAFA 2013,

Black,

Modgil and

Oren, eds, LNAI, Vol. 8306, Springer-Verlag, Berlin, Heidelberg, 2013, pp. 176–193. doi:10.1007/978-3-642-54373-9_12.

37.

Cerutti,

Giacomin and

Vallati, ArgSemSAT: Solving argumentation problems using SAT, in: Computational Models of Argument – Proceedings of COMMA, 2014, pp. 455–456.

38.

Cerutti,

Giacomin,

Vallati and

Zanella, An SCC recursive meta-algorithm for computing preferred labellings in abstract argumentation, in: Proc. of KR, 2014, pp. 42–51.

39.

Cerutti,

Vallati and

Giacomin, An efficient Java-based solver for abstract argumentation framework: jArgSemSAT, Int. Journal of Articial Intelligence Tools26(2) (2017), 1–26.

40.

Cerutti,

Vallati,

Giacomin and

Zanetti, ArgSemSAT-2017, 2017.

41.

Cohen,

Gottifredi,

A.J.

García and

G.R.

Simari, A survey of different approaches to support in argumentation systems, The Knowledge Engineering Review29 (2014), 513–550. doi:10.1017/S0269888913000325.

42.

Cohen,

Gottifredi,

A.J.

García and

G.R.

Simari, An approach to abstract argumentation with recursive attack and support, Journal of Applied Logic13(4) (2015), 509–533. doi:10.1016/j.jal.2014.12.001.

43.

Coste-Marquis,

Devred and

Marquis, Constrained argumentation frameworks, in: Proc. of KR, Lake District, 2006, pp. 112–122.

44.

Coste-Marquis,

Konieczny,

J.-G.

Mailly and

Marquis, On the revision of argumentation systems: Minimal change of argument statuses, in: International Conference on Principles of Knowledge Representation and Reasoning (KR),

Baral and

De Giacomo, eds, AAAI Press, 2014, pp. 72–81.

45.

Coste-Marquis,

Konieczny,

J.-G.

Mailly and

Marquis, A translation-based approach for revision of argumentation frameworks, in: Logics in Artificial Intelligence, Springer, 2014, pp. 397–411. doi:10.1007/978-3-319-11558-0_28.

46.

Devred,

Doutre,

Lefèvre and

Nicolas, Dialectical proofs for constrained argumentation, in: Computational Models of Argument – Proceedings of COMMA, 2010, pp. 159–170.

47.

Diller,

Dvorak,

Puhrer,

Wallner and

Woltran, Applications of ASP in formal argumentation, in: Proc. of TAASP Workshop, 2018.

48.

Diller,

Haret,

Linsbichler,

Rümmele and

Woltran, An extension-based approach to belief revision in abstract argumentation, in: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015), 2015, pp. 2926–2932.

49.

Diller,

Wallner and

Woltran, Reasoning in Abstract Dialectical Frameworks using quantified Boolean formulas, Argument & Computation6(2) (2015), 149–177. doi:10.1080/19462166.2015.1036922.

50.

Diller,

J.P.

Wallner and

Woltran, Reasoning in Abstract Dialectical Frameworks using quantified Boolean formulas, in: Proceedings of the 5th Conference on Computational Models of Argument (COMMA’2014),

Parsons,

Oren,

Reed and

Cerutti, eds, Frontiers in Artificial Intelligence and Applications, Vol. 266, Pitlochry, Scottish Highlands, UK, 2014, pp. 241–252, Held in Atholl Palace Hotel.

51.

Dimopoulos,

J.-G.

Mailly and

Moraitis, Control argumentation frameworks, in: Proc. of AAAI, 2018, pp. 4678–4685.

52.

Doutre,

Herzig and

Perrussel, A dynamic logic framework for abstract argumentation, in: Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR’2014),

Baral,

De Giacomo and

Eiter, eds, AAAI Press, Vienna, Austria, 2014.

53.

Doutre and

J.-G.

Mailly, Constraints and changes a survey of abstract argumentation dynamics, Argument & Computation9(3) (2018), 223–248. doi:10.3233/AAC-180425.

54.

P.M.

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

55.

Dupin de Saint-Cyr,

Bisquert,

Cayrol and

Lagasquie-Schiex, Argumentation update in YALLA (Yet Another Logic Language for Argumentation), Int. J. Approx. Reasoning75 (2016), 57–92. doi:10.1016/j.ijar.2016.04.003.

56.

Dvořák,

Gaggl,

Linsbichler and

Wallner, Reduction-based approaches to implement Modgil’s extended argumentation frameworks, in: Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation – Essays Dedicated to Gerhard Brewka on the Occasion of His 60th Birthday,

Eiter,

Strass,

Truszczynski and

Woltran, eds, Lecture Notes in Computer Science, Vol. 9060, Springer, 2015, pp. 249–264. doi:10.1007/978-3-319-14726-0_17.

57.

Dvořák,

S.A.

Gaggl and

Woltran, The ASPARTIX website, https://www.dbai.tuwien.ac.at/research/argumentation/aspartix/.

58.

Dvorak,

Järvisalo,

Wallner and

Woltran, Complexity-sensitive decision procedures for abstract argumentation, Artificial Intelligence206 (2014), 53–78. doi:10.1016/j.artint.2013.10.001.

59.

Dvořák,

Järvisalo,

J.P.

Wallner and

Woltran, CEGARTIX: A SAT-based argumentation system, in: Proc. of Pragmatics of SAT, Workshop of SAT Conference, 2012.

60.

Dvořák,

Järvisalo,

J.P.

Wallner and

Woltran, The CEGARTIX website, https://www.dbai.tuwien.ac.at/proj/argumentation/cegartix/.

61.

Egly,

S.A.

Gaggl and

Woltran, Answer-set programming encodings for argumentation frameworks, Argument & Computation1(2) (2010), 147–177. doi:10.1080/19462166.2010.486479.

62.

Faber,

Vallati,

Cerutti and

Giacomin, Enumerating preferred extensions using ASP domain heuristics: The ASPrMin solver, in: Proc. of COMMA, 2018, pp. 459–460.

63.

Fandinno and

Fariñas del Cerro, Constructive logic covers argumentation and logic programming, in: Proc. of Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018),

F.T.M.

Thielscher and

Wolter, eds, AAAI Press, 2018, pp. 128–137.

64.

D.M.

Gabbay, Fibring argumentation frames, Studia Logica93 (2009), 231–295. doi:10.1007/s11225-009-9217-y.

65.

D.M.

Gabbay, Semantics for higher level attacks in extended argumentation frames part 1: Overview, Studia Logica93(2–3) (2009), 357–381. doi:10.1007/s11225-009-9211-4.

66.

D.M.

Gabbay, Meta-Logical Investigations in Argumentation Networks, Studies in Logic, Vol. 44, College Publications, 2013.

67.

D.M.

Gabbay and

Gabbay, The attack as strong negation, part I, Logic Journal of the IGPL23(6) (2015), 881–941. doi:10.1093/jigpal/jzv033.

68.

D.M.

Gabbay and

Gabbay, The attack as intuitionistic negation, Logic Journal of the IGPL24(5) (2016), 807–837. doi:10.1093/jigpal/jzw012.

69.

S.A.

Gaggl, Towards a general argumentation system based on answer-set programming, in: Technical Communications of the 26th International Conference on Logic Programming (ICLP 2010),

M.V.

Hermenegildo and

Schaub, eds, LIPIcs, Vol. 7, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2010, pp. 265–269.

70.

Grossi, On the logic of argumentation theory, in: Proc. of AAMAS, 2010, pp. 409–416.

71.

Karacapilidis and

Papadias, Computer supported argumentation and collaborative decision making: The Hermes system, Information Systems26(4) (2001), 259–277. doi:10.1016/S0306-4379(01)00020-5.

72.

Lagniez,

Lonca and

Mailly, CoQuiAAS: A constraint-based quick abstract argumentation solver, in: 27th IEEE International Conference on Tools with Artificial Intelligence, ICTAI, 2015, pp. 928–935.

73.

Lefèvre and

Nicolas, The ASPeRiX website, http://www.info.univ-angers.fr/pub/claire/asperix/Argumentation/.

74.

Lehtonen,

Niskanen and

Järvisalo, SAT-based approaches to adjusting, repairing, and computing largest extensions of argumentation frameworks, in: Computational Models of Argument – Proceedings of COMMA, 2018, pp. 193–204.

75.

Linsbichler,

Maratea,

Niskanen,

Wallner and

Woltran, Novel algorithms for Abstract Dialectical Frameworks based on complexity analysis of subclasses and SAT solving, in: Proc. of IJCAI, 2018, pp. 1905–1911.

76.

Modgil, Reasoning about preferences in argumentation frameworks, Artificial Intelligence173 (2009), 901–934. doi:10.1016/j.artint.2009.02.001.

77.

Niskanen and

Järvisal, μ-toksia. Participating in ICCMA 2019, 2019.

78.

Nouioua, AFs with necessities: Further semantics and labelling characterization, in: Proc. of the International Conference on Scalable Uncertainty Management (SUM), 2013, pp. 120–133. doi:10.1007/978-3-642-40381-1_10.

79.

Nouioua and

Risch, Bipolar argumentation frameworks with specialized supports, in: Proc. of the IEEE International Conference on Tools with Artificial Intelligence (ICTAI), IEEE Computer Society, 2010, pp. 215–218.

80.

Nouioua and

Risch, Argumentation frameworks with necessities, in: Proc. of the International Conference on Scalable Uncertainty Management (SUM), Springer-Verlag, 2011, pp. 163–176. doi:10.1007/978-3-642-23963-2_14.

81.

Oren and

T.J.

Norman, Semantics for evidence-based argumentation, in: Proc of the 2nd International Conference on Computational Models of Argument (COMMA),

Besnard,

Doutre and

Hunter, eds, IOS Press, 2008, pp. 276–284.

82.

Oren,

Reed and

Luck, Moving between argumentation frameworks, in: Proceeding of the Conference on Computational Models of Argument (COMMA), IOS Press, Amsterdam, The Netherlands, 2010, pp. 379–390.

83.

Osorio and

J.C.

Nieves, Range-based argumentation semantics as two-valued models, TPLP17(1) (2017), 75–90.

84.

Osorio,

J.C.

Nieves and

Santoyo, Complete extensions as Clark’s completion semantics, in: Mexican International Conference on Computer Science, ENC 2013, Morelia, Michoacán, Mexico, October 30–Nov. 1, 2013, 2013, pp. 81–88.

85.

Polberg, Understanding the abstract dialectical framework, in: Proc. of JELIA, 2016, pp. 430–446.

86.

Polberg, Intertranslatability of abstract argumentation frameworks, Technical report, DBAI-TR-2017-104, DBAI (Institut für Informationssysteme Abteilung Datenbanken und Artificial Intelligence Technische Universität Wien), 2017.

87.

Polberg and

Oren, Revisiting support in abstract argumentation systems, Technical report, TU Wien, Institut for Informatics, 2014.

88.

Pu,

Luo and

Jiang, Encoding argumentation semantics by Boolean algebra, IEICE Transactions100D(4) (2017), 838–848. doi:10.1587/transinf.2016EDP7313.

89.

Sakama and

Rienstra, Representing argumentation frameworks in answer set programming, Fundamenta Informaticae155(3) (2017), 261–292. doi:10.3233/FI-2017-1585.

90.

Toni and

Sergot, Argumentation and answer set programming, in: Logic Programming, Knowledge Representation and Nonmonotonic Reasoning: Essays in Honor of Michael Gelfond,

Balduccini and

T.C.

Son, eds, Springer, 2010, pp. 164–180.

91.

Verheij, DEFLOG: On the logical interpretation of prima facie justified assumptions, Journal of Logic in Computation13 (2003), 319–346. doi:10.1093/logcom/13.3.319.

92.

Villata,

Boella,

D.M.

Gabbay and

van der Torre, Modelling defeasible and prioritized support in bipolar argumentation, Annals of Mathematics and Artificial Intelligence66(1–4) (2012), 163–197. doi:10.1007/s10472-012-9317-7.

93.

Villata,

Boella,

D.M.

Gabbay,

van der Torre and

Hulstijn, A logic of argumentation for specification and verification of abstract argumentation frameworks, Annals of Mathematics and Artificial Intelligence66(1–4) (2012), 199–230. doi:10.1007/s10472-012-9318-6.

94.

Walicki and

Dyrkolbotn, Finding kernels or solving SAT, Discrete Algorithms10 (2012), 146–164. doi:10.1016/j.jda.2011.11.004.

95.

J.P.

Wallner,

Weissenbacher and

Woltran, Advanced SAT techniques for abstract argumentation, in: Computational Logic in Multi-Agent Systems – 14th International Workshop, CLIMA XIV, Proceedings, Corunna, Spain, September 16–18, 2013, 2013, pp. 138–154.

96.

Wu,

Caminada and

D.M.

Gabbay, Complete extensions in argumentation coincide with 3-valued stable models in logic programming, Studia Logica: An International Journal for Symbolic Logic93(2/3) (2009), 383–403. doi:10.1007/s11225-009-9210-5.

in ADF	Sufficient condition of $φ_{b} = a$	Necessary condition of $φ_{b} = a$	Sufficient condition of $φ_{a} = b$	Necessary condition of $φ_{a} = b$
in BAF	Deductive meaning of $(a, b)$	Necessary meaning of $(a, b)$	Necessary meaning of $(a, b)$	Deductive meaning of $(a, b)$

$a_{0}$	Mr. X is not guilty of premeditated murder of Mrs. X, his wife.
$a_{1}$	Mr. X is guilty of premeditated murder of Mrs. X.
$a_{2}$	The defendant has an alibi, his business associate has solemnly sworn that he met him at the time of the murder.
$a_{3}$	The close working business relationships between Mr. X and his associate induce suspicions about his testimony.
$a_{4}$	Mr. X loves his wife so deeply that he asked her to marry him twice. A man who loves his wife cannot be her killer.
$a_{5}$	Mr. X has a reputation for being promiscuous.
$a_{6}$	The defendant had no interest to kill his wife, since he was not the beneficiary of the huge life insurance she contracted.
$a_{7}$	The defendant is a man known to be venal and his “love” for a very rich woman could be only lure of profit.

Logical theories and abstract argumentation: A survey of existing works

Abstract

Keywords

1. Introduction

1 For instance, an encoding of logic programs under the form of argumentation frameworks, or the creation of an argumentation framework using logical knowledge bases (see for instance, papers as [14]).

2.1. Argumentation frameworks

Def. 1 (AF [54]).

4 Generally assumed to be finite.

Def. 4 (RAF [28]).

Def. 5 (Extension-based semantics [54]).

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

Def. 7 (Labelling-based semantics [6]).

Prop. 1 (Characterizing complete labellings).

3. ADF (Abstract Dialectical Frameworks)

8 In ADF, this condition is generally a propositional formula, but there also exist some works on ADF that specify acceptance conditions as Boolean functions that may be represented in different ways. In this survey, we only consider the case where acceptance conditions are propositional formulae.

Def. 10 (Three-valued operator).

Def. 11 (Preordering ⩽ t on two-valued interpretations).

Def. 12 (Preordering ⩽ i on three-valued interpretations).

10 The definition for the stable models is not given here but can be found in [21] (a model being an interpretation v such that ∀ s ∈ S , v ( s ) = v ( φ s ) ).

13 This list is not exhaustive. For instance, the reader can also refer to YADF [19] or to k++ADF [75].

4.1. The syntactic sugar way

15 See also Section 6. In the YALLA language, a specific predicate has been introduced for encoding an attack between sets of arguments: x ⊳ y .

4.3. The approach by Gabbay and Gabbay

16 If y is unattacked then this formula is equivalent to y ↔ ⊤ as the conjunction of an empty set of formulae is always true.

5. QBF-formalization of AF

21 The quantification ensures ranging over all interpretations: conjunction over all a ∈ A fails to bind other propositional atoms that presumably occur in φ a .

6. Dedicated languages for abstract argumentation

6.1. YALLA (Yet Another Logic Language for Argumentation)

6.1.1. Main definitions

Def. 19 (Structure).

Def. 20 (Formula describing an AF).

23 When t denotes a term of YALLA U , t is identified with the subset of A U which interprets t. It is the case for { x } for instance.

6.2. The approach by Villata et al.

7. Encoding of extension-based semantics

7.1. The approach by Besnard and Doutre

7.1.1. Description of the approach

7.1.2. Some implementations

7.2. The CEGARTIX approach

8. Encoding of labelling-based semantics

25 Various definitions have been recalled in Section 2 and Section 5.

26 An example of the use of circumscription in order to solve AF reasoning problems is described in [1].

8.3. Some implementations

9. Argumentation frameworks and logic programming

9.1. From an AF to a logic program

9.2.1. AFNs and logic programs

9.3. Some implementations

10. Argumentation frameworks and modal logic

10.1. Modal logic preliminaries

10.2. The approach by Grossi

28 That is, the codomain of I is the powerset of A .

10.4. The modal setting of Villata et al.

10.5. The object-level approach of Caminada and Gabbay

11. Translation of an AF into intuitionistic logic

11.1. Background about intuitionistic logic

11.2. Abstract argumentation and intuitionistic logic

12. Analysis and conclusion

12.1. Comparison criteria

30 The other direction could be the object of another survey that would cover the relationship between logical frameworks and formal argumentation, including structured argumentation.

Footnotes

Acknowledgements

References

¹
For instance, an encoding of logic programs under the form of argumentation frameworks, or the creation of an argumentation framework using logical knowledge bases (see for instance, papers as [14]).

⁴
Generally assumed to be finite.

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

Def. 11 (Preordering $⩽_{t}$ on two-valued interpretations).

Def. 12 (Preordering $⩽_{i}$ on three-valued interpretations).

¹⁰
The definition for the stable models is not given here but can be found in [21] (a model being an interpretation v such that $\forall s \in S$ , $v (s) = v (φ_{s})$ ).

¹³
This list is not exhaustive. For instance, the reader can also refer to YADF [19] or to k++ADF [75].

¹⁵
See also Section 6. In the YALLA language, a specific predicate has been introduced for encoding an attack between sets of arguments: $x ⊳ y$ .

¹⁶
If y is unattacked then this formula is equivalent to $y \leftrightarrow ⊤$ as the conjunction of an empty set of formulae is always true.

²¹
The quantification ensures ranging over all interpretations: conjunction over all $a \in A$ fails to bind other propositional atoms that presumably occur in $φ_{a}$ .

²³
When t denotes a term of ${YALLA}_{U}$ , t is identified with the subset of $A_{U}$ which interprets t. It is the case for ${x}$ for instance.

²⁵
Various definitions have been recalled in Section 2 and Section 5.

²⁶
An example of the use of circumscription in order to solve AF reasoning problems is described in [1].

²⁸
That is, the codomain of I is the powerset of $A$ .

³⁰
The other direction could be the object of another survey that would cover the relationship between logical frameworks and formal argumentation, including structured argumentation.