Answer-set programming encodings for argumentation frameworks

Egly, Uwe; Gaggl, Sarah Alice; Woltran, Stefan

doi:10.1080/19462166.2010.486479

Answer-set programming encodings for argumentation frameworks

Article type: Research Article

Authors: Egly, Uwe^a | Gaggl, Sarah Alice^a | Woltran, Stefan^{a; *}

Affiliations: [a] Institute of Information Systems 184, Vienna University of Technology, Favoritenstrasse 9-11, A-1040, Vienna, Austria

Correspondence: [*] E-mail: [email protected]

Keywords: abstract argumentation frameworks, answer-set programming, implementation

DOI: 10.1080/19462166.2010.486479

Journal: Argument & Computation, vol. 1, no. 2, pp. 147-177, 2010

Received 6 August 2009

Accepted 8 April 2010

Published: 1 June 2010

Get PDF

Abstract

Answer-set programming (ASP) has emerged as a declarative programming paradigm where problems are encoded as logic programs, such that the so-called answer sets of theses programs represent the solutions of the encoded problem. The efficiency of the latest ASP solvers reached a state that makes them applicable for problems of practical importance. Consequently, problems from many different areas, including diagnosis, data integration, and graph theory, have been successfully tackled via ASP. In this work, we present such ASP-encodings for problems associated to abstract argumentation frameworks (AFs) and generalisations thereof. Our encodings are formulated as fixed queries, such that the input is the only part depending on the actual AF to process. We illustrate the functioning of this approach, which is underlying a new argumentation system called ASPARTIX in detail and show its adequacy in terms of computational complexity.

1.Motivation

In Artificial Intelligence (AI), the area of argumentation (the survey by Bench-Capon and Dunne (2007) gives an excellent overview) has become one of the central issues during the last decade. Argumentation provides a formal treatment for reasoning problems arising in a number of applications fields, including Multi-Agent Systems and Law Research. In a nutshell, the so-called abstract argumentation frameworks (AFs) formalise statements together with a relation denoting rebuttals between them, such that the semantics gives an abstract handle to solve the inherent conflicts between statements by selecting admissible subsets of them. The reasoning underlying such AFs turned out to be a very general principle capturing many other important formalisms from the areas of AI and knowledge representation.

The increasing interest in argumentation led to numerous proposals for formalisations of argumentation. These approaches differ in many aspects. First, there are several ways as to how “admissibility” of a subset of statements can be defined; second, the notion of rebuttal has different meanings (or even additional relationships between statements are taken into account); finally, statements are augmented with priorities, such that the semantics yields those admissible sets which contain statements of higher priority. Thus, in order to compare these different proposals, it is desirable to have a system at hand, which is capable of dealing with a large number of argumentation semantics.

Argumentation problems are, in general, intractable; for instance, deciding if an argument is contained in some preferred extension is known to be NP-complete. Therefore, developing dedicated algorithms for the different reasoning problems is non-trivial. A promising way to implement such systems is to use a reduction method, where the given problem is translated into another language, for which sophisticated systems already exist.

In this work, we present an approach which meets these challenges, i.e. we describe a system which, on the one hand, implements numerous approaches for abstract argumentation, and, on the other hand, gains its efficiency by exploiting highly sophisticated solvers to which we can map the problems in question. The declarative programming paradigm of Answer-Set Programming (ASP) (Niemelä 1999; Leone et al. 2006) is especially well suited for this purpose due to the following three characteristics.

• The prototypical language of ASP (i.e. logic programming under the answer-set semantics (Gelfond and Lifschitz 1991), also known as stable logic programming or A-Prolog) is very expressible and allows to formulate queries (in an extended datalog fashion) over databases, such that multiple results can be obtained. In our context, queries thus can be employed to obtain multiple extensions for AFs, where the actual AF to process is just given as an input database.
• Advanced ASP-solvers such as Smodels, DLV, GnT, Cmodels, Clasp, or ASSAT are nowadays able to deal with large problem instances, see, e.g. (Gebser et al. 2007). Thus, using our proposed reduction method delegates the burden of optimisation to these systems.
• Depending on the syntactical structure of a given ASP query, the complexity of evaluating that query on input databases (i.e. the data complexity of ASP) varies from classes P, NP, coNP up to Σ2P and to Π2P. Hence, for the different types of problems in abstract argumentation, we are able to formulate queries which are “well suited” from a complexity point of view. In other words, the complexity of evaluating ASP queries representing some argumentation problem lies in the same complexity class as the original problem.

The main aim of this paper is to present ASP queries for reasoning problems within different types of AFs. To be more specific, we give queries for the most important types of extensions (i.e. admissible, preferred, stable, semi-stable, complete, and grounded (Dung 1995; Caminada 2006)) in terms of Dung's original abstract framework, the preference-based AF by Amgoud and Cayrol (2002), the value-based argumentation framework (VAF) by Bench-Capon (2003), and the bipolar argumentation framework (BAF) (Cayrol and Lagasquie-Schiex 2005; Amgoud, Cayrol, Lagasquie-Schiex, and Livet 2008).

We have implemented these queries in a system called ASPARTIX, which makes use of the prominent answer set solver DLV (Leone et al. 2006). All necessary programs to run ASPARTIX and some illustrating examples are available at

www.dbai.tuwien.ac.at/research/project/argumentation/systempage/

We believe that our system is a useful tool for researchers in the argumentation community to compare different argumentation semantics on concrete examples within a uniform setting. In fact, investigating the relationship between different argumentation semantics has received increasing interest lately (Baroni and Giacomin 2008b).

Earlier work already proposed reductions from argumentation problems to certain target formalisms. Most notably are encodings in terms of (quantified) propositional logic (Besnard and Doutre 2004; Egly and Woltran 2006; Besnard, Hunter, and Woltran 2009) and logic programs (Nieves, Osorio, and Cortés 2008; Nieves, Osorio, and Zepeda 2009; Osorio, Zepeda, Nieves, and Cortés 2005; Wakaki and Nitta 2008; we will come back to the earlier work on reductions to logic programs, which is indeed most closely related to ours, in the discussion section at the end of this article).

The main difference of this earlier work compared with our approach is the necessity of compiling (at least, for some of the semantics) each problem instance into a different instance of the target formalism (e.g. into a different logic program).

In our approach, all semantics are encoded within a fixed query (independent from the concrete AF to process). Thus, we are more in the tradition of a classical implementation because we construct an interpreter in ASP which takes an AF given as input. Although there is no advantage of the interpreter approach from a theoretical point of view (as long as the reductions are polynomial-time computable), there are several practical ones. The interpreter is easier to understand, easier to debug, and easier to extend. Additionally, proving properties like correspondence between answer sets and extensions is simpler. Moreover, the input AF can be changed easily and dynamically without translating the whole formula. This indeed simplifies the answering of questions like “What happens if I add this new argument?”.

The remainder of the article is organised as follows. In the next section, we recall the necessary concepts of ASP and AFs. Furthermore we give some illustrative examples and recall the respective complexity results. In Section 3, we gradually introduce the encodings for the particular semantics and in Section 4, we adapt these encodings for some generalisations of AFs. Finally, in Section 5, we give an overview of related approaches and discuss future work.

2.Preliminaries

2.1.Answer-set programming

We first give a brief overview of the syntax and semantics of the ASP-formalism we consider, i.e. disjunctive datalog under the answer-set semantics (Gelfond and Lifschitz 1991). Then, we illustrate useful programming techniques on some simple examples. Finally, we briefly recall some important complexity results for disjunctive datalog. We refer to Eiter, Gottlob, and Mannila (1997) and Leone et al. (2006) for a broader exposition on all of these topics.

In what follows, we fix a countable set 𝒰 of (domain) elements, also called constants and suppose a total order < over these elements. An atom is an expression p(t₁, …,t_n), where p is a predicate symbol of arity n≥0 and each t_i is either a variable or an element from 𝒰. An atom is ground if it is free of variables.

A (disjunctive) rule r is of the form

a1∨⋯∨an:−b1,…,bk,notbk+1,…,notbm

with n≥0, m≥k≥0, n+m>0, and where a1,…,an,b1,…,bm are atoms, and “not ” stands for default negation.

The head of r is the set H(r) = {a1,…,an} and the body of r is B(r)={b1,…,bk,notbk+1,…,notbm}. Furthermore, B⁺(r) = {b1,…,bk} and B⁻(r) = {bk+1,…,bm}. A rule r is normal (or disjunction-free) if n≤1 and a constraint if n=0. A rule r is safe if each variable in r occurs in B⁺(r). A rule r is ground if no variable occurs in r. If each rule in a program is normal (resp., ground), we call the program normal (resp., ground). A fact is a disjunction-free ground rule with an empty body.

A program is a finite set of safe (disjunctive) rules. Employing database notation, we call a finite set of facts also an input database and a set of non-ground rules a query. For a query Π and an input database D, we often write Π(D), instead of the program D∪Π, in order to indicate that D serves as input for query Π.

A normal program Π is called stratified if no atom a depends by recursion through negation on itself (Apt, Blair, and Walker 1988). More formally, Π is stratified if there exists an assignment α(·) of integers to the predicates in Π, such that for each rule r∈Π, the following holds: If predicate p occurs in the head of r and predicate q occurs

(i) in the positive body of r, then α(p)⩾α(q) holds;
(ii) in the negative body of r, then α(p)>α(q) holds.

As an example, consider the following program Π:

Π={a(X):−notb(X),d(X);b(X):−a(X)}.

In order to find an assignment α(·) satisfying the above conditions for Π, observe that the first rule of Π requires α(a)>α(b), but the second rule, in turn, forces α(b)⩾α(a). In other words, each assignment α(·) violates at least one of the conditions, and hence, Π is not stratified.

For the program

Π′={a(X):−notb(X),d(X);b(X):−c(X);c(X):−b(X)},

we can use the assignment α(a)=2,α(b)=α(c)=α(d)=1 to show that Π′ is stratified. The concept of stratified programs is very important in logic programming, since it allows for a restricted form of negation, but does not lead to an increase in the complexity (see also the complexity results below, which show that stratified programs still can be evaluated efficiently, while this is not the case for normal or disjunctive programs).

For any program Π, let UΠ be the set of all constants appearing in Π (if no constant appears in Π, an arbitrary constant is added to UΠ), and let B_Π be the set of all ground atoms constructible from the predicate symbols appearing in Π and the constants of UΠ. Moreover, Gr(Π) is the set of rules rσ obtained by applying, to each rule r∈Π, all possible substitutions σ from the variables in Π to elements of UΠ.

Let the set of all ground atoms over 𝒰 be denoted by BU. An interpretationI⊆BUsatisfies a ground rule r iff H(r)∩I≠∅ whenever B+(r)⊆I and B−(r)∩I=∅. A ground program Π is satisfied by I, if I satisfies each r∈Π. A non-ground rule r (resp., a non-ground program Π) is satisfied by I, if I satisfies all groundings of r (resp., Gr(Π)). An interpretation I⊆BU is an answer set of Π iff it is a subset-minimal set satisfying the Gelfond–Lifschitz reduct

ΠI={H(r):−B+(r)∣I∩B−(r)=∅,r∈Gr(Π)}.

For a program Π, we denote the set of its answer sets by AS(Π). We note that for each I∈AS(Π), I⊆BΠ holds. Moreover, a program can have multiple answer sets. A stratified program has at most one answer set, and a constraint-free stratified program has exactly one answer set.

Let us discuss some typical concepts of ASP which are important for the implementation later on by providing queries for some graph problems (see Leone et al. (2006) for a more detailed discussion of similar examples). First, consider the problem of reachability in directed graphs. We assume that an input graph G is given as a set of facts edge(a,b), indicating that there is an edge from vertex a to vertex b in G. Moreover, we assume that each such input database D also contains a fact start(a) for a designated vertex a. The goal is now to compute all vertices reachable from a via the edges in G. Therefore, we use the predicate reached(·) in the following program:

πreach={reached(X):−start(X);reached(Y):−reached(X),edge(X,Y)}

Given an input database D as specified above, we get that predicate reached(b) is in the answer set of πreach(D) iff vertex b is reachable in G from the designated start vertex a. Note that πreach does neither contain disjunction nor negation. Moreover, there is no constraint in πreach, hence πreach(D) has exactly one answer set, for each input database D. Minimality of the answer-set semantics guarantees that the answer set of πreach(D) does not contain predicates reached(c), if vertex c is not reachable from a in G.

Before we give some further examples, let us introduce the concept of splitting sets (Lifschitz and Turner 1994). Given a program Π, a set S of predicate symbols is a splitting set for Π, iff, for every rule r∈Π, it holds that if some atom with predicate symbol from S occurs in the head of r, then each atom in r has its predicate symbol from S as well. Any splitting set S for program Π divides Π in two parts. The top of Π (with respect to S), in symbols ΠSt, contains all rules of Π which have an occurrence of a predicate symbol not contained in S, while the bottom of Π (with respect to S) is defined as ΠSb=Π∖ΠSt. To have an example, recall the program Π′={a(X):−notb(X),d(X);b(X):−c(X);c(X):−b(X)}. The set S={b, c} is a splitting set for Π′, and we obtain (Π′)St={a(X):−notb(X),d(X)} and (Π′)Sb={b(X):−c(X);c(X):−b(X)}. Splitting sets allow to compute the answer sets of a program step-by-step due to the following result, known as the Splitting Theorem.

Proposition 2.1

Let S be a splitting set of a program Π, and letI⊆BU. ThenI∈AS(Π)iffI∈AS(ΠSt(J)), whereJ=I∩BΠSbandJ∈AS(ΠSb).

We next illustrate a typical use of default negation. We consider here the problem of 3-colourability of an (undirected) graph. Suppose a graph's vertices are defined via the predicate vertex(·) and its edges via the predicate edge(·,·). We employ default negation to guess a colour for each node in the graph, and then check whether adjacent vertices have indeed different colours.

πcol=πguess∪πcheckwhereπguess={red(X):−vertex(X),notgreen(X),notblue(X);(1)green(X):−vertex(X),notred(X),notblue(X);(2)blue(X):−vertex(X),notred(X),notgreen(X)}(3)πcheck={fail:−red(X),red(Y),edge(X,Y);(4)fail:−green(X),green(Y),edge(X,Y);(5)fail:−blue(X),blue(Y),edge(X,Y);(6):−fail}(7)

The three rules of πguess are typical “guessing rules” which assign to each vertex exactly one colour. To illustrate this, let D be an input database over predicates vertex and edge, and assume D contains three vertices {vertex(a),vertex(b),vertex(c)}. Then, the program πguess(D) possesses 27 answer sets, namely

D∪{red(a),red(b),red(c)},D∪{red(a),red(b),green(c)},…

We note that the fact that no vertex gets assigned to more than one colour is ensured by the interplay between minimality and the notion of a reduct. Also observe that πguess is not stratified. Indeed, we would require a mapping α(·), such that α(red)>α(green) (because of rule (1)) and α(green)>α(red) (because of rule (2)). Such a mapping obviously does not exist.

Now let use consider πcheck. The role of this program is to exclude answer set candidates provided by πguess. In our case, we want to rule out candidates having adjacent vertices of the same colour. Thanks to the Splitting Theorem, we indeed are allowed to first compute the answer sets of πguess(D) and then compute the answer sets of πcheck(J) for each J∈AS(πguess(D)), in order to obtain the answer sets of the entire program πcol(D). In fact, the set S={vertex,edge,red,green,blue} is a splitting set for πcol(D), for any input database D over atoms with predicate symbols from S. The top of πcol(D) with respect to S is thus given by (πcol(D))St=πcheck, and the bottom of πcol(D) with respect to S is given by (πcol(D))Sb=πguess(D). For illustration, assume D contains edge(a,b), edge(b,c), and edge(c,a). Assume the answer set J=D∪{red(a),red(b),green(c)} of πguess(D) is used as input now to πcheck. Then, the rule fail:−red(X),red(Y),edge(X,Y) derives fail, but then rule (7) cannot be satisfied. Thus, J does not satisfy πcol(D), and consequently, J cannot become an answer set of πcol(D). On the other hand, D∪{red(a),green(b),blue(c)} (which is also an answer set of πguess(D)) satisfies all rules of πcheck and thus becomes an answer set of πcol(D). In fact, for the example graph represented in D, πcol(D) possesses six answer sets.

Actually, instead of the rules (1)–(3), we could have used disjunction to guess a colour for each vertex. As we shall see next, disjunction is a more expressive concept than default negation. While with default negation, one is able to formulate an exclusive guess (as we did in the above example), disjunction can be additionally employed for a certain saturation technique, which allows for representing even more complex problems. The term “saturation” indicates that all atoms which are subject to a guess can also be jointly contained in an interpretation. To saturate a guess, it is however necessary that the checking part of a program interacts with the guessing part.

As a very simple example, let us compare the following two programs:

Π={p∨q:−;Π′={p:−notq;q:−notp;p:−q;q:−p}p:−q;q:−p}

In Π we are guessing p or q via disjunction and in Π′ we have formulated the same guess via two normal rules. Note that the remaining rules p:− q and q:− p however saturate any such guess between p and q by adding the respective other predicate. In fact, this saturation of the guess shows the difference between programs Π and Π′ in the following sense: We have that {p, q} is the unique answer set of Π (which can be seen by the fact that {p, q} is the minimal interpretation satisfying Π; note that Π does not contain default negation, so there is no need to consider the reduct.). On the other hand, for Π′ we obtain as the reduct (Π′){p,q}={p:−q;q:−p}. But now, {p, q} is not the minimal interpretation satisfying (Π′){p,q}, since we could also take the empty interpretation (i.e., both p and q are set to false). Thus, {p, q} is not an answer set of Π′. In fact, Π′ has no answer set at all.

To have a slightly more meaningful application of this saturation technique, let us now reduce also the non-3-colourability problem to the problem of deciding whether an answer set exists. Therefore, we adapt the encoding πcol from above as follows. First, we use disjunction in rule (8) to guess the colour of vertices. Second, we have the same rules (9)–(11) to derive fail as we had in πcol. Finally, instead of the constraint :−fail to exclude invalid colourings, we “saturate” the guess via rules (12)–(14) and add as constraint :−notfail.

πncol={red(X)∨green(X)∨blue(X):−vertex(X);(8){fail:−red(X),red(Y),edge(X,Y);(9){fail:−green(X),green(Y),edge(X,Y);(10){fail:−blue(X),blue(Y),edge(X,Y);(11){red(X):−fail,vertex(X);(12){green(X):−fail,vertex(X);(13){blue(X):−fail,vertex(X);(14){:−notfail}(15)

Suppose graphs are represented by inputs D as above. The only possible answer set J of πncol(D) (if one exists) contains fail because of the last rule :−notfail. But if fail is contained in J, J has to contain red(X), green(X), and blue(X) for each vertex X. Thus J has to be of the form D∪{fail}∪{red(a),green(a),blue(a)∣vertex(a)∈D}. We observe that the reduct (πncol(D))J is given by πncol(D)∖{:−notfail}. Note that interpretations satisfying (πncol(D))J do not necessarily contain fail. Indeed, we can come up with such an interpretation (not containing fail), exactly in the case where the input D represents a 3-colourable graph. But this means that D represents a graph which is not 3-colourable iff J is (the unique) answer set of πncol(D). We refer to the work by Eiter and Polleres (2006) for a general discussion on how this saturation technique can be further exploited in ASP queries.

We conclude this section by recalling some central complexity results for ASP. Credulous and skeptical reasoning in terms of programs are defined as follows. Given a program Π and a set A of ground atoms, we denote by Π⊧cA that A is contained in some answer sets of Π. Likewise, we denote by Π⊧sA that A is contained in all answer sets of Π. In the former case, we reason credulously; in the latter case, we reason skeptically.

Since we will deal with fixed programs, we focus on results for data complexity. Recall that data complexity in our context addresses the problem Π(D)⊧A where the query Π is fixed, while the input database D and ground atoms A are inputs of the decision problem. Depending on the concrete definition of ⊧, we get the complexity results in Table 1, compiled from (Dantsin, Eiter, Gottlob, and Voronkov 2001) and the references therein.

Table 1.

Data complexity for datalog (all results are completeness results).

	Stratified programs	Normal programs	General case
⊧c	P	NP	Σ2P
⊧s	P	coNP	Π2P

2.2.Basic argumentation frameworks

In this section, we recall the most important semantics for the basic version of abstract AFs and highlight complexity results for typical decision problems. Later, in Section 4, we will introduce some generalisations of AFs.

In order to relate frameworks to programs, we use the universe 𝒰 of domain elements (introduced in the previous subsection) also in the following basic definition.

Definition 2.2

An AF is a pair F=(A, R) whereA⊆Uis a finite set of arguments andR⊆A×A. The pair (a, b)∈R means that a attacks (or defeats) b. A set S⊆ A of arguments defeats b in F, if there is an a∈S, such that (a, b)∈R. An argument a∈A is defended by S ⊆ A in F iff, for each b∈A, it holds that, if (b, a)∈R, then S defeats b in F.

An AF can be naturally represented as a directed graph.

Example 2.3

Let F=(A, R) be an AF with A={a,b,c,d,e} and R={(a, b), (c, b), (c, d), (d, c), (d, e), (e, e)}. The graph representation of F is the following.

In order to be able to reason about such frameworks, it is necessary to group arguments with special properties to extensions. One of the basic properties is the absence of conflicts between arguments contained in the same extension.

Definition 2.4

Let F=(A, R) be an AF. A set S⊆ A is said to be conflict-free in F, if there are no a, b∈S, such that (a, b)∈R. We denote the collection of sets which are conflict-free in F by cf(F).

For our framework F=(A, R) from Example 2.3, we have

cf(F)={∅,{a},{b},{c},{d},{a,c},{a,d},{b,d}}.

As a first concept of extensions, we present the stable extensions which are based on the idea that an extension should not only be internally consistent but also be able to reject the arguments that are outside the extension.

Definition 2.5

Let F=(A, R) be an AF. A set S is a stable extension of F, ifS∈cf(F)and eacha∈A∖Sis defeated by S in F. We denote the collection of all stable extensions of F bystable(F).

The framework F from Example 2.3 has a single stable extension {a, d}. Indeed, {a, d} is conflict-free, and each further element b, c, e is defeated by either a or d. In turn, {a, c} for instance is not contained in stable(F), although it is conflict-free as well. The obvious reason is that e is not defeated by {a, c}.

Stable semantics in terms of argumentation are considered to be quite restricted. Moreover, it is not guaranteed that a framework possesses at least one stable extension (consider, e.g. the simple cyclic framework ({a},{(a,a)})). Therefore it is also reasonable to consider those arguments which are able to defend themselves from external attacks, like the admissible semantics proposed by Dung (1995).

Definition 2.6

Let F=(A, R) be an AF. A set S is an admissible extension of F (or S is admissible in F), ifS∈cf(F)and each a∈S is defended by S in F. We denote the collection of all admissible extensions of F by adm(F).

For the framework F from Example 2.3, we obtain

adm(F)={∅,{a},{c},{d},{a,c},{a,d}}.

By definition, the empty set is always an admissible extension, therefore reasoning over admissible extensions is also limited. In fact, skeptical acceptance (i.e. given an AF F=(A, R), and a∈A, is a contained in all extensions of F) becomes trivial w.r.t. admissible extensions. Thus, many researchers consider maximal (w.r.t. set-inclusion) admissible sets, called preferred extensions, as more important.

Definition 2.7

Let F=(A, R) be an AF. A set S is a preferred extension of F, ifS∈adm(F)and for eachT∈adm(F), S⊄T. We denote the collection of all preferred extensions of F by pref(F).

Obviously, the preferred extensions of the framework F from Example 2.3 are {a, c} and {a, d}. We note that each stable extension is also preferred, but the converse does not hold, as witnessed by this example.

The next semantics we consider is the semi-stable semantics, recently introduced by Caminada (2006) and investigated also in (Dunne and Caminada 2008). Semi-stable semantics are located in-between stable and preferred semantics, in the sense that each stable extension of an AF F is also a semi-stable extension of F, and each semi-stable extension of F is a preferred extension of F. However, in general, both inclusions do not hold in the opposite direction. In contrast to the stable semantics, semi-stability guarantees that there exists at least one extension (in case of finite AFs). We use the definition given by Dunne and Caminada (2008).

Definition 2.8

Let F=(A, R) be an AF, and for a set S⊆ A, let S⁺_Rbe defined asS∪{b∣∃a∈S,such that(a,b)∈R}. A set S is a semi-stable extension of F, ifS∈adm(F)and for eachT∈adm(F), SR+⊄TR+. We denote the collection of all semi-stable extensions of F by semi(F).

For our example framework (A, R), the only semi-stable extension coincides with the stable extension T={a, d}. In contrast, S={a, c} is not semi-stable because SR+={a,b,c,d}⊂{a,b,c,d,e}=TR+.

Finally, we introduce complete and grounded extensions which Dung considered as skeptical counterparts of admissible and preferred extensions, respectively.

Definition 2.9

Let F=(A, R) be an AF. A set S is a complete extension of F, ifS∈adm(F)and, for each a∈A defended by S in F, a∈S holds. The least (w.r.t. set inclusion) complete extension of F is called the grounded extension of F. We denote the collection of all complete (resp., grounded) extensions of F by comp(F) (resp., ground(F)).

The complete extensions of framework F from Example 2.3 are {a, c}, {a, d}, and {a}, with the last being also the grounded extension of F.

This concludes our collection of argumentation semantics that we consider in this paper. The relations between the semantics are depicted in Figure 1, where an arrow from e to f indicates that each e-extension is also an f-extension.

Figure 1.

Overview of argumentation semantics and their relations.

We briefly review the complexity of reasoning in AFs. To this end, we define the following decision problems for e∈{stable,adm,pref,semi,comp,ground}:

• Cred_e: Given AF F=(A, R) and a∈A. Is a contained in some S∈e(F)?
• Skept_e: Given AF F=(A, R) and a∈A. Is a contained in all S∈e(F)?

The complexity results are depicted in Table 2 (many of them follow implicitly from Dimopoulos and Torres (1996); for the remaining results and discussions, see (Dunne and Bench-Capon 2002, 2004; Coste-Marquis, Devred, and Marquis 2005; Dunne and Caminada 2008; Dvořák and Woltran 2009)). In the table, “𝒞-c” refers to a problem which is complete for class 𝒞, while “in 𝒞” is assigned to problems for which a tight lower complexity bound is not known. A few further comments are in order. We already mentioned that skeptical reasoning over admissible extensions always is trivially false. Moreover, we note that credulous reasoning over preferred extensions is easier than skeptical reasoning. This is due to the fact that the additional maximality criterion only comes into play for the latter task. Indeed, for credulous reasoning the following simple observation makes clear why there is no increase in complexity compared with credulous reasoning over admissible extensions: a is contained in some S∈adm(F) iff a is contained in some S∈pref(F). A similar argument immediately shows why skeptical reasoning over complete extensions reduces to skeptical reasoning over the grounded extension. Finally, we recall that reasoning over the grounded extension is tractable (Dung 1995), since the least fixed point of the following operator captures (for finite AFs) the grounded extension and can be computed in polynomial time.

Table 2.

Complexity for decision problems in AFs.

	stable	adm	pref	semi	comp	ground
Cred_e	NP-c	NP-c	NP-c	Σ2P-c	NP-c	in P
Skept_e	coNP-c	(trivial)	Π2P-c	Π2P-c	in P	in P

Proposition 2.10

The grounded extension of an AF F=(A, R) is given by the least fixed point of Γ_F, where the operatorΓF:2A→2Ais defined as

ΓF(S)={a∈A∣ais defended bySinF}.

3.ASP-encodings for abstract argumentation frameworks

We now provide fixed queries π_e for each extension of type e introduced in the previous section, in such a way that the AF F is given as an input database [Fcirc] and the answer sets of the combined program πe(Fˆ) are in a certain one-to-one correspondence with the respective extensions. Note that having established the fixed query π_e, the only translation required is to provide a given AF F as input database [Fcirc] to π_e. For an AF F=(A, R), we define

Fˆ={arg(a)∣a∈A}∪{defeat(a,b)∣(a,b)∈R}.

In most cases, we have to guess candidates for the selected type of extensions and then check whether a guessed candidate satisfies the corresponding conditions. As we have outlined in Section 2.1, default negation is an appropriate concept to formulate such a guess within a query. In what follows, we use unary predicates in(·) and out(·) to perform a guess for a set S⊆ A, where in(a) represents that a∈S. The following notion of correspondence is relevant for our purposes.

Definition 3.1

LetS⊆2Ube a collection of sets of domain elements and letI⊆2BUbe a collection of sets of ground atoms. We say that 𝒮 and ℐ correspond to each other, in symbolsS≅I, iff (i) for eachS∈S, there exists anI∈I, such that{a∣in(a)∈I}=S; and (ii) for eachI∈I, it holds that{a∣in(a)∈I}∈S.

Note that S≅I thus implies |S|=|I|. In what follows, we will stepwise introduce the rules from which our queries will be built.

Let F=(A, R) be an AF. The following program fragment guesses, when augmented by [Fcirc], any subset S⊆ A and then checks whether the guess is conflict-free in F:

πcf={in(X):−notout(X),arg(X);{out(X):−notin(X),arg(X);{:−in(X),in(Y),defeat(X,Y).

For our framework F from Example 2.3, we have as input

Fˆ={arg(a),arg(b),arg(c),arg(d),arg(e),{defeat(a,b),defeat(c,b),defeat(c,d),{defeat(d,c),defeat(d,e),defeat(e,e).

Moreover, using [Fcirc] together with π_cf, we obtain

AS(πcf(Fˆ))={S∅,Sa,Sb,Sc,Sd,Sac,Sad,Sbd},

where

S∅=Fˆ∪{out(a),out(b),out(c),out(d),out(e)},Sa=Fˆ∪{in(a),out(b),out(c),out(d),out(e)},Sb=Fˆ∪{in(b),out(a),out(c),out(d),out(e)},Sc=Fˆ∪{in(c),out(a),out(b),out(d),out(e)},Sd=Fˆ∪{in(d),out(a),out(b),out(c),out(e)},Sac=Fˆ∪{in(a),in(c),out(b),out(d),out(e)},Sad=Fˆ∪{in(a),in(d),out(b),out(c),out(e)},Sbd=Fˆ∪{in(b),in(d),out(a),out(c),out(e)}.

Proposition 3.2

For any AF F, cf(F)≅AS(πcf(Fˆ)).

Proof

Let F=(A, R) and S∈cf(F). We show that the interpretation

I=Fˆ∪{in(a)∣a∈S}∪{out(a)∣a∈A∖S}

(corresponding to S) is an answer set of πcf(Fˆ). We have to show that I satisfies πcf(Fˆ) (we recall that an interpretation I satisfies a program Π iff I satisfies Π^I), and that no J⊂I satisfies (πcf(Fˆ))I. To show that I satisfies πcf(Fˆ), we have to show that I satisfies each r∈Gr(πcf(Fˆ)). Note that

Gr(πcf(Fˆ))=Fˆ∪{in(a):−notout(a),arg(a)∣a∈A}∪(16){out(a):−notin(a),arg(a)∣a∈A}∪(17){:−in(a),in(b),defeat(a,b)∣a,b∈A}.(18)

Clearly, I satisfies [Fcirc], since Fˆ⊆I. Moreover, I satisfies each instance of rule (16) (and likewise of rule (17)), since either in(a) or out(a) is contained in I, for each a∈A. Finally, each instance of constraint (18) is satisfied by I, since B+(r)⊈I. This can be seen as follows: Suppose r is of the form :−in(a),in(b),defeat(a,b). In case, {in(a),in(b)}⊈I, B+(r)⊈I is clear. Otherwise, then both a and b are contained in S, by definition of I. Since S∈cf(F) by assumption, (a,b)∉R has to hold. Thus, by definition, defeat(a,b)∉Fˆ (and thus defeat(a,b)∉I). Hence B+(r)⊈I.

This shows that I satisfies πcf(Fˆ). Now let J⊆ I, such that J satisfies (πcf(Fˆ))I. We show that then J=I. Note that the reduct is always grounded by definition. We have

(πcf(Fˆ))I=Fˆ∪{in(a):−arg(a)∣a∈A,out(a)∉I}∪(19){out(a):−arg(a)∣a∈A,in(a)∉I}∪(20){:−in(a),in(b),defeat(a,b)∣a,b∈A}.(21)

Since J satisfies (πcf(Fˆ))I, Fˆ⊆J. Moreover, since J satisfies each rule in Equation (19), for each a∈A, such that out(a)∉I, in(a) has to be in J. But since, for each a∈A, we have that out(a)∉I iff in(a)∈I, we get that in(a)∈J iff in(a)∈I. Similarly, using the rules from Equation (20), we obtain that out(a)∈J iff out(a)∈I. J=I follows. Hence, there is no J⊂I, such that J satisfies (πcf(Fˆ))I. This concludes the proof for I∈AS(πcf(Fˆ)).

Now suppose I∈AS(πcf(Fˆ)). Consequently, Fˆ⊆I, and no further atom of the form defeat(·,·) or arg(·) is contained in I (by the minimality of answer sets, and since such predicates do not occur in heads of rules apart from [Fcirc]). We show that S∈cf(F) for S={a∣in(a)∈I}. Since I∈AS(πcf(Fˆ)), I satisfies πcf(Fˆ), i.e. I satisfies the grounding of πcf(Fˆ), Gr(πcf(Fˆ)), as given above. In particular, I satisfies each constraint in Equation (18), thus jointly in(a)∈I and in(b)∈I, only if defeat(a,b)∉I. By our observation from above, defeat(a,b)∉Fˆ, and thus (a,b)∉R. Thus, for each a, b jointly occurring in S, a and b do not attack each other in F. Thus S is conflict-free for F. ▪

3.1.Stable extensions

We are now prepared to present our first encoding. Two additional rules for the stability test are required and we define

πstable=πcf∪πsrulesπsrules={defeated(X):−in(Y),defeat(Y,X);{:−out(X),notdefeated(X)}.

The first rule of πsrules computes those arguments attacked by the current guess, while the constraint in πsrules eliminates those guesses where some argument not contained in the guess remains undefeated.

Note that we can use the Splitting Theorem (Section 2.1) as follows. The splitting set C={in,out,arg,defeat} divides the program πstable(Fˆ) into (πstable(Fˆ))Ct=πsrules and (πstable(Fˆ))Cb=πcf(Fˆ). Therefore, we make direct use of the answer sets of πcf(Fˆ). For our example, let us first consider the collection 𝒞 of answer sets of

πcf(Fˆ)∪{defeated(X):−in(Y),defeat(Y,X)}.

In fact, using our calculations from the previous subsection, we obtain

C={S∅,{Sa∪{defeated(b)},{Sb,{Sc∪{defeated(b),defeated(d)},{Sd∪{defeated(c),defeated(e)},{Sac∪{defeated(b),defeated(d)},{Sad∪{defeated(b),defeated(c),defeated(e)},{Sbd∪{defeated(c),defeated(e)}}.

If we now apply the constraint :−out(X),notdefeated(X) to each element in 𝒞, we observe that any set from 𝒞 except Sad∪{defeated(b),defeated(c),defeated(e)} is violated by that constraint. In fact, each other set contains at least one atom out(y) without the matching defeated(y).

In general, our encoding for stable extensions satisfies the following correspondence result.

Proposition 3.3

For any AF F, stable(F)≅AS(πstable(Fˆ)).

Proof

First, let us formally describe the application of the Splitting Theorem (Proposition 2.1) as sketched above with the splitting set C={in,out,arg,defeat}. Then, we obtain

AS(πstable(Fˆ))=⋃J∈AS(πcf(Fˆ))AS(J∪πsrules).(22)

Let F=(A, R) and S∈stable(F). Since S∈stable(F), S∈cf(F), and by Proposition 3.2, there exists an interpretation

J=(Fˆ∪{in(a)∣a∈S}∪{out(a)∣a∈A∖S})∈AS(πcf(Fˆ)).

By Equation (22), we know that each answer set of J∪πsrules is also an answer set of πstable(Fˆ). We now show that I given as

Fˆ∪{in(a)∣a∈S}∪{out(a)∣a∈A∖S}∪{defeated(a)∣b∈S,(b,a)∈R}

is indeed an answer set of πstable(Fˆ). We first show that I satisfies the grounding of J∪πsrules. Clearly, I satisfies J, since J⊆ I. The groundings of the remaining rules are given by

{defeated(a):−in(b),defeat(b,a)∣a,b∈A}(23){:−out(a),notdefeated(a)∣a∈A}.(24)

Note that, for each argument b, we have in(b)∈I iff b∈S. Moreover, we already know defeat(a,b)∈J iff (a, b)∈R. Thus, I satisfies each instance of rule (23). Further, since S is stable, we know that each a∈A∖S is defeated by S in F. By definition, if a∈A∖S then out(a)∈I. But this shows that either out(a)∉I or defeated(a)∈I holds for each a∈A. Thus I satisfies each instance of constraint (24). This shows that I satisfies πstable(Fˆ). In order to show that I∈AS(πstable(Fˆ)), let K⊆ I be an interpretation satisfying (πstable(Fˆ))I. First, we know K∩Bπcf(Fˆ)=I∩Bπcf(Fˆ), otherwise J∉AS(πcf(Fˆ)) (in that case we would have K∩Bπcf(Fˆ)⊂I∩Bπcf(Fˆ), but then also K∩Bπcf(Fˆ)⊂J holds since J=I∩Bπcf(Fˆ); further, by assumption, K (and thus also K∩Bπcf(Fˆ)) satisfies (πcf(Fˆ))J=(πcf(Fˆ))I⊆(πstable(Fˆ))I). Second, since K satisfies the rules in Equation (23) – which are all without default negation and thus contained in the reduct – defeated(a)∈K iff defeated(a)∈I. Hence K=I. This shows I∈AS(πstable(Fˆ)).

Let now I∈AS(πstable(Fˆ)). We show that S={a∣in(a)∈I} is a stable extension of F. Since I∈AS(πstable(Fˆ)) there exists (because of relation (22)) a J∈AS(πcf(Fˆ)) such that I∈AS(J∪πsrules). It is not hard to see that S={a∣in(a)∈J}. By Proposition 3.2, S is conflict-free in F. Since I∈AS(J∪πsrules), we get (by analogous observations as above) that defeated(a)∈I iff a is defeated by S in F. Now, since I satisfies πstable(Fˆ)), I has to satisfy each instance of constraint (24). In particular, we obtain that for each a such that out(a)∈I, also defeated(a)∈I. But this yields that each a∉S is defeated by S in F. Thus S∈stable(F). ▪

3.2.Admissible extensions

We next give the rules for the admissibility test:

πadm=πcf∪{defeated(X):−in(Y),defeat(Y,X);{:−in(X),defeat(Y,X),notdefeated(Y)}.

The first rule is the same as in πstable. The new constraint rules out sets containing a non-defended argument. Indeed, we can identify non-defended arguments as those, which are defeated by an argument, which itself is undefeated.

For our example framework, we start from a collections 𝒞 of sets as above but now we check which sets violate the new constraint :−in(X),defeat(Y,X),notdefeated(Y). This is the case for two of the candidates.

(1) S_b contains in(b) and defeat(a,b) but since defeated(a) is not contained, the constraint applies;
(2) for Sbd∪{defeated(c),defeated(e)}, the argumentation is analogous.

Hence, we obtain

AS(πadm(Fˆ))={S∅,{Sa∪{defeated(b)},{Sc∪{defeated(b),defeated(d)},{Sd∪{defeated(c),defeated(e)},{Sac∪{defeated(b),defeated(d)},{Sd∪{defeated(b),defeated(c),defeated(e)}}.

Again, we observe a one-to-one correspondence to the admissible extensions of F. The general result is as follows.

Proposition 3.4

For any AF F, adm(F)≅AS(πadm(Fˆ)).

The proof is similar to the one of Proposition 3.3.

3.3.Complete extensions

We proceed with the encoding for complete extensions. We define

πcomp=πadm∪{undefended(X):−defeat(Y,X),notdefeated(Y);{i:−out(X),notundefended(X)}.

Once more, we use our running example to illustrate π_comp. Again, we proceed in two steps and first compute the answer sets of the program without the constraint :−out(X),notundefended(X). Here, we can directly use the sets from AS(πadm(Fˆ)) and check which predicates undefended(·) can be derived. The answer sets of πadm(Fˆ)∪{undefended(X):−defeat(Y,X),notdefeated(Y)} are

S∅∪{undefended(b),undefended(c),undefended(d),undefended(e)},Sa∪{defeated(b),undefended(b),undefended(c),{undefended(d),undefended(e)},Sc∪{defeated(b),defeated(d),undefended(b),undefended(d),undefended(e)},Sd∪{defeated(c),defeated(e),undefended(b),undefended(c),undefended(e)},Sac∪{defeated(b),defeated(d),undefended(b),undefended(d),undefended(e)},Sad∪{defeated(b),defeated(c),defeated(e),{undefended(b),undefended(c),undefended(e)}.

Obviously, each candidate which contains out(a) (i.e. the sets S_∅, S_c, and S_d) is ruled out by the constraint :−out(X),notundefended(X), since no such candidate set contains undefended(a). One can check that all other sets, i.e., S_a, S_ac, and S_ad, do not violate the constraint, and thus are answer sets of πcomp(Fˆ). Again, these three sets characterise the complete extensions of F, as desired.

Proposition 3.5

For any AF F, comp(F)≅AS(πcomp(Fˆ)).

The proof is similar to the one of Proposition 3.3.

3.4.Grounded extension

Computing the grounded extension of a given AF could also be done by the “Guess & Check” method we used in the previous encodings. But since reasoning via the grounded extension is tractable (Table 2), we aim to find an encoding in a tractable subclass of datalog (the encodings we used so far are not contained in such a tractable subclass). Inspecting Table 1 shows that stratified programs are the appropriate candidate. However, as discussed in Section 2.1, stratified negation is too weak to formalise guesses as we did in the encodings above. Instead, a suitable encoding of the operator Γ_F as introduced in Proposition 2.10 is possible. Therefore, we recursively derive in(·) predicates according to the definition of the operator Γ_F (following the same idea as we used to derive the reached(·) predicates in the example program for reachability in graphs, discussed in Section 2.1). To compute (in a stratified program) the required predicate for being defended, we have to use the order < over the domain elements (such an order is provided by all ASP-solvers) and derive corresponding predicates for infimum, supremum, and successor w.r.t. <. In fact, we shall use these predicates to perform “loops” over all arguments given by the input database.

π<={lt(X,Y):−arg(X),arg(Y),X<Y;{nsucc(X,Z):−lt(X,Y),lt(Y,Z);{succ(X,Y):−lt(X,Y),notnsucc(X,Y);{ninf(Y):−lt(X,Y);{inf(X):−arg(X),notninf(X);{nsup(X):−lt(X,Y);{sup(X):−arg(X),notnsup(X)}.

Note that π_< is indeed stratified and constraint-free. Hence, π<(Fˆ) yields exactly one answer set for each AF F. To illustrate the purpose of π_<, recall our example framework F, and assume the arguments are ordered as follows: a<b<c<d<e. For this particular order, the single answer set S₀ of π<(Fˆ) contains

{inf(a),succ(a,b),succ(b,c),succ(c,d),succ(d,e),sup(e)}.

The other atoms (which however will not be used in later calculations) contained in S₀ are lt(a, b), lt(a, c), lt(a, d), lt(a, e), lt(b, c), lt(b, d), lt(b, e), lt(c, d), lt(c, e), lt(d, e), nsucc(a,c), nsucc(a,d), nsucc(a,e), nsucc(b,d), nsucc(b,e), nsucc(c,e), ninf(b), ninf(c), ninf(d), ninf(e), nsup(a), nsup(b), nsup(c), and nsup(d).

We now define the required predicate defended(X) which itself is obtained via a predicate defended_upto(X,Y) with the intended meaning that argument X is defended by the current assignment with respect to all arguments U≤Y. In other words, we perform a loop starting with the infimum Y and then use the successor predicate to derive defended_upto(X,Y) for all further Y. If we arrive at the supremum element in this way, i.e. defended_upto(X,Y) is derived for the supremum Y, we finally obtain defended(X). We define

πdefended={defended_upto(X,Y):−inf(Y),arg(X),notdefeat(Y,X);(25)idefended_upto(X,Y):−inf(Y),in(Z),defeat(Z,Y),defended_upto(X,Y):−pdefeat(Y,X);(26)idefended_upto(X,Y):−succ(Z,Y),defended_upto(X,Z),defended_upto(X,Y):−pnotdefeat(Y,X);(27)idefended_upto(X,Y):−succ(Z,Y),defended_upto(X,Z),defended_upto(X,Y):−pin(V),defeat(V,Y),defeat(Y,X);(28)pidefended(X):−sup(Y),defended_upto(X,Y),and(29)πground=π<∪πdefended∪{in(X):−defended(X)}.

Note that πground is also stratified. We also mention that the relevant predicate in(a) is derived for some argument a if defended_upto(a,b) holds for each b. However, if there is an unattacked argument c which attacks a, defended_upto(a,c) is not derived. It is thus not relevant in which order we derive the predicates defended_upto(a,b). Consequently, the particular definition of the order <, from which we obtained the inf(·), succ(·,·), and sup(·) predicates used in πdefended, plays no role. Any total order over the constants can be used.

For illustration, we compute the answer set for Fˆ∪π<∪πdefended step by step, for our example AF F. Recall that we already have given S₀, the answer set of Fˆ∪π<. Since πground only derives distinguished predicates defended_upto(·,·) and defended(·), we can view S₀ as input to πground.

In the “first round” of computation, we have no in(·) predicate derived so far; hence only the rules (25) and (27) in πdefended are of interest. In fact, for inf(a), the rule (25) in πdefended yields

defended_upto(a,a),defended_upto(c,a),defended_upto(d,a),defended_upto(e,a).

Note that defended_upto(b,a) is missing, since we have defeat(a,b)∈Fˆ. Now we use rule (27) and succ(a,b) to obtain

defended_upto(a,b),defended_upto(c,b),defended_upto(d,b),defended_upto(e,b).

The remaining atoms we derive are

defended_upto(a,c),defended_upto(c,c),defended_upto(e,c).

Note that, since d is attacked by c, defended_upto(d,c) cannot be derived. Finally, we get

defended_upto(a,d),defended_upto(a,e).

However, as a does not defend any argument, it can be checked that no further atoms can be derived. Thus we obtain that in the single answer set of πground(Fˆ) the only in(·) predicate is in(a). This corresponds to the grounded extension of F, as desired.

Proposition 3.6

For any AF F, ground(F)≅AS(πground(Fˆ)).

Proof

Let F=(A, R) and let [Fcirc]_< be the answer set of π<(Fˆ). Recall that each F possesses a unique grounded extension which is given by the least fixed point of Γ_F. In order to prove the correspondence between the operator Γ_F, and the unique answer set of the program πground(Fˆ), we first define the operator ΔFˆ representing the derivation of the answer set Fˆground of πground(Fˆ) as follows.

ΔFˆ(I)=I∪{defended_upto(a,b)∣arg(a),arg(b)∈I,∀cs.t.arg(c)∈Iandc⩽b:defeat(c,a)∉Ior∃ds.t.defeat(d,c)∈Iandin(d)∈I}∪{defended(a),in(a)∣arg(a)∈I,∀cs.t.arg(c)∈I:defeat(c,a)∉Ior∃ds.t.defeat(d,c)∈Iandin(d)∈I}.

Using the one-step provability operator for logic programs (see e.g. van Emden and Kowalski (1976) for details on that operator), it can be shown that for every AF F=(A, R), the answer set of the program πground(Fˆ) is given by the least fixed point of ΔFˆ. It remains to show that, in turn, the least fixed point of ΔFˆ equals the grounded extension of F.

Therefore, let ΔFˆ0=ΔFˆ(Fˆ<) and, for i>0, ΔFˆi=ΔFˆ(ΔFˆi−1). Likewise, for the operator Γ defined in Proposition 2.10, let ΓF0=ΓF(∅), and ΓFi=ΓF(ΓFi−1).

We now show, given an AF F=(A, R), that

ΓFi={a∈A∣in(a)∈ΔFˆi}(30)

holds for every i≥0. The proof is by induction on i.

Induction base

Suppose i=0 and let a∈ΓF0. We show that in(a)∈ΔFˆ0. Since a∈ΓF0 and ΓF0=ΓF(∅), a is not attacked in F, i.e. there is no c∈A with (c, a)∈R. By definition, arg(a)∈Fˆ<, and there is no c such that defeat(c,a)∈Fˆ<. Hence, in(a)∈ΔFˆ0 by construction. To show that, for each a∈A with in(a)∈ΔFˆ0, also a∈ΓF0 holds, can be done in a similar manner.

Induction step

Let i>0, and suppose Relation (30) holds for all 0≤j<i; in particular, we can assume that ΓFi−1={a∈A∣in(a)∈ΔFˆi−1} holds. Let a∈ΓFi∖ΓFi−1. We show in(a)∈ΔFˆi. Since a∈ΓFi, it must hold that for each c∈A with (c, a)∈R, there exists an argument d∈ΓFi−1 with (d, c)∈R. Therefore, in(d)∈ΔFˆi−1 holds by induction hypothesis. Moreover, we clearly have arg(e)∈ΔFˆi−1 for all e∈A, and defeat(e,f)∈ΔFˆi−1 for all (e, f)∈R (recall that Fˆ⊆ΔFˆi−1). Hence, we know that for each c with arg(c)∈ΔFˆi−1, such that defeat(c,a)∈ΔFˆi−1, there exists an argument d, such that defeat(d,c)∈ΔFˆi−1 and in(d)∈ΔFˆi−1. By definition, in(a)∈ΔFˆi. Again, the other direction is by similar arguments. ▪

Obviously, we could have used the defended(·) predicate in previous programs. Indeed, π_comp could be defined as

πcf∪π<∪πdefended∪{:−in(X),notdefended(X);:−out(X),defended(X)}.

We continue with the more involved encodings for preferred and semi-stable extensions. Compared with the one for admissible extensions, these encodings require an additional maximality test. However, this is quite complicate to encode and requires the use of disjunction, together with the saturation technique introduced in Section 2.1 for the encoding of the complement of the 3-colourability problem.

3.5.Preferred extensions

To compute the preferred extensions of an AF, we will use the saturation technique described in Section 2.1 as follows: Having computed an admissible extension S (characterised via predicates in(·) and out(·) using our encoding πadm(Fˆ)), we perform a second guess using new predicates, say inN(·) and outN(·), to represent a further guess T⊃ S. In order to check whether the first guess (via in(·) and out(·)) characterises a preferred extension, we have to ensure that no guess of the second form (i.e., via inN(·) and outN(·)) characterises an admissible extension. Recall that in Section 2.1, we already have seen how to encode (using the program πncol) such a complementary problem when we considered the problem of non-3-colourability. Here the saturation module looks as follows:

πsatpref={inN(X)∨outN(X):−out(X);(31){inN(X):−in(X);(32){fail:−eq;(33){fail:−inN(X),inN(Y),defeat(X,Y);(34){fail:−inN(X),outN(Y),defeat(Y,X),undefeated(Y);(35){inN(X):−fail,org(X);(36){outN(X):−fail,org(X);(37){:−notfail}.(38)

Let us for the moment also assume that predicates eq (rule (33)) and undefeated(·) (rule (35)) are defined (we will give the additional modules for those predicates below) and provide the following information:

• eq is derived if the guess S via in(·) and out(·) equals the second guess T via inN(·) and outN(·); in other words, eq is derived if S=T;
• undefeated(a) is derived if argument a is not defeated in F by the second guess T.

In what follows, we discuss the functioning of πsatpref when conjoined with the program πadm(Fˆ) from Section 3.2, for a given AF F. First, rule (31) guesses a set T⊆ A as already discussed above. Rule (32) ensures that the new guess satisfies S⊆ T (recall that S is characterised by predicates in(·) and out(·) from π_adm).

The task of the rules (33)–(35) is to check whether the new guess T is a proper superset of S and characterises an admissible extension of the given AF F. If this is not the case, we derive the predicate fail. More specifically, rule (33) checks whether S=T, and in case this holds we derive fail; rule (34) checks whether T is not conflict-free in F, and in case this holds we derive fail; rule (35) checks whether T contains an argument not defended by T in F, and in case this holds we derive fail. In other words, we have not derived fail if T⊃ S and T is admissible in F. By definition, S then cannot be a preferred extension of F.

The remaining rules (36)–(38) saturate the guess in case fail was derived, and finally ensure that fail has to be in an answer set. We already discussed the underlying idea of such rules for the program πncol in terms of the non-3-colourability encoding in Section 2.1 (see rules (12)–(15) of program πncol).

Let us illustrate now the behaviour of πsatpref for two scenarios. First, suppose the first guess S (via predicates in(·) and out(·)) is a preferred extension of the given AF F=(A, R). Hence, for each T⊃ S, T must not be admissible. But then, we have that every new guess T (via predicates inN(·) and outN(·)) derives fail. Due to the spoiling rules (36) and (37), we thus have no interpretation (without predicate fail) which satisfies πsatpref. However, the saturated interpretation (which contains fail and both inN(a) and outN(a) for each a∈A) does satisfy the program and also becomes an answer set of the program.

Now suppose the first guess S (via predicates in(·) and out(·)) is an admissible but not a preferred extension of the given AF F. Then there exists a set T⊃ S, such that T is admissible for F. If we consider the interpretation I characterising T (i.e. we have inN(a)∈I, for each a∈T, and outN(a)∈I, for each a∈A∖T), then I does not contain fail and satisfies the rules (31)–(37). But this shows that we cannot have an answer set J which characterises S. Due to rule (38) such an answer set J has to contain fail and by rules (36) and (37), J contains both inN(a) and outN(a) for each a∈A. Note that we thus have I⊂J (if I and J characterise the same initial guess S). Moreover, I satisfies the reduct of our program with respect to J. This can be seen by the fact that the only occurrence of default negation is in rule (38). In other words, there is an I⊂J satisfying the reduct and thus J cannot be an answer set. This, however, is as desired, since the initial guess S characterised by J is not a preferred extension.

We still have to define the rules for the predicates eq and undefeated(·). Basically, these predicates would be easy to define, but as we have seen in the discussion above, default negation plays a central rule in the saturation technique (recall the functioning of :−notfail). We therefore have to find encodings which suitably define the required predicates only with a limited use of negation. In fact, we are only allowed to have stratified negation in these modules. Therefore, we employ similar techniques as we have used for the predicate defended(·) as defined in Section 3.4 where we also required a stratified program. In fact, both predicates eq and undefeated(·) are computed via predicates eq_upto(·) (resp., undefeated_upto(·,·)) in the same manner as we used defended_upto(·,·) for defended(·) in the module πdefended in Section 3.4. We thus make use of the helper predicates from π_< as defined in the previous subsection and define

πeq={eq_upto(X):−inf(X),in(X),inN(X);{eq_upto(X):−inf(X),out(X),outN(X);{eq_upto(X):−succ(Y,X),in(X),inN(X),eq_upto(Y);{eq_upto(X):−succ(Y,X),out(X),outN(X),eq_upto(Y);{eq:−sup(X),eq_upto(X)};πundefeated={undefeated_upto(X,Y):−inf(Y),outN(X),outN(Y);{undefeated_upto(X,Y):−inf(Y),outN(X),notdefeat(Y,X);{undefeated_upto(X,Y):−succ(Z,Y),undefeated_upto(X,Z),undefeated_upto(X,Y):−outN(Y);{undefeated_upto(X,Y):−succ(Z,Y),undefeated_upto(X,Z),undefeated_upto(X,Y):−notdefeat(Y,X);{undefeated(X):−sup(Y),undefeated_upto(X,Y)}.

With these predicates at hand, we can now formally define the module for preferred extensions, πpref=πadm∪π<∪πeq∪πundefeated∪πsatpref. The general result is as follows.

Proposition 3.7

For any AF F, pref(F)≅AS(πpref(Fˆ)).

To illustrate how π_pref applies to our example framework, note that a step-by-step evaluation as used before is no longer possible. In particular, the sub-program Π=πeq∪πundefeated∪πsatpref has to be treated as a whole, due to the cyclic dependencies among the atoms (in other words, we obtain only trivial splitting sets for Π). However, we can still split π_pref into πadm∪π< and Π. We already know the single answer set S₀ of π<(Fˆ) (see Section 3.4) and the collection {S∅,Sa,Sc,Sd,Sac,Sad}=AS(πadm(Fˆ)) of answer sets of πadm(Fˆ) (see Section 3.2). As is easily checked, we get

AS(Fˆ∪πadm∪π<)={S0∪S∣S∈AS(πadm(Fˆ))}.

Hence, let us illustrate the program Π for the two inputs S1=S0∪Sa and S2=S0∪Sac (We omit the further atoms from the corresponding answer sets in Fˆ∪πadm∪π<, since they play no role in Π.). Indeed, we expect that S₁ does not lead to an answer set of πpref(Fˆ), while the second set S₂ corresponds to a preferred extension of F, and thus should be part of an answer set of πpref(Fˆ). As discussed above, the only potential answer set I₁ of Π(S₁) contains

S1∪{inN(a),inN(b),inN(c),inN(d),inN(e),{outN(a),outN(b),outN(c),outN(d),outN(e),fail}.

We next check whether some J1⊂I1 satisfies Π(S1)I1=Π(S1)∖{:−notfail}. If this is not the case, I₁ becomes an answer set. Indeed, one can check that the set J₁

Sa∪{inN(a),outN(b),inN(c),outN(d),outN(e)}

satisfies Π(S1)I1. This can be seen as follows: The above set J₁ does not contain fail, thus the bodies of rules (33–35) must not be satisfied. For the first rule, this is the case since eq is not derived (we leave it to the reader to check this), for the second rule this is the case as well, since the vertices for which inN(·) holds are not adjacent. Finally, for rule (35), we first mention that the predicate undefeated(·) is derived for the following instantiations undefeated(a), undefeated(c), undefeated(e). One can now check that the bodies of rule (35) are not satisfied. As well, rules (36) and (37) are not applied (since fail has not been derived). Thus, we found a proper subset J₁ of I₁, such that J1⊧Π(S1)I1. Consequently, I₁ cannot be an answer set of Π(S₁) and thus not of πpref(Fˆ).

The situation is different for set S2=S0∪Sac. As before, the only potential answer set I₂ of Π(S₂) contains

S2∪{inN(a),inN(b),inN(c),inN(d),inN(e),{outN(a),outN(b),outN(c),outN(d),outN(e),fail}.

Moreover, Π(S2)I2=Π(S2)∖{:−notfail} as before, and we thus seek for sets J2⊂I2, such that J2⊧Π(S2)I2. Note that rule (32) guarantees that J₂ contains at least inN(a),inN(c) but further inN(·) predicates could be contained in J₂. However, if the only inN(·) predicates in J₂ are inN(a),inN(c), predicate eq is derived and we saturate. As well, if a further inN(·) predicate is contained in J₂ then we already know that such a set characterises a subset S′⊆A which cannot be conflict-free. Indeed, rule (34) applies in this case, and we obtain fail. As soon as fail is derived, rules (36) and (37) “turn J₂ into I₂”. From this observation, it is clear that we cannot find a J2⊂I2, such that J2⊧Π(S2)I2. Thus I₂ becomes an answer set of Π(S₂) and therefore also of πpref(Fˆ). This meets our expectation, since S_ac relates to the preferred extension {a, c} of F.

3.6.Semi-stable extensions

We conclude our encodings for the different types of extensions with a query for the semi-stable semantics. The basic intuition for the forthcoming encoding is the same as for the preferred semantics. The main difference lies in the fact that, given an admissible extension S for an AF F=(A, R), we now have to test whether no T∈adm(F) with SR+⊂TR+ exists, while for preferred extensions, it was sufficient to test whether no such T exists for which S⊂T holds. This requires the following changes. First, we have to guess an arbitrary set T (for preferred extensions, we could restrict ourselves to supersets of S). Then we saturate (as before) in case T is not admissible. Finally, we explicitly get rid of the cases where SR+⊄TR+ (for preferred extensions, we only had to exclude the case S=T via the predicate eq). Hence, we need a new predicate eqplus which tests for S⁺_R=T⁺_R, and we saturate if eqplus is derived, or in case there exists an a∈S⁺_R not contained in T⁺_R.

We reuse the modules π_adm, π_<, as well as πundefeated and define the additional rules

πeq+={eqplus_upto(X):−inf(X),in(X),inN(X);{eqplus_upto(X):−inf(X),in(X),inN(Y),defeat(Y,X);{eqplus_upto(X):−inf(X),in(Y),inN(X),defeat(Y,X);{eqplus_upto(X):−inf(X),in(Y),inN(Z),defeat(Y,X),defeat(Z,X);{eqplus_upto(X):−inf(X),out(X),outN(X),notdefeated(X),eqplus_upto(X):−undefeated(X);{eqplus_upto(X):−succ(Z,X),in(X),inN(X),eqplus_upto(Z);{eqplus_upto(X):−succ(Z,X),in(X),inN(Y),defeat(Y,X),eqplus_upto(Z);{eqplus_upto(X):−succ(Z,X),in(Y),inN(X),defeat(Y,X),eqplus_upto(Z);{eqplus_upto(X):−succ(Z,X),in(Y),inN(U),defeat(Y,X),defeat(U,X),eqplus_upto(X):−eqplus_upto(Z);{eqplus_upto(X):−succ(Y,X),out(X),outN(X),notdefeated(X),eqplus_upto(X):−undefeated(X),eqplus_upto(Y);{eqplus:−sup(X),eqplus_upto(X)}

and

πsatsemi={inN(X)∨outN(X):−arg(X);{fail:−eqplus;{fail:−inN(X),inN(Y),defeat(X,Y);{fail:−inN(X),outN(Y),defeat(Y,X),undefeated(Y);{fail:−in(X),outN(X),undefeated(X);{fail:−in(Y),defeat(Y,X),outN(X),undefeated(X);{inN(X):−fail,arg(X);{outN(X):−fail,arg(X);{:−notfail}.

We define πsemi=πadm∪π<∪πeq+∪πundefeated∪πsatsemi and obtain the following result.

Proposition 3.8

For any AF F, semi(F)≅AS(πsemi(Fˆ)).

3.7.Summary and combinations of encodings

We summarise the results from this section.

Theorem 3.9

For any AF F ande∈{stable,adm,pref,semi,comp,ground}, it holds thate(F)≅AS(πe(Fˆ)).

We note that our encodings are adequate in the sense that the data complexity of the encodings mirrors the complexity of the encoded task. In fact, depending on the chosen reasoning task, the queries which have to be used are depicted in Table 3. Recall that credulous reasoning over preferred extensions reduces to credulous reasoning over admissible extensions and skeptical reasoning over complete extensions reduces to reasoning over the single grounded extension. The only proper disjunctive programs involved are π_pref and π_semi; all other encodings are disjunction-free. Moreover, πground is stratified and constraint-free. Recall that such programs have exactly one answer set; hence there is no need to distinguish between ⊧c and ⊧s. If one now assigns the complexity entries from Table 1 to the type of queries used in Table 3, one obtains Table 2. This shows that the complexity of the encoded decision problem of AFs meets the corresponding complexity of the employed datalog fragment.

Table 3.

Overview of the encodings of the reasoning tasks for AF F=(A, R) and a∈A.

	stable	adm	pref	semi	comp	ground
Crede	πstable(Fˆ)⊧ca	πadm(Fˆ)⊧ca	πadm(Fˆ)⊧ca	πsemi(Fˆ)⊧ca	πcomp(Fˆ)⊧ca	πground(Fˆ)⊧a
Skepte	πstable(Fˆ)⊧sa	(trivial)	πpref(Fˆ)⊧sa	πsemi(Fˆ)⊧sa	πground(Fˆ)⊧a	πground(Fˆ)⊧a

We are now able to encode more involved decision problems using our queries. As a first example, consider the Π2P-complete problem of coherence (Dunne and Bench-Capon 2002), which decides whether for a given AF F, pref(F)⊆stable(F) (recall that pref(F)⊇stable(F) always holds). We can decide this problem by extending π_pref in such a way that an answer set of π_pref survives only if it does not correspond to a stable extension. By definition, the only possibility to do so is if some undefeated argument is not contained in the extension.

Corollary 3.10

The coherence problem for an AF F holds iff the program

πpref(Fˆ)∪{v:−out(X),notdefeated(X);:−notv}

has no answer set.

As a second example, we give a program which decides, for a given AF F, whether the semi-stable and the preferred extension of F coincide. Dunne and Caminada (2008) have shown Π2P-completeness for this problem.

Again, we can decide this problem by reusing some of the modules from previous encodings. In this particular case, however, we need to separate some of the atoms which are used in common by π_pref and π_semi. For this reason, we require new atoms inNN(·), outNN(·), undefeatedN(·) and undefeatedN_upto(·,·), and denote by πundefeatedN the program resulting from πundefeated by using the new atoms instead of inN(·), outN(·), undefeated(·) and undefeated_upto(·,·), respectively. Similarly, we obtain πeqN+ from π_eq⁺. Consider now the following program.

πcoincide=πpref∪πundefeatedN∪πeqN+∪π{inNN(X)∨outNN(X):−arg(X);π:−eqplus;π:−inNN(X),inNN(Y),defeat(X,Y);π:−inNN(X),outNN(Y),defeat(Y,X),undefeatedN(Y);π:−in(X),outNN(X),undefeated(X);π:−in(Y),defeat(Y,X),outNN(X),undefeatedN(X)}.

Corollary 3.11

Given an AF F, it holds thatsemi(F)=pref(F)iffπcoincide(Fˆ)has no answer set.

Roughly speaking, we combine here the program which computes the preferred extensions with a program which checks whether the input is not semi-stable. The latter test can be accomplished via constraints (instead of the saturation technique used above), since it is sufficient here to just get rid off candidates which already have been checked to be preferred but are not semi-stable.

4.Encodings for generalisations of argumentation frameworks

In this section, we again show the flexibility of our approach by reusing the queries from the previous section in the context of generalisations of abstract AFs.

4.1.Value-based argumentation frameworks

As a first example for generalising basic AFs, we deal with value-based AFs (VAFs) (Bench-Capon 2003) which themselves generalise the preference-based AFs (Amgoud and Cayrol 2002). Again we give the definition w.r.t. the universe 𝒰.

Definition 4.1

A VAF is a 5-tuple F=(A, R, Σ, σ, <) whereA⊆Uare arguments, R⊆A×Adenotes the attack relation, Σ⊆Uis a non-empty set of values disjoint from A, σ:A→Σassigns a value to each argument from A and < is a preference relation (irreflexive, asymmetric) between values. Let ≪ be the transitive closure of <. An argument a∈A defeats an argument b∈A in F iff (a, b)∈R and(σ(b),σ(a))∉≪.

Example 4.2

Consider the following VAF F=(A, R, Σ, σ, <). Let A={a, b, c}, R={(b,a),(c,b)}, Σ={red,blue}, σ(a)=blue, σ(b)=blue, σ(c)=red, and <={(red,blue)}. The graph representation of F is as follows.

We obtain that c defeats b, because (c, b)∈R and (σ(b),σ(c))∉≪ holds. But, if (blue,red)∈<, this does not hold any longer.

Using this notion of defeat, we say in accordance with Definition 2.2 that a set S⊆ A of arguments defeats b in F, if there is an a∈S which defeats b.

An argument a∈A is defended by S ⊆ A in F iff, for each b∈A, it holds that, if b defeats a in F, then S defeats b in F. Using these notions of defeat and defence, the definitions in Bench-Capon (2003) for conflict-free sets, admissible extensions, and preferred extensions are exactly along the lines of Definitions 2.4, 2.6, and 2.7, respectively.

In order to compute these extensions for VAFs, we thus only need to slightly adapt the modules introduced in Section 3.

In fact, we now use, for a VAF F,

F˜={arg(a)∣a∈A}∪{att(a,b)∣(a,b)∈R}∪{val(a,σ(a))∣a∈A}∪{valpref(v,w)∣v<w}

and we require a further module, which obtains the defeat(·,·) relation accordingly:

πvaf={valpref(X,Y):−valpref(X,Z),valpref(Z,Y);{pref(X,Y):−valpref(U,V),val(X,U),val(Y,V);{defeat(X,Y):−att(X,Y),notpref(Y,X)}.

We obtain the following theorem using the new concepts for [Ftilde] and π_vaf, as well as reusing π_adm and π_pref from Section 3.

Theorem 4.3

For any VAF F ande∈{adm,pref}, e(F)≅AS(πvaf∪πe(Fˆ)).

For the other notions of extensions, we can employ our encodings from Section 3 in a similar way. The concrete composition of the modules however depends on the exact definitions, and whether they make use of the notion of a defeat in a uniform way.

In (Bench-Capon 2002), for instance, stable extensions for a VAF F are defined as those conflict-free subsets S of arguments, such that each argument not in S is attacked (rather than defeated) by S. Still, we can obtain a suitable encoding quite easily using the following redefined module:

πvaf_stable=πcf∪{attacked(X):−in(Y),att(Y,X);{:−out(X),notattacked(X)}.

Theorem 4.4

For any VAF F, stable(F)≅AS(πvaf∪πvaf_stable(Fˆ)).

The coherence problem for VAFs thus can be decided as follows.

Corollary 4.5

The coherence problem for a VAF F holds iff the program

πpref(Fˆ)∪{attacked(X):−in(Y),att(Y,X);{v:−out(X),notattacked(X);:−notv}

has no answer set.

4.2.Bipolar argumentation frameworks

Bipolar AFs (BAFs) (Cayrol and Lagasquie-Schiex 2005) augment basic AFs by a second relation between arguments which indicates supports independent from defeats.

Definition 4.6

A BAF is a tupleF=(A,Rd,Rs)whereA⊆Uis a set of arguments, andRd⊆A×AandRs⊆A×Aare the attack, and resp., support relation of F.

An argument a defeats an argument b in F if there exists a sequence a1,…,an+1 of arguments from A (for n≥1), such that a₁=a, and a_n+1=b, and either

• (ai,ai+1)∈Rs for each 1⩽i⩽n−1 and (an,an+1)∈Rd; or
• (a1,a2)∈Rd and (ai,ai+1)∈Rs for each 2≤i≤n.

A BAF can be represented by a directed graph called the bipolar interaction graph. In order to distinguish between the two relations, two kinds of edges are used. For two arguments a and b, (a, b)∈R_d is represented by a→b and (a, b)∈R_s is represented by a⇢b.

Example 4.7

Consider the following F=(A,Rd,Rs). Let A={a,b,c,d,e}, Rd={(a,e),(d,c)} and Rs={(a,b),(b,c),(d,e)}. Then the bipolar interaction graph looks as follows.

As before, we say that a set S⊆ A defeats an argument b in F if some a∈S defeats b. An argument a∈A is defended by S ⊆ A in F iff, for each b∈A, it holds that, if b defeats a in F, then S defeats b in F.

Again, we just need to adapt the input database and incorporate the new defeat-relation. Other modules from Section 3 can then be reused. In fact, we define for a given BAF F=(A,Rd,Rs),

F¯={arg(a)∣a∈A}∪{att(a,b)∣(a,b)∈Rd}∪{support(a,b)∣(a,b)∈Rs},

and for the defeat relation, we first compute the transitive closure of the support(·,·) predicate and then define defeat(·,·) accordingly.

πbaf={support(X,Y):−support(X,Z),support(Z,Y);{defeat(X,Y):−att(X,Y);{defeat(X,Y):−att(Z,Y),support(X,Z);{defeat(X,Y):−att(X,Z),support(Z,Y)}.

Following Cayrol and Lagasquie-Schiex (2005), we can use this notion of defeat to define conflict-free sets, stable extensions, admissible extensions, and preferred extensions (these extensions are respectively called d-admissible and d-preferred in Cayrol and Lagasquie-Schiex (2005)) exactly along the lines of Definitions 2.4–2.7, respectively.

Theorem 4.8

For any BAF F ande∈{stable,adm,pref}, e(F)≅AS(πbaf∪πe(Fˆ)).

More specific variants of admissible extensions from Cayrol and Lagasquie-Schiex (2005) are obtained by replacing the notion of a conflict-free set by other concepts.

Definition 4.9

LetF=(A,Rd,Rs)be a BAF and S⊆ A. Then S is called safe in F if for each a∈A, such that S defeats a, a∉S and there is no sequencea1,…,an (n≥2), such that a₁∈S, a_n=a, and(ai,ai+1)∈Rs, for each1⩽i⩽n−1. A set S is closed under R_sif, for each (a, b)∈R_s, it holds that a∈S if and only if b∈S.

Note that for a BAF F, each safe set in F is conflict-free in F. We also remark that a set S of arguments is closed under R_s iff S is closed under the transitive closure of R_s.

Definition 4.10

LetF=(A,Rd,Rs)be a BAF. A set S⊆ A is called an s -admissible extension of F if S is safe in F and each a∈S is defended by S in F. A set S⊆ A is called a c -admissible extension of F if S is closed under R_s, conflict-free in F, and each a∈S is defended by S in F. We denote the collection of all s -admissible extensions (resp., of all c -admissible extensions) of F by sadm(F) (resp., by cadm(F)).

We define now further programs as follows:

πsadm=πadm∪{supported(X):−in(Y),support(Y,X);πcadm=:−supported(X),defeated(X)};πcadm=πadm∪{:−support(X,Y),in(X),out(Y);πcadm=:−support(X,Y),out(X),in(Y)}.

The two constraints in π_cadm rule out, according to the definition of closed sets, all answer sets where (a, b)∈R_s but either a∈S and b¬∈S or a¬∈S and b∈S (note that the relation support is not symmetric).

Finally, one defines s-preferred (resp., c-preferred) extensions as maximal (w.r.t. set-inclusion) s-admissible (resp., c-admissible) extensions.

Definition 4.11

LetF=(A,Rd,Rs)be a BAF. A set S⊆ A is called an s -preferred extension of F ifS∈sadm(F)and for eachT∈sadm(F), S⊄T. Likewise, a set S⊆ A is called a c -preferred extension of F ifS∈cadm(F)and for eachT∈cadm(F), S⊄T. By spref(F) (resp., cpref(F)) we denote the collection of all s -preferred extensions (resp., of all c -preferred extensions) of F.

For the framework F from Example 4.7, we obtain pref(F)={{a,b,d}}, spref(F)={{d},{a,b}}, and cpref(F)={∅}.

Again, we can reuse parts of the program π_pref from Section 3. The only addition necessary is to saturate in case the additional requirements are violated.

We define

πspref=πsadm∪π<∪πeq∪πundefeated∪πsatpref∪π{supported(X):−inN(Y),support(Y,X);πfail:−supported(X),defeated(X)};πcpref=πcadm∪π<∪πeq∪πundefeated∪πsatpref∪π{fail:−support(X,Y),inN(X),outN(Y);πfail:−support(X,Y),outN(X),inN(Y)}.

Theorem 4.12

For any BAF F ande∈{sadm,cadm,spref,cpref}, we havee(F)≅AS(πbaf∪πe(Fˆ)).

Slightly different semantics for BAFs occur in Amgoud et al. (2008), where the notion of defence is based on R_d, while the notion of conflict remains evaluated with respect to the more general concept of defeat as given in Definition 4.6. However, also such variants can be encoded within our system by a suitable composition of the concepts introduced so far.

Again, we note that we can put together encodings for complete and grounded extensions for BAFs, which, to the best of our knowledge, have not been studied in the literature yet.

5.Discussion

In this work we provided ASP-encodings for computing different types of extensions in Dung's AF as well as in some recent extensions of it. Our system ASPARTIX, together with some illustrating examples, is available at www.dbai.tuwien.ac.at/research/project/argumentation/systempage/

Besides the types of extensions discussed in this paper, the current version of ASPARTIX also implements the recently proposed concept of ideal semantics (Dung, Mancarella, and Toni 2007). For the respective encoding for ideal semantics, we refer to the paper by Faber and Woltran (2009).

To the best of our knowledge, so far no system is available which supports such a broad range of different semantics, although nowadays a reasonable number of different implementations exists. (See http://wyner.info/LanguageLogicLawSoftware/index.php/software/ for an overview.) In short, one can divide these systems into two categories: graphical representation of AFs and computation of acceptable arguments. The first category contains systems like Argunet (http://www.argunet.org/debates/) and Araucaria (Reed and Rowe 2004). To the second category belong systems like:

• ArgKit (South, Vreeswijk, and Fox 2008), a Java reasoner capable of reasoning with grounded and preferred extensions which can be integrated in Araucaria.
• A system by Verheij (2007) which computes grounded, preferred, stable and semi-stable semantics via labelings.
• The epistemic and practical reasoner by Visser (2008) which is an implementation of an argument-based practical reasoning system. From a given belief base of formulas (in a propositional modal logic with a single modality D standing for desire) and a query formula, one selects between different argument games including one for grounded semantics and one for credulous reasoning over admissible extensions.
• PARMENIDES (Cartwright and Atkinson 2008), a system for e-democracy that makes use of argumentation tools including VAFs.
• CASAPI (Gaertner and Toni 2007), a Prolog implementation for credulous and sceptical argumentation based upon the computation of dispute derivations for grounded, admissible and ideal beliefs for the generalised assumption-based frameworks.
• An implementation of a query-answering algorithm due to Vreeswijk (2006) for grounded and admissible semantics. Compared with the other systems, this algorithm computes the so-called defence sets around the queried argument rather than the entire collection of extensions.
• An implementation (Efstathiou and Hunter 2008) for logic-based formalisations of argumentation (Besnard and Hunter 2001), which constructs arguments using connection graphs.

The work which is related closest to ours is by Nieves et al. (2008, 2009) who also suggested to use ASP for computing extensions of AFs. One aspect in their work is to use a fixed encoding schema to represent AFs as logic programs, and then show how different semantics for logic programs can be used to compute different forms of extensions using this particular schema. Most notably, they showed that in their setting the stable semantics (for logic programs) captures stable extensions of AFs, the well-founded semantics captures the grounded extension of AFs, and a novel stratification semantics (Nieves et al. 2009) captures the CF2 semantics due to Baroni, Giacomin and Guida (2005). Osorio et al. (2005) present an algorithm for computing preferred extensions (based on abductive logic programming) using a fixed logic program to characterise the admissible sets in the same manner we have used here. In Nieves et al. (2008), a different approach to compute preferred extensions by means of logic programs has been proposed. However, this work requires a recompilation of the encoding for each particular AF. Similarly, Wakaki and Nitta (2008) also provide ASP encodings for different semantics. In contrast to our work, their encodings for complete and stable semantics are based on labellings, whereas for grounded, preferred and semi-stable semantics they use a meta-programming technique by applying additional translations for each AF into normal logic programs. We recall that in our system, fixed disjunctive queries which require the actual instance just as an input database are used for all these semantics. We believe that our approach is thus more reliable and easily extendible to further formalisms.

Future work includes a comparison of the efficiency of different implementations. Preliminary tests show that our approach is able to deal with more than 100 arguments for all considered semantics in Dung's abstract framework. Another direction of future work is to extend our system by incorporating further recent notions of semantics. In particular, it is planned to implement the resolution-based semantics due to Baroni and Giacomin (2008a), semantics based on decomposition into strongly connected components (like, for instance, the CF2 semantics) due to Baroni et al. (2005), novel approaches to preferential semantics due to Amgoud and Vesic (2009), and semantics based on meta-attacks as introduced by Modgil (2009).

Acknowledgements

The authors thank the anonymous referees for valuable comments which helped in improving the paper. This work was supported by the Austrian Science Fund (FWF) under the grant P20704-N18 and the Vienna Science and Technology Fund (WWTF) under the grant ICT08-028. A short version of this article was presented at the Proceedings of the ICLP’08 Workshop Answer-Set Programming and Other Computing Paradigms (ASPOCP).

References

1	Amgoud, L. and Cayrol, C. (2002) . A Reasoning Model Based on the Production of Acceptable Arguments. Annals of Mathematics and Artificial Intelligence, 34: : 197–215.
2	Amgoud, L. and Vesic, S. Repairing Preference-Based Argumentation Frameworks. Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009). pp. 665–670.
3	Amgoud, L., Cayrol, C., Lagasquie-Schiex, M.C. and Livet, P. (2008) . On Bipolarity in Argumentation Frameworks. International Journal of Intelligent Systems, 23: : 1–32.
4	Apt, K.R., Blair, H.A. and Walker, A. (1988) . “Towards a Theory of Declarative Knowledge”. In Foundations of Deductive Databases and Logic Programming, Edited by: Minker, J. 89–148. Morgan Kaufmann Publishers, Inc.
5	Baroni, P. and Giacomin, M. Resolution-based Argumentation Semantics. Proceedings of the 2nd Conference on Computational Models of Argument (COMMA 2008). Edited by: Besnard, P., Doutre, S. and Hunter, A. pp. 25–36. Toulouse: IOS Press. Vol. 172 of Frontiers in Artificial Intelligence and Applications
6	Baroni, P. and Giacomin, M. A Systematic Classification of Argumentation Frameworks Where Semantics Agree. Proceedings of the 2nd Conference on Computational Models of Argument (COMMA 2008). Edited by: Besnard, P., Doutre, S. and Hunter, A. pp. 37–48. Toulouse: IOS Press. Vol. 172 of Frontiers in Artificial Intelligence and Applications
7	Baroni, P., Giacomin, M. and Guida, G. (2005) . SCC-Recursiveness: A General Schema for Argumentation Semantics. Artificial Intelligence, 168: : 162–210.
8	Bench-Capon, T.J.M. Value-based Argumentation Frameworks. Proceedings of the 9th International Workshop on Non-Monotonic Reasoning (NMR 2002). Edited by: Benferhat, S. and Giunchiglia, E. pp. 443–454. Toulouse
9	Bench-Capon, T.J.M. (2003) . Persuasion in Practical Argument Using Value-based Argumentation Frameworks. Journal of Logic and Computation, 13: : 429–448.
10	Bench-Capon, T.J.M. and Dunne, P.E. (2007) . Argumentation in Artificial Intelligence. Artificial Intelligence, 171: : 619–641.
11	Besnard, P. and Doutre, S. Checking the Acceptability of a Set of Arguments. Proceedings of the 10th International Workshop on Non-Monotonic Reasoning (NMR 2004). Edited by: Delgrande, J.P. and Schaub, T. pp. 59–64. Whistler
12	Besnard, P. and Hunter, A. (2001) . A Logic-based Theory of Deductive Arguments. Artificial Intelligence, 128: : 203–235.
13	Besnard, P., Hunter, A. and Woltran, S. (2009) . Encoding Deductive Argumentation in Quantified Boolean Formulae. Artificial Intelligence, 173: : 1406–1423.
14	Caminada, M. Semi-Stable Semantics. Proceedings of the 1st Conference on Computational Models of Argument (COMMA 2006). Edited by: Dunne, P.E. and Bench-Capon, T.J.M. pp. 121–130. Liverpool: IOS Press. Vol. 144 of Frontiers in Artificial Intelligence and Applications
15	Cartwright, D. and Atkinson, K. Political Engagement Through Tools for Argumentation. Proceedings of the 2nd Conference on Computational Models of Argument (COMMA 2008). Edited by: Besnard, P., Doutre, S. and Hunter, A. pp. 116–127. Toulouse: IOS Press. Vol. 172 of Frontiers in Artificial Intelligence and Applications
16	Cayrol, C. and Lagasquie-Schiex, M.C. On the Acceptability of Arguments in Bipolar Argumentation Frameworks. Proceedings of the 8th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2005). Edited by: Godo, L. pp. 378–389. Barcelona: Springer. Vol. 3571 of LNCS
17	Coste-Marquis, S., Devred, C. and Marquis, P. Symmetric Argumentation Frameworks. Proceedings of the 8th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2005). Edited by: Godo, L. pp. 317–328. Barcelona: Springer. Vol. 3571 of LNCS
18	Dantsin, E., Eiter, T., Gottlob, G. and Voronkov, A. (2001) . Complexity and Expressive Power of Logic Programming. ACM Computing Surveys, 33: : 374–425.
19	Dimopoulos, Y. and Torres, A. (1996) . Graph Theoretical Structures in Logic Programs and Default Theories. Theoretical Computer Science, 170: : 209–244.
20	Dung, P.M. (1995) . On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games. Artificial Intelligence, 77: : 321–358.
21	Dung, P.M., Mancarella, P. and Toni, F. (2007) . Computing Ideal Sceptical Argumentation. Artificial Intelligence, 171: : 642–674.
22	Dunne, P.E. and Bench-Capon, T.J.M. (2002) . Coherence in Finite Argument Systems. Artificial Intelligence, 141: : 187–203.
23	Dunne, P.E. and Bench-Capon, T.J.M. Complexity in Value-Based Argument Systems. Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004). Edited by: Alferes, J.J. and Leite, J.A. pp. 360–371. Lisbon: Springer. Vol. 3229 of LNCS
24	Dunne, P.E. and Caminada, M. Computational Complexity of Semi-Stable Semantics in Abstract Argumentation Frameworks. Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA 2008). Edited by: Hölldobler, S., Lutz, C. and Wansing, H. pp. 153–165. Dresden: Springer. Vol. 5293 of LNCS
25	Dvořák, W. and Woltran, S. (2009) . Technical Note: Complexity of Stage Semantics in Argumentation Frameworks. Technical Report DBAI-TR-2009-66, Technische Universität Wien, Database and Artificial Intelligence Group
26	Efstathiou, V. and Hunter, A. Algorithms for Effective Argumentation in Classical Propositional Logic: A Connection Graph Approach. Proceedings of the 5th International Symposium on Foundations of Information and Knowledge Systems, (FoIKS 2008). Edited by: Hartmann, S. and Kern-Isberner, G. pp. 272–290. Pisa: Springer. February, Vol. 4932 of Lecture Notes in Computer Science
27	Egly, U. and Woltran, S. Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas. Proceedings of the 1st Conference on Computational Models of Argument (COMMA 2006). Edited by: Dunne, P.E. and Bench-Capon, T.J.M. pp. 133–144. Liverpool: IOS Press. Vol. 144 of Frontiers in Artificial Intelligence and Applications
28	Eiter, T. and Polleres, A. (2006) . Towards Automated Integration of Guess and Check Programs in Answer Set Programming: A Meta-Interpreter and Applications. Theory and Practice of Logic Programming, 6: : 23–60.
29	Eiter, T., Gottlob, G. and Mannila, H. (1997) . Disjunctive Datalog. ACM Transactions on Database Systems, 22: : 364–418.
30	Faber, W. and Woltran, S. Manifold Answer-Set Programs for Meta-Reasoning. Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2009). Edited by: Erdem, E., Lin, F. and Schaub, T. pp. 115–128. Potsdam: Springer. Vol. 5753 of LNCS
31	Gaertner, D. and Toni, F. CaSAPI – A System for Credulous and Sceptical Argumentation. Proceedings of the First International Workshop on Argumentation and Nonmonotonic Reasoning (ArgNMR 2007). Edited by: Simari, G.R. and Torroni, P. pp. 80–95. May, Arizona
32	Gebser, M., Liu, L., Namasivayam, G., Neumann, A., Schaub, T. and Truszczyński, M. The First Answer Set Programming System Competition. Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2007). Edited by: Baral, C., Brewka, G. and Schlipf, J.S. pp. 3–17. Tempe, AZ, , USA: Springer. Vol. 4483 of LNCS
33	Gelfond, M. and Lifschitz, V. (1991) . Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9: : 365–386.
34	Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S. and Scarcello, F. (2006) . The DLV System for Knowledge Representation and Reasoning. ACM Transactions on Computational Logic, 7: : 499–562.
35	Lifschitz, V. and Turner, H. Splitting a Logic Program. Proceedings of the 11th International Conference on Logic Programming (ICLP’94). pp. 23–37. Santa Margherita Ligure: MIT Press.
36	Modgil, S. (2009) . Reasoning about Preferences in Argumentation Frameworks. Artificial Intelligence, 173: : 901–934.
37	Niemelä, I. (1999) . Logic Programming with Stable Model Semantics as a Constraint Programming Paradigm. Annals of Mathematics and Artificial Intelligence, 25: : 241–273.
38	Nieves, J.C., Osorio, M. and Cortés, U. (2008) . Preferred Extensions as Stable Models. Theory and Practice of Logic Programming, 8: : 527–543.
39	Nieves, J.C., Osorio, M. and Zepeda, C. Expressing Extension-Based Semantics Based on Stratified Minimal Models. Proceedings of the 16th International Workshop on Logic, Language, Information and Computation, (WoLLIC 2009). Edited by: Ono, H., Kanazawa, M. and de Queiroz, R.J.G.B. pp. 305–319. Tokyo: Springer. Vol. 5514 of LNCS
40	Osorio, M., Zepeda, C., Nieves, J.C. and Cortés, U. Inferring Acceptable Arguments with Answer Set Programming. Proceedings of the 6th Mexican International Conference on Computer Science (ENC 2005). pp. 198–205. Puebla: IEEE Computer Society.
41	Reed, C. and Rowe, G. (2004) . Araucaria: Software for Argument Analysis, Diagramming and Representation. International Journal on Artificial Intelligence Tools (IJAIT), 13: : 961–979.
42	South, M., Vreeswijk, G. and Fox, J. Dungine: A Java Dung Reasoner. Proceedings of the 2nd Conference on Computational Models of Argument (COMMA 2008). Edited by: Besnard, P., Doutre, S. and Hunter, A. pp. 360–368. Toulouse: IOS Press. Vol. 172 of Frontiers in Artificial Intelligence and Applications
43	van Emden, M. and Kowalski, R. (1976) . The Semantics of Predicate Logic as a Programming Language. Journal of the ACM, 23: : 733–742.
44	Verheij, B. A Labeling Approach to the Computation of Credulous Acceptance in Argumentation. Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007). Edited by: Veloso, M.M. pp. 623–628. Hyderabad: AAAI Press.
45	Visser, W. (2008) . “Implementation of Argument-Based Practical Reasoning”. Master's thesis, Utrecht University
46	Vreeswijk, G. An Algorithm to Compute Minimally Grounded and Admissible Defence Sets in Argument Systems. Proceedings of the 1st Conference on Computational Models of Argument (COMMA 2006). Edited by: Dunne, P.E. and Bench-Capon, T.J.M. pp. 109–120. Liverpool: IOS Press. Vol. 144 of Frontiers in Artificial Intelligence and Applications
47	Wakaki, T. and Nitta, K. Computing Argumentation Semantics in Answer Set Programming. New Frontiers in Artificial Intelligence (JSAI 2008), Conference and Workshops. Edited by: Hattori, H., Kawamura, T., Idé, T., Yokoo, M. and Murakami, Y. pp. 254–269. Asahikawa: Springer. Vol. 5447 of LNCS

Abstract

1.Motivation

2.Preliminaries

2.1.Answer-set programming

Proposition 2.1

Table 1.

2.2.Basic argumentation frameworks

Definition 2.2

Example 2.3

Definition 2.4

Definition 2.5

Definition 2.6

Definition 2.7

Definition 2.8

Definition 2.9

Figure 1.

Table 2.

Proposition 2.10

3.ASP-encodings for abstract argumentation frameworks

Definition 3.1

Proposition 3.2

Proof

3.1.Stable extensions

Proposition 3.3

Proof

3.2.Admissible extensions

Proposition 3.4

3.3.Complete extensions

Proposition 3.5

3.4.Grounded extension

Proposition 3.6

Proof

Induction base

Induction step

3.5.Preferred extensions

Proposition 3.7

3.6.Semi-stable extensions

Proposition 3.8

3.7.Summary and combinations of encodings

Theorem 3.9

Table 3.

Corollary 3.10

Corollary 3.11

4.Encodings for generalisations of argumentation frameworks

4.1.Value-based argumentation frameworks

Definition 4.1

Example 4.2

Theorem 4.3

Theorem 4.4

Corollary 4.5

4.2.Bipolar argumentation frameworks

Definition 4.6

Example 4.7

Theorem 4.8

Definition 4.9

Definition 4.10

Definition 4.11

Theorem 4.12

5.Discussion

Acknowledgements

References

Share this:

North America

Europe

Asia