Answer-set programming encodings for argumentation frameworks

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 ${\mathrm{\Sigma }}_2^{\mathit{P}}$ and to ${\mathrm{\Pi }}_2^{\mathit{P}}$ . 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 $${\mathit{a}}_1\vee \cdots \vee {\mathit{a}}_{\mathit{n}}:-{\mathit{b}}_1\mathrm{,}\dots \mathrm{,}{\mathit{b}}_{\mathit{k}}\mathrm{,}\mathrm{not}{\mathit{b}}_{\mathit{k}+1}\mathrm{,}\dots \mathrm{,}\mathrm{not}{\mathit{b}}_{\mathit{m}}$$ with n≥0, m≥k≥0, n+m>0, and where ${\mathit{a}}_1\mathrm{,}\dots \mathrm{,}{\mathit{a}}_{\mathit{n}}\mathrm{,}{\mathit{b}}_1\mathrm{,}\dots \mathrm{,}{\mathit{b}}_{\mathit{m}}$ are atoms, and “not ” stands for default negation.

The head of r is the set H(r) = $\{{\mathit{a}}_1\mathrm{,}\dots \mathrm{,}{\mathit{a}}_{\mathit{n}}\}$ and the body of r is $\mathit{B}\mathrm{(}\mathit{r}\mathrm{)}=\{{\mathit{b}}_1\mathrm{,}\dots \mathrm{,}{\mathit{b}}_{\mathit{k}}\mathrm{,}\text{not}{\mathit{b}}_{\mathit{k}+1}\mathrm{,}\dots \mathrm{,}$ $\text{not}{\mathit{b}}_{\mathit{m}}\}$ . Furthermore, B⁺(r) = $\{{\mathit{b}}_1\mathrm{,}\dots \mathrm{,}{\mathit{b}}_{\mathit{k}}\}$ and B⁻(r) = $\{{\mathit{b}}_{\mathit{k}+1}\mathrm{,}\dots \mathrm{,}{\mathit{b}}_{\mathit{m}}\}$ . 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 $\mathit{\alpha }\mathrm{(}·\mathrm{)}$ 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

in the positive body of r, then $\mathit{\alpha }\mathrm{(}\mathit{p}\mathrm{)}⩾\mathit{\alpha }\mathrm{(}\mathit{q}\mathrm{)}$ holds;

in the negative body of r, then $\mathit{\alpha }\mathrm{(}\mathit{p}\mathrm{)}\mathrm{>}\mathit{\alpha }\mathrm{(}\mathit{q}\mathrm{)}$ holds.

As an example, consider the following program Π: $$\mathrm{\Pi }=\{\mathit{a}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{not}\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathit{d}\mathrm{(}\mathit{X}\mathrm{)};\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}:-\mathit{a}\mathrm{(}\mathit{X}\mathrm{)}\}.$$ In order to find an assignment $\mathit{\alpha }\mathrm{(}·\mathrm{)}$ satisfying the above conditions for Π, observe that the first rule of Π requires $\mathit{\alpha }\mathrm{(}\mathit{a}\mathrm{)}\mathrm{>}\mathit{\alpha }\mathrm{(}\mathit{b}\mathrm{)}$ , but the second rule, in turn, forces $\mathit{\alpha }\mathrm{(}\mathit{b}\mathrm{)}⩾\mathit{\alpha }\mathrm{(}\mathit{a}\mathrm{)}$ . In other words, each assignment $\mathit{\alpha }\mathrm{(}·\mathrm{)}$ violates at least one of the conditions, and hence, Π is not stratified.

For the program $${\mathrm{\Pi }}^{\prime }=\{\mathit{a}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{not}\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathit{d}\mathrm{(}\mathit{X}\mathrm{)};\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}:-\mathit{c}\mathrm{(}\mathit{X}\mathrm{)};\mathit{c}\mathrm{(}\mathit{X}\mathrm{)}:-\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}\}\mathrm{,}$$ we can use the assignment $\mathit{\alpha }\mathrm{(}\mathit{a}\mathrm{)}=2\mathrm{,}\mathit{\alpha }\mathrm{(}\mathit{b}\mathrm{)}=\mathit{\alpha }\mathrm{(}\mathit{c}\mathrm{)}=\mathit{\alpha }\mathrm{(}\mathit{d}\mathrm{)}=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 ${\mathcal{U}}_{\mathrm{\Pi }}$ be the set of all constants appearing in Π (if no constant appears in Π, an arbitrary constant is added to ${\mathcal{U}}_{\mathrm{\Pi }}$ ), and let B_Π be the set of all ground atoms constructible from the predicate symbols appearing in Π and the constants of ${\mathcal{U}}_{\mathrm{\Pi }}$ . Moreover, Gr(Π) is the set of rules rσ obtained by applying, to each rule $\mathit{r}\in \mathrm{\Pi }$ , all possible substitutions σ from the variables in Π to elements of ${\mathcal{U}}_{\mathrm{\Pi }}$ .

Let the set of all ground atoms over 𝒰 be denoted by ${\mathit{B}}_{\mathcal{U}}$ . An interpretation $\mathit{I}\subseteq {\mathit{B}}_{\mathcal{U}}$ satisfies a ground rule r iff $\mathit{H}\mathrm{(}\mathit{r}\mathrm{)}\cap \mathit{I}\ne \varnothing$ whenever ${\mathit{B}}^{+}\mathrm{(}\mathit{r}\mathrm{)}\subseteq \mathit{I}$ and ${\mathit{B}}^{-}\mathrm{(}\mathit{r}\mathrm{)}\cap \mathit{I}=\varnothing$ . 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 $\mathit{I}\subseteq {\mathit{B}}_{\mathcal{U}}$ is an answer set of Π iff it is a subset-minimal set satisfying the Gelfond–Lifschitz reduct $${\mathrm{\Pi }}^{\mathit{I}}=\{\mathit{H}\mathrm{(}\mathit{r}\mathrm{)}:-{\mathit{B}}^{+}\mathrm{(}\mathit{r}\mathrm{)}\mid \mathit{I}\cap {\mathit{B}}^{-}\mathrm{(}\mathit{r}\mathrm{)}=\varnothing \mathrm{,}\mathit{r}\in \mathit{Gr}\mathrm{(}\mathrm{\Pi }\mathrm{)}\}.$$ For a program Π, we denote the set of its answer sets by $\mathcal{AS}\mathrm{(}\mathrm{\Pi }\mathrm{)}$ . We note that for each $\mathit{I}\in \mathcal{AS}\mathrm{(}\mathrm{\Pi }\mathrm{)}$ , $\mathit{I}\subseteq {\mathcal{B}}_{\mathrm{\Pi }}$ 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 $\mathrm{edge}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}$ , 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 $\mathrm{start}\mathrm{(}\mathit{a}\mathrm{)}$ 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 $\mathrm{reached}\mathrm{(}·\mathrm{)}$ in the following program: $$\begin{array}{cc}{\mathit{\pi }}_{\mathrm{reach}}\hfill & =\{\mathrm{reached}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{start}\mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \mathrm{reached}\mathrm{(}\mathit{Y}\mathrm{)}:-\mathrm{reached}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{edge}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\}\hfill \end{array}$$ Given an input database D as specified above, we get that predicate $\mathrm{reached}\mathrm{(}\mathit{b}\mathrm{)}$ is in the answer set of ${\mathit{\pi }}_{\mathrm{reach}}\mathrm{(}\mathit{D}\mathrm{)}$ iff vertex b is reachable in G from the designated start vertex a. Note that ${\mathit{\pi }}_{\mathrm{reach}}$ does neither contain disjunction nor negation. Moreover, there is no constraint in ${\mathit{\pi }}_{\mathrm{reach}}$ , hence ${\mathit{\pi }}_{\mathrm{reach}}\mathrm{(}\mathit{D}\mathrm{)}$ has exactly one answer set, for each input database D. Minimality of the answer-set semantics guarantees that the answer set of ${\mathit{\pi }}_{\mathrm{reach}}\mathrm{(}\mathit{D}\mathrm{)}$ does not contain predicates $\mathrm{reached}\mathrm{(}\mathit{c}\mathrm{)}$ , 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 ${\mathrm{\Pi }}_{\mathit{S}}^{\mathit{t}}$ , 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 ${\mathrm{\Pi }}_{\mathit{S}}^{\mathit{b}}=\mathrm{\Pi }\setminus {\mathrm{\Pi }}_{\mathit{S}}^{\mathit{t}}$ . To have an example, recall the program ${\mathrm{\Pi }}^{\prime }=\{\mathit{a}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{not}\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathit{d}\mathrm{(}\mathit{X}\mathrm{)};\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}:-\mathit{c}\mathrm{(}\mathit{X}\mathrm{)};\mathit{c}\mathrm{(}\mathit{X}\mathrm{)}:-\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}\}$ . The set S={b, c} is a splitting set for Π′, and we obtain ${\mathrm{(}{\mathrm{\Pi }}^{\prime }\mathrm{)}}_{\mathit{S}}^{\mathit{t}}=\{\mathit{a}\mathrm{(}\mathit{X}\mathrm{)}$ : $-\mathrm{not}\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathit{d}\mathrm{(}\mathit{X}\mathrm{)}\}$ and ${\mathrm{(}{\mathrm{\Pi }}^{\prime }\mathrm{)}}_{\mathit{S}}^{\mathit{b}}=\{\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}:-\mathit{c}\mathrm{(}\mathit{X}\mathrm{)};\mathit{c}\mathrm{(}\mathit{X}\mathrm{)}:-\mathit{b}\mathrm{(}\mathit{X}\mathrm{)}\}$ . 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 let $\mathit{I}\subseteq {\mathit{B}}_{\mathcal{U}}$ . Then $\mathit{I}\in \mathcal{AS}\mathrm{(}\mathrm{\Pi }\mathrm{)}$ iff $\mathit{I}\in \mathcal{AS}\mathrm{(}{\mathrm{\Pi }}_{\mathit{S}}^{\mathit{t}}\mathrm{(}\mathit{J}\mathrm{)}\mathrm{)}$ , where $\mathit{J}=\mathit{I}\cap {\mathit{B}}_{{\mathrm{\Pi }}_{\mathit{S}}^{\mathit{b}}}$ and $\mathit{J}\in \mathcal{AS}\mathrm{(}{\mathrm{\Pi }}_{\mathit{S}}^{\mathit{b}}\mathrm{)}$ .

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 $\mathrm{vertex}\mathrm{(}·\mathrm{)}$ and its edges via the predicate $\mathrm{edge}\mathrm{(}·\mathrm{,}·\mathrm{)}$ . We employ default negation to guess a colour for each node in the graph, and then check whether adjacent vertices have indeed different colours. $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{col}}& ={\mathit{\pi }}_{\mathrm{guess}}\cup {\mathit{\pi }}_{\mathrm{check}}\text{where}\hfill \\ \hfill {\mathit{\pi }}_{\mathrm{guess}}& =\{\mathrm{red}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{vertex}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{green}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{blue}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}1\mathrm{)}\\ \hfill & \mathrm{green}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{vertex}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{red}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{blue}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}2\mathrm{)}\\ \hfill & \mathrm{blue}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{vertex}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{red}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{green}\mathrm{(}\mathit{X}\mathrm{)}\}\hfill & \hfill \mathrm{(}3\mathrm{)}\\ \hfill {\mathit{\pi }}_{\mathrm{check}}& =\{\mathrm{fail}:-\mathrm{red}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{red}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{edge}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill & \hfill \mathrm{(}4\mathrm{)}\\ \hfill & \mathrm{fail}:-\mathrm{green}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{green}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{edge}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill & \hfill \mathrm{(}5\mathrm{)}\\ \hfill & \mathrm{fail}:-\mathrm{blue}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{blue}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{edge}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill & \hfill \mathrm{(}6\mathrm{)}\\ \hfill & :-\mathrm{fail}\}\hfill & \hfill \mathrm{(}7\mathrm{)}\end{array}$$

The three rules of ${\mathit{\pi }}_{\mathrm{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 $\{\mathrm{vertex}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{vertex}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{vertex}\mathrm{(}\mathit{c}\mathrm{)}\}$ . Then, the program ${\mathit{\pi }}_{\mathrm{guess}}\mathrm{(}\mathit{D}\mathrm{)}$ possesses 27 answer sets, namely $$\mathit{D}\cup \{\mathrm{red}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{red}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{red}\mathrm{(}\mathit{c}\mathrm{)}\}\mathrm{,}\mathit{D}\cup \{\mathrm{red}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{red}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{green}\mathrm{(}\mathit{c}\mathrm{)}\}\mathrm{,}\dots$$ 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 ${\mathit{\pi }}_{\mathrm{guess}}$ is not stratified. Indeed, we would require a mapping $\mathit{\alpha }\mathrm{(}·\mathrm{)}$ , such that $\mathit{\alpha }\mathrm{(}\mathrm{red}\mathrm{)}\mathrm{>}\mathit{\alpha }\mathrm{(}\mathrm{green}\mathrm{)}$ (because of rule (1)) and $\mathit{\alpha }\mathrm{(}\mathrm{green}\mathrm{)}\mathrm{>}\mathit{\alpha }\mathrm{(}\mathrm{red}\mathrm{)}$ (because of rule (2)). Such a mapping obviously does not exist.

Now let use consider ${\mathit{\pi }}_{\mathrm{check}}$ . The role of this program is to exclude answer set candidates provided by ${\mathit{\pi }}_{\mathrm{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 ${\mathit{\pi }}_{\mathrm{guess}}\mathrm{(}\mathit{D}\mathrm{)}$ and then compute the answer sets of ${\mathit{\pi }}_{\mathrm{check}}\mathrm{(}\mathit{J}\mathrm{)}$ for each $\mathit{J}\in \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{guess}}\mathrm{(}\mathit{D}\mathrm{)}\mathrm{)}$ , in order to obtain the answer sets of the entire program ${\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}$ . In fact, the set $\mathit{S}=\{\mathrm{vertex}\mathrm{,}\mathrm{edge}\mathrm{,}\mathrm{red}\mathrm{,}\mathrm{green}\mathrm{,}\mathrm{blue}\}$ is a splitting set for ${\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}$ , for any input database D over atoms with predicate symbols from S. The top of ${\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}$ with respect to S is thus given by ${\mathrm{(}{\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}\mathrm{)}}_{\mathit{S}}^{\mathit{t}}={\mathit{\pi }}_{\mathrm{check}}$ , and the bottom of ${\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}$ with respect to S is given by ${\mathrm{(}{\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}\mathrm{)}}_{\mathit{S}}^{\mathit{b}}={\mathit{\pi }}_{\mathrm{guess}}\mathrm{(}\mathit{D}\mathrm{)}$ . For illustration, assume D contains $\mathrm{edge}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}$ , $\mathrm{edge}\mathrm{(}\mathit{b}\mathrm{,}\mathit{c}\mathrm{)}$ , and $\mathrm{edge}\mathrm{(}\mathit{c}\mathrm{,}\mathit{a}\mathrm{)}$ . Assume the answer set $\mathit{J}=\mathit{D}\cup \{\mathrm{red}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{red}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{green}\mathrm{(}\mathit{c}\mathrm{)}\}$ of ${\mathit{\pi }}_{\mathrm{guess}}\mathrm{(}\mathit{D}\mathrm{)}$ is used as input now to ${\mathit{\pi }}_{\mathrm{check}}$ . Then, the rule $\mathrm{fail}:-\mathrm{red}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{red}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{edge}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}$ derives fail, but then rule (7) cannot be satisfied. Thus, J does not satisfy ${\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}$ , and consequently, J cannot become an answer set of ${\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}$ . On the other hand, $\mathit{D}\cup \{\mathrm{red}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{green}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{blue}\mathrm{(}\mathit{c}\mathrm{)}\}$ (which is also an answer set of ${\mathit{\pi }}_{\mathrm{guess}}\mathrm{(}\mathit{D}\mathrm{)}$ ) satisfies all rules of ${\mathit{\pi }}_{\mathrm{check}}$ and thus becomes an answer set of ${\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}$ . In fact, for the example graph represented in D, ${\mathit{\pi }}_{\mathrm{col}}\mathrm{(}\mathit{D}\mathrm{)}$ 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: $$\begin{array}{cccc}\mathrm{\Pi }=\{\mathit{p}\hfill & \vee \mathit{q}:-;\hfill & {\mathrm{\Pi }}^{\prime }=\hfill & \{\mathit{p}:-\mathrm{not}\mathit{q};\mathit{q}:-\mathrm{not}\mathit{p};\hfill \\ \hfill & \mathit{p}:-\mathit{q};\mathit{q}:-\mathit{p}\}\hfill & \hfill & \mathit{p}:-\mathit{q};\mathit{q}:-\mathit{p}\}\hfill \end{array}$$ 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 ${\mathrm{(}{\mathrm{\Pi }}^{\prime }\mathrm{)}}^{\{\mathit{p}\mathrm{,}\mathit{q}\}}=\{\mathit{p}:-\mathit{q};\mathit{q}:-\mathit{p}\}$ . But now, {p, q} is not the minimal interpretation satisfying ${\mathrm{(}{\mathrm{\Pi }}^{\prime }\mathrm{)}}^{\{\mathit{p}\mathrm{,}\mathit{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 ${\mathit{\pi }}_{\mathrm{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 ${\mathit{\pi }}_{\mathrm{col}}$ . Finally, instead of the constraint $:-\mathrm{fail}$ to exclude invalid colourings, we “saturate” the guess via rules (12)–(14) and add as constraint $:-\mathrm{not}\mathrm{fail}$ . $$\begin{array}{ccc}\hfill {\mathit{\pi }}_{\mathrm{ncol}}=& \{\mathrm{red}\mathrm{(}\mathit{X}\mathrm{)}\vee \mathrm{green}\mathrm{(}\mathit{X}\mathrm{)}\vee \mathrm{blue}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{vertex}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}8\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{red}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{red}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{edge}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill & \hfill \mathrm{(}9\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{green}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{green}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{edge}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill & \hfill \mathrm{(}10\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{blue}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{blue}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{edge}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill & \hfill \mathrm{(}11\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{red}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{fail}\mathrm{,}\mathrm{vertex}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}12\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{green}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{fail}\mathrm{,}\mathrm{vertex}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}13\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{blue}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{fail}\mathrm{,}\mathrm{vertex}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}14\mathrm{)}\\ \hfill & \phantom{\{}:-\mathrm{not}\mathrm{fail}\}\hfill & \hfill \mathrm{(}15\mathrm{)}\end{array}$$ Suppose graphs are represented by inputs D as above. The only possible answer set J of ${\mathit{\pi }}_{\mathrm{ncol}}\mathrm{(}\mathit{D}\mathrm{)}$ (if one exists) contains fail because of the last rule $:-\mathrm{not}\mathrm{fail}$ . But if fail is contained in J, J has to contain red(X), $\mathrm{green}\mathrm{(}\mathit{X}\mathrm{)}$ , and $\mathrm{blue}\mathrm{(}\mathit{X}\mathrm{)}$ for each vertex X. Thus J has to be of the form $\mathit{D}\cup \{\mathrm{fail}\}\cup \{\mathrm{red}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{green}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{blue}\mathrm{(}\mathit{a}\mathrm{)}\mid \mathrm{vertex}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{D}\}$ . We observe that the reduct ${\mathrm{(}{\mathit{\pi }}_{\mathrm{ncol}}\mathrm{(}\mathit{D}\mathrm{)}\mathrm{)}}^{\mathit{J}}$ is given by ${\mathit{\pi }}_{\mathrm{ncol}}\mathrm{(}\mathit{D}\mathrm{)}\setminus \{:-\mathrm{not}\mathrm{fail}\}$ . Note that interpretations satisfying ${\mathrm{(}{\mathit{\pi }}_{\mathrm{ncol}}\mathrm{(}\mathit{D}\mathrm{)}\mathrm{)}}^{\mathit{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 ${\mathit{\pi }}_{\mathrm{ncol}}\mathrm{(}\mathit{D}\mathrm{)}$ . 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 $\mathrm{\Pi }{\vDash }_{\mathrm{c}}\mathit{A}$ that A is contained in some answer sets of Π. Likewise, we denote by $\mathrm{\Pi }{\vDash }_{\mathrm{s}}\mathit{A}$ 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 $\mathrm{\Pi }\mathrm{(}\mathit{D}\mathrm{)}\vDash \mathit{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
${\vDash }_{\mathrm{c}}$	P	NP	${\mathrm{\Sigma }}_2^{\mathit{P}}$
${\vDash }_{\mathrm{s}}$	P	coNP	${\mathrm{\Pi }}_2^{\mathit{P}}$

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) where $\mathit{A}\subseteq \mathcal{U}$ is a finite set of arguments and $\mathit{R}\subseteq \mathit{A}\times \mathit{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 $\mathit{A}=\{\mathit{a}\mathrm{,}\mathit{b}\mathrm{,}\mathit{c}\mathrm{,}\mathit{d}\mathrm{,}\mathit{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 $$\mathrm{cf}\mathrm{(}\mathit{F}\mathrm{)}=\{\varnothing \mathrm{,}\{\mathit{a}\}\mathrm{,}\{\mathit{b}\}\mathrm{,}\{\mathit{c}\}\mathrm{,}\{\mathit{d}\}\mathrm{,}\{\mathit{a}\mathrm{,}\mathit{c}\}\mathrm{,}\{\mathit{a}\mathrm{,}\mathit{d}\}\mathrm{,}\{\mathit{b}\mathrm{,}\mathit{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, if $\mathit{S}\in \mathrm{cf}\mathrm{(}\mathit{F}\mathrm{)}$ and each $\mathit{a}\in \mathit{A}\setminus \mathit{S}$ is defeated by S in F. We denote the collection of all stable extensions of F by $\mathrm{stable}\mathrm{(}\mathit{F}\mathrm{)}$ .

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 $\mathrm{stable}\mathrm{(}\mathit{F}\mathrm{)}$ , 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 $\mathrm{(}\{\mathit{a}\}\mathrm{,}\{\mathrm{(}\mathit{a}\mathrm{,}\mathit{a}\mathrm{)}\}\mathrm{)}$ ). 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), if $\mathit{S}\in \mathrm{cf}\mathrm{(}\mathit{F}\mathrm{)}$ 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 $$\mathit{adm}\mathrm{(}\mathit{F}\mathrm{)}=\{\varnothing \mathrm{,}\{\mathit{a}\}\mathrm{,}\{\mathit{c}\}\mathrm{,}\{\mathit{d}\}\mathrm{,}\{\mathit{a}\mathrm{,}\mathit{c}\}\mathrm{,}\{\mathit{a}\mathrm{,}\mathit{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, if $\mathit{S}\in \mathrm{adm}\mathrm{(}\mathit{F}\mathrm{)}$ and for each $\mathit{T}\in \mathrm{adm}\mathrm{(}\mathit{F}\mathrm{)}$ , $\mathit{S}\not\subset \mathit{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⁺ _R be defined as $\mathit{S}\cup \{\mathit{b}\mid \exists \mathit{a}\in \mathit{S}\mathrm{,}\text{such that}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\in \mathit{R}\}$ . A set S is a semi-stable extension of F, if $\mathit{S}\in \mathrm{adm}\mathrm{(}\mathit{F}\mathrm{)}$ and for each $\mathit{T}\in \mathrm{adm}\mathrm{(}\mathit{F}\mathrm{)}$ , ${\mathit{S}}_{\mathit{R}}^{+}\not\subset {\mathit{T}}_{\mathit{R}}^{+}$ . 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 ${\mathit{S}}_{\mathit{R}}^{+}=\{\mathit{a}\mathrm{,}\mathit{b}\mathrm{,}\mathit{c}\mathrm{,}\mathit{d}\}\subset \{\mathit{a}\mathrm{,}\mathit{b}\mathrm{,}\mathit{c}\mathrm{,}\mathit{d}\mathrm{,}\mathit{e}\}={\mathit{T}}_{\mathit{R}}^{+}$ .

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, if $\mathit{S}\in \mathrm{adm}\mathrm{(}\mathit{F}\mathrm{)}$ 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., $\mathrm{ground}\mathrm{(}\mathit{F}\mathrm{)}$ ).

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 $\mathit{e}\in \{\mathrm{stable}\mathrm{,}\mathrm{adm}\mathrm{,}\mathrm{pref}\mathrm{,}\mathrm{semi}\mathrm{,}\mathrm{comp}\mathrm{,}\mathrm{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 $\mathit{S}\in \mathit{adm}\mathrm{(}\mathit{F}\mathrm{)}$ iff a is contained in some $\mathit{S}\in \mathrm{pref}\mathrm{(}\mathit{F}\mathrm{)}$ . 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	${\mathrm{\Sigma }}_2^{\mathit{P}}$ -c	NP-c	in P
Skept e	coNP-c	(trivial)	${\mathrm{\Pi }}_2^{\mathit{P}}$ -c	${\mathrm{\Pi }}_2^{\mathit{P}}$ -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 ${\mathrm{\Gamma }}_{\mathit{F}}:2^{\mathit{A}}\to 2^{\mathit{A}}$ is defined as $${\mathrm{\Gamma }}_{\mathit{F}}\mathrm{(}\mathit{S}\mathrm{)}=\{\mathit{a}\in \mathit{A}\mid \mathit{a}\text{is defended by}\mathit{S}\text{in}\mathit{F}\}.$$

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 ${\mathit{\pi }}_{\mathit{e}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ 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 $$\hat{\mathit{F}}=\{\arg \mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\}\cup \{\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mid \mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\in \mathit{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 $\mathrm{in}\mathrm{(}·\mathrm{)}$ and $\mathrm{out}\mathrm{(}·\mathrm{)}$ 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

Let $\mathcal{S}\subseteq 2^{\mathcal{U}}$ be a collection of sets of domain elements and let $\mathcal{I}\subseteq 2^{{\mathit{B}}_{\mathcal{U}}}$ be a collection of sets of ground atoms. We say that 𝒮 and ℐ correspond to each other, in symbols $\mathcal{S}\cong \mathcal{I}$ , iff (i) for each $\mathit{S}\in \mathcal{S}$ , there exists an $\mathit{I}\in \mathcal{I}$ , such that $\{\mathit{a}\mid \mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}\}=\mathit{S}$ ; and (ii) for each $\mathit{I}\in \mathcal{I}$ , it holds that $\{\mathit{a}\mid \mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}\}\in \mathcal{S}$ .

Note that $\mathcal{S}\cong \mathcal{I}$ thus implies $|\mathcal{S}|=|\mathcal{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: $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{cf}}=& \{\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{not}\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{not}\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}:-\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}.\hfill \end{array}$$

For our framework F from Example 2.3, we have as input $$\begin{array}{cc}\hfill \hat{\mathit{F}}=& \{\arg \mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{e}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\{}\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{c}\mathrm{,}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{c}\mathrm{,}\mathit{d}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\{}\mathrm{defeat}\mathrm{(}\mathit{d}\mathrm{,}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{d}\mathrm{,}\mathit{e}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{e}\mathrm{,}\mathit{e}\mathrm{)}.\hfill \end{array}$$

Moreover, using [Fcirc] together with π_cf, we obtain $$\mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}=\{{\mathit{S}}_{\varnothing }\mathrm{,}{\mathit{S}}_{\mathit{a}}\mathrm{,}{\mathit{S}}_{\mathit{b}}\mathrm{,}{\mathit{S}}_{\mathit{c}}\mathrm{,}{\mathit{S}}_{\mathit{d}}\mathrm{,}{\mathit{S}}_{\mathit{ac}}\mathrm{,}{\mathit{S}}_{\mathit{ad}}\mathrm{,}{\mathit{S}}_{\mathit{bd}}\}\mathrm{,}$$ where $$\begin{array}{cc}\hfill {\mathit{S}}_{\varnothing }& =\hat{\mathit{F}}\cup \{\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{a}}& =\hat{\mathit{F}}\cup \{\mathbf{in}\mathrm{(}\mathbf{a}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{b}}& =\hat{\mathit{F}}\cup \{\mathbf{in}\mathrm{(}\mathbf{b}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{c}}& =\hat{\mathit{F}}\cup \{\mathbf{in}\mathrm{(}\mathbf{c}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{d}}& =\hat{\mathit{F}}\cup \{\mathbf{in}\mathrm{(}\mathbf{d}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{ac}}& =\hat{\mathit{F}}\cup \{\mathbf{in}\mathrm{(}\mathbf{a}\mathrm{)}\mathrm{,}\mathbf{in}\mathrm{(}\mathbf{c}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{ad}}& =\hat{\mathit{F}}\cup \{\mathbf{in}\mathrm{(}\mathbf{a}\mathrm{)}\mathrm{,}\mathbf{in}\mathrm{(}\mathbf{d}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{bd}}& =\hat{\mathit{F}}\cup \{\mathbf{in}\mathrm{(}\mathbf{b}\mathrm{)}\mathrm{,}\mathbf{in}\mathrm{(}\mathbf{d}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{e}\mathrm{)}\}.\hfill \end{array}$$

Proposition 3.2

For any AF F, $\mathrm{cf}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

Proof

Let F=(A, R) and $\mathit{S}\in \mathit{cf}\mathrm{(}\mathit{F}\mathrm{)}$ . We show that the interpretation $$\mathit{I}=\hat{\mathit{F}}\cup \{\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{S}\}\cup \{\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\setminus \mathit{S}\}$$ (corresponding to S) is an answer set of ${\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . We have to show that I satisfies ${\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ (we recall that an interpretation I satisfies a program Π iff I satisfies Π ^I ), and that no J⊂I satisfies ${\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}^{\mathit{I}}$ . To show that I satisfies ${\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ , we have to show that I satisfies each $\mathit{r}\in \mathrm{Gr}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ . Note that $$\begin{array}{cc}\hfill \mathrm{Gr}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}=& \hat{\mathit{F}}\cup \hfill \\ \hfill & \{\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}:-\mathrm{not}\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\}\cup \hfill & \hfill \mathrm{(}16\mathrm{)}\\ \hfill & \{\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}:-\mathrm{not}\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\}\cup \hfill & \hfill \mathrm{(}17\mathrm{)}\\ \hfill & \{:-\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mid \mathit{a}\mathrm{,}\mathit{b}\in \mathit{A}\}.\hfill & \hfill \mathrm{(}18\mathrm{)}\end{array}$$ Clearly, I satisfies [Fcirc], since $\hat{\mathit{F}}\subseteq \mathit{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 ${\mathit{B}}^{+}\mathrm{(}\mathit{r}\mathrm{)}⊈\mathit{I}$ . This can be seen as follows: Suppose r is of the form $:-\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}$ . In case, $\{\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{b}\mathrm{)}\}⊈\mathit{I}$ , ${\mathit{B}}^{+}\mathrm{(}\mathit{r}\mathrm{)}⊈\mathit{I}$ is clear. Otherwise, then both a and b are contained in S, by definition of I. Since $\mathit{S}\in \mathrm{cf}\mathrm{(}\mathit{F}\mathrm{)}$ by assumption, $\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\notin \mathit{R}$ has to hold. Thus, by definition, $\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\notin \hat{\mathit{F}}$ (and thus $\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\notin \mathit{I}$ ). Hence ${\mathit{B}}^{+}\mathrm{(}\mathit{r}\mathrm{)}⊈\mathit{I}$ .

This shows that I satisfies ${\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . Now let J⊆ I, such that J satisfies ${\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}^{\mathit{I}}$ . We show that then J=I. Note that the reduct is always grounded by definition. We have $$\begin{array}{cc}\hfill {\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}^{\mathit{I}}=& \hat{\mathit{F}}\cup \hfill \\ \hfill & \{\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}:-\arg \mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\notin \mathit{I}\}\cup \hfill & \hfill \mathrm{(}19\mathrm{)}\\ \hfill & \{\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}:-\arg \mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\notin \mathit{I}\}\cup \hfill & \hfill \mathrm{(}20\mathrm{)}\\ \hfill & \{:-\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mid \mathit{a}\mathrm{,}\mathit{b}\in \mathit{A}\}.\hfill & \hfill \mathrm{(}21\mathrm{)}\end{array}$$ Since J satisfies ${\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}^{\mathit{I}}$ , $\hat{\mathit{F}}\subseteq \mathit{J}$ . Moreover, since J satisfies each rule in Equation (19), for each a∈A, such that $\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\notin \mathit{I}$ , in(a) has to be in J. But since, for each a∈A, we have that $\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\notin \mathit{I}$ iff $\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}$ , we get that $\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{J}$ iff $\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}$ . Similarly, using the rules from Equation (20), we obtain that $\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{J}$ iff $\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}$ . J=I follows. Hence, there is no J⊂I, such that J satisfies ${\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}^{\mathit{I}}$ . This concludes the proof for $\mathit{I}\in \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

Now suppose $\mathit{I}\in \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ . Consequently, $\hat{\mathit{F}}\subseteq \mathit{I}$ , and no further atom of the form $\mathrm{defeat}\mathrm{(}·\mathrm{,}·\mathrm{)}$ or $\arg \mathrm{(}·\mathrm{)}$ 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 $\mathit{S}\in \mathrm{cf}\mathrm{(}\mathit{F}\mathrm{)}$ for $\mathit{S}=\{\mathit{a}\mid \mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}\}$ . Since $\mathit{I}\in \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ , I satisfies ${\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ , i.e. I satisfies the grounding of ${\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ , $\mathrm{Gr}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ , as given above. In particular, I satisfies each constraint in Equation (18), thus jointly $\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}$ and $\mathrm{in}\mathrm{(}\mathit{b}\mathrm{)}\in \mathit{I}$ , only if $\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\notin \mathit{I}$ . By our observation from above, $\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\notin \hat{\mathit{F}}$ , and thus $\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\notin \mathit{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 $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{stable}}=& {\mathit{\pi }}_{\mathrm{cf}}\cup {\mathit{\pi }}_{\mathrm{srules}}\hfill \\ \hfill {\mathit{\pi }}_{\mathrm{srules}}=& \{\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)}\}.\hfill \end{array}$$ The first rule of ${\mathit{\pi }}_{\mathrm{srules}}$ computes those arguments attacked by the current guess, while the constraint in ${\mathit{\pi }}_{\mathrm{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 $\mathit{C}=\{\mathrm{in}\mathrm{,}\mathrm{out}\mathrm{,}\arg \mathrm{,}\mathrm{defeat}\}$ divides the program ${\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ into ${\mathrm{(}{\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}_{\mathit{C}}^{\mathit{t}}={\mathit{\pi }}_{\mathrm{srules}}$ and ${\mathrm{(}{\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}_{\mathit{C}}^{\mathit{b}}={\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . Therefore, we make direct use of the answer sets of ${\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . For our example, let us first consider the collection 𝒞 of answer sets of $${\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\cup \{\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\}.$$

In fact, using our calculations from the previous subsection, we obtain $$\begin{array}{cc}\hfill \mathcal{C}=& \{{\mathit{S}}_{\varnothing }\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{a}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{b}}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{c}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{d}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{d}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{ac}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{d}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{ad}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{bd}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{e}\mathrm{)}\}\}.\hfill \end{array}$$

If we now apply the constraint $:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)}$ to each element in 𝒞, we observe that any set from 𝒞 except ${\mathit{S}}_{\mathit{ad}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{e}\mathrm{)}\}$ is violated by that constraint. In fact, each other set contains at least one atom out(y) without the matching $\mathrm{defeated}\mathrm{(}\mathit{y}\mathrm{)}$ .

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

Proposition 3.3

For any AF F, $\mathit{stable}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

Proof

First, let us formally describe the application of the Splitting Theorem (Proposition 2.1) as sketched above with the splitting set $\mathit{C}=\{\mathrm{in}\mathrm{,}\mathrm{out}\mathrm{,}\arg \mathrm{,}\mathrm{defeat}\}$ . Then, we obtain $$\begin{array}{cc}\mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}={\displaystyle \bigcup }_{\mathit{J}\in \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}\mathcal{AS}\mathrm{(}\mathit{J}\cup {\mathit{\pi }}_{\mathrm{srules}}\mathrm{)}.\hfill & \hfill \mathrm{(}22\mathrm{)}\end{array}$$ Let F=(A, R) and $\mathit{S}\in \mathrm{stable}\mathrm{(}\mathit{F}\mathrm{)}$ . Since $\mathit{S}\in \mathrm{stable}\mathrm{(}\mathit{F}\mathrm{)}$ , $\mathit{S}\in \mathrm{cf}\mathrm{(}\mathit{F}\mathrm{)}$ , and by Proposition 3.2, there exists an interpretation $$\mathit{J}=\mathrm{(}\hat{\mathit{F}}\cup \{\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{S}\}\cup \{\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\setminus \mathit{S}\}\mathrm{)}\in \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}.$$ By Equation (22), we know that each answer set of $\mathit{J}\cup {\mathit{\pi }}_{\mathrm{srules}}$ is also an answer set of ${\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . We now show that I given as $$\hat{\mathit{F}}\cup \{\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{S}\}\cup \{\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\setminus \mathit{S}\}\cup \{\mathrm{defeated}\mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{b}\in \mathit{S}\mathrm{,}\mathrm{(}\mathit{b}\mathrm{,}\mathit{a}\mathrm{)}\in \mathit{R}\}$$ is indeed an answer set of ${\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . We first show that I satisfies the grounding of $\mathit{J}\cup {\mathit{\pi }}_{\mathrm{srules}}$ . Clearly, I satisfies J, since J⊆ I. The groundings of the remaining rules are given by $$\begin{array}{cc}\{\mathrm{defeated}\mathrm{(}\mathit{a}\mathrm{)}:-\mathrm{in}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{b}\mathrm{,}\mathit{a}\mathrm{)}\mid \mathit{a}\mathrm{,}\mathit{b}\in \mathit{A}\}\hfill & \hfill \mathrm{(}23\mathrm{)}\\ \{:-\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\}.\hfill & \hfill \mathrm{(}24\mathrm{)}\end{array}$$ Note that, for each argument b, we have $\mathrm{in}\mathrm{(}\mathit{b}\mathrm{)}\in \mathit{I}$ iff b∈S. Moreover, we already know $\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\in \mathit{J}$ iff (a, b)∈R. Thus, I satisfies each instance of rule (23). Further, since S is stable, we know that each $\mathit{a}\in \mathit{A}\setminus \mathit{S}$ is defeated by S in F. By definition, if $\mathit{a}\in \mathit{A}\setminus \mathit{S}$ then $\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}$ . But this shows that either $\mathrm{out}\mathrm{(}\mathit{a}\mathrm{)}\notin \mathit{I}$ or $\mathrm{defeated}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}$ holds for each a∈A. Thus I satisfies each instance of constraint (24). This shows that I satisfies ${\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . In order to show that $\mathit{I}\in \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ , let K⊆ I be an interpretation satisfying ${\mathrm{(}{\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}^{\mathit{I}}$ . First, we know $\mathit{K}\cap {\mathit{B}}_{{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}}=\mathit{I}\cap {\mathit{B}}_{{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}}$ , otherwise $\mathit{J}\notin \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ (in that case we would have $\mathit{K}\cap {\mathit{B}}_{{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}}\subset \mathit{I}\cap {\mathit{B}}_{{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}}$ , but then also $\mathit{K}\cap {\mathit{B}}_{{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}}\subset \mathit{J}$ holds since $\mathit{J}=\mathit{I}\cap {\mathit{B}}_{{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}}$ ; further, by assumption, K (and thus also $\mathit{K}\cap {\mathit{B}}_{{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}}$ ) satisfies ${\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}^{\mathit{J}}={\mathrm{(}{\mathit{\pi }}_{\mathrm{cf}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}^{\mathit{I}}\subseteq {\mathrm{(}{\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}}^{\mathit{I}}$ ). Second, since K satisfies the rules in Equation (23) – which are all without default negation and thus contained in the reduct – $\mathrm{defeated}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{K}$ iff $\mathrm{defeated}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}$ . Hence K=I. This shows $\mathit{I}\in \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

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

3.2. Admissible extensions

We next give the rules for the admissibility test: $$\begin{array}{cc}{\mathit{\pi }}_{\mathrm{adm}}={\mathit{\pi }}_{\mathrm{cf}}\cup \hfill & \{\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}:-\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{Y}\mathrm{)}\}.\hfill \end{array}$$ The first rule is the same as in ${\mathit{\pi }}_{\mathrm{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 $:-\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{Y}\mathrm{)}$ . This is the case for two of the candidates.

S _b contains in(b) and $\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}$ but since $\mathrm{defeated}\mathrm{(}\mathit{a}\mathrm{)}$ is not contained, the constraint applies;

for ${\mathit{S}}_{\mathit{bd}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{e}\mathrm{)}\}$ , the argumentation is analogous.

Hence, we obtain $$\begin{array}{cc}\hfill \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}=& \{{\mathit{S}}_{\varnothing }\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{a}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{c}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{d}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{d}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{ac}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{d}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill & \phantom{\{}{\mathit{S}}_{\mathit{d}}\cup \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{e}\mathrm{)}\}\}.\hfill \end{array}$$ 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, $\mathrm{adm}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

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 $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{comp}}={\mathit{\pi }}_{\mathrm{adm}}\cup & \{\mathrm{undefended}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{\mathit{i}}:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{undefended}\mathrm{(}\mathit{X}\mathrm{)}\}.\hfill \end{array}$$ 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 $:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{undefended}\mathrm{(}\mathit{X}\mathrm{)}$ . Here, we can directly use the sets from $\mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ and check which predicates $\mathrm{undefended}\mathrm{(}·\mathrm{)}$ can be derived. The answer sets of ${\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\cup \{\mathrm{undefended}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{Y}\mathrm{)}\}$ are $$\begin{array}{cc}\hfill {\mathit{S}}_{\varnothing }\cup & \{\mathrm{undefended}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{a}}\cup & \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\{}\mathrm{undefended}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{c}}\cup & \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{d}}\cup & \{\mathrm{defeated}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{e}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{ac}}\cup & \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{e}\mathrm{)}\}\mathrm{,}\hfill \\ \hfill {\mathit{S}}_{\mathit{ad}}\cup & \{\mathrm{defeated}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{e}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\{}\mathrm{undefended}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{undefended}\mathrm{(}\mathit{e}\mathrm{)}\}.\hfill \end{array}$$ Obviously, each candidate which contains out(a) (i.e. the sets S_∅, S _c , and S _d ) is ruled out by the constraint $:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{undefended}\mathrm{(}\mathit{X}\mathrm{)}$ , since no such candidate set contains $\mathrm{undefended}\mathrm{(}\mathit{a}\mathrm{)}$ . 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 ${\mathit{\pi }}_{\mathrm{comp}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . Again, these three sets characterise the complete extensions of F, as desired.

Proposition 3.5

For any AF F, $\mathrm{comp}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{comp}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

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 $\mathrm{in}\mathrm{(}·\mathrm{)}$ predicates according to the definition of the operator Γ _F (following the same idea as we used to derive the $\mathrm{reached}\mathrm{(}·\mathrm{)}$ 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. $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{<}}=& \{\mathrm{lt}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\arg \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathit{X}\mathrm{<}\mathit{Y};\hfill \\ \hfill & \phantom{\{}\mathrm{nsucc}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Z}\mathrm{)}:-\mathrm{lt}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{lt}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{Z}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{succ}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{lt}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{nsucc}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{ninf}\mathrm{(}\mathit{Y}\mathrm{)}:-\mathrm{lt}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\inf \mathrm{(}\mathit{X}\mathrm{)}:-\arg \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{ninf}\mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{nsup}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{lt}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\sup \mathrm{(}\mathit{X}\mathrm{)}:-\arg \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{nsup}\mathrm{(}\mathit{X}\mathrm{)}\}.\hfill \end{array}$$

Note that π_< is indeed stratified and constraint-free. Hence, ${\mathit{\pi }}_{\mathrm{<}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ 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 ${\mathit{\pi }}_{\mathrm{<}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ contains $$\{\inf \mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{succ}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{succ}\mathrm{(}\mathit{b}\mathrm{,}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{succ}\mathrm{(}\mathit{c}\mathrm{,}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{succ}\mathrm{(}\mathit{d}\mathrm{,}\mathit{e}\mathrm{)}\mathrm{,}\sup \mathrm{(}\mathit{e}\mathrm{)}\}.$$ 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), $\mathrm{nsucc}\mathrm{(}\mathit{a}\mathrm{,}\mathit{c}\mathrm{)}$ , $\mathrm{nsucc}\mathrm{(}\mathit{a}\mathrm{,}\mathit{d}\mathrm{)}$ , $\mathrm{nsucc}\mathrm{(}\mathit{a}\mathrm{,}\mathit{e}\mathrm{)}$ , $\mathrm{nsucc}\mathrm{(}\mathit{b}\mathrm{,}\mathit{d}\mathrm{)}$ , $\mathrm{nsucc}\mathrm{(}\mathit{b}\mathrm{,}\mathit{e}\mathrm{)}$ , $\mathrm{nsucc}\mathrm{(}\mathit{c}\mathrm{,}\mathit{e}\mathrm{)}$ , ninf(b), ninf(c), ninf(d), ninf(e), nsup(a), nsup(b), nsup(c), and nsup(d).

We now define the required predicate $\mathrm{defended}\mathrm{(}\mathit{X}\mathrm{)}$ which itself is obtained via a predicate $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}$ 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 $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}$ for all further Y. If we arrive at the supremum element in this way, i.e. $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}$ is derived for the supremum Y, we finally obtain $\mathrm{defended}\mathrm{(}\mathit{X}\mathrm{)}$ . We define $$\begin{array}{ccc}\hfill {\mathit{\pi }}_{\mathrm{defended}}=& \{\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\inf \mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}25\mathrm{)}\\ \hfill & \phantom{\mathit{i}}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\inf \mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{Z}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathit{p}}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}26\mathrm{)}\\ \hfill & \phantom{\mathit{i}}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Z}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathit{p}}\mathrm{not}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}27\mathrm{)}\\ \hfill & \phantom{\mathit{i}}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Z}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathit{p}}\mathrm{in}\mathrm{(}\mathit{V}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{V}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}28\mathrm{)}\\ \hfill & \phantom{\mathit{p}\mathit{i}}\mathrm{defended}\mathrm{(}\mathit{X}\mathrm{)}:-\sup \mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\text{and}\hfill & \hfill \mathrm{(}29\mathrm{)}\\ \hfill {\mathit{\pi }}_{\mathrm{ground}}=& {\mathit{\pi }}_{\mathrm{<}}\cup {\mathit{\pi }}_{\mathrm{defended}}\cup \{\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{defended}\mathrm{(}\mathit{X}\mathrm{)}\}.\hfill \end{array}$$ Note that ${\mathit{\pi }}_{\mathrm{ground}}$ is also stratified. We also mention that the relevant predicate in(a) is derived for some argument a if $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}$ holds for each b. However, if there is an unattacked argument c which attacks a, $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{a}\mathrm{,}\mathit{c}\mathrm{)}$ is not derived. It is thus not relevant in which order we derive the predicates $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}$ . Consequently, the particular definition of the order <, from which we obtained the $\inf \mathrm{(}·\mathrm{)}$ , $\mathrm{succ}\mathrm{(}·\mathrm{,}·\mathrm{)}$ , and $\sup \mathrm{(}·\mathrm{)}$ predicates used in ${\mathit{\pi }}_{\mathrm{defended}}$ , plays no role. Any total order over the constants can be used.

For illustration, we compute the answer set for $\hat{\mathit{F}}\cup {\mathit{\pi }}_{\mathrm{<}}\cup {\mathit{\pi }}_{\mathrm{defended}}$ step by step, for our example AF F. Recall that we already have given S₀, the answer set of $\hat{\mathit{F}}\cup {\mathit{\pi }}_{\mathrm{<}}$ . Since ${\mathit{\pi }}_{\mathrm{ground}}$ only derives distinguished predicates $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}·\mathrm{,}·\mathrm{)}$ and $\mathrm{defended}\mathrm{(}·\mathrm{)}$ , we can view S₀ as input to ${\mathit{\pi }}_{\mathrm{ground}}$ .

In the “first round” of computation, we have no $\mathrm{in}\mathrm{(}·\mathrm{)}$ predicate derived so far; hence only the rules (25) and (27) in ${\mathit{\pi }}_{\mathrm{defended}}$ are of interest. In fact, for inf(a), the rule (25) in ${\mathit{\pi }}_{\mathrm{defended}}$ yields $$\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{a}\mathrm{,}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{c}\mathrm{,}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{d}\mathrm{,}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{e}\mathrm{,}\mathit{a}\mathrm{)}.$$ Note that $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{b}\mathrm{,}\mathit{a}\mathrm{)}$ is missing, since we have $\mathrm{defeat}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\in \hat{\mathit{F}}$ . Now we use rule (27) and $\mathrm{succ}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}$ to obtain $$\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{c}\mathrm{,}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{d}\mathrm{,}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{e}\mathrm{,}\mathit{b}\mathrm{)}.$$ The remaining atoms we derive are $$\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{a}\mathrm{,}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{c}\mathrm{,}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{e}\mathrm{,}\mathit{c}\mathrm{)}.$$ Note that, since d is attacked by c, $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{d}\mathrm{,}\mathit{c}\mathrm{)}$ cannot be derived. Finally, we get $$\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{a}\mathrm{,}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{a}\mathrm{,}\mathit{e}\mathrm{)}.$$ 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 ${\mathit{\pi }}_{\mathrm{ground}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ the only $\mathrm{in}\mathrm{(}·\mathrm{)}$ predicate is in(a). This corresponds to the grounded extension of F, as desired.

Proposition 3.6

For any AF F, $\mathrm{ground}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{ground}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

Proof

Let F=(A, R) and let [Fcirc]_< be the answer set of ${\mathit{\pi }}_{\mathrm{<}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . 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 ${\mathit{\pi }}_{\mathrm{ground}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ , we first define the operator ${\mathrm{\Delta }}_{\hat{\mathit{F}}}$ representing the derivation of the answer set ${\hat{\mathit{F}}}_{\mathrm{ground}}$ of ${\mathit{\pi }}_{\mathrm{ground}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ as follows. $$\begin{array}{cc}\hfill {\mathrm{\Delta }}_{\hat{\mathit{F}}}\mathrm{(}\mathit{I}\mathrm{)}=\mathit{I}& \cup \{\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mid \arg \mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\arg \mathrm{(}\mathit{b}\mathrm{)}\in \mathit{I}\mathrm{,}\forall \mathit{c}\text{s.t.}\arg \mathrm{(}\mathit{c}\mathrm{)}\in \mathit{I}\text{and}\mathit{c}⩽\mathit{b}:\hfill \\ \hfill & \mathrm{defeat}\mathrm{(}\mathit{c}\mathrm{,}\mathit{a}\mathrm{)}\notin \mathit{I}\text{or}\exists \mathit{d}\text{s.t.}\mathrm{defeat}\mathrm{(}\mathit{d}\mathrm{,}\mathit{c}\mathrm{)}\in \mathit{I}\text{and}\mathrm{in}\mathrm{(}\mathit{d}\mathrm{)}\in \mathit{I}\}\cup \hfill \\ \hfill & \{\mathrm{defended}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\mid \arg \mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}\mathrm{,}\forall \mathit{c}\text{s.t.}\arg \mathrm{(}\mathit{c}\mathrm{)}\in \mathit{I}:\hfill \\ \hfill & \mathrm{defeat}\mathrm{(}\mathit{c}\mathrm{,}\mathit{a}\mathrm{)}\notin \mathit{I}\text{or}\exists \mathit{d}\text{s.t.}\mathrm{defeat}\mathrm{(}\mathit{d}\mathrm{,}\mathit{c}\mathrm{)}\in \mathit{I}\text{and}\mathrm{in}\mathrm{(}\mathit{d}\mathrm{)}\in \mathit{I}\}.\hfill \end{array}$$

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 ${\mathit{\pi }}_{\mathrm{ground}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ is given by the least fixed point of ${\mathrm{\Delta }}_{\hat{\mathit{F}}}$ . It remains to show that, in turn, the least fixed point of ${\mathrm{\Delta }}_{\hat{\mathit{F}}}$ equals the grounded extension of F.

Therefore, let ${\mathrm{\Delta }}_{\hat{\mathit{F}}}^0={\mathrm{\Delta }}_{\hat{\mathit{F}}}\mathrm{(}{\hat{\mathit{F}}}_{\mathrm{<}}\mathrm{)}$ and, for i>0, ${\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}}={\mathrm{\Delta }}_{\hat{\mathit{F}}}\mathrm{(}{\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}\mathrm{)}$ . Likewise, for the operator Γ defined in Proposition 2.10, let ${\mathrm{\Gamma }}_{\mathit{F}}^0={\mathrm{\Gamma }}_{\mathit{F}}\mathrm{(}\varnothing \mathrm{)}$ , and ${\mathrm{\Gamma }}_{\mathit{F}}^{\mathit{i}}={\mathrm{\Gamma }}_{\mathit{F}}\mathrm{(}{\mathrm{\Gamma }}_{\mathit{F}}^{\mathit{i}-1}\mathrm{)}$ .

We now show, given an AF F=(A, R), that $$\begin{array}{cc}{\mathrm{\Gamma }}_{\mathit{F}}^{\mathit{i}}=\{\mathit{a}\in \mathit{A}\mid \mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}}\}\hfill & \hfill \mathrm{(}30\mathrm{)}\end{array}$$ holds for every i≥0. The proof is by induction on i.

Induction base

Suppose i=0 and let $\mathit{a}\in {\mathrm{\Gamma }}_{\mathit{F}}^0$ . We show that $\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^0$ . Since $\mathit{a}\in {\mathrm{\Gamma }}_{\mathit{F}}^0$ and ${\mathrm{\Gamma }}_{\mathit{F}}^0={\mathrm{\Gamma }}_{\mathit{F}}\mathrm{(}\varnothing \mathrm{)}$ , a is not attacked in F, i.e. there is no c∈A with (c, a)∈R. By definition, $\arg \mathrm{(}\mathit{a}\mathrm{)}\in {\hat{\mathit{F}}}_{\mathrm{<}}$ , and there is no c such that $\mathrm{defeat}\mathrm{(}\mathit{c}\mathrm{,}\mathit{a}\mathrm{)}\in {\hat{\mathit{F}}}_{\mathrm{<}}$ . Hence, $\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^0$ by construction. To show that, for each a∈A with $\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^0$ , also $\mathit{a}\in {\mathrm{\Gamma }}_{\mathit{F}}^0$ 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 ${\mathrm{\Gamma }}_{\mathit{F}}^{\mathit{i}-1}=\{\mathit{a}\in \mathit{A}\mid \mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}\}$ holds. Let $\mathit{a}\in {\mathrm{\Gamma }}_{\mathit{F}}^{\mathit{i}}\setminus {\mathrm{\Gamma }}_{\mathit{F}}^{\mathit{i}-1}$ . We show $\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}}$ . Since $\mathit{a}\in {\mathrm{\Gamma }}_{\mathit{F}}^{\mathit{i}}$ , it must hold that for each c∈A with (c, a)∈R, there exists an argument $\mathit{d}\in {\mathrm{\Gamma }}_{\mathit{F}}^{\mathit{i}-1}$ with (d, c)∈R. Therefore, $\mathrm{in}\mathrm{(}\mathit{d}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}$ holds by induction hypothesis. Moreover, we clearly have $\arg \mathrm{(}\mathit{e}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}$ for all e∈A, and $\mathrm{defeat}\mathrm{(}\mathit{e}\mathrm{,}\mathit{f}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}$ for all (e, f)∈R (recall that $\hat{\mathit{F}}\subseteq {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}$ ). Hence, we know that for each c with $\arg \mathrm{(}\mathit{c}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}$ , such that $\mathrm{defeat}\mathrm{(}\mathit{c}\mathrm{,}\mathit{a}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}$ , there exists an argument d, such that $\mathrm{defeat}\mathrm{(}\mathit{d}\mathrm{,}\mathit{c}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}$ and $\mathrm{in}\mathrm{(}\mathit{d}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}-1}$ . By definition, $\mathrm{in}\mathrm{(}\mathit{a}\mathrm{)}\in {\mathrm{\Delta }}_{\hat{\mathit{F}}}^{\mathit{i}}$ . Again, the other direction is by similar arguments.   ▪

Obviously, we could have used the $\mathrm{defended}\mathrm{(}·\mathrm{)}$ predicate in previous programs. Indeed, π_comp could be defined as $${\mathit{\pi }}_{\mathrm{cf}}\cup {\mathit{\pi }}_{\mathrm{<}}\cup {\mathit{\pi }}_{\mathrm{defended}}\cup \{:-\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defended}\mathrm{(}\mathit{X}\mathrm{)};:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{defended}\mathrm{(}\mathit{X}\mathrm{)}\}.$$ 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 $\mathrm{in}\mathrm{(}·\mathrm{)}$ and $\mathrm{out}\mathrm{(}·\mathrm{)}$ using our encoding ${\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ ), we perform a second guess using new predicates, say $\mathrm{inN}\mathrm{(}·\mathrm{)}$ and $\mathrm{outN}\mathrm{(}·\mathrm{)}$ , to represent a further guess T⊃ S. In order to check whether the first guess (via $\mathrm{in}\mathrm{(}·\mathrm{)}$ and $\mathrm{out}\mathrm{(}·\mathrm{)}$ ) characterises a preferred extension, we have to ensure that no guess of the second form (i.e., via $\mathrm{inN}\mathrm{(}·\mathrm{)}$ and $\mathrm{outN}\mathrm{(}·\mathrm{)}$ ) characterises an admissible extension. Recall that in Section 2.1, we already have seen how to encode (using the program ${\mathit{\pi }}_{\mathrm{ncol}}$ ) such a complementary problem when we considered the problem of non-3-colourability. Here the saturation module looks as follows: $$\begin{array}{ccc}\hfill {\mathit{\pi }}_{\mathrm{satpref}}=& \{\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\vee \mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}31\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}32\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{eq};\hfill & \hfill \mathrm{(}33\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill & \hfill \mathrm{(}34\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{undefeated}\mathrm{(}\mathit{Y}\mathrm{)};\hfill & \hfill \mathrm{(}35\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{fail}\mathrm{,}\mathrm{org}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}36\mathrm{)}\\ \hfill & \phantom{\{}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{fail}\mathrm{,}\mathrm{org}\mathrm{(}\mathit{X}\mathrm{)};\hfill & \hfill \mathrm{(}37\mathrm{)}\\ \hfill & \phantom{\{}:-\mathrm{not}\mathrm{fail}\}.\hfill & \hfill \mathrm{(}38\mathrm{)}\end{array}$$

Let us for the moment also assume that predicates eq (rule (33)) and $\mathrm{undefeated}\mathrm{(}·\mathrm{)}$ (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 $\mathrm{in}\mathrm{(}·\mathrm{)}$ and $\mathrm{out}\mathrm{(}·\mathrm{)}$ equals the second guess T via $\mathrm{inN}\mathrm{(}·\mathrm{)}$ and $\mathrm{outN}\mathrm{(}·\mathrm{)}$ ; in other words, eq is derived if S=T;

$\mathrm{undefeated}\mathrm{(}\mathit{a}\mathrm{)}$ is derived if argument a is not defeated in F by the second guess T.

In what follows, we discuss the functioning of ${\mathit{\pi }}_{\mathrm{satpref}}$ when conjoined with the program ${\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ 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 $\mathrm{in}\mathrm{(}·\mathrm{)}$ and $\mathrm{out}\mathrm{(}·\mathrm{)}$ 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 ${\mathit{\pi }}_{\mathrm{ncol}}$ in terms of the non-3-colourability encoding in Section 2.1 (see rules (12)–(15) of program ${\mathit{\pi }}_{\mathrm{ncol}}$ ).

Let us illustrate now the behaviour of ${\mathit{\pi }}_{\mathrm{satpref}}$ for two scenarios. First, suppose the first guess S (via predicates $\mathrm{in}\mathrm{(}·\mathrm{)}$ and $\mathrm{out}\mathrm{(}·\mathrm{)}$ ) 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 $\mathrm{inN}\mathrm{(}·\mathrm{)}$ and $\mathrm{outN}\mathrm{(}·\mathrm{)}$ ) derives fail. Due to the spoiling rules (36) and (37), we thus have no interpretation (without predicate fail) which satisfies ${\mathit{\pi }}_{\mathrm{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 $\mathrm{in}\mathrm{(}·\mathrm{)}$ and $\mathrm{out}\mathrm{(}·\mathrm{)}$ ) 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 $\mathrm{inN}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}$ , for each a∈T, and $\mathrm{outN}\mathrm{(}\mathit{a}\mathrm{)}\in \mathit{I}$ , for each $\mathit{a}\in \mathit{A}\setminus \mathit{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 $\mathrm{undefeated}\mathrm{(}·\mathrm{)}$ . 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 $:-\mathrm{not}\mathrm{fail}$ ). 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 $\mathrm{defended}\mathrm{(}·\mathrm{)}$ as defined in Section 3.4 where we also required a stratified program. In fact, both predicates eq and $\mathrm{undefeated}\mathrm{(}·\mathrm{)}$ are computed via predicates $\mathrm{eq}\text{\_}\mathrm{upto}\mathrm{(}·\mathrm{)}$ (resp., $\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}·\mathrm{,}·\mathrm{)}$ ) in the same manner as we used $\mathrm{defended}\text{\_}\mathrm{upto}\mathrm{(}·\mathrm{,}·\mathrm{)}$ for $\mathrm{defended}\mathrm{(}·\mathrm{)}$ in the module ${\mathit{\pi }}_{\mathrm{defended}}$ in Section 3.4. We thus make use of the helper predicates from π_< as defined in the previous subsection and define $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{eq}}=& \{\mathrm{eq}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\inf \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eq}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\inf \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eq}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{eq}\text{\_}\mathrm{upto}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eq}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{eq}\text{\_}\mathrm{upto}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eq}:-\sup \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{eq}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}\};\hfill \\ \hfill {\mathit{\pi }}_{\mathrm{undefeated}}=& \{\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\inf \mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\inf \mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Z}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-}\mathrm{outN}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Z}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-}\mathrm{not}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{undefeated}\mathrm{(}\mathit{X}\mathrm{)}:-\sup \mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\}.\hfill \end{array}$$ With these predicates at hand, we can now formally define the module for preferred extensions, ${\mathit{\pi }}_{\mathrm{pref}}={\mathit{\pi }}_{\mathrm{adm}}\cup {\mathit{\pi }}_{\mathrm{<}}\cup {\mathit{\pi }}_{\mathrm{eq}}\cup {\mathit{\pi }}_{\mathrm{undefeated}}\cup {\mathit{\pi }}_{\mathrm{satpref}}$ . The general result is as follows.

Proposition 3.7

For any AF F, $\mathrm{pref}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{pref}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

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 $\mathrm{\Pi }={\mathit{\pi }}_{\mathrm{eq}}\cup {\mathit{\pi }}_{\mathrm{undefeated}}\cup {\mathit{\pi }}_{\mathrm{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 ${\mathit{\pi }}_{\mathrm{adm}}\cup {\mathit{\pi }}_{\mathrm{<}}$ and Π. We already know the single answer set S₀ of ${\mathit{\pi }}_{\mathrm{<}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ (see Section 3.4) and the collection $\{{\mathit{S}}_{\varnothing }\mathrm{,}{\mathit{S}}_{\mathit{a}}\mathrm{,}{\mathit{S}}_{\mathit{c}}\mathrm{,}{\mathit{S}}_{\mathit{d}}\mathrm{,}{\mathit{S}}_{\mathit{ac}}\mathrm{,}{\mathit{S}}_{\mathit{ad}}\}=\mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ of answer sets of ${\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ (see Section 3.2). As is easily checked, we get $$\mathcal{AS}\mathrm{(}\hat{\mathit{F}}\cup {\mathit{\pi }}_{\mathrm{adm}}\cup {\mathit{\pi }}_{\mathrm{<}}\mathrm{)}=\{{\mathit{S}}_0\cup \mathit{S}\mid \mathit{S}\in \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}\}.$$ Hence, let us illustrate the program Π for the two inputs ${\mathit{S}}_1={\mathit{S}}_0\cup {\mathit{S}}_{\mathit{a}}$ and ${\mathit{S}}_2={\mathit{S}}_0\cup {\mathit{S}}_{\mathit{ac}}$ (We omit the further atoms from the corresponding answer sets in $\hat{\mathit{F}}\cup {\mathit{\pi }}_{\mathrm{adm}}\cup {\mathit{\pi }}_{\mathrm{<}}$ , since they play no role in Π.). Indeed, we expect that S₁ does not lead to an answer set of ${\mathit{\pi }}_{\mathrm{pref}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ , while the second set S₂ corresponds to a preferred extension of F, and thus should be part of an answer set of ${\mathit{\pi }}_{\mathrm{pref}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . As discussed above, the only potential answer set I₁ of Π(S₁) contains $$\begin{array}{cc}\hfill {\mathit{S}}_1\cup & \{\mathrm{inN}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{e}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\{}\mathrm{outN}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{e}\mathrm{)}\mathrm{,}\mathrm{fail}\}.\hfill \end{array}$$ We next check whether some ${\mathit{J}}_1\subset {\mathit{I}}_1$ satisfies $\mathrm{\Pi }{\mathrm{(}{\mathit{S}}_1\mathrm{)}}^{{\mathit{I}}_1}=\mathrm{\Pi }\mathrm{(}{\mathit{S}}_1\mathrm{)}\setminus \{:-\mathrm{not}\mathrm{fail}\}$ . If this is not the case, I₁ becomes an answer set. Indeed, one can check that the set J₁ $${\mathit{S}}_{\mathit{a}}\cup \{\mathrm{inN}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{e}\mathrm{)}\}$$ satisfies $\mathrm{\Pi }{\mathrm{(}{\mathit{S}}_1\mathrm{)}}^{{\mathit{I}}_1}$ . 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 $\mathrm{inN}\mathrm{(}·\mathrm{)}$ holds are not adjacent. Finally, for rule (35), we first mention that the predicate undefeated(·) is derived for the following instantiations $\mathrm{undefeated}\mathrm{(}\mathit{a}\mathrm{)}$ , $\mathrm{undefeated}\mathrm{(}\mathit{c}\mathrm{)}$ , $\mathrm{undefeated}\mathrm{(}\mathit{e}\mathrm{)}$ . 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 ${\mathit{J}}_1\vDash \mathrm{\Pi }{\mathrm{(}{\mathit{S}}_1\mathrm{)}}^{{\mathit{I}}_1}$ . Consequently, I₁ cannot be an answer set of Π(S₁) and thus not of ${\mathit{\pi }}_{\mathrm{pref}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ .

The situation is different for set ${\mathit{S}}_2={\mathit{S}}_0\cup {\mathit{S}}_{\mathit{ac}}$ . As before, the only potential answer set I₂ of Π(S₂) contains $$\begin{array}{cc}\hfill {\mathit{S}}_2\cup & \{\mathrm{inN}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{e}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\{}\mathrm{outN}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{d}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{e}\mathrm{)}\mathrm{,}\mathrm{fail}\}.\hfill \end{array}$$ Moreover, $\mathrm{\Pi }{\mathrm{(}{\mathit{S}}_2\mathrm{)}}^{{\mathit{I}}_2}=\mathrm{\Pi }\mathrm{(}{\mathit{S}}_2\mathrm{)}\setminus \{:-\mathrm{not}\mathrm{fail}\}$ as before, and we thus seek for sets ${\mathit{J}}_2\subset {\mathit{I}}_2$ , such that ${\mathit{J}}_2\vDash \mathrm{\Pi }{\mathrm{(}{\mathit{S}}_2\mathrm{)}}^{{\mathit{I}}_2}$ . Note that rule (32) guarantees that J₂ contains at least $\mathrm{inN}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{c}\mathrm{)}$ but further $\mathrm{inN}\mathrm{(}·\mathrm{)}$ predicates could be contained in J₂. However, if the only $\mathrm{inN}\mathrm{(}·\mathrm{)}$ predicates in J₂ are $\mathrm{inN}\mathrm{(}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{c}\mathrm{)}$ , predicate eq is derived and we saturate. As well, if a further $\mathrm{inN}\mathrm{(}·\mathrm{)}$ predicate is contained in J₂ then we already know that such a set characterises a subset ${\mathit{S}}^{\prime }\subseteq \mathit{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 ${\mathit{J}}_2\subset {\mathit{I}}_2$ , such that ${\mathit{J}}_2\vDash \mathrm{\Pi }{\mathrm{(}{\mathit{S}}_2\mathrm{)}}^{{\mathit{I}}_2}$ . Thus I₂ becomes an answer set of Π(S₂) and therefore also of ${\mathit{\pi }}_{\mathrm{pref}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ . 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 $\mathit{T}\in \mathit{adm}\mathrm{(}\mathit{F}\mathrm{)}$ with ${\mathit{S}}_{\mathit{R}}^{+}\subset {\mathit{T}}_{\mathit{R}}^{+}$ 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 ${\mathit{S}}_{\mathit{R}}^{+}\not\subset {\mathit{T}}_{\mathit{R}}^{+}$ (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 ${\mathit{\pi }}_{\mathrm{undefeated}}$ and define the additional rules $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{eq}}^{+}=& \{\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\inf \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\inf \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\inf \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\inf \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{Z}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\inf \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-}\mathrm{undefeated}\mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{Z}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{Z}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{Z}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{U}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{U}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{Z}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{succ}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\hfill \\ \hfill & \phantom{\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}:-}\mathrm{undefeated}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{eqplus}:-\sup \mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{eqplus}\text{\_}\mathrm{upto}\mathrm{(}\mathit{X}\mathrm{)}\}\hfill \end{array}$$ and $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{satsemi}}=& \{\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\vee \mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}:-\arg \mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{eqplus};\hfill \\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{undefeated}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{undefeated}\mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{fail}:-\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{undefeated}\mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{fail}\mathrm{,}\arg \mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{fail}\mathrm{,}\arg \mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}:-\mathrm{not}\mathrm{fail}\}.\hfill \end{array}$$

We define ${\mathit{\pi }}_{\mathrm{semi}}={\mathit{\pi }}_{\mathrm{adm}}\cup {\mathit{\pi }}_{\mathrm{<}}\cup {\mathit{\pi }}_{\mathrm{eq}}^{+}\cup {\mathit{\pi }}_{\mathrm{undefeated}}\cup {\mathit{\pi }}_{\mathrm{satsemi}}$ and obtain the following result.

Proposition 3.8

For any AF F, $\mathrm{semi}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{semi}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

3.7. Summary and combinations of encodings

We summarise the results from this section.

Theorem 3.9

For any AF F and $\mathit{e}\in \{\mathrm{stable}\mathrm{,}\mathrm{adm}\mathrm{,}\mathrm{pref}\mathrm{,}\mathrm{semi}\mathrm{,}\mathrm{comp}\mathrm{,}\mathrm{ground}\}$ , it holds that $\mathit{e}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathit{e}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

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, ${\mathit{\pi }}_{\mathrm{ground}}$ is stratified and constraint-free. Recall that such programs have exactly one answer set; hence there is no need to distinguish between ${\vDash }_{\mathrm{c}}$ and ${\vDash }_{\mathrm{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
${\mathsf{Cred}}_{\mathit{e}}$	${\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}{\vDash }_{\mathrm{c}}\mathit{a}$	${\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}{\vDash }_{\mathrm{c}}\mathit{a}$	${\mathit{\pi }}_{\mathrm{adm}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}{\vDash }_{\mathrm{c}}\mathit{a}$	${\mathit{\pi }}_{\mathrm{semi}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}{\vDash }_{\mathrm{c}}\mathit{a}$	${\mathit{\pi }}_{\mathrm{comp}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}{\vDash }_{\mathrm{c}}\mathit{a}$	${\mathit{\pi }}_{\mathrm{ground}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\vDash \mathit{a}$
${\mathsf{Skept}}_{\mathit{e}}$	${\mathit{\pi }}_{\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}{\vDash }_{\mathrm{s}}\mathit{a}$	(trivial)	${\mathit{\pi }}_{\mathrm{pref}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}{\vDash }_{\mathrm{s}}\mathit{a}$	${\mathit{\pi }}_{\mathrm{semi}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}{\vDash }_{\mathrm{s}}\mathit{a}$	${\mathit{\pi }}_{\mathrm{ground}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\vDash \mathit{a}$	${\mathit{\pi }}_{\mathrm{ground}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\vDash \mathit{a}$

We are now able to encode more involved decision problems using our queries. As a first example, consider the ${\mathrm{\Pi }}_2^{\mathit{P}}$ -complete problem of coherence (Dunne and Bench-Capon 2002), which decides whether for a given AF F, $\mathrm{pref}\mathrm{(}\mathit{F}\mathrm{)}\subseteq \mathrm{stable}\mathrm{(}\mathit{F}\mathrm{)}$ (recall that $\mathrm{pref}\mathrm{(}\mathit{F}\mathrm{)}\supseteq \mathrm{stable}\mathrm{(}\mathit{F}\mathrm{)}$ 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 $${\mathit{\pi }}_{\mathrm{pref}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\cup \{\mathit{v}:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)};:-\mathrm{not}\mathit{v}\}$$ 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 ${\mathrm{\Pi }}_2^{\mathit{P}}$ -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 $\mathrm{inNN}\mathrm{(}·\mathrm{)}$ , $\mathrm{outNN}\mathrm{(}·\mathrm{)}$ , $\mathrm{undefeatedN}\mathrm{(}·\mathrm{)}$ and $\mathrm{undefeatedN}\text{\_}\mathrm{upto}\mathrm{(}·\mathrm{,}·\mathrm{)}$ , and denote by ${\mathit{\pi }}_{\mathrm{undefeatedN}}$ the program resulting from ${\mathit{\pi }}_{\mathrm{undefeated}}$ by using the new atoms instead of $\mathrm{inN}\mathrm{(}·\mathrm{)}$ , $\mathrm{outN}\mathrm{(}·\mathrm{)}$ , $\mathrm{undefeated}\mathrm{(}·\mathrm{)}$ and $\mathrm{undefeated}\text{\_}\mathrm{upto}\mathrm{(}·\mathrm{,}·\mathrm{)}$ , respectively. Similarly, we obtain ${\mathit{\pi }}_{\mathrm{eqN}}^{+}$ from π_eq⁺. Consider now the following program. $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{coincide}}=& {\mathit{\pi }}_{\mathrm{pref}}\cup {\mathit{\pi }}_{\mathrm{undefeatedN}}\cup {\mathit{\pi }}_{\mathrm{eqN}}^{+}\cup \hfill \\ \hfill & \phantom{\mathit{\pi }}\{\mathrm{inNN}\mathrm{(}\mathit{X}\mathrm{)}\vee \mathrm{outNN}\mathrm{(}\mathit{X}\mathrm{)}:-\arg \mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\mathit{\pi }}:-\mathrm{eqplus};\hfill \\ \hfill & \phantom{\mathit{\pi }}:-\mathrm{inNN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inNN}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\mathit{\pi }}:-\mathrm{inNN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outNN}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{undefeatedN}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\mathit{\pi }}:-\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outNN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{undefeated}\mathrm{(}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\mathit{\pi }}:-\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{defeat}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outNN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{undefeatedN}\mathrm{(}\mathit{X}\mathrm{)}\}.\hfill \end{array}$$

Corollary 3.11

Given an AF F, it holds that $\mathrm{semi}\mathrm{(}\mathit{F}\mathrm{)}=\mathrm{pref}\mathrm{(}\mathit{F}\mathrm{)}$ iff ${\mathit{\pi }}_{\mathrm{coincide}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}$ 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, Σ, σ, <) where $\mathit{A}\subseteq \mathcal{U}$ are arguments, $\mathit{R}\subseteq \mathit{A}\times \mathit{A}$ denotes the attack relation, $\mathrm{\Sigma }\subseteq \mathcal{U}$ is a non-empty set of values disjoint from A, $\mathit{\sigma }:\mathit{A}\to \mathrm{\Sigma }$ 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 $\mathrm{(}\mathit{\sigma }\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathit{\sigma }\mathrm{(}\mathit{a}\mathrm{)}\mathrm{)}\notin \ll$ .

Example 4.2

Consider the following VAF F=(A, R, Σ, σ, <). Let A={a, b, c}, $\mathit{R}=\{\mathrm{(}\mathit{b}\mathrm{,}\mathit{a}\mathrm{)}\mathrm{,}\mathrm{(}\mathit{c}\mathrm{,}\mathit{b}\mathrm{)}\}$ , $\mathrm{\Sigma }=\{\mathrm{red}\mathrm{,}\mathrm{blue}\}$ , $\mathit{\sigma }\mathrm{(}\mathit{a}\mathrm{)}=\mathrm{blue}$ , $\mathit{\sigma }\mathrm{(}\mathit{b}\mathrm{)}=\mathrm{blue}$ , $\mathit{\sigma }\mathrm{(}\mathit{c}\mathrm{)}=\mathrm{red}\mathrm{,}$ and $\mathrm{<}=\{\mathrm{(}\mathrm{red}\mathrm{,}\mathrm{blue}\mathrm{)}\}$ . The graph representation of F is as follows. We obtain that c defeats b, because (c, b)∈R and $\mathrm{(}\mathit{\sigma }\mathrm{(}\mathit{b}\mathrm{)}\mathrm{,}\mathit{\sigma }\mathrm{(}\mathit{c}\mathrm{)}\mathrm{)}\notin \ll$ holds. But, if $\mathrm{(}\mathrm{blue}\mathrm{,}\mathrm{red}\mathrm{)}\in \mathrm{<}$ , 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, $$\begin{array}{cc}\hfill \tilde{\mathit{F}}=& \{\arg \mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\}\cup \{\mathrm{att}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mid \mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\in \mathit{R}\}\cup \hfill \\ \hfill & \{\mathrm{val}\mathrm{(}\mathit{a}\mathrm{,}\mathit{\sigma }\mathrm{(}\mathit{a}\mathrm{)}\mathrm{)}\mid \mathit{a}\in \mathit{A}\}\cup \{\mathrm{valpref}\mathrm{(}\mathit{v}\mathrm{,}\mathit{w}\mathrm{)}\mid \mathit{v}\mathrm{<}\mathit{w}\}\hfill \end{array}$$ and we require a further module, which obtains the $\mathrm{defeat}\mathrm{(}·\mathrm{,}·\mathrm{)}$ relation accordingly: $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{vaf}}=& \{\mathrm{valpref}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{valpref}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Z}\mathrm{)}\mathrm{,}\mathrm{valpref}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{pref}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{valpref}\mathrm{(}\mathit{U}\mathrm{,}\mathit{V}\mathrm{)}\mathrm{,}\mathrm{val}\mathrm{(}\mathit{X}\mathrm{,}\mathit{U}\mathrm{)}\mathrm{,}\mathrm{val}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{V}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{defeat}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{att}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{pref}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)}\}.\hfill \end{array}$$ 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 and $\mathit{e}\in \{\mathrm{adm}\mathrm{,}\mathrm{pref}\}$ , $\mathit{e}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{vaf}}\cup {\mathit{\pi }}_{\mathit{e}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

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: $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{vaf}\text{\_}\mathrm{stable}}={\mathit{\pi }}_{\mathrm{cf}}\cup & \{\mathrm{attacked}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{att}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{attacked}\mathrm{(}\mathit{X}\mathrm{)}\}.\hfill \end{array}$$

Theorem 4.4

For any VAF F, $\mathrm{stable}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{vaf}}\cup {\mathit{\pi }}_{\mathrm{vaf}\text{\_}\mathrm{stable}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

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 $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{pref}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\cup & \{\mathrm{attacked}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{att}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathit{v}:-\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{not}\mathrm{attacked}\mathrm{(}\mathit{X}\mathrm{)};:-\mathrm{not}\mathit{v}\}\hfill \end{array}$$ 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 tuple $\mathit{F}=\mathrm{(}\mathit{A}\mathrm{,}{\mathit{R}}_{\mathit{d}}\mathrm{,}{\mathit{R}}_{\mathit{s}}\mathrm{)}$ where $\mathit{A}\subseteq \mathcal{U}$ is a set of arguments, and ${\mathit{R}}_{\mathit{d}}\subseteq \mathit{A}\times \mathit{A}$ and ${\mathit{R}}_{\mathit{s}}\subseteq \mathit{A}\times \mathit{A}$ are the attack, and resp., support relation of F.

An argument a defeats an argument b in F if there exists a sequence ${\mathit{a}}_1\mathrm{,}\dots \mathrm{,}{\mathit{a}}_{\mathit{n}+1}$ of arguments from A (for n≥1), such that a₁=a, and a_n+1=b, and either

$\mathrm{(}{\mathit{a}}_{\mathit{i}}\mathrm{,}{\mathit{a}}_{\mathit{i}+1}\mathrm{)}\in {\mathit{R}}_{\mathit{s}}$ for each $1⩽\mathit{i}⩽\mathit{n}-1$ and $\mathrm{(}{\mathit{a}}_{\mathit{n}}\mathrm{,}{\mathit{a}}_{\mathit{n}+1}\mathrm{)}\in {\mathit{R}}_{\mathit{d}}$ ; or

$\mathrm{(}{\mathit{a}}_1\mathrm{,}{\mathit{a}}_2\mathrm{)}\in {\mathit{R}}_{\mathit{d}}$ and $\mathrm{(}{\mathit{a}}_{\mathit{i}}\mathrm{,}{\mathit{a}}_{\mathit{i}+1}\mathrm{)}\in {\mathit{R}}_{\mathit{s}}$ 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 $\mathit{a}\to \mathit{b}$ and (a, b)∈R _s is represented by $\mathit{a}⇢\mathit{b}$ .

Example 4.7

Consider the following $\mathit{F}=\mathrm{(}\mathit{A}\mathrm{,}{\mathit{R}}_{\mathit{d}}\mathrm{,}{\mathit{R}}_{\mathit{s}}\mathrm{)}$ . Let $\mathit{A}=\{\mathit{a}\mathrm{,}\mathit{b}\mathrm{,}\mathit{c}\mathrm{,}\mathit{d}\mathrm{,}\mathit{e}\}$ , ${\mathit{R}}_{\mathit{d}}=\{\mathrm{(}\mathit{a}\mathrm{,}\mathit{e}\mathrm{)}\mathrm{,}\mathrm{(}\mathit{d}\mathrm{,}\mathit{c}\mathrm{)}\}$ and ${\mathit{R}}_{\mathit{s}}=\{\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mathrm{,}\mathrm{(}\mathit{b}\mathrm{,}\mathit{c}\mathrm{)}\mathrm{,}\mathrm{(}\mathit{d}\mathrm{,}\mathit{e}\mathrm{)}\}$ . 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 $\mathit{F}=\mathrm{(}\mathit{A}\mathrm{,}{\mathit{R}}_{\mathit{d}}\mathrm{,}{\mathit{R}}_{\mathit{s}}\mathrm{)}$ , $$\overline{\mathit{F}}=\{\arg \mathrm{(}\mathit{a}\mathrm{)}\mid \mathit{a}\in \mathit{A}\}\cup \{\mathrm{att}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mid \mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\in {\mathit{R}}_{\mathit{d}}\}\cup \{\mathrm{support}\mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\mid \mathrm{(}\mathit{a}\mathrm{,}\mathit{b}\mathrm{)}\in {\mathit{R}}_{\mathit{s}}\}\mathrm{,}$$ and for the defeat relation, we first compute the transitive closure of the support(·,·) predicate and then define $\mathrm{defeat}\mathrm{(}·\mathrm{,}·\mathrm{)}$ accordingly. $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{baf}}=& \{\mathrm{support}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{support}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Z}\mathrm{)}\mathrm{,}\mathrm{support}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{defeat}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{att}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{defeat}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{att}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{support}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Z}\mathrm{)};\hfill \\ \hfill & \phantom{\{}\mathrm{defeat}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}:-\mathrm{att}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Z}\mathrm{)}\mathrm{,}\mathrm{support}\mathrm{(}\mathit{Z}\mathrm{,}\mathit{Y}\mathrm{)}\}.\hfill \end{array}$$ 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 and $\mathit{e}\in \{\mathrm{stable}\mathrm{,}\mathrm{adm}\mathrm{,}\mathrm{pref}\}$ , $\mathit{e}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathrm{baf}}\cup {\mathit{\pi }}_{\mathit{e}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

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

Let $\mathit{F}=\mathrm{(}\mathit{A}\mathrm{,}{\mathit{R}}_{\mathit{d}}\mathrm{,}{\mathit{R}}_{\mathit{s}}\mathrm{)}$ 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 sequence ${\mathit{a}}_1\mathrm{,}\dots \mathrm{,}{\mathit{a}}_{\mathit{n}}$ (n≥2), such that a₁∈S, a _n =a, and $\mathrm{(}{\mathit{a}}_{\mathit{i}}\mathrm{,}{\mathit{a}}_{\mathit{i}+1}\mathrm{)}\in {\mathit{R}}_{\mathit{s}}$ , for each $1⩽\mathit{i}⩽\mathit{n}-1$ . A set S is closed under R _s if, 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

Let $\mathit{F}=\mathrm{(}\mathit{A}\mathrm{,}{\mathit{R}}_{\mathit{d}}\mathrm{,}{\mathit{R}}_{\mathit{s}}\mathrm{)}$ 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: $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{sadm}}=& {\mathit{\pi }}_{\mathrm{adm}}\cup \{\mathrm{supported}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{support}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{{\mathit{\pi }}_{\mathrm{cadm}}=}:-\mathrm{supported}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)}\};\hfill \\ \hfill {\mathit{\pi }}_{\mathrm{cadm}}=& {\mathit{\pi }}_{\mathrm{adm}}\cup \{:-\mathrm{support}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{{\mathit{\pi }}_{\mathrm{cadm}}=}:-\mathrm{support}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{out}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{in}\mathrm{(}\mathit{Y}\mathrm{)}\}.\hfill \end{array}$$

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

Let $\mathit{F}=\mathrm{(}\mathit{A}\mathrm{,}{\mathit{R}}_{\mathit{d}}\mathrm{,}{\mathit{R}}_{\mathit{s}}\mathrm{)}$ be a BAF. A set S⊆ A is called an s -preferred extension of F if $\mathit{S}\in \mathrm{sadm}\mathrm{(}\mathit{F}\mathrm{)}$ and for each $\mathit{T}\in \mathrm{sadm}\mathrm{(}\mathit{F}\mathrm{)}$ , $\mathit{S}\not\subset \mathit{T}$ . Likewise, a set S⊆ A is called a c -preferred extension of F if $\mathit{S}\in \mathrm{cadm}\mathrm{(}\mathit{F}\mathrm{)}$ and for each $\mathit{T}\in \mathrm{cadm}\mathrm{(}\mathit{F}\mathrm{)}$ , $\mathit{S}\not\subset \mathit{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 $\mathrm{pref}\mathrm{(}\mathit{F}\mathrm{)}=\{\{\mathit{a}\mathrm{,}\mathit{b}\mathrm{,}\mathit{d}\}\}$ , $\mathrm{spref}\mathrm{(}\mathit{F}\mathrm{)}=\{\{\mathit{d}\}\mathrm{,}\{\mathit{a}\mathrm{,}\mathit{b}\}\}$ , and $\mathrm{cpref}\mathrm{(}\mathit{F}\mathrm{)}=\{\varnothing \}$ .

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 $$\begin{array}{cc}\hfill {\mathit{\pi }}_{\mathrm{spref}}=& {\mathit{\pi }}_{\mathrm{sadm}}\cup {\mathit{\pi }}_{\mathrm{<}}\cup {\mathit{\pi }}_{\mathrm{eq}}\cup {\mathit{\pi }}_{\mathrm{undefeated}}\cup {\mathit{\pi }}_{\mathrm{satpref}}\cup \hfill \\ \hfill & \phantom{\mathit{\pi }}\{\mathrm{supported}\mathrm{(}\mathit{X}\mathrm{)}:-\mathrm{inN}\mathrm{(}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{support}\mathrm{(}\mathit{Y}\mathrm{,}\mathit{X}\mathrm{)};\hfill \\ \hfill & \phantom{\mathit{\pi }}\mathrm{fail}:-\mathrm{supported}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{defeated}\mathrm{(}\mathit{X}\mathrm{)}\};\hfill \\ \hfill {\mathit{\pi }}_{\mathrm{cpref}}=& {\mathit{\pi }}_{\mathrm{cadm}}\cup {\mathit{\pi }}_{\mathrm{<}}\cup {\mathit{\pi }}_{\mathrm{eq}}\cup {\mathit{\pi }}_{\mathrm{undefeated}}\cup {\mathit{\pi }}_{\mathrm{satpref}}\cup \hfill \\ \hfill & \phantom{\mathit{\pi }}\{\mathrm{fail}:-\mathrm{support}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{Y}\mathrm{)};\hfill \\ \hfill & \phantom{\mathit{\pi }}\mathrm{fail}:-\mathrm{support}\mathrm{(}\mathit{X}\mathrm{,}\mathit{Y}\mathrm{)}\mathrm{,}\mathrm{outN}\mathrm{(}\mathit{X}\mathrm{)}\mathrm{,}\mathrm{inN}\mathrm{(}\mathit{Y}\mathrm{)}\}.\hfill \end{array}$$

Theorem 4.12

For any BAF F and $\mathit{e}\in \{\mathrm{sadm}\mathrm{,}\mathrm{cadm}\mathrm{,}\mathrm{spref}\mathrm{,}\mathrm{cpref}\}$ , we have $\mathit{e}\mathrm{(}\mathit{F}\mathrm{)}\cong \mathcal{AS}\mathrm{(}{\mathit{\pi }}_{\mathit{baf}}\cup {\mathit{\pi }}_{\mathit{e}}\mathrm{(}\hat{\mathit{F}}\mathrm{)}\mathrm{)}$ .

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).