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.
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 . 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 , 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  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 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
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?
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 ), 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 ,3 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 . 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 , 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 : 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].
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
According to , an abstract argumentation framework consists of a set of arguments together with a binary relation between arguments.
Def. 1(AF ).
An argumentation framework (AF) is a pair where is a set4 of abstract arguments and is a binary relation on , called the attack relation: 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 with vertices as arguments and edges as attacks.
The AF defined by and 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 , the support relation is left general so that the bipolar framework keeps a high level of abstraction.
Def. 2(BAF ).
A bipolar argumentation framework (BAF) is a triple where is a set of abstract arguments, (resp. ) is a binary relation on , 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).
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 , necessary support [79,80], evidential support [81,82]). These proposals have been developed quite independently, based on different intuitions and with different formalizations. In , is presented a comparative study in order to restate these proposals in a common setting, the bipolar argumentation framework (see also  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 :6
An Evidence-Based Argumentation Framework (EBAF) is a 4-tuple where is a set of arguments, is the attack relation, is the support relation, and 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  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 ), or for modelling situations where an attack might be defeated by an argument, without contesting the acceptability of the source of the attack . Attacks to attacks and supports have been first considered in  with higher level networks, then in ; and more generally, in  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 ).
A recursive argumentation framework (RAF) is a tuple where is a finite and non-empty set of arguments, is a finite set disjunct from representing attack names, s is a function from to mapping each interaction to its source, and t is a function from to mapping each interaction to its target.
Note that an AF can be viewed as a particular RAF with t being a mapping from to .
A RAF can also be represented graphically.
The RAF in which an attack named α (with and ) being the target of an attack β (with ) 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.
Case of AF. Acceptability semantics can be defined in terms of extensions  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 ).
Given and .
S is conflict-free iff for all .
is acceptable w.r.t. S (or equivalently S defends a) iff for each with , there is with .
The characteristic function of is defined by: .
S is admissible iff S is conflict-free and .
S is a complete extension of iff it is conflict-free and a fixed point of .
S is the grounded extension of iff it is the minimal (w.r.t. ⊆) fixed point7 of .
S is a preferred extension of iff it is a maximal (w.r.t. ⊆) complete extension.
S is a stable extension of iff it is conflict-free and for each , there is with .
Note that the complete (resp. grounded, preferred, stable) semantics satisfies the conflict-freeness, defence and reinstatement principles.
2.1.1 (cont’d) In this example, the set is the grounded, complete, preferred and stable extension.
Acceptability semantics can also be defined in terms of labellings, as in , for instance.
Def. 6(Labelling ).
Let be an AF. A labelling for is a total function .
Let be a labelling of .
An -labelled argument is said to be legally iff all its attackers are labelled .
An -labelled argument is said to be legally iff at least one of its attackers is labelled .
An -labelled argument is said to be legally iff it doesn’t have an attacker that is labelled and not all its attackers are labelled .
Standard labelling-based semantics are defined as follows:
Def. 7(Labelling-based semantics ).
Let be a labelling for .
is an admissible labelling iff each -labelled argument is legally and each -labelled argument is legally .
is a complete labelling iff each -labelled argument is legally , each -labelled argument is legally , and each -labelled argument is legally .
is the grounded labelling iff it is the complete labelling that minimizes (w.r.t. ⊆) the set of -labelled arguments.
is a preferred labelling iff it is a complete labelling of that maximizes (w.r.t. ⊆) the set of -labelled arguments.
is a stable labelling iff it is a complete labelling with no -labelled argument.
Alternative characterizations of complete labellings can be found in . 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 .
(1) is a complete labelling iff for each argument a, it holds that:
If a is -labelled, then all its attackers are -labelled
If a is -labelled, then it has at least one attacker that is -labelled
If a is -labelled, then it has at least one attacker that is not -labelled and it does not have an attacker that is -labelled
(2) is a complete labelling iff for each argument a, it holds that:
a is -labelled iff all its attackers are -labelled
a is -labelled iff it has at least one attacker that is -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 ). In recent works (see for instance ), 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 .
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 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.
An ADF is a directed graph defined as follows:
An abstract dialectical framework (ADF) is a tuple where S is a finite set of nodes, is a set of links, and is a set of propositional formulae (acceptance conditions). Each is built over the set (i.e. 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
Second, let s be an argument, let be the set of the parents of s in the dependence graph, let be the acceptance condition associated with s and consider . denotes the truth value of using the truth value of the elements of R. Then is used for determining the status of s: if (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: .
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 be an ADF. The two-valued operator takes a two-valued interpretation v of each argument and returns a two-valued interpretation mapping each argument s to the truth value that is obtained by evaluating its acceptance condition with v.
Thus, for v a two-valued interpretation, where for , .
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 be an ADF. The three-valued operator takes a three-valued interpretation v of each argument and returns a three-valued interpretation 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 on two-valued interpretations).
Let be an ADF. Let and be two-valued interpretations. if and only if , .
Def. 12(Preordering on three-valued interpretations).
Let be an ADF. Let and be three-valued interpretations. if and only if , .
Some semantics can be defined as follows:10
Let be an ADF. Let v be a three-valued interpretation.
v is complete for D iff .
v is admissible for D iff .
v is preferred for D iff v is -maximal admissible.
v is grounded for D iff v is the -least fixed point of .
Note that the well-known relationships between AF semantics also hold for ADF semantics:
Let 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
Case of AF: Let be an AF, its associated ADF is defined by the pair with . 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).Example 3.2.6 given in the next section illustrates the above ideas.
∗ 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).
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  for translating an AFRA into an AF). See Ex. 2.1.3 in the next section.
The previous ADF definitions are illustrated on the following examples (most of them are issued from ).
Consider the ADF represented by:
Intuitively, states that a should be accepted. Condition expresses a kind of self-support for b. says that c will be accepted if both a and b are accepted whereas 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 (nodes = interpretations and edges = the relation between two interpretations defined by the operator).
Consider for instance . For each acceptance condition, it can be seen how the operator produces the updated interpretation :
: so (v has no impact since a has no parent in the ADF);
: so (v has an impact since b is its own parent);
: so (v has an impact since a and b are the parents of c);
: so (v has an impact since b is the parent of d).
So, the operator applied to produces the interpretation .
Consider now and, using the same way, compute the interpretation . It is easy to see that is exactly . So is a fixed point for the operator . 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 , see Fig. 4 (given at the end of this paper). Note that the set of two-valued interpretations over 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 ( three-valued interpretations), we do not represent the preordering and the corresponding complete meet-lattice in a figure. Nevertheless, some interesting three-valued interpretations can be identified:
that is also a two-valued interpretation and a fixed point of (so a two-valued model),
that is also a two-valued interpretation and a fixed point of (so a two-valued model),
The next example illustrates the three-valued operator and the preordering.
Consider the ADF represented by:
Figure 5 (given at the end of this paper) represents the evolution of interpretations by the three-valued operator for the ADF (nodes = interpretations and edges = the relation between two interpretations defined by the operator).
First, consider . The two possible two-valued interpretations that extend v are: and . Consider now each acceptance condition and let us see how the operator produces the updated interpretation :
∗ : so ( has no impact since a has no parent in the ADF);
∗ : so ( has an impact since b as three parents – a, b and c –);
∗ : so ( has an impact since c as two parents – a and b –);
∗ : so ( has no impact since a has no parent in the ADF);
∗ : so ( has an impact since b as three parents – a, b and c –);
∗ : so ( has an impact since c as two parents – a and b –);
Another example of this process can be given with the interpretation . The two possible two-valued interpretations that extend are: and .
With , we obtain , and .
With , we obtain , , .
Then, using and , the consensus truth value for each argument is , , . This three-valued interpretation is one of the three fixed points of this example.
In this example, the preordering is given by Fig. 6 (given at the end of this paper). Note that the set of three-valued interpretations over 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:
(that is also a two-valued model),
(that is also a two-valued model).
, and are complete (they are the only fixed points of ), and are preferred and is grounded.
The following examples illustrate the use of ADF as a modelling tool.
The sequence of two attacks can be translated into the following ADF:
Applying the or the operators gives only one fixed point: . That corresponds to the complete, preferred and grounded extension.
Two attacks to the same argument can be translated into the following ADF:
An even-length cycle of attacks can be translated into the following ADF:
Applying the operator gives three fixed points: , and . That corresponds to the complete extensions, being the grounded one and , being the preferred ones.
The following graph represents a weighted AF.
Considering that the set 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:
2.1.2 (cont’d) Consider a BAF with only one support from a to b. Following , 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 and . So, in this case, 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):
With the proposed encoding, the sufficient condition given by encodes exactly the deductive meaning of the support but the necessary condition issued from 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):
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 and ). 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 :
|in ADF||Sufficient condition of||Necessary condition of||Sufficient condition of||Necessary condition of|
|in BAF||Deductive meaning of||Necessary meaning of||Necessary meaning of||Deductive meaning of|
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.
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 ):
This AF can be in turn represented by the following ADF:
(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).
is a system for solving reasoning problems on ADF using Quantified Boolean Formulae (QBF).14 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.
(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 . Optionally, the output can be converted into the format readable by ASPARTIX (see Section 9.3) or DIAMOND.
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.
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 . 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  is a standard argumentation graph (links encode attacks) and not a dependence graph,
there is a unique acceptance condition in  and not one attached to each argument,
In  are defined new semantics by combining standard semantics with the satisfaction of the acceptance condition.
The following example illustrates this approach.
Consider the CAF built with the following AF and the propositional formula :
There are 2 preferred extensions and 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 ( in , in 15). These special atoms are considered as always true.
The description needs not include propositional atoms of the form (or the like) that would explicitly list the nodes of the argumentation graph.
4.2.The approach by Cayrol et al.
In the case of an AF, the atoms are of the form and . For a node a of the argumentation graph, expresses the status of being accepted, whereas expresses that a cannot be accepted (implicitly: with regard to a given argumentation semantics). Note that the meaning of is stronger than “a is not accepted”.
The theory generated by  consists of the following axioms:
For every in the input AF
For every argument b in the input AF
Such formulae express (by transitivity of material implication) conflict-freeness of extension-based semantics: whenever . Such formulae also express that if an argument cannot be accepted then it is not accepted: , or, equivalently, .
In the case of RAFs, the authors use a two-sorted logic with equality. There are a sort for arguments and a sort for attacks. In addition to and as above, the language also admits atoms of the form for attack names in the input RAF (intuitively, 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 to capture source and target of the attack. The target can be either of sort or of sort and the source can only be of sort (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:
Of course, the generated theory includes RAF-dependent axioms (assuming the arguments of the input RAF are and the attack names are ) as follows:
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 , for every AF, a theory is generated with the axiom:
Similarly, a conflict-freeness axiom is needed:
The theory generated by  consists of four kinds of formulae:
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:
The corresponding stability axiom given in  is:
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 ) together with an extension-based semantics. The output is a quantified Boolean formula (QBF)18 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 and ). 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 and to be false). A general constraint rules out the possibility for and 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 .
Let us recall that a labelling for an AF , is a total function : . We consider complete labellings, characterized by the following conditions (see Section 2.2):
For each argument a,
If a is -labelled, then all its attackers are -labelled;
If a is -labelled, then it has at least one attacker that is -labelled;
If a is -labelled, then it has at least one attacker that is not -labelled and it does not have an attacker that is -labelled.
The assignments of truth values to (name of) nodes are captured syntactically, that is, through formulae. This is done as follows:
For an unsigned atom a and unsigned formulae ϕ, ψ, define the following signed formulae:
The encoding then expands to
For an unsigned formula ϕ:
The main definition is:19
Let and . Define
The role of 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 is:
Also, stable extensions can be captured:
Quantified Boolean formulae enter the picture as minimization or maximization is required. For an AF such that , an example is:
This formula can be read as follows. Considering a current labelling for the n arguments in , look at all labellings so that if one of them satisfies and is smaller than the current labelling (this is what expresses) then the current labelling must be in fact the same as this labelling. In other words, any model of this formula and of defines a minimal complete extension, so that (according to well-known results in abstract argumentation) it defines the grounded extension.
5.3.A QBF approach for ADF
This approach also uses a signed language, with the same atoms as given in Def. 14, namely and for every (interestingly, the notation for these atoms is the same in both approaches).
The same constraint (see above) ruling out a contradictory assignment of truth values is enforced, i.e., for every :
The main difference with the approach due to Arieli and Caminada is that the existence of the acceptance condition in ADF is addressed by Boolean quantification, even prior to any minimization/maximization:21
This formula expresses that the current labelling is admissible. It can then be used to obtain a formula for complete labellings, again using Boolean quantification. In turn, Boolean quantification over can be used to obtain, e.g., a formula characterizing the grounded extension.
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 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, 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).
 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 . For instance, if the domain is a knowledge base then and are the set of all arguments and interactions that may be built from the formulae of the base. In the following example issued from , it is assumed that and are explicitly provided:
During a trial concerning a defendant (Mr. X), several arguments can be involved to determine his guilt. The set of arguments and the graphical representation of the relation are given below.
|Mr. X is not guilty of premeditated murder of Mrs. X, his wife.|
|Mr. X is guilty of premeditated murder of Mrs. X.|
|The defendant has an alibi, his business associate has solemnly sworn that he met him at the time of the murder.|
|The close working business relationships between Mr. X and his associate induce suspicions about his testimony.|
|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.|
|Mr. X has a reputation for being promiscuous.|
|The defendant had no interest to kill his wife, since he was not the beneficiary of the huge life insurance she contracted.|
|The defendant is a man known to be venal and his “love” for a very rich woman could be only lure of profit.|
In , an AF is defined w.r.t. to a given universe , so the definition differs slightly from the definition of  in the sense that arguments and interactions must be built according to the universe.
An AF on is a pair where
An example of AF on the universe described in Ex. 6.1.1 could be:
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 ():
 has proposed a first-order logical theory capable of describing abstract AFs built on a given finite universe , where with k being the cardinal of . The signature of the associated language is defined as follows:22
where the set of constants with , the set of functions and the set of predicates .
As the logical theory has been built for describing AFs on a given universe, terms and formulae of the language will be interpreted on AFs built on this universe. Formally, the semantics of is defined thanks to a structure over , on which terms and formulae will be interpreted. So a structure is associated with an AF built on the universe and its domain is , which is not empty.
A structure over the signature , associated with , is a pair where is the domain of the structure and is an interpretation function associating:
(1) a unique element of to each constant symbol (in particular the empty set is associated with the constant symbol ),
(2) the binary set theoretic union operator (function from to ) to the function symbol ,
(3) the characterization of the subsets of to the predicate symbol : if and only if ,
(4) the binary set theoretic inclusion relation (binary relation on ) to the predicate symbol ⊆,
(5) the binary relation of attack between sets of arguments induced by , and defined by if and only if , and , , such that , to the predicate symbol ⊳.
Among the formulae that can be built on the signature , we find the specific axioms of the theory, that will allow to describe AFs on the universe:
Let x, y, z be variables of ,
Axioms for set inclusion
Axioms for set operators
Axioms combining set operators and attack relation
Axioms for the predicate
An AF belonging to can be described by its characteristic formula in the language .
Def. 20(Formula describing an AF).
Let the function be defined as follows:
is called the characteristic formula of .23
Note that determines the unique structure (Def. 19) which is a model of .
Some additional notations are used for encoding the argumentation semantics: let and be terms of ,
Then the principles used in argumentation semantics can be encoded in terms of formulae:
Let be a set of arguments and be an AF such that and . Let t, , , be terms of .
t is conflict-free in if and only if . The latter formula is denoted by .
defends each element of in if and only if . The latter formula is denoted by .
t is admissible in if and only if . The latter formula is denoted by .
t is a complete extension of if and only if . The latter formula is denoted by .
t is the grounded extension of if and only if . The latter formula is denoted by .
t is a stable extension of if and only if . The latter formula is denoted by .
t is a preferred extension of if and only if . The latter formula is denoted by .
Due to the finite size of a universe, each formula can be viewed as a propositional formula and the satisfiability problem of a base is a NP-complete problem.
In  is used for expressing update in argumentation dynamics. For instance, in the case of a debate, classical update amounts to consider a formula φ in 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 be a set of authorized transitions, an update operator is a mapping from to which associates with any formula φ and any formula α a formula, denoted by satisfying . In , 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].
Let be the formula and be the formula .
We have , , . However is not a model of , as is not a subset of .
More complex assertions can be expressed in , such as, for instance, the fact that b does not belong to the grounded extension of :
also enables the expression of incomplete knowledge held by an agent about AFs built on the universe, as shown by the following example:
6.1.1 (cont’d) Let us consider the universe given in the trial example. Assume that Agent has only a partial knowledge about the AF built by Agent . Indeed, hesitates between two possible situations for ’s AF, namely and given in Fig. 2. So Agent has a doubt about the existence of and of the attacks from to and from to .
The knowledge held by can be expressed by the following formula:
φ is satisfied by only two structures which correspond to and .
Note that .
6.2.The approach by Villata et al.
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 is interpreted in as “there is an argument in p that attacks an argument in q”, where p, q denote subsets of . There is also a logical connective for defence, which can be defined in terms of the attack connective, as follows:
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 , , or for instance. The formula (resp. , ) is interpreted in as “the set of arguments of denoted by p is conflict-free (resp. admissible, the grounded extension) in ”. 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 idea is as follows. Let σ be an extension-based semantics, be an AF and S be a subset of . A formula 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 .
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 set of propositional symbols is introduced to represent the elements of . For simplicity, the same symbol is used, i.e., a is regarded as a propositional symbol whenever . An argumentative semantics σ can then be mapped to a propositional formula (dependent on a subset S of ) that happens to be satisfiable iff S is a σ-extension of .
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:
General test:. is a σ-extension of iff the formula below is satisfiable:
In the above formula, captures the conditions expressing that S is a σ-extension of .
For example, in the formula enabling to determine whether S is a stable extension of there is:
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 ), 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 , the encoding proposed by Besnard and Doutre in  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 , the encoding proposed by Besnard and Doutre in  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 , the encoding proposed by Besnard and Doutre in  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 , a specific encoding of some extension-based semantics is proposed, using two propositional symbols for each argument (for an argument a, the symbols are and ). For instance, the formula corresponding to the complete semantics is the following one:
For a given ,
As it is said in : “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 ( is true iff either is true or some 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 and ; let us prove that the end of the second line of implies that each argument defended by the conflict-free extension is contained in the extension:
a is defended by the extension is encoded by .
Let us assume that: s.t. , .
By definition of (first part of the second line of ), we have that: s.t. .
From the end of the second line of , we can deduce , that is by definition, .
Moreover, from the first part of the first line of (conflict-free requirement), we have that .
So we obtain .
Models of characterize the complete extensions of in the sense that is true in a model 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 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 , 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 , and .
Intuitively, given an AF denoted by , and a labelling , an interpretation of the language can be obtained: is taken as the domain, the predicate R is interpreted by the attack relation of the AF and is used to get the interpretation of the predicates , and as follows: iff labels a as , iff labels a as ; iff labels a as .
Let us consider the following classical theory denoted by (or Δ for short):
(2) for ,
Any model of the above theory Δ with domain D defines an argumentation framework with , and a complete labelling defined from the elements satisfying the predicates , and .
Then other labellings can be characterized as particular models of Δ. For instance, the grounded labelling is obtained with a model that minimizes , whereas the preferred labellings are obtained with models that maximize . Note that second-order formulae are needed in order to express the concept “ is minimal” or “ is maximal”. That leads to the circumscription technique.26 In short, standard circumscription gives the minimal relation(s) that enjoy a given set of properties (e.g., circumscribing 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 denote the set of axioms describing :
8.2.The approach by Cerutti et al.
In , three propositional symbols are defined for each argument: , and meaning that the value of a in the labelling is respectively , or . 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 , we have for the value :
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:
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  and  can be matched, owing to the equivalence between the alternative definitions of complete labellings provided in  (see Section 2.2).
At least three systems have been developed using the approach proposed in .
In , an algorithm using a SAT solver is proposed for computing the preferred semantics. This algorithm is called PrefSAT.
In , 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 , 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 .
9.Argumentation frameworks and logic programming
The close connection between AF semantics and Logic Programming (LP) semantics goes back to Dung’s work . 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 , 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  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:
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 .
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 ) 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 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 ).
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 . Given an AF , the associated logic program consists of three parts:
The rules describing the attacks in : .
The rules defining acceptability: .
The rules defining defeat:
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 meaning “x cannot belong to an admissible set”. So the logic program P contains rules that define 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 ).
The encoding captures both conflict-freeness and admissibility principles.
The predicate is used. 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 if y attacks x. So, P− defines given the attackers of x.
∗ P+ contains rules of the form if are all the attackers of some y attacker of x. Such a rule defines given the defenders of x against y.
Then, acceptability can be encoded through the predicate , where means “x can be considered as accepted”, with the rule .
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.
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:
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:
Consider the following AF:
The associated logic program is:
3.4.1 (cont’d) The associated logic program is:
The approach of  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
, where are all the attackers of x.
for each y attacker of x.
for each y attacker of x.
, where are all the attackers of x.
The part specific to the grounded semantics contains rules of the form: .
3.2.3 (cont’d) The associated logic program under the grounded semantics is:
The unique stable model is .
3.2.4 (cont’d) The associated logic program under the grounded semantics is:
The unique stable model is .
9.1.1 (cont’d) The associated logic program under the grounded semantics is:
The unique stable model is .
Towards logic programs under 3-valued semantics. Let us consider the approach described in . 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 ).
The logic program contains rules of the form , where 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 ).
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.
3.2.3 (cont’d) The associated logic program is:
3.2.4 (cont’d) The associated logic program is:
9.1.1 (cont’d) The associated logic program is:
3.4.1 (cont’d) The associated logic program is:
Consider the following AF:
The associated logic program is:
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  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 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 contains all the weak atoms , with attacks a, and all the strong atoms , with supports a.
For each support E, there is a rule for each .
There are correspondences between AFN labelling-based semantics and three-valued semantics of the program which is obtained.
Consider the following AFN:
The associated logic program is:
9.2.2.Argumentation frameworks with higher level attacks and logic programs by Gabbay
In  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 is created.
Assume that e is attacked by the arguments through the attacks named . Assume that each is itself attacked by the arguments through the attacks named . Then the following formula is created: .
The above formula must be turned into several clauses in order to get a normal logic program.
Gabbay, in , 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  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  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.
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.
(Answer Set Programming Argumentation Reasoning Tool) supports reasoning in AFs using the ASP formalism (see  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).
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  for the description of the ASP solver ASPeRiX and its application to the credulous acceptance problem in a CAF).
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  (see Section 8.3).
10.Argumentation frameworks and modal logic
As outlined in , 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 .
Models for K have the form where is the set of possible worlds, , and h is the assignment function giving for each atomic proposition q a subset of S.
Satisfaction is defined as follows:
iff for all s such that ,
A holds in iff for all ,
The system K can be axiomatized as follows:
10.2.The approach by Grossi
In  a well-known modal logic (the extension of K with universal modality) is used to formalize basic notions of argumentation theory.
Let . is viewed as a modal frame, where the set of possible worlds is the set of arguments and the accessibility relation is the inverse of the attack relation (intuitively the “being attacked” relation).
An assignment I on is a function from a set of propositional atoms to the subsets of arguments.28 The fact that an argument a belongs to can be interpreted as “argument a has property p”.
An argumentation model has the form where I is an assignment on . As an example of assignment, we find the labellings: A labelling function on can be viewed as an assignment on the propositional symbols (intuitively ).
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”.
whose intuitive reading is “there exists an argument attacking the current one such that”, and
whose intuitive reading is “there exists an argument such that”.
As usual, there are also the dual operators and .
The semantics is as follows: In a given model :
iff there exists s such that s attacks a in and .
iff there exists s such that .
Consider for instance the particular case of a labelling. Let a be an argument. reads “there exists at least one attacker of a labelled ”.
Given an argumentation model , the statement “argument a is attacked by an argument in the set of arguments of that satisfy the property ϕ” can be encoded as . As reads “s belongs to the set of arguments in that satisfy ϕ”, it follows that encodes the statement “argument a is attacked by the set of arguments in that satisfy ϕ”. Similarly, the statement encodes the statement “argument a is defended by the set of arguments in that satisfy ϕ”.
The modal logic that is obtained is an extension of the modal logic K, denoted by . It enables to capture basic principles of argumentation semantics, as for instance:
encodes that 29 is conflict-free.
encodes that is acceptable w.r.t. .
encodes that is stable.
Consider the particular case of a labelling. A labelling is a complete labelling for iff the model satisfies the following formula:
Then model-checking can be used in order to determine whether a given formula is conflict-free, admissible, stable.
Furthermore, Grossi, in , presents a game-theoretic proof procedure based on model-checking games for the logic . In such a game, a proponent tries to prove that holds in a given model 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
Arguments are viewed as possible worlds; so 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 , , .
More precisely, given a labelling on , the associated assignment I is defined as follows:
The modality □ means “being attacked by”, namely iff for all s such that s attacks a in , . As usual, ♢ denotes the dual modality.
Note that the modality □ corresponds to the modality of . However there is no modality corresponding to .
Complete labellings can be characterized with a set of axioms including for instance:
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 is a complete extension iff .
10.4.The modal setting of Villata et al.
The purpose of the work reported in  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 approach of  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: and . The modality means “attacks”, namely iff for all q such that p attacks q in the AF, . is a universal modality (as in ).
As in the propositional variant, primitives of the modal language (such as , ) represent semantics. Moreover, in order to abbreviate formulae, a connective for collective attack is defined as follows: .
The modal logic that is obtained enables to express characterizations such as:
For any pair of sets of arguments such that p attacks q, they cannot be subsets of a conflict-free extension:
The grounded semantics admits a single extension:
10.5.The object-level approach of Caminada and Gabbay
The object-level approach of  can be summarized as follows. Given ,
Arguments are viewed as atomic propositions in the modal provability logic .
The content of is represented by a formula of the logic .
The possible world models of are in one-to-one correspondence with the labellings of .
The modal formula is as follows:
The provability logic has the following axioms and rules:
(1) axioms and rules of modal logic K
11.Translation of an AF into intuitionistic logic
The translation of an AF into an intuitionistic logic theory has been first considered in . The idea is to use intuitionistic negation to model an attack. The intuitionistic models of the obtained theory characterize the complete extensions.
More recently,  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 can be understood as a means to construct a proof of the truth of in terms of a proof of the truth of .
Strong negation can be understood as the existence of a proof of the falsity of ϕ.
Intuitionistic negation is defined as . 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”.
Intuitively, can be understood as a means to construct a proof of the truth of given a proof of the truth of and the fact that there cannot be a proof of its falsity (or in other words given a “consistent” proof of ).
11.2.Abstract argumentation and intuitionistic logic
In , intuitionistic logic is used for translating an AF or an EBAF.
Translation of an AF. The translation presented in  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:
In other words, says that the acceptability of allows to construct a proof of the falsity of , and a proof of the falsity of is identified with being defeated.
Given , the associated theory in constructive logic is:
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 . Recall that the attack relation is a subset of , the support relation is a subset of , and is the set of distinguished prima-facie arguments (see Section 2.1).
Using the notation that denotes “the conjunction of the elements of B”, the associated theory in constructive logic is:
Note that the support from the set of arguments B to an argument b is translated by the formula which says that the acceptability of B enables to construct a proof of the truth of b.
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.
Recall that our initial choice was to identify and to compare approaches that “use logic for doing argumentation”.30
At least four criteria can be used:
(1) 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.
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  Recursive [34,65] Weighted none With preference  With collective interactions [55,63] On a universe  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 : the acceptance condition is used only for removing some extensions Requirements On the AF or the semantics : 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]
(2) 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: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.
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.
(3) 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.
(4) 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 ). Table 4 synthetizes all these implementations.
12.2.An illustrating example
The following example illustrates the different encodings that can be obtained.
2.1.1 (cont’d) The AF is a simple Dung’s framework that has only one complete extension: .
With ADF approach (translation of the AF into a dependence graph):
See Section 3. The AF is encoded by the following dependence formulae:
The language is propositional with the vocabulary . Then, using the ADF machinery (the computation of the fixed points of the operator) a 3-valued model is produced, which corresponds to the complete extension .
Translation of the AF into a logical base:
Several approaches exist, each of them including an encoding of semantics.
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).
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 ).
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  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  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  is lengthy compared to the encoding in modal logic proposed by .
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 : 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.
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 ).
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).
3 YALLA: Yet Another Logic Language for Argumentation.
4 Generally assumed to be finite.
5 We will often use “argumentation graph” in place of “argumentation framework”.
7 It can be proved that the minimal fixed point of is conflict-free.
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.
9 t for true, f for false and u for unknown.
10 The definition for the stable models is not given here but can be found in  (a model being an interpretation v such that , ).
11 Note that the grounded interpretation is unique.
12 Moreover, is also the stable model of the ADF.
14 These formulae are a generalization of the propositional formulae in which both existential quantifiers and universal quantifiers can be applied to each variable.
15 See also Section 6. In the YALLA language, a specific predicate has been introduced for encoding an attack between sets of arguments: .
16 If y is unattacked then this formula is equivalent to as the conjunction of an empty set of formulae is always true.
17 If y is unattacked then the formula is equivalent to ⊥ as the disjunction of an empty set of formulae is always false.
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: .
19 means that .
20 This set of rules is partitioned in 3 subsets: rules for assigning to each argument the value t, then f, then u.
21 The quantification ensures ranging over all interpretations: conjunction over all fails to bind other propositional atoms that presumably occur in .
22 For each function or predicate symbol, the arity is indicated by an exponent attached to the symbol.
23 When t denotes a term of , t is identified with the subset of which interprets t. It is the case for for instance.
24 Note that the absence of an attack is expressed only if this attack is in the universe: is in as c attacks b in U, whereas is not in as b does not attack a in U.
26 An example of the use of circumscription in order to solve AF reasoning problems is described in .
27 Note that the rules with an empty head represent constraints.
28 That is, the codomain of I is the powerset of .
29 denotes the set of arguments in that satisfy ϕ.
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.
31 Without trivial formulae such as, for instance, .
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.
M. Alviano, Argumentation reasoning via circumscription with Pyglaf, Fundamenta Informaticae 167(1–2) (2019), 1–30. doi:10.3233/FI-2019-1808.
L. Amgoud and C. Cayrol, A reasoning model based on the production of acceptable arguments, Annals of Mathematics and Artificial Intelligence 34 (2002), 197–216. doi:10.1023/A:1014490210693.
L. Amgoud, N. Maudet and S. Parsons, Modelling dialogues using argumentation, in: Proc. of ICMAS, 2000, pp. 31–38.
O. Arieli and M. Caminada, A general QBF-based formalization of abstract argumentation theory, in: Proceedings of the 4th Conference on Computational Models of Argument (COMMA’2012), B. Verheij, S. Szeider and S. Woltran, eds, Frontiers in Artificial Intelligence and Applications, Vol. 245, IOS Press, Vienna, Austria, 2012, pp. 105–116.
O. Arieli and M.W.A. Caminada, A QBF-based formalization of abstract argumentation semantics, J. Applied Logic 11(2) (2013), 229–252. doi:10.1016/j.jal.2013.03.009.
P. Baroni, M. Caminada and M. Giacomin, An introduction to argumentation semantics, Knowledge Eng. Review 26(4) (2011), 365–410. doi:10.1017/S0269888911000166.
P. Baroni, F. Cerutti, M. Giacomin and G. Guida, AFRA: Argumentation framework with recursive attacks, International Journal of Approximate Reasoning 52 (2011), 19–37. doi:10.1016/j.ijar.2010.05.004.
H. Barringer, D.M. Gabbay and J. Woods, Temporal dynamics of support and attack networks: From argumentation to zoology, in: Mechanizing Mathematical Reasoning, D. Hutter and W. Stephan, eds, LNAI, Vol. 2605, Springer-Verlag, 2005, pp. 59–98. doi:10.1007/978-3-540-32254-2_5.
C. Beierle, F. Brons and N. 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.
P. Besnard, J. Boudou, S. Doutre, Van Hieu Ho and D. Longin, The SESAME website, https://www.irit.fr/SESAME/.
P. Besnard and S. Doutre, Checking the acceptability of a set of arguments, in: 10th International Workshop on Non-Monotonic Reasoning (NMR’04), J.P. Delgrande and T. Schaub, eds, Whistler, Canada, 2004, pp. 59–64.
P. Besnard, S. Doutre and A. 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, A. Laurent, O. Strauss, B. Bouchon-Meunier and R.R. Yager, eds, Communications in Computer and Information Science, Vol. 443, Springer, http://www.springerlink.com, 2014, pp. 345–354.
P. Besnard, S. Doutre, V.H. Ho and D. 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, M. Thimm, F. Cerutti, H. Strass and M. Vallati, eds, CEUR Workshop Proceedings, Vol. 1672, http://CEUR-WS.org, 2016, pp. 40–51.
P. Besnard and A. Hunter, A logic-based theory of deductive arguments, Artificial Intelligence 128(1–2) (2001), 203–235. doi:10.1016/S0004-3702(01)00071-6.
P. Bisquert, C. Cayrol, F. Dupin de Saint-Cyr Bannay and M.-C. Lagasquie-Schiex, Characterizing change in abstract argumentation systems, in: Trends in Belief Revision and Argumentation Dynamics, E. Fermé, D. Gabbay and G. Simari, eds, Studies in Logic, Vol. 48, College Publications, http://www.collegepublications.co.uk/, 2013, pp. 75–102.
S. Bistarelli, F. Santini, L. Kotthoff, T. Mantadelis and C. Taticchi, Int. competition on computational models of argumentation, 2019, https://www.iccma2019.dmi.unipg.it/.
G. Boella, D.M. Gabbay, L. van der Torre and S. 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.
R. Booth, S. Kaci, T. Rienstra and L. van der Torre, A logical theory about dynamics in abstract argumentation, in: Scalable Uncertainty Management, W. Liu, V.S. Subrahmanian and J. 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.
G. Brewka, M. Diller, G. Heissenberger, T. Linsbichler and S. Woltran, Solving advanced argumentation problems with answer-set programming, in: Proc. of AAAI, 2017, pp. 1077–1083.
G. Brewka, S. Ellmauthaler, H. Strass, J.P. Wallner and S. Woltran, Abstract Dialectical Frameworks. An overview, The IfCoLog Journal of Logics and Their Applications 4(8) (2017), 2263–2318.
G. Brewka, S. Ellmauthaler, H. Strass, J.P. Wallner and S. Woltran, Abstract Dialectical Frameworks, in: Handbook of Formal Argumentation, P. Baroni, D. Gabbay, M. Giacomin and L. van der Torre, eds, College Publications, 2018, pp. 237–286, Chapter 5.
G. Brewka and S. Woltran, The ADF project website, http://www.dbai.tuwien.ac.at/research/project/adf/.
G. Brewka and S. Woltran, The GRAPPA project website, http://www.dbai.tuwien.ac.at/proj/grappa/.
M. Caminada, S. Sá, J. Alcântara and W. Dvorák, On the equivalence between logic programming semantics and argumentation semantics, Int. J. Approx. Reasoning 58 (2015), 87–111. doi:10.1016/j.ijar.2014.12.004.
M.W.A. Caminada and D.M. Gabbay, A logical account of formal argumentation, Studia Logica 93(2–3) (2009), 109–145. doi:10.1007/s11225-009-9218-x.
J.L. Carballido, J.C. Nieves and M. Osorio, Inferring preferred extensions by pstable semantics, Inteligencia Artificial, Revista Iberoamericana de Inteligencia Artificial 13(41) (2009), 38–53.
C. Cayrol, F. Dupin de Saint-Cyr Bannay and M.-C. Lagasquie-Schiex, Change in abstract argumentation frameworks: Adding an argument, Journal of Artificial Intelligence Research 38 (2010), 49–84. doi:10.1613/jair.2965.
C. Cayrol, J. Fandinno, L. 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.
C. Cayrol, J. Fandinno, L. 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), F. Ferrarotti and S. Woltran, eds, LNCS, Vol. 10833, Springer-Verlag, 2018, pp. 150–169. doi:10.1007/978-3-319-90050-6_9.
C. Cayrol, L. 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.
C. 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), L. Godo, ed., LNAI, Vol. 3571, Springer-Verlag, Barcelona, Spain, 2005, pp. 366–377.
C. Cayrol and M.-C. Lagasquie-Schiex, Bipolarity in argumentation graphs: Towards a better understanding, International Journal of Approximate Reasoning 54(7) (2013), 876–899. doi:10.1016/j.ijar.2013.03.001.
C. 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.
C. 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.
C. Cayrol and M.-C. Lagasquie-Schiex, The Grafix website, http://www.irit.fr/grafix.
F. Cerutti, P.E. Dunne, M. Giacomin and M. Vallati, Computing preferred extensions in abstract argumentation: A SAT-based approach, in: Theory and Applications of Formal Argumentation, TAFA 2013, E. Black, S. Modgil and N. Oren, eds, LNAI, Vol. 8306, Springer-Verlag, Berlin, Heidelberg, 2013, pp. 176–193. doi:10.1007/978-3-642-54373-9_12.
F. Cerutti, M. Giacomin and M. Vallati, ArgSemSAT: Solving argumentation problems using SAT, in: Computational Models of Argument – Proceedings of COMMA, 2014, pp. 455–456.
F. Cerutti, M. Giacomin, M. Vallati and M. Zanella, An SCC recursive meta-algorithm for computing preferred labellings in abstract argumentation, in: Proc. of KR, 2014, pp. 42–51.
F. Cerutti, M. Vallati and M. Giacomin, An efficient Java-based solver for abstract argumentation framework: jArgSemSAT, Int. Journal of Articial Intelligence Tools 26(2) (2017), 1–26.
F. Cerutti, M. Vallati, M. Giacomin and T. Zanetti, ArgSemSAT-2017, 2017.
A. Cohen, S. Gottifredi, A.J. García and G.R. Simari, A survey of different approaches to support in argumentation systems, The Knowledge Engineering Review 29 (2014), 513–550. doi:10.1017/S0269888913000325.
A. Cohen, S. Gottifredi, A.J. García and G.R. Simari, An approach to abstract argumentation with recursive attack and support, Journal of Applied Logic 13(4) (2015), 509–533. doi:10.1016/j.jal.2014.12.001.
S. Coste-Marquis, C. Devred and P. Marquis, Constrained argumentation frameworks, in: Proc. of KR, Lake District, 2006, pp. 112–122.
S. Coste-Marquis, S. Konieczny, J.-G. Mailly and P. Marquis, On the revision of argumentation systems: Minimal change of argument statuses, in: International Conference on Principles of Knowledge Representation and Reasoning (KR), C. Baral and G. De Giacomo, eds, AAAI Press, 2014, pp. 72–81.
S. Coste-Marquis, S. Konieczny, J.-G. Mailly and P. 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.
C. Devred, S. Doutre, C. Lefèvre and P. Nicolas, Dialectical proofs for constrained argumentation, in: Computational Models of Argument – Proceedings of COMMA, 2010, pp. 159–170.
M. Diller, W. Dvorak, J. Puhrer, J. Wallner and S. Woltran, Applications of ASP in formal argumentation, in: Proc. of TAASP Workshop, 2018.
M. Diller, A. Haret, T. Linsbichler, S. Rümmele and S. 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.
M. Diller, J. Wallner and S. Woltran, Reasoning in Abstract Dialectical Frameworks using quantified Boolean formulas, Argument & Computation 6(2) (2015), 149–177. doi:10.1080/19462166.2015.1036922.
M. Diller, J.P. Wallner and S. Woltran, Reasoning in Abstract Dialectical Frameworks using quantified Boolean formulas, in: Proceedings of the 5th Conference on Computational Models of Argument (COMMA’2014), S. Parsons, N. Oren, C. Reed and F. Cerutti, eds, Frontiers in Artificial Intelligence and Applications, Vol. 266, Pitlochry, Scottish Highlands, UK, 2014, pp. 241–252, Held in Atholl Palace Hotel.
Y. Dimopoulos, J.-G. Mailly and P. Moraitis, Control argumentation frameworks, in: Proc. of AAAI, 2018, pp. 4678–4685.
S. Doutre, A. Herzig and L. Perrussel, A dynamic logic framework for abstract argumentation, in: Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR’2014), C. Baral, G. De Giacomo and T. Eiter, eds, AAAI Press, Vienna, Austria, 2014.
S. Doutre and J.-G. Mailly, Constraints and changes a survey of abstract argumentation dynamics, Argument & Computation 9(3) (2018), 223–248. doi:10.3233/AAC-180425.
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.
F. Dupin de Saint-Cyr, P. Bisquert, C. Cayrol and M. Lagasquie-Schiex, Argumentation update in YALLA (Yet Another Logic Language for Argumentation), Int. J. Approx. Reasoning 75 (2016), 57–92. doi:10.1016/j.ijar.2016.04.003.
W. Dvořák, S. Gaggl, T. Linsbichler and J. 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, T. Eiter, H. Strass, M. Truszczynski and S. Woltran, eds, Lecture Notes in Computer Science, Vol. 9060, Springer, 2015, pp. 249–264. doi:10.1007/978-3-319-14726-0_17.
W. Dvořák, S.A. Gaggl and S. Woltran, The ASPARTIX website, https://www.dbai.tuwien.ac.at/research/argumentation/aspartix/.
W. Dvorak, M. Järvisalo, J. Wallner and S. Woltran, Complexity-sensitive decision procedures for abstract argumentation, Artificial Intelligence 206 (2014), 53–78. doi:10.1016/j.artint.2013.10.001.
W. Dvořák, M. Järvisalo, J.P. Wallner and S. Woltran, CEGARTIX: A SAT-based argumentation system, in: Proc. of Pragmatics of SAT, Workshop of SAT Conference, 2012.
W. Dvořák, M. Järvisalo, J.P. Wallner and S. Woltran, The CEGARTIX website, https://www.dbai.tuwien.ac.at/proj/argumentation/cegartix/.
U. Egly, S.A. Gaggl and S. Woltran, Answer-set programming encodings for argumentation frameworks, Argument & Computation 1(2) (2010), 147–177. doi:10.1080/19462166.2010.486479.
W. Faber, M. Vallati, F. Cerutti and M. Giacomin, Enumerating preferred extensions using ASP domain heuristics: The ASPrMin solver, in: Proc. of COMMA, 2018, pp. 459–460.
J. Fandinno and L. 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 F. Wolter, eds, AAAI Press, 2018, pp. 128–137.
D.M. Gabbay, Fibring argumentation frames, Studia Logica 93 (2009), 231–295. doi:10.1007/s11225-009-9217-y.
D.M. Gabbay, Semantics for higher level attacks in extended argumentation frames part 1: Overview, Studia Logica 93(2–3) (2009), 357–381. doi:10.1007/s11225-009-9211-4.
D.M. Gabbay, Meta-Logical Investigations in Argumentation Networks, Studies in Logic, Vol. 44, College Publications, 2013.
D.M. Gabbay and M. Gabbay, The attack as strong negation, part I, Logic Journal of the IGPL 23(6) (2015), 881–941. doi:10.1093/jigpal/jzv033.
D.M. Gabbay and M. Gabbay, The attack as intuitionistic negation, Logic Journal of the IGPL 24(5) (2016), 807–837. doi:10.1093/jigpal/jzw012.
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 T. Schaub, eds, LIPIcs, Vol. 7, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2010, pp. 265–269.
D. Grossi, On the logic of argumentation theory, in: Proc. of AAMAS, 2010, pp. 409–416.
N. Karacapilidis and D. Papadias, Computer supported argumentation and collaborative decision making: The Hermes system, Information Systems 26(4) (2001), 259–277. doi:10.1016/S0306-4379(01)00020-5.
J. Lagniez, E. Lonca and J. Mailly, CoQuiAAS: A constraint-based quick abstract argumentation solver, in: 27th IEEE International Conference on Tools with Artificial Intelligence, ICTAI, 2015, pp. 928–935.
C. Lefèvre and P. Nicolas, The ASPeRiX website, http://www.info.univ-angers.fr/pub/claire/asperix/Argumentation/.
T. Lehtonen, A. Niskanen and M. 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.
T. Linsbichler, M. Maratea, A. Niskanen, J. Wallner and S. Woltran, Novel algorithms for Abstract Dialectical Frameworks based on complexity analysis of subclasses and SAT solving, in: Proc. of IJCAI, 2018, pp. 1905–1911.
S. Modgil, Reasoning about preferences in argumentation frameworks, Artificial Intelligence 173 (2009), 901–934. doi:10.1016/j.artint.2009.02.001.
A. Niskanen and M. Järvisal, μ-toksia. Participating in ICCMA 2019, 2019.
F. 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.
F. Nouioua and V. 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.
F. Nouioua and V. 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.
N. Oren and T.J. Norman, Semantics for evidence-based argumentation, in: Proc of the 2nd International Conference on Computational Models of Argument (COMMA), P. Besnard, S. Doutre and A. Hunter, eds, IOS Press, 2008, pp. 276–284.
N. Oren, C. Reed and M. 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.
M. Osorio and J.C. Nieves, Range-based argumentation semantics as two-valued models, TPLP 17(1) (2017), 75–90.
M. Osorio, J.C. Nieves and A. 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.
S. Polberg, Understanding the abstract dialectical framework, in: Proc. of JELIA, 2016, pp. 430–446.
S. 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.
S. Polberg and N. Oren, Revisiting support in abstract argumentation systems, Technical report, TU Wien, Institut for Informatics, 2014.
F. Pu, G. Luo and Z. Jiang, Encoding argumentation semantics by Boolean algebra, IEICE Transactions 100D(4) (2017), 838–848. doi:10.1587/transinf.2016EDP7313.
C. Sakama and T. Rienstra, Representing argumentation frameworks in answer set programming, Fundamenta Informaticae 155(3) (2017), 261–292. doi:10.3233/FI-2017-1585.
F. Toni and M. Sergot, Argumentation and answer set programming, in: Logic Programming, Knowledge Representation and Nonmonotonic Reasoning: Essays in Honor of Michael Gelfond, M. Balduccini and T.C. Son, eds, Springer, 2010, pp. 164–180.
B. Verheij, DEFLOG: On the logical interpretation of prima facie justified assumptions, Journal of Logic in Computation 13 (2003), 319–346. doi:10.1093/logcom/13.3.319.
S. Villata, G. Boella, D.M. Gabbay and L. van der Torre, Modelling defeasible and prioritized support in bipolar argumentation, Annals of Mathematics and Artificial Intelligence 66(1–4) (2012), 163–197. doi:10.1007/s10472-012-9317-7.
S. Villata, G. Boella, D.M. Gabbay, L. van der Torre and J. Hulstijn, A logic of argumentation for specification and verification of abstract argumentation frameworks, Annals of Mathematics and Artificial Intelligence 66(1–4) (2012), 199–230. doi:10.1007/s10472-012-9318-6.
M. Walicki and S. Dyrkolbotn, Finding kernels or solving SAT, Discrete Algorithms 10 (2012), 146–164. doi:10.1016/j.jda.2011.11.004.
J.P. Wallner, G. Weissenbacher and S. 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.
Y. Wu, M. 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 Logic 93(2/3) (2009), 383–403. doi:10.1007/s11225-009-9210-5.