Sage Journals: Discover world-class research

Abstract

Abstract dialectical frameworks (ADFs) constitute a recent and powerful generalisation of Dung's argumentation frameworks (AFs), where the relationship between the arguments can be specified via Boolean formulas. Recent results have shown that this enhancement comes with the price of higher complexity compared to AFs. In fact, acceptance problems in the world of ADFs can be hard even for the third level of the polynomial hierarchy. In order to implement reasoning problems on ADFs, systems for quantified Boolean formulas (QBFs) thus are suitable engines to be employed. In this paper we give complexity sensitive QBF encodings of ADF problems generalising recent work on QBFs for AF labellings. Our encodings provide a uniform and modular way of translating reasoning in ADFs to QBFs, that can be used as the basis for novel systems for ADF reasoning.

Keywords

abstract dialectical frameworks quantified Boolean formulas computational complexity encodings

1. Introduction

Since its invention by Dung (1995), abstract argumentation constitutes one of the main research branches for computational models of argument. Hereby, the conflict resolution between arguments is done by abstracting away from the arguments' contents, yielding a simple yet powerful framework for reasoning used as a core model in many argumentation tasks and applications. Although very general, Dung's argumentation frameworks (AFs) do not directly support modelling more complex interactions between arguments. For this and similar issues, several extensions of AFs have been proposed to date (e.g. those presented by Baroni, Cerutti, Giacomin, Guida, 2011; Bench-Capon, 2003; Cayrol & Lagasquie-Schiex, 2005; Brewka, Polberg, & Woltran, 2014 provide a survey of this line of research), one of the most general being that of abstract dialectical frameworks (ADFs) by Brewka and Woltran (2010). In this last framework, acceptance conditions in the form of arbitrary Boolean formulas are associated to every argument. Proper generalisations of Dung's semantics have been given by Brewka, Ellmauthaler, Strass, Wallner, and Woltran (2013).

Various reasoning tasks can be defined on abstract argumentation frameworks, some of the central ones being those that evaluate the ‘acceptability’ of an argument with respect to a given framework and semantics. Already for AFs, most of the reasoning tasks have been shown to suffer from high computational complexity (see e.g. the work by Dunne & Bench-Capon, 2002). For ADFs, the complexity of many of the main reasoning tasks with respect to the generalised semantics jump up one level of the polynomial hierarchy (as has been shown by Strass & Wallner, 2014; Wallner, 2014), resulting in some of the reasoning tasks even being on the third level of the polynomial hierarchy.

One successful approach for implementing problems of high computational complexity is to employ a so-called reduction approach (Charwat, Dvořák, Gaggl, Wallner, & Woltran, 2015). Hereby the underlying idea is to exploit existing efficient software which has originally been developed for other purposes. To this end, one has to formalise the reasoning problems within other formalisms like, for instance, propositional logic, thus directly benefiting from the high level of sophistication today's systems for SAT (satisfiability in propositional logic) have reached (Franco & Martin, 2009).

In this work we follow this idea and present translations of the main reasoning tasks defined for ADFs into the satisfiability problem of quantified Boolean formulas (QBFs). QBFs are an extension of propositional logic, allowing for quantification over propositional atoms (Büning Bubeck, 2009). Its associated satisfiability problem (QSAT) is complete for PSPACE while types of QBFs classified according to the structure of quantification provide us with complete problems for each level of the polynomial hierarchy. These results indicate that reasoning problems for ADFs can be efficiently transformed into QSAT problems with a certain quantifier structure. Employing the framework of QBFs thus allows for

a uniform translation of ADF reasoning tasks into one widely studied formal language;

complexity sensitive encodings, that is, encodings to a subclass of QBFs whose complexity matches the complexity of the encoded reasoning task; and

utilisation of ever more efficient solvers for QSAT (see, e.g. the results presented by Lonsing & Seidl, 2013).

Providing reductions to QSAT is increasingly seen as a promising approach to tackle computational problems in the polynomial hierarchy. Planning (see the work by Ferraris & Giunchiglia, 2000; Rintanen, 1999) and formal methods for determining correctness of software systems (as shown by Benedetti & Mangassarian, 2008; Bryant, Lahiri, & Seshia, 2003; Giunchiglia, Narizzano, & Tacchella, 2007; Ling, Singh, & Brown, 2005; Mneimneh & Sakallah, 2003) are notable examples of areas where QSAT solvers have found their way into practice. Moreover, reductions of many reasoning problems in different areas including knowledge representation and reasoning (reductions of autoepistemic, default logic, disjunctive logic programming, and circumscription problems into QSAT are given by Egly, Eiter, Tompits, & Woltran, 2000 for example) into QSAT have also been proposed in the literature. Giunchiglia, Marin, and Narizzano (2009) list several more examples of reductions of computational problems to QSAT.

Our work specifically continues the line of of study that has been initiated for Dung style AFs by Egly and Woltran (2006) and Arieli and Caminada (2013). In both of these works, reductions of the problems of evaluating Dung style AFs into the setting of quantified Boolean logic are given. The more recent work by Arieli and Caminada in particular, which is based on a so called ‘labelling approach’ (Caminada & Gabbay, 2009) to defining the semantics of AFs presents some parallels with the approach followed by Brewka et al. (2013) and Strass (2013), respectively, to define the semantics for ADFs. Thus this work has been particularly influential for the approach we follow to give encodings for the reasoning problems defined for ADFs.

Summarising, in this article we provide complexity sensitive encodings of all the main reasoning problems defined for ADFs (evaluation, credulous acceptance, skeptical acceptance and verification) with respect to the most prominent semantics (two valued models, admissible, complete, preferred, grounded and stable) in the context of QBFs. Further, we present the formal framework required to prove that our encodings are correct as well as detailed proofs. This article extends the work of Diller, Wallner, and Woltran (2014) and Diller (2014) by three novel contributions: (1) we additionally consider the reasoning task of verifying a given candidate solution, (2) we expanded all proofs, and (3) we present here complexity sensitive encodings also for the grounded and stable semantics.

2. Background

2.1. Quantified Boolean formulas

We recall the necessary background of Boolean logic and QBFs: for further details see also the survey of the theory of QBFs by Büning & Bubeck (2009).

Quantified Boolean logic is an extension to propositional logic. The basis of propositional logic is a set of propositional variables $P$ , to which we also refer to as atoms. Propositional formulas are built as usual from the connectives $\land, \lor$ , and ¬, denoting the logical conjunction, disjunction and negation, respectively. As for truth constants, we use ⊤ for the value true and $⊥ : = \neg ⊤$ for false. QBFs additionally use the universal quantifier ∀ and the existential quantifier ∃. If ϕ is a (quantified) Boolean formula, then $Q p φ$ is a QBF with $Q \in {\forall, \exists}$ and $p \in P$ . QBFs may be nested using the logical connectives. Further $Q p_{1}, p_{2}, \dots, p_{n} φ$ or also $Q P φ$ with $P = {p_{1}, p_{2}, \dots, p_{n}}$ is a shorthand for $Q p_{1} Q p_{2}, \dots, Q p_{n} φ$ . The order of variables in consecutive quantifiers of the same type does not matter. We define shorthands for (material) implication and equivalence: $φ \to φ^{'} : = \neg φ \lor φ^{'}$ and $φ \leftrightarrow φ^{'} : = (φ \to φ^{'}) \land (φ^{'} \to φ)$ .

A propositional variable p in a QBF ϕ is free if it does not occur within the scope of a quantifier; otherwise it is bound. If ϕ contains no free variable, then ϕ is said to be closed; otherwise it is open. Further we will write $φ [p / ψ]$ to denote the result of uniformly substituting each free occurrence of p with ψ in the formula ϕ.

An interpretation $\hat{v} : P \to {t, f}$ defines for each propositional variable a truth assignment. We sometimes explicitly highlight that a $\hat{v}$ is defined on a set $P \subseteq P$ . The evaluation on atoms generalises as usual to arbitrary formulas: given a formula ϕ and an interpretation $\hat{v}$ , then ϕ evaluates to true under $\hat{v}$ ( $\hat{v}$ satisfies ϕ or $\hat{v}$ is a model of ϕ, denoted by $\hat{v} ⊧ φ$ ) if one of the following holds, with $p \in P$ and QBFs ψ, $ψ_{1}$ and $ψ_{2}$ .

$φ = p$ and $\hat{v} (p) = t$ ;

$φ = ⊤$ ;

$φ = \neg ψ$ and ψ does not evaluate to true under $\hat{v}$ ;

$φ = ψ_{1} \land ψ_{2}$ and both $ψ_{1}$ and $ψ_{2}$ evaluate to true under $\hat{v}$ ;

$φ = ψ_{1} \lor ψ_{2}$ and one of $ψ_{1}$ and $ψ_{2}$ evaluates to true under $\hat{v}$ ;

$φ = \exists p ψ$ and one of $ψ [p / ⊤]$ and $ψ [p / ⊥]$ evaluates to true under $\hat{v}$ ;

$φ = \forall p ψ$ and both $ψ [p / ⊤]$ and $ψ [p / ⊥]$ evaluate to true under $\hat{v}$ .

We extend the evaluation function $\hat{v}$ to formulas, that is, $\hat{v} (φ)$ is the evaluation of ϕ under $\hat{v}$ . Note that the concepts of satisfiability and validity which can be extended in a direct manner from propositional logic to QBFs are equivalent for closed formulas; hence, closed QBFs that are satisfiable are often called ‘true’ while those which are unsatisfiable are called ‘false’.

Given two interpretations $\hat{v}$ and $\hat{w}$ as well as a set of propositional variables P, $\hat{v} [P / \hat{w} (P)]$ denotes the interpretation ${\hat{v}}^{'}$ defined as:

${\hat{v}}^{'} (p) : = \hat{w} (p)$ for $p \in P$ .

${\hat{v}}^{'} (q) : = \hat{w} (q)$ if $q \in P$ and $q \notin P$ .

We will often use the simplified notation $\hat{v} [p / x]$ with $x \in {t, f}$ in the case that $P = {p}$ and $\hat{w} (p) = x$ in the definition above. (Observe that we use brackets both to denote ‘substitution’ in the context of formulas and interpretations.)

The following lemma and corollary are straightforward consequences of the semantics of QBFs that we make often use of for proving the correctness of the encodings we present in this work.

Lemma 2.1.
Let ψ be a QBF, and P a set of propositional variables. If $φ = \exists P ψ$ $(φ = \forall P ψ),$ then $\hat{v} ⊧ φ$ if and only if $\hat{v} [P / \hat{w} (P)] ⊧ ψ$ for some (all) interpretation(s) $\hat{w}$ .
Corollary 2.2.
Let ψ be a closed QBF, and P a set of propositional variables. If $φ = \exists P ψ$ $(φ = \forall P ψ),$ then ϕ is true if and only if for some (all) interpretation(s) $\hat{v},$ $\hat{v} ⊧ ψ$ .

One final use of brackets as notational device we introduce for QBFs is $φ [P / \hat{v} (P)]$ to denote the formula ϕ where every occurrence of any variable $p \in P$ is replaced for ⊤ in case that $\hat{v} (p) = t$ and replaced for ⊥ in the case that $\hat{v} (p) = f$ . For $φ [{p} / \hat{v} ({p})]$ we use the simplified notation $φ [p / \hat{v} (p)]$ . Another immediate result we make use of in this work is the following.
Lemma 2.3.
Let $\hat{v}$ be an interpretation, ϕ a QBF, and $p \in P$ . Then $\hat{v} ⊧ φ$ if and only if $\hat{v} ⊧ φ [p / \hat{v} (p)]$ . Also, if P are all the free variables of ϕ, then $\hat{v} ⊧ φ$ if and only if for all interpretations $\hat{w}$ it is the case that $\hat{w} ⊧ φ [P / \hat{v} (P)]$ .

Normal forms of (quantified) formulas play an important role for theoretical and practical purposes. A well-known normal form for QBFs is the prenex normal form (PNF). A QBF ϕ is in PNF if ϕ is of the form $Q_{1} p_{1} Q_{2} p_{2}, \dots, Q_{n} p_{n} ψ$ with $p_{i} \in P$ and $Q_{i} \in {\forall, \exists}$ for $1 ⩽ i ⩽ n$ as well as ψ being a quantifier-free formula. The computational complexity of deciding whether ϕ is satisfiable depends on the prefix type. Every propositional formula has the prefix type $Σ_{0} = Π_{0}$ . Let ϕ be a closed QBF with prefix type $Σ_{i}$ (respectively, $Π_{i}$ ) and P a set of $m > 0$ propositional variables. Then the formula $\forall P φ$ (respectively, $\exists P φ$ ) is of type $Π_{i + 1}$ (respectively, $Σ_{i + 1}$ ) for $i ⩾ 0$ .

We assume familiarity with the complexity classes P, $NP$ and $coNP$ . We also make use of the polynomial hierarchy, that can be defined (using oracle Turing machines as superscript) as follows: $Σ_{0}^{P} = Π_{0}^{P} = P$ , $Σ_{i + 1}^{P} = {NP}^{Σ_{i}^{P}}$ , $Π_{i + 1}^{P} = {coNP}^{Σ_{i}^{P}}$ for $i ⩾ 0$ . In general, deciding whether a QBF ϕ is satisfiable is $Σ_{k}^{P}$ complete if ϕ has prefix type $Σ_{k}$ and otherwise if ϕ has prefix type $Π_{k}$ , then the problem is $Π_{k}^{P}$ complete ( $k ⩾ 1$ ).

A language is in the complexity class $D^{P}$ if it is the intersection of a language in $NP$ and a language in $coNP$ . The canonical problem of $D^{P}$ is SAT UNSAT, the problem of deciding whether for a pair $(φ_{1}, φ_{2})$ of propositional formulas, $φ_{1}$ is satisfiable and $φ_{2}$ is unsatisfiable.
2.2. Abstract dialectical frameworks

An abstract dialectical framework (ADF) is a directed graph whose vertices represent statements which can be accepted or not. The links represent dependencies: the status of a node s only depends on the status of its parents (denoted $parents (s)$ ), that is, the nodes with a direct link to s. In addition, each node s has an associated acceptance condition $C_{s}$ specifying the conditions under which s can be accepted. $C_{s}$ is a function assigning to each subset of $parents (s)$ one of the truth values t , f .

Definition 2.4.
An ADF is a tuple $D = (S, L, C)$ where
S is a set of statements (positions, nodes $),$

$L \subseteq S \times S$ is a set of links,

$C = {C_{s}}_{s \in S}$ is a set of total functions $C_{s} : 2^{parents (s)} \to {t, f},$ one for each statement s. $C_{s}$ is called acceptance condition of s.

We represent the acceptance conditions C as a collection ${φ_{s}}_{s \in S}$ of propositional formulas, which provide a compact way to specify Boolean functions. This leads to the logical representation of ADFs we use in this paper where an ADF D is a pair $(S, C)$ with the set of links L implicitly given as $(a, b) \in L$ iff a appears in $φ_{b}$ .

We consider ADF semantics as defined by Brewka et al. (2013). A semantics σ assigns to an ADF D a collection of two or three valued interpretations, denoted by $σ (D)$ . To distinguish between interpretations of ADFs and QBFs we use $\hat{v}, \hat{w}$ for QBF interpretations and $v, w$ for interpretations of ADFs. For σ we consider in this paper admissible, complete, grounded, preferred, model and stable semantics of ADFs. We denote the semantics by $adm$ , $com$ , $grd$ , $prf$ , $\mod$ and $stb$ .

The interpretations map statements to truth values. We use ${t, f, u}$ as truth values, denoting true, false and undecided, respectively. The three truth values are partially ordered by $⩽_{i}$ according to their information content: we have $u <_{i} t$ and $u <_{i} f$ and no other pair in $<_{i}$ . The information ordering $⩽_{i}$ extends in a straightforward way to interpretations $v_{1}, v_{2}$ over S in that $v_{1} ⩽_{i} v_{2}$ iff $v_{1} (s) ⩽_{i} v_{2} (s)$ for all $s \in S$ .

A three valued interpretation v is two valued if all statements are mapped to either true or false. For a three valued interpretation v, we say that a two valued interpretation w extends v iff $v ⩽_{i} w$ . This means that all statements mapped to u by v are mapped to t or f by w. We denote by ${[v]}_{2}$ the set of all two valued interpretations that extend v.

For an ADF $D = (S, C)$ , $s \in S$ and a three valued interpretation v, the characteristic function $Γ_{D} (v) = v^{'}$ is given by $v^{'} (s) = \{\begin{matrix} t if w (φ_{s}) = t for all w \in {[v]}_{2}, \\ f if w (φ_{s}) = f for all w \in {[v]}_{2}, \\ u otherwise . \end{matrix}$ That is, the operator returns a three valued interpretation, mapping a statement s to t , or, respectively f , if all two-valued interpretations extending v evaluate $φ_{s}$ to true, respectively false. If there are $w_{1}, w_{2} \in {[v]}_{2}$ , s.t. $w_{1} (φ_{s}) = t$ and $w_{2} (φ_{s}) = f$ , then the result is u . Note that the characteristic function is defined on three-valued interpretations, while we evaluate acceptance conditions under two-valued interpretations (two-valued extensions of three-valued interpretations).
Definition 2.5.
Let $D = (S, L, C)$ be an ADF. A three valued interpretation v is
in $adm (D)$ if $v ⩽_{i} Γ_{D} (v);$

in $com (D)$ if $v = Γ_{D} (v);$

in $grd (D)$ if $v \in com (D)$ and there is no $w \in com (D)$ with $w <_{i} v;$

in $prf (D)$ if $v \in adm (D)$ and there is no $w \in adm (D)$ with $v <_{i} w$ .
No other elements except those stipulated by the items above are in $adm (D),$ $com (D),$ $grd (D)$ and $prf (D)$ , respectively.

For any ADF one has that all preferred interpretations are complete and all complete interpretations are admissible. Brewka et al. (2013) have also shown that the operator $Γ_{D}$ is monotonic for any ADF D, hence an interpretation v is the grounded interpretation of an ADF D if and only if it is equal to the $⩽_{i}$ least fixpoint (l.f.p.) of $Γ_{D}$ . The l.f.p. can be calculated by iteratively applying $Γ_{D}$ starting with the interpretation $U^{S}$ mapping all statements $s \in S$ of D to u . Then $Γ_{D}^{0} : = U^{S}$ and $Γ_{D}^{i + 1} : = Γ_{D} (Γ_{D}^{i})$ for $i ⩾ 0$ .

The $\mod$ and $stb$ semantics rely on two valued interpretations. A two valued interpretation v is a model of an ADF $D = (S, C = {φ_{s}}_{s \in S})$ if $v (s) = v (φ_{s})$ for all $s \in S$ . Stable models are defined via a reduct.
Definition 2.6.
Let $D = (S, L, C)$ be an ADF with $C = {φ_{s}}_{s \in S}$ . A two-valued model v of D is a stable model of D iff $E_{v} = {s \in S ∣ v (s) = t}$ equals the statements set to true in the grounded interpretation of the reduced ADF $D^{v} = (E_{v}, L^{v}, C^{v}),$ where $L^{v} = L \cap (E_{v} \times E_{v})$ and for $s \in E_{v}$ we set $φ_{s}^{v} = φ_{s} [b / ⊥ : v (b) = f]$ .
Example 2.7.
In Figure 1 we see an example ADF $D = ({a, b, c}, C)$ with $φ_{a} = b \lor \neg b \equiv ⊤$ , $φ_{b} = b$ and $φ_{c} = c \to b$ . The acceptance conditions are also shown below the statements.
Figure 1.
ADF example.
The admissible interpretations of D are shown in Table 1. Furthermore the right-most column shows further semantics the interpretations belong to. For instance the interpretation $v_{8}$ mapping each statement to true is admissible, complete and preferred in D and a model of D. This ADF has no stable model. The only model of D is $v_{8}$ , with the reduct of this model being $D^{v_{8}} = D$ . The grounded interpretation of D is $v_{6}$ , which is different than $v_{8}$ . Therefore $v_{8}$ is not a stable model.

We recall three important reasoning tasks on ADFs for a semantics σ. A statement s is credulously accepted in an ADF D for σ if s is true in at least one $v \in σ (D)$ . The corresponding decision problem is denoted by ${Cred}_{σ}$ . If s is true in all $v \in σ (D)$ , then it is skeptically accepted in D w.r.t. σ, the decision problem denoted by ${Skept}_{σ}$ . Lastly, the verification problem, ${Ver}_{σ}$ , decides whether a given three (two) valued interpretation v is a σ interpretation for a given ADF D, that is, whether it holds that $v \in σ (D)$ . The computational complexity of reasoning in ADFs is summarised in Table 2. The results were shown by Brewka et al. (2013), Strass and Wallner (2014) and Wallner (2014).
Table 1.
All admissible interpretations of the ADF from Figure 1.

a b c

$v_{1}$ u u u $adm$

$v_{2}$ u f u $adm$

$v_{3}$ u t u $adm$

$v_{4}$ t t u $adm$

$v_{5}$ u t t $adm$

$v_{6}$ t u u $adm$ , $com$ , $grd$

$v_{7}$ t f u $adm$ , $com$ , $prf$

$v_{8}$ t t t $adm$ , $com$ , $prf$ , $\mod$

Note: Right-most column shows further semantics the interpretations belong to.

Table 2.
Complexity results for semantics of ADFs.

σ $adm$ $com$ $prf$ $grd$ $\mod$ $stb$

${Cred}_{σ}$ $Σ_{2}^{P}$ -c $Σ_{2}^{P}$ -c $Σ_{2}^{P}$ -c coNP-c NP-c $Σ_{2}^{P}$ -c

${Skept}_{σ}$ trivial coNP-c $Π_{3}^{P}$ -c coNP-c coNP-c $Π_{2}^{P}$ -c

${Ver}_{σ}$ coNP-c $D^{P}$ -c $Π_{2}^{P}$ -c $D^{P}$ -c in P coNP-c

Example 2.8.
Continuing Example 2.7 we can see that a is skeptically accepted w.r.t. preferred semantics in the ADF D. (i.e. ${Skept}_{prf} (a, D)$ is true). The statement b is not skeptically accepted for preferred semantics, however it is credulously accepted under this semantics. In fact here all statements are credulously accepted under admissible, complete, preferred and model semantics. As on all ADFs, credulous and skeptical acceptance coincide for grounded semantics and in this example only a is accepted w.r.t. the grounded semantics.
3. Encodings

	a	b	c
$v_{1}$	u	u	u	$adm$
$v_{2}$	u	f	u	$adm$
$v_{3}$	u	t	u	$adm$
$v_{4}$	t	t	u	$adm$
$v_{5}$	u	t	t	$adm$
$v_{6}$	t	u	u	$adm$ , $com$ , $grd$
$v_{7}$	t	f	u	$adm$ , $com$ , $prf$
$v_{8}$	t	t	t	$adm$ , $com$ , $prf$ , $\mod$

σ	$adm$	$com$	$prf$	$grd$	$\mod$	$stb$
${Cred}_{σ}$	$Σ_{2}^{P}$ -c	$Σ_{2}^{P}$ -c	$Σ_{2}^{P}$ -c	coNP-c	NP-c	$Σ_{2}^{P}$ -c
${Skept}_{σ}$	trivial	coNP-c	$Π_{3}^{P}$ -c	coNP-c	coNP-c	$Π_{2}^{P}$ -c
${Ver}_{σ}$	coNP-c	$D^{P}$ -c	$Π_{2}^{P}$ -c	$D^{P}$ -c	in P	coNP-c

In this section we present the encodings of reasoning tasks for ADFs into QBFs. After dealing with some preliminaries for our encodings, we develop for each semantics $σ \in {adm, com, grd, prf, \mod, stb}$ a defining encoding function, denoted by $E_{σ}$ . Given an ADF $D = (S, C)$ , $E_{σ}$ returns a QBF whose models correspond to the σ interpretations of D. Such defining encoding functions return the encoding of the enumeration problem for the different semantics and can be used in a generic fashion to provide encodings for the reasoning tasks we consider in this work. We describe how to do so at the end of Section 3.2.

This method for providing encodings has the advantage of being general in the sense that the encodings of the reasoning tasks we provide at the end of Section 3.2 for some semantics σ remain correct if the defining encoding function $E_{σ}$ is redefined. On the other hand, whether or not the encodings for the reasoning tasks are mapped to a fragment of QSAT that matches the complexity of the tasks depends on the definition of the encoding function. For a few of the reasoning tasks we consider in this work, the defining encoding functions we provide result in encodings that are not sensitive to the complexity of the tasks. These cases either are equivalent to some other reasoning task for which we provide encodings that are adequate with respect to the complexity, or otherwise we provide alternative complexity sensitive encodings in Section 3.3.

As indicated above, we begin with some preliminaries. To express constraints on the values to which an interpretation on ADFs can map statements, in our encodings we make use of variables that stand for the statements of an ADF. Since the definitions of semantics of ADFs often refer to several interpretations (e.g. the extensions of a given interpretation) to express such definitions in the language of quantified Boolean logic we in fact need to use several disjoint sets of propositional variables standing for statements to implicitly refer to these different interpretations in our encodings. We generate such sets by using priming (with $p^{'}$ denoting the primed version of a propositional variable p) on a base set of variables representing the statements of a given ADF. We call variables which stand for statements of ADFs variable set copies of the set of statements.

Definition 3.1.
Let S be a set of statements. Then (by abuse of notation) S as a set of propositional variables is a variable set copy of S. If P is a variable set copy of S, then so is $P^{'} : = {p^{'} ∣ p \in P}$ .

The (meta) notation $\bar{S}$ refers to an arbitrary variable set copy of S. $\bar{s}$ then denotes the variable corresponding to $s \in S$ in $\bar{S}$ . Given a propositional formula ϕ, $\bar{φ}$ is ϕ but with each variable s appearing in ϕ replaced with $\bar{s}$ . For an ADF $D = (S, C = {φ_{s}}_{s \in S})$ we define $\bar{C} : = {{\bar{φ}}_{s}}_{s \in S}$ . $\bar{\bar{S}}$ also refers to an arbitrary variable set copy of S. $\bar{\bar{s}},$ $\bar{\bar{φ}}$ and $\bar{\bar{C}}$ are defined analogously to $\bar{s},$ $\bar{φ},$ and $\bar{C}$ .

The purpose of introducing the notation $\bar{S}$ and $\bar{\bar{S}}$ in Definition 3.1 is that this enables stating the content of the propositions in this section in a manner that covers any possible variable set copy that can be used when instantiating the encodings the propositions refer to. This makes it possible to simplify proofs about properties of encodings which are constructed in a modular fashion.

To encode expressions about two valued interpretations on a set of statements S as QBFs we use a variable set copy of S. To refer to three valued interpretations inside QBFs on the other hand we follow the procedure that has already been used by Arieli and Caminada (2013) to encode expressions about (three valued) labellings for AFs. Specifically, we assume that for every set $\bar{S}$ of propositional variables representing statements of some ADF the alphabet of QBFs also contains the set of signed variables corresponding to $\bar{S}$ .
Definition 3.2.
Let $\bar{S}$ be a variable set copy of a set of statements S. Then ${\bar{S}}_{3} : = {{\bar{s}}^{\oplus} ∣ s \in S} \cup {{\bar{s}}^{⊖} ∣ s \in S}$ is the set of signed variables associated to $\bar{S}$ .

The intended meaning of ${\bar{s}}^{\oplus}$ is that s is accepted and ${\bar{s}}^{⊖}$ that s is rejected under some interpretation. Intuitively, a statement is undecided if both ${\bar{s}}^{\oplus}$ and ${\bar{s}}^{⊖}$ are false in a model.

ADF semantics are based on three or two truth values. Since there are four possible truth value assignments for a statement s via ${\bar{s}}^{\oplus}, {\bar{s}}^{⊖} \in {\bar{S}}_{3}$ , we need to restrict attention to coherent interpretations for QBFs, which exclude the possibility for a model to satisfy both ${\bar{s}}^{\oplus}$ and ${\bar{s}}^{⊖}$ .
Definition 3.3.
Let $\bar{S}$ be a variable set copy of a set of statements of S. A two valued interpretation $\hat{v}$ is coherent on ${\bar{S}}_{3}$ if there is no $s \in S$ such that $\hat{v} ({\bar{s}}^{\oplus}) = t$ and $\hat{v} ({\bar{s}}^{⊖}) = t$ .

We now formally define the correspondence we require of the models of the QBFs returned by a defining encoding $E_{σ}$ for a semantics σ and the σ interpretations of the ADFs.
Definition 3.4.
Let S be a set of statements and $\bar{S}$ a variable set copy of S. A two valued interpretation $\hat{v}$ on $\bar{S}$ corresponds to a two valued interpretation v on S, denoted as $\hat{v} ≅_{\bar{S}} v$ if $v (s) = \hat{v} (\bar{s})$ for all $s \in S$ . A coherent two valued interpretation ${\hat{v}}^{'}$ on ${\bar{S}}_{3}$ corresponds to a three valued interpretation $v^{'}$ on S, denoted as ${\hat{v}}^{'} ≅_{{\bar{S}}_{3}} v^{'}$ if the following three conditions are met:
$v^{'} (s) = t$ if and only if ${\hat{v}}^{'} ({\bar{s}}^{\oplus}) = t$ and ${\hat{v}}^{'} ({\bar{s}}^{⊖}) = f;$

$v^{'} (s) = f$ if and only if ${\hat{v}}^{'} ({\bar{s}}^{\oplus}) = f$ and ${\hat{v}}^{'} ({\bar{s}}^{⊖}) = t;$ and

$v^{'} (s) = u$ if and only if ${\hat{v}}^{'} ({\bar{s}}^{\oplus}) = f$ and ${\hat{v}}^{'} ({\bar{s}}^{⊖}) = f$ .

The following lemma is a straightforward consequence of Definition 3.4 we make often use of in the proofs of correctness of the encodings we provide in this work.
Lemma 3.5.
Let S be a set of statements, $\bar{S}$ and $\bar{\bar{S}}$ variable set copies of S, ${\hat{v}}_{1}$ and ${\hat{v}}_{2}$ two valued (QBF) interpretations, and $v_{1}$ and $v_{2}$ three or two valued interpretations on S.
Assume that ${\bar{S}}_{3}$ and ${\bar{\bar{S}}}_{3}$ are disjoint, $\hat{v_{1}}$ is coherent on ${\bar{S}}_{3},$ $\hat{v_{2}}$ is coherent on ${\bar{\bar{S}}}_{3},$ $\hat{v_{1}} ≅_{{\bar{S}}_{3}} v_{1}$ and $\hat{v_{2}} ≅_{{\bar{\bar{S}}}_{3}} v_{2}$ . Then $\hat{v} : = \hat{v_{1}} [{\bar{\bar{S}}}_{3} / \hat{v_{2}} ({\bar{\bar{S}}}_{3})]$ is also coherent on each of ${\bar{S}}_{3}$ and ${\bar{\bar{S}}}_{3},$ and it is also the case that $\hat{v} ≅_{{\bar{S}}_{3}} v_{1}$ and $\hat{v} ≅_{{\bar{\bar{S}}}_{3}} v_{2}$ .

Assume that $\hat{v_{1}}$ is coherent on ${\bar{S}}_{3},$ $\hat{v_{1}} ≅_{{\bar{S}}_{3}} v_{1}$ and $\hat{v_{2}} ≅_{\bar{\bar{S}}} v_{2}$ . Then $\hat{v} : = \hat{v_{1}} [\bar{\bar{S}} / \hat{v_{2}} (\bar{\bar{S}})]$ is also coherent on ${\bar{S}}_{3}$ and it is also the case that $\hat{v} ≅_{{\bar{S}}_{3}} v_{1}$ and $\hat{v} ≅_{\bar{\bar{S}}} v_{2}$ .

Assume that $\hat{v_{2}}$ is coherent on ${\bar{\bar{S}}}_{3},$ $\hat{v_{1}} ≅_{\bar{S}} v_{1}$ and $\hat{v_{2}} ≅_{{\bar{\bar{S}}}_{3}} v_{2}$ . Then $\hat{v} : = \hat{v_{1}} [{\bar{\bar{S}}}_{3} / \hat{v_{2}} ({\bar{\bar{S}}}_{3})]$ is also coherent on ${\bar{\bar{S}}}_{3}$ and it is also the case that $\hat{v} ≅_{\bar{S}} v_{1}$ and $\hat{v} ≅_{{\bar{\bar{S}}}_{3}} v_{2}$ .

Assume that $\bar{S}$ and $\bar{\bar{S}}$ are disjoint, $\hat{v_{1}} ≅_{\bar{S}} v_{1}$ and $\hat{v_{2}} ≅_{\bar{\bar{S}}} v_{2}$ . Then for $\hat{v} : = \hat{v_{1}} [{\bar{\bar{S}}}_{3} / \hat{v_{2}} ({\bar{\bar{S}}}_{3})]$ it is also the case that $\hat{v} ≅_{\bar{S}} v_{1}$ and $\hat{v} ≅_{\bar{\bar{S}}} v_{2}$ .

Proof (sketch)
Let $T_{1} = {\bar{S}}_{3}$ and $T_{2} = {\bar{\bar{S}}}_{3}$ in item (1), $T_{1} = {\bar{S}}_{3}$ and $T_{2} = \bar{\bar{S}}$ in item (2), $T_{1} = \bar{S}$ and $T_{2} = {\bar{\bar{S}}}_{3}$ in item (3) and $T_{1} = \bar{S}$ and $T_{2} = \bar{\bar{S}}$ in item (4). Then all these items follow from the fact that $\hat{v}$ and $\hat{v_{1}}$ as defined in each of the items agree on the variables in $T_{1}$ while $\hat{v}$ and ${\hat{v}}_{2}$ agree on the variables in $T_{2}$ (and that $T_{1}$ and $T_{2}$ are disjoint).

We are finally in a position to provide the formal definition of a defining encoding function $E_{σ}$ for a given semantics σ for ADFs. Given an ADF $D = (S, C)$ , $E_{σ}$ returns a QBF whose every model corresponds (in the sense of Definition 3.4) to one of the σ interpretations of D (‘soundness’). In turn, every σ interpretation corresponds to a model of ϕ (‘completeness’). Given a variable set copy $\bar{S}$ of S and depending on whether σ returns two valued or three valued interpretations, $E_{σ}$ returns a QBF with free variables in a set of signed ( ${\bar{S}}_{3}$ ) or unsigned ( $\bar{S}$ ) variables standing for the statements of the ADFs, respectively. We thus write $E_{σ} [(\bar{S}, \bar{C})]$ for the application of the defining encoding function $E_{σ}$ to the ADF $D = (S, C)$ . In addition to soundness and completeness, when σ returns three valued interpretations ( $σ \in {adm, com, prf, grd, \mod, stb}$ ), $E_{σ} [(\bar{S}, \bar{C})]$ must also be a QBF whose models are coherent on ${\bar{S}}_{3}$ in the sense of Definition 3.3.
Definition 3.6.
Let $σ \in {adm, com, prf, grd, \mod, stb}$ . A defining encoding function for σ is a total function $E_{σ}$ from ADFs to QBFs. Given an ADF $D = (S, C)$ and a variable set copy $\bar{S}$ of S it returns a QBF $E_{σ} [(\bar{S}, \bar{C})]$ with free variables in ${\bar{S}}_{3}$ if $σ \in {adm, com, prf, grd}$ and in $\bar{S}$ if $σ \in {\mod, stb}$ . Furthermore,
(Coherence) If $σ \in {adm, com, prf, grd},$ then any two valued interpretation $\hat{v}$ such that $\hat{v} ⊧ E_{σ} [\bar{S}, \bar{C}]$ is coherent on ${\bar{S}}_{3}$ .

(Soundness)
If $σ \in {adm, com, prf, grd}$ and $\hat{v}$ is a two valued interpretation such that $\hat{v} ⊧ E_{σ} [\bar{S}, \bar{C}],$ then the three valued interpretation v on S such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ is a σ interpretation of D.

If $σ \in {\mod, stb}$ and $\hat{v}$ is a two valued interpretation such that $\hat{v} ⊧ E_{σ} [\bar{S}, \bar{C}],$ then the two valued interpretation v on S such that $\hat{v} ≅_{\bar{S}} v$ is a σ interpretation of D.

(Completeness)
If $σ \in {adm, com, prf, grd}$ and v is a three valued σ interpretation of D, then for any two valued interpretation $\hat{v}$ such that $\hat{v} ≅_{{\bar{S}}_{3}} v,$ it holds that $\hat{v} ⊧ E_{σ} [\bar{S}, \bar{C}]$ .

If $σ \in {\mod, stb}$ and v is a two valued σ interpretation of D, then for any two valued interpretation $\hat{v}$ such that $\hat{v} ≅_{\bar{S}} v,$ it holds that $\hat{v} ⊧ E_{σ} [\bar{S}, \bar{C}]$ .

3.1. Basic modules

When encoding the reasoning tasks associated to ADFs as QBFs we make repeated use of some simple modules. In the first place, given a variable set copy $\bar{S}$ of a set of statements S, the following formula ‘filters out’ interpretations which are not coherent on ${\bar{S}}_{3}$ : $coh [\bar{S}] : = \underset{s \in S}{⋀} \neg ({\bar{s}}^{\oplus} \land {\bar{s}}^{⊖}) .$

Lemma 3.7.
Let $\bar{S}$ be a variable set copy of a set of statements S. A two valued interpretation $\hat{v}$ is coherent on ${\bar{S}}_{3}$ if and only if $\hat{v} ⊧ coh [\bar{S}]$ .
Proof.
A two valued valuation $\hat{v}$ is coherent on ${\bar{S}}_{3}$ according to Definition 3.3 if and only if there is no $s \in S$ such that $\hat{v} ({\bar{s}}^{\oplus}) = t$ and $\hat{v} ({\bar{s}}^{⊖}) = t$ . This is the case if and only if for each $s \in S$ , $\hat{v} ⊧ \neg ({\bar{s}}^{\oplus} \land {\bar{s}}^{⊖})$ , that is, $\hat{v} ⊧ ⋀_{s \in S} \neg ({\bar{s}}^{\oplus} \land {\bar{s}}^{⊖}) = coh [\bar{S}]$ .

In order to encode the definitions of ADF semantics as QBFs we often need to express that $v (s) ⩽_{i} v^{'} (s)$ on all $s \in S$ for two interpretations of an ADF $D = (S, C)$ . The formula ${\bar{S}}_{3} ⩽_{i} {\bar{\bar{S}}}_{3} : = \underset{s \in S}{⋀} (({\bar{s}}^{\oplus} \to {\bar{\bar{s}}}^{\oplus}) \land ({\bar{s}}^{⊖} \to {\bar{\bar{s}}}^{⊖}))$ does precisely that assuming both v and $v^{'}$ are three valued and using the variable set copies $\bar{S}$ and $\bar{\bar{S}}$ to implicitly refer to the mappings to truth values of v and $v^{'}$ , respectively.
Lemma 3.8.
Let S be a set of statements, $\bar{S}$ and $\bar{\bar{S}}$ disjoint variable set copies of S.
Let $\hat{v}$ be a two valued interpretation that is coherent on ${\bar{S}}_{3}$ and ${\bar{\bar{S}}}_{3}$ such that $\hat{v} ⊧ {\bar{S}}_{3} ⩽_{i} {\bar{\bar{S}}}_{3}$ . Then for three valued interpretations v, $v^{'}$ on S such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ and $\hat{v} ≅_{{\bar{\bar{S}}}_{3}} v^{'}$ it is the case that $v ⩽_{i} v^{'}$ .

Let v and $v^{'}$ be three valued interpretations on S such that $v ⩽_{i} v^{'}$ . Then for any two valued interpretation $\hat{v}$ such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ and $\hat{v} ≅_{{\bar{\bar{S}}}_{3}} v^{'},$ it is the case that $\hat{v} ⊧ {\bar{S}}_{3} ⩽_{i} {\bar{\bar{S}}}_{3}$ .

Proof.

Let $\hat{v}$ be a two valued interpretation that is coherent on ${\bar{S}}_{3}$ and ${\bar{\bar{S}}}_{3}$ and assume that $\hat{v} ⊧ {\bar{S}}_{3} ⩽_{i} {\bar{\bar{S}}}_{3} = ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{\bar{s}}}^{\oplus}) \land ({\bar{s}}^{⊖} \to {\bar{\bar{s}}}^{⊖}))$ . Let also v, $v^{'}$ be three valued interpretations on S such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ and $\hat{v} ≅_{{\bar{\bar{S}}}_{3}} v^{'}$ . For an arbitrary $s \in S$ , since $\hat{v} ⊧ ({\bar{s}}^{\oplus} \to {\bar{\bar{s}}}^{\oplus}) \land ({\bar{s}}^{⊖} \to {\bar{\bar{s}}}^{⊖})$ and $\hat{v} ≅_{{\bar{S}}_{3}} v$ as well as $\hat{v} ≅_{{\bar{\bar{S}}}_{3}} v^{'}$ if $v (s) = t$ then $\hat{v} ({\bar{s}}^{\oplus}) = t$ , hence $\hat{v} ({\bar{\bar{s}}}^{\oplus}) = t$ and so also $v^{'} (s) = t$ . In the same manner, one can conclude that if $v (s) = f$ then $v^{'} (s) = f$ must be the case. Finally if $v (s) = u$ , then $v (s) ⩽_{i} v^{'} (s)$ whatever the value of $v^{'} (s)$ . In conclusion, $v (s) ⩽_{i} v^{'} (s)$ and since $s \in S$ was arbitrary $v ⩽_{i} v^{'}$ .

Let v and $v^{'}$ be three valued interpretations on S such that $v ⩽_{i} v^{'}$ and $\hat{v}$ a two valued interpretation such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ and $\hat{v} ≅_{{\bar{\bar{S}}}_{3}} v^{'}$ . For an arbitrary $s \in S$ , if $v (s) = x \in {t, f}$ then also $v^{'} (s) = x$ must be the case. Hence, it follows from Definition 3.4 that if $\hat{v} ({\bar{s}}^{\oplus}) = t$ then also $\hat{v} ({\bar{\bar{s}}}^{\oplus}) = t$ and if $\hat{v} ({\bar{s}}^{⊖}) = t$ then $\hat{v} ({\bar{\bar{s}}}^{⊖}) = t$ . Therefore $\hat{v} ⊧ ({\bar{s}}^{\oplus} \to {\bar{\bar{s}}}^{\oplus}) \land ({\bar{s}}^{⊖} \to {\bar{\bar{s}}}^{⊖})$ and since $s \in S$ was arbitrary $\hat{v} ⊧ ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{\bar{s}}}^{\oplus}) \land ({\bar{s}}^{⊖} \to {\bar{\bar{s}}}^{⊖})) = {\bar{S}}_{3} ⩽_{i} {\bar{\bar{S}}}_{3}$ .

Note that the reason Lemma 3.8 is split into two items instead of being written using an ‘if and only if’ is that, given a set S of statements and variable set copies $\bar{S}$ and $\bar{\bar{S}}$ of S, there exist exactly two three valued interpretations v and $v^{'}$ on S that correspond to a coherent two valued interpretation $\hat{v}$ on ${\bar{S}}_{3}$ and ${\bar{\bar{S}}}_{3}$ , respectively, while for three valued interpretations v and $v^{'}$ on S there exist (infinitely) many coherent two valued interpretations on ${\bar{S}}_{3}$ and ${\bar{\bar{S}}}_{3}$ that correspond to v and $v^{'}$ (all variables that are not in ${\bar{S}}_{3}$ and ${\bar{\bar{S}}}_{3}$ can be assigned any truth value).

The formula below ${\bar{S}}_{3} ⩽_{i} \bar{\bar{S}} : = \underset{s \in S}{⋀} (({\bar{s}}^{\oplus} \to \bar{\bar{s}}) \land ({\bar{s}}^{⊖} \to \neg \bar{\bar{s}}))$ encodes that $v ⩽_{i} v^{'}$ in case v is a three valued interpretation on a set of statements S and $v^{'}$ is a two valued interpretation on S.
Lemma 3.9.
Let S be a set of statements, $\bar{S}$ and $\bar{\bar{S}}$ variable set copies of S.
Let $\hat{v}$ be a two valued interpretation that is coherent on the set of signed variables ${\bar{S}}_{3}$ and such that $\hat{v} ⊧ {\bar{S}}_{3} ⩽_{i} \bar{\bar{S}}$ . Then for the three and two valued interpretations v and $v^{'}$ on S such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ and $\hat{v} ≅_{\bar{\bar{S}}} v^{'},$ it is the case that $v ⩽_{i} v^{'}$ .

Let v and $v^{'}$ be three and two valued interpretations on S such that $v ⩽_{i} v^{'}$ . Then for any two valued interpretation $\hat{v}$ such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ and $\hat{v} ≅_{\bar{\bar{S}}} v^{'},$ it is the case that $\hat{v} ⊧ {\bar{S}}_{3} ⩽_{i} \bar{\bar{S}}$ .

Proof.
The proof is similar to that of Lemma 3.8.
3.2. Encodings

Having covered the preliminaries, in this section we set out to provide the encodings of ADF reasoning to QSAT. As already explained, we do so by first giving defining encoding functions for each of the semantics we consider in this work. To give a defining encoding function for admissible semantics of ADFs we slightly reformulate the definition of admissible interpretations.

Proposition 3.10.
Let $D = (S, {φ_{s}}_{s \in S})$ be an ADF and v a three valued interpretation on S. Then $v \in adm (D)$ iff $v (s) ⩽_{i} w (φ_{s})$ for all $s \in S$ and $w \in {[v]}_{2}$ .
Proof.
Let v be a three valued interpretation such that $v \in adm (D)$ . For an arbitrary $s \in S$ , if $v (s) = x$ for $x \in {t, f}$ , one has that $v (s) ⩽_{i} Γ_{D} (v) (s) ⩽_{i} w (φ_{s})$ for all $w \in {[v]}_{2}$ . If $v (s) = u$ then $v (s) ⩽_{i} w (φ_{s})$ whatever the value of $w (φ_{s})$ for all $w \in {[v]}_{2}$ . In conclusion, since $s \in S$ was arbitrary $v (s) ⩽_{i} w (φ_{s})$ for all $s \in S$ and $w \in {[v]}_{2}$ .

Assume now that $v (s) ⩽_{i} w (φ_{s})$ for all $s \in S$ and $w \in {[v]}_{2}$ . For an arbitrary $s \in S$ , assume first that $w (φ_{s}) = t$ for all $w \in {[v]}_{2}$ . In that case $v (s) = t$ or $v (s) = u$ and, hence, $v (s) ⩽_{i} Γ_{D} (v) (s) = t$ . In the same manner if $w (φ_{s}) = f$ for all $w \in {[v]}_{2}$ , then $v (s) = f$ or $v (s) = u$ must be the case and again $v (s) ⩽_{i} Γ_{D} (v) (s) = f$ . Finally, if neither $w (φ_{s}) = t$ nor $w (φ_{s}) = f$ for all $w \in {[v]}_{2}$ , that is, there exist $w, w^{'} \in {[v]}_{2}$ such that $w (s) = t$ and $w^{'} (s) = f$ , then $v (s) = u = Γ_{D} (v) (s)$ . In conclusion, $v (s) ⩽_{i} Γ_{D} (v) (s)$ and since $s \in S$ was arbitrary $v ⩽_{i} Γ_{D} (v)$ .

This leads us to the defining encoding function for admissible semantics of ADFs, which essentially encodes evaluation of ADFs with respect to the admissible semantics by recasting the condition expressed in Proposition 3.10 in the language of QBFs.
Proposition 3.11.
Given an ADF $D = (S, C = {φ_{s}}_{s \in S})$ and a variable set copy $\bar{S}$ of S, let the function $E_{adm}$ return a QBF with free variables in ${\bar{S}}_{3}$ $E_{adm} [\bar{S}, \bar{C}] : = coh [\bar{S}] \land \forall \bar{S} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \to \underset{s \in S}{⋀} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s}))) .$ Then $E_{adm}$ is a defining encoding function for $adm$ .
Proof.
Coherence of $E_{adm}$ follows from the fact that for any two valued interpretation $\hat{v}$ such that $\hat{v} ⊧ E_{adm} [\bar{S}, \bar{C}]$ for an arbitrary ADF $D = (S, C)$ it is also the case that $\hat{v} ⊧ coh [\bar{S}]$ and, hence, according to Lemma 3.7, $\hat{v}$ is coherent on ${\bar{S}}_{3}$ .

In order to prove soundness assume that $\hat{v}$ is a two valued interpretation, $D = (S, C = {φ_{s}}_{s \in S})$ an ADF, and $\hat{v} ⊧ E_{adm} [\bar{S}, \bar{C}]$ . Then, $\hat{v} ⊧ \forall \bar{S} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \to ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s})))$ which, by Lemma 2.1 implies that $\hat{v} [\bar{S} / \bar{w} (\bar{S})] ⊧ ({\bar{S}}_{3} ⩽_{i} \bar{S}) \to ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s}))$ for any two valued interpretation $\bar{w}$ . In particular, $\hat{z} ⊧ ({\bar{S}}_{3} ⩽_{i} \bar{S}) \to ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s}))$ with $\hat{z} : = \hat{v} [\bar{S} / \bar{w} (\bar{S})]$ for any two valued valuation $\hat{w}$ such that $\hat{w} ≅_{\bar{S}} w$ for some $w \in {[v]}_{2}$ . Now, by Lemma 3.5 $\hat{z}$ is coherent on ${\bar{S}}_{3}$ and $\hat{z} ≅_{{\bar{S}}_{3}} v$ as well as $\hat{z} ≅_{\bar{S}} w$ . Since $w \in {[v]}_{2}$ it follows that $v ⩽_{i} w$ and according to Lemma 3.9, $\hat{z} ⊧ {\bar{S}}_{3} ⩽_{i} \bar{S}$ . Hence, also $\hat{z} ⊧ ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s}))$ must be the case. Consider now an arbitrary $s \in S$ and assume that $v (s) = t$ . In that case, since $\hat{z} ≅_{{\bar{S}}_{3}} v$ , by Definition 3.4 $\hat{z} ({\bar{s}}^{\oplus}) = t$ and, hence, since $\hat{z} ⊧ {\bar{s}}^{\oplus} \to \bar{φ_{s}}$ , also $\hat{z} ⊧ \bar{φ_{s}}$ must be the case. Since $\hat{z} ≅_{\bar{S}} w$ , this means that also $w ⊧ φ_{s}$ , that is, $w (φ_{s}) = t$ must be the case. In the same manner, if $v (s) = f$ , since $\hat{z} ⊧ {\bar{s}}^{⊖} \to \neg \bar{φ_{s}}$ , $w (\neg φ_{s}) = t$ holds, that is, $w (φ_{s}) = f$ . Finally, if $v (s) = u$ , then $v (s) ⩽_{i} w (φ_{s})$ whatever the value of $w (φ_{s})$ . In conclusion, $v (s) ⩽_{i} w (φ_{s})$ and, since s and w are arbitrary, moreover $v (s) ⩽_{i} w (φ_{s})$ for every $s \in S$ and $w \in {[v]}_{2}$ . In conclusion, by Proposition 3.10 $v \in adm (D)$ is the case.

To prove completeness, assume $v \in adm (D)$ for an ADF $D = (S, C = {φ_{s}}_{s \in S})$ . Consider a two valued interpretation $\hat{v}$ such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ . By Definition 3.4 and Lemma 3.7 then also $\hat{v} ⊧ coh [\bar{S}]$ . Consider now an arbitrary two valued interpretation $\hat{w}$ and assume that $\hat{z} ⊧ {\bar{S}}_{3} ⩽_{i} \bar{S}$ for $\hat{z} : = \hat{v} [\bar{S} / \bar{w} (\bar{S})]$ . By Lemma 3.5 $\hat{z}$ is also coherent on ${\bar{S}}_{3}$ while $\hat{z} ≅_{{\bar{S}}_{3}} v$ as well as $\hat{z} ≅_{\bar{S}} w$ . Hence, according to Lemma 3.9, $v ⩽_{i} w$ and since w is two valued this means that $w \in {[v]}_{2}$ . Since $v \in adm (D)$ according to Proposition 3.10 this means that $v (s) ⩽_{i} w (φ_{s})$ for all $s \in S$ . Consider an arbitrary $s \in S$ . If $\hat{z} ({\bar{s}}^{\oplus}) = t$ , then since $\hat{z}$ is coherent on ${\bar{S}}_{3}$ and $\hat{z} ≅_{{\bar{S}}_{3}} v$ it must be the case that $v (s) = t$ . Hence, since $v (s) ⩽_{i} w (φ_{s})$ also $w (φ_{s}) = t$ must hold and, therefore, since $\hat{z} ≅_{\bar{S}} w$ also $\hat{z} (\bar{φ_{s}}) = t$ must be the case. Therefore $\hat{z} ⊧ {\bar{s}}^{\oplus} \to \bar{φ_{s}}$ . In the same manner, from the assumption that $\hat{z} ({\bar{s}}^{⊖}) = t$ one arrives at $\hat{z} ⊧ {\bar{s}}^{⊖} \to \neg \bar{φ_{s}}$ . In conclusion, $\hat{z} ⊧ ({\bar{s}}^{\oplus} \to \bar{φ_{s}}) \land ({\bar{s}}^{⊖} \to \neg \bar{φ_{s}})$ and since $s \in S$ was arbitrary in fact $\hat{z} ⊧ ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s}))$ . Hence $\hat{z} ⊧ ({\bar{S}}_{3} ⩽_{i} \bar{S}) \to ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s}))$ and since $\hat{w}$ in $\hat{z} : = \hat{v} [\bar{S} / \hat{w} (\bar{S})]$ was arbitrary according to Lemma 2.1 $\hat{v} ⊧ \forall \bar{S} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \to ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s})))$ . Finally, it follows that $\hat{v} ⊧ coh [\bar{S}] \land \forall \bar{S} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \to ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s}))) = E_{adm} [\bar{S}, \bar{C}]$ .
Example 3.12.
The following is the encoding for the ADF $D = (S, C)$ from Example 2.7 w.r.t. the admissible semantics (using $\bar{S} = S$ as variable set copy). Here we use the abbreviation $S_{3} ⩽_{i} {φ_{s}}_{s \in S} : = ⋀_{s \in S} (({\bar{s}}^{\oplus} \to {\bar{φ}}_{s}) \land ({\bar{s}}^{⊖} \to \neg {\bar{φ}}_{s}))$ to express the conjunct at the end of the encoding presented in Proposition 3.11. $\begin{matrix} E_{adm} [S, C] & = coh [S] \land \forall {a, b, c} ((S_{3} ⩽_{i} S) \to (S_{3} ⩽_{i} {φ_{s}}_{s \in S})) \\ coh [S] & = \neg (a^{\oplus} \land a^{⊖}) \land \neg (b^{\oplus} \land b^{⊖}) \land \neg (c^{\oplus} \land c^{⊖}) \\ S_{3} ⩽_{i} S & = ((a^{\oplus} \to a) \land (a^{⊖} \to \neg a)) \land ((b^{\oplus} \to b) \land (b^{⊖} \to \neg b)) \\ \land ((c^{\oplus} \to c) \land (c^{⊖} \to \neg c)) \\ S_{3} ⩽_{i} {φ_{s}}_{s \in S} & = ((a^{\oplus} \to (b \lor \neg b)) \land (a^{⊖} \to \neg (b \lor \neg b))) \land \\ ((b^{\oplus} \to b) \land (b^{⊖} \to \neg b)) \land ((c^{\oplus} \to (c \to b)) \land (c^{⊖} \to \neg (c \to b))) \end{matrix}$

Any interpretation mapping the free variables $a^{\oplus}$ and $b^{⊖}$ to t and $a^{⊖}$ , $b^{\oplus}$ , $c^{\oplus}$ , $c^{⊖}$ to f satisfies $E_{adm} [S, C]$ and corresponds to the interpretation $v_{7} \in adm (D)$ from Table 1.

The following proposition gives the defining encoding for the complete semantics. The first conjunct of $E_{com} [\bar{S}, \bar{C}]$ for some ADF $D = (S, C = {φ_{s}}_{s \in S})$ and variable set copy $\bar{S}$ ensures that any model of $E_{com} [\bar{S}, \bar{C}]$ corresponds to an admissible interpretation v of D. The conjunct on the right is slightly more involved and expresses that v is also complete if $v (s) = u$ for some $s \in S$ only if there exist $w, w^{'} \in {[v]}_{2}$ such that $w (φ_{s}) = t$ and $w^{'} (φ_{s}) = f$ (see the proof sketch of Proposition 3.13).
Proposition 3.13.
Given an ADF $D = (S, C = {φ_{s}}_{s \in S})$ and a variable set copy $\bar{S}$ of S, let the function $E_{com}$ return a QBF with free variables in ${\bar{S}}_{3}$ $E_{com} [\bar{S}, \bar{C}] : = E_{adm} [\bar{S}, \bar{C}] \land \underset{s \in S}{⋀} ((\neg {\bar{s}}^{\oplus} \land \neg {\bar{s}}^{⊖}) \to \exists {\bar{S}}^{'} \cup {\bar{S}}^{″} (({\bar{S}}_{3} ⩽_{i} {\bar{S}}^{'}) \land ({\bar{S}}_{3} ⩽_{i} {\bar{S}}^{″}) \land {\bar{φ_{s}}}^{'} \land \neg {\bar{φ_{s}}}^{″})) .$ Then $E_{com}$ is a defining encoding function for $com$ .
Proof (sketch)
Note first that for a three valued valuation v and an ADF $D = (S, C = {φ_{s}}_{s \in S})$ , $v \in com (D)$ if and only if (i) $v \in adm (D)$ and (ii) $v (s) = u$ is the case for some $s \in S$ only if there exist $w, w^{'} \in {[v]}_{2}$ such that $w (φ_{s}) = t$ and $w^{'} (φ_{s}) = t$ . That $v \in com (D)$ implies that v satisfies (i) and (ii) is immediate from the definition of complete interpretations. For the converse, (i), that is, $v ⩽_{i} Γ_{D} (v)$ , implies that $v (s) = Γ_{D} (v) (s)$ for $s \in S$ such that $v (s) = t$ and $v (s) = f$ . On the other hand (ii), which spells out the conditions under which $Γ_{D} (v) (s) = u$ for some $s \in S$ , implies that also $v (s) = Γ_{D} (v) (s)$ for $s \in S$ such that $v (s) = u$ .

Coherence follows directly from Proposition 3.11 and the fact that for any two valued interpretation $\hat{v}$ such that $\hat{v} ⊧ E_{com} [\bar{S}, \bar{C}]$ it is also the case that $\hat{v} ⊧ E_{adm} [\bar{S}, \bar{C}]$ for any ADF $D = (S, C)$ . Proof of soundness and completeness involves showing that for a two valued interpretation $\hat{v}$ , $\hat{v} ⊧ E_{com} [\bar{S}, \bar{C}]$ if and only if the three valued interpretation v such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ satisfies (i) as defined above which is encoded via $E_{adm} [\bar{S}, \bar{C}]$ and (ii) which is encoded via $⋀_{s \in S} ((\neg {\bar{s}}^{\oplus} \land \neg {\bar{s}}^{⊖}) \to \exists {\bar{S}}^{'} \cup {\bar{S}}^{″} (({\bar{S}}_{3} ⩽_{i} {\bar{S}}^{'}) \land ({\bar{S}}_{3} ⩽_{i} {\bar{S}}^{″}) \land {\bar{φ}}_{s}^{'} \land \neg {\bar{φ}}_{s}^{″}))$ . This can be shown in a similar fashion to the proof of Proposition 3.14 via Lemmas 2.1, 3.5 and 3.9 as well as Proposition 3.11.

Using again the encoding for admissibility we encode preferred semantics in the next proposition. The defining encoding function returns a QBF that specifies that the result should correspond to an admissible interpretation v and for any admissible interpretation $v^{'}$ with greater or equal information content it must be the case that $v (s) = v^{'} (s)$ for all $s \in S$ , that is, v is an admissible interpretation that is maximally informative with respect to $⩽_{i}$ .
Proposition 3.14.
Given an ADF $D = (S, C)$ and a variable set copy $\bar{S}$ of S, let the function $E_{prf}$ return a QBF with free variables in ${\bar{S}}_{3}$ $E_{prf} [\bar{S}, \bar{C}] : = E_{adm} [\bar{S}, \bar{C}] \land \forall {\bar{S}}_{3}^{'} (E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}] \to (({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}) \to ({\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3}))) .$ Then $E_{prf}$ is a defining encoding function for $prf$ .
Proof.
Coherence of $E_{prf}$ follows from the fact that for any two valued interpretation $\hat{v}$ such that $\hat{v} ⊧ E_{prf} [\bar{S}, C]$ for an arbitrary ADF $D = (S, C)$ it is also the case that $\hat{v} ⊧ E_{adm} [\bar{S}, \bar{C}]$ and, hence, according to Proposition 3.11, $\hat{v}$ is coherent on ${\bar{S}}_{3}$ .

In order to prove soundness assume that $\hat{v}$ is a two valued interpretation, $D = (S, C)$ an ADF, and $\hat{v} ⊧ E_{prf} [\bar{S}, \bar{C}]$ . Then, also $\hat{v} ⊧ E_{adm} [\bar{S}, \bar{C}]$ and, hence, according to Proposition 3.11, any three valued interpretation v such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ is an admissible interpretation of D. Assume that there exists $v^{'} \in adm (D)$ such that $v^{'} >_{i} v$ . Now, since $\hat{v} ⊧ E_{prf} [\bar{S}, \bar{C}]$ it is also the case that $\hat{v} ⊧ \forall {\bar{S}}_{3}^{'} (E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}] \to (({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}) \to ({\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3})))$ and, hence, according to Lemma 2.1 $\hat{v} [{\bar{S}}_{3}^{'} / w ({\bar{S}}_{3}^{'})] ⊧ E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}] \to (({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}) \to ({\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3}))$ for any interpretation $\hat{w}$ . In particular, $\hat{z} ⊧ E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}] \to (({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}) \to ({\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3}))$ with $\hat{z} : = \hat{v} [{\bar{S}}_{3}^{'} / {\hat{v}}^{'} ({\bar{S}}_{3}^{'})]$ for any two valued valuation ${\hat{v}}^{'}$ such that ${\hat{v}}^{'} ≅_{{\bar{S}}_{3}^{'}} v^{'}$ . Now, by Lemma 3.5 $\hat{z} ≅_{{\bar{S}}_{3}} v$ and $\hat{z} ≅_{{\bar{S}}_{3}^{'}} v^{'}$ . Since $\hat{z} ≅_{{\bar{S}}_{3}^{'}} v^{'}$ by Proposition 3.11 $\hat{v} ⊧ E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}]$ . Also, since $v^{'} >_{i} v$ , by Lemma 3.8, $\hat{z} ⊧ {\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}$ and, hence, it must also be the case that $\hat{z} ⊧ {\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3}$ which, according to Lemma 3.8 contradicts the assumption that $v^{'} >_{i} v$ . Hence, there does not exist $v^{'} \in adm (D)$ such that $v^{'} >_{i} v$ and v is therefore a preferred interpretation of D.

To prove completeness, assume $v \in prf (D)$ . Consider a two valued interpretation $\hat{v}$ such that $\hat{v} ≅_{{\bar{S}}_{3}} v$ . Since $v \in adm (D)$ by Proposition 3.11, $\hat{v} ⊧ E_{adm} [\bar{S}, \bar{C}]$ . Consider now an arbitrary two valued interpretation ${\hat{v}}^{'}$ such that $\hat{w} ⊧ E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}]$ for $\hat{w} : = \hat{v} [{\bar{S}}_{3}^{'} / {\hat{v}}^{'} ({\bar{S}}_{3}^{'})]$ , that is, also ${\hat{v}}^{'} ⊧ E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}]$ . By Proposition 3.11 this means that $v^{'} \in adm (D)$ for the three valued interpretation $v^{'}$ such that $\hat{w} ≅_{{\bar{\bar{S}}}_{3}^{'}} v^{'}$ (and ${\hat{v}}^{'} ≅_{{\bar{\bar{S}}}_{3}^{'}} v^{'}$ ). Assume now that also $\hat{w} ⊧ {\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}$ but $\hat{w} ⊭ {\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3}$ . Since by Lemma 3.5 also $\hat{w} ≅_{{\bar{\bar{S}}}_{3}} v$ and hence $\hat{w}$ is coherent on ${\bar{S}}_{3}$ in addition to ${\bar{S}}_{3}^{'}$ , by Lemma 3.8 this implies that $v ⩽_{i} v^{'}$ and $v^{'} ≰_{i} v$ , that is, $v^{'} >_{i} v$ , which is in contradiction with $v \in prf (D)$ . Hence $\hat{w} ⊧ ({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}) \to ({\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3})$ and, therefore, $\hat{w} ⊧ E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}] \to (({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}) \to ({\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3}))$ . Since ${\hat{v}}^{'}$ in $\hat{w} : = \hat{v} [{\bar{S}}_{3}^{'} / {\bar{v}}^{'} ({\bar{S}}_{3}^{'})]$ was arbitrary, by Lemma 2.1 this means that $\hat{v} ⊧ \forall {\bar{S}}_{3}^{'} (E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}] \to (({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}) \to ({\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3})))$ . In conclusion we have $\hat{v} ⊧ E_{adm} [\bar{S}, \bar{C}] \land \forall {\bar{S}}_{3}^{'} (E_{adm} [{\bar{S}}^{'}, {\bar{C}}^{'}] \to (({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}) \to ({\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}_{3}))) = E_{prf} [\bar{S}, \bar{C}]$ .
Example 3.15.
The following is the encoding for the ADF $D = (S, C)$ from Example 2.7 w.r.t. the preferred semantics (using $\bar{S} = S$ as variable set copy). $\begin{matrix} E_{prf} [S, C] & = E_{adm} [S, C] \land \forall {a^{' \oplus}, a^{' ⊖}, b^{' \oplus}, b^{' ⊖}, c^{' \oplus}, c^{' ⊖}} (E_{adm} [S^{'}, C^{'}] \\ \to ((S_{3} ⩽_{i} S_{3}^{'}) \to (S_{3}^{'} ⩽_{i} S_{3}))) \\ E_{adm} [S, C] & = coh [S] \land \forall {a, b, c} ((S_{3} ⩽_{i} S) \to (S_{3} ⩽_{i} {φ_{s}}_{s \in S})) \\ coh [S] & = \neg (a^{\oplus} \land a^{⊖}) \land \neg (b^{\oplus} \land b^{⊖}) \land \neg (c^{\oplus} \land c^{⊖}) \\ S_{3} ⩽_{i} S & = ((a^{\oplus} \to a) \land (a^{⊖} \to \neg a)) \land ((b^{\oplus} \to b) \land (b^{⊖} \to \neg b)) \\ \land ((c^{\oplus} \to c) \land (c^{⊖} \to \neg c)) \\ S_{3} ⩽_{i} {φ_{s}}_{s \in S} & = ((a^{\oplus} \to (b \lor \neg b)) \land (a^{⊖} \to \neg (b \lor \neg b))) \land ((b^{\oplus} \to b) \land (b^{⊖} \to \neg b)) \\ \land ((c^{\oplus} \to (c \to b)) \land (c^{⊖} \to \neg (c \to b))) \\ E_{adm} [S^{'}, C^{'}] & = coh [S^{'}] \land \forall {a^{'}, b^{'}, c^{'}} ((S_{3}^{'} ⩽_{i} S^{'}) \to (S_{3}^{'} ⩽_{i} {φ_{s}^{'}}_{s \in S})) \\ coh [S^{'}] & = \neg (a^{' \oplus} \land a^{' ⊖}) \land \neg (b^{' \oplus} \land b^{' ⊖}) \land \neg (c^{' \oplus} \land c^{' ⊖}) \\ S_{3}^{'} ⩽_{i} S^{'} & = ((a^{' \oplus} \to a^{'}) \land (a^{' ⊖} \to \neg a^{'})) \land ((b^{' \oplus} \to b^{'}) \land (b^{' ⊖} \to \neg b^{'})) \\ \land ((c^{' \oplus} \to c^{'}) \land (c^{' ⊖} \to \neg c^{'})) \\ S_{3}^{'} ⩽_{i} {φ_{s}^{'}}_{s \in S} & = ((a^{' \oplus} \to (b^{'} \lor \neg b^{'})) \land (a^{' ⊖} \to \neg (b^{'} \lor \neg b^{'}))) \land ((b^{' \oplus} \to b^{'}) \land (b^{' ⊖} \to \neg b^{'})) \\ \land ((c^{' \oplus} \to (c^{'} \to b^{'})) \land (c^{' ⊖} \to \neg (c^{'} \to b^{'}))) \\ S_{3} ⩽_{i} S_{3}^{'} & = ((a^{\oplus} \to a^{' \oplus}) \land (a^{⊖} \to a^{' ⊖})) \land ((b^{\oplus} \to b^{' \oplus}) \land (b^{⊖} \to b^{' ⊖})) \\ \land ((c^{\oplus} \to c^{' \oplus}) \land (c^{⊖} \to c^{' ⊖})) \\ S_{3}^{'} ⩽_{i} S_{3} & = ((a^{' \oplus} \to a^{\oplus}) \land (a^{' ⊖} \to a^{⊖})) \land ((b^{' \oplus} \to b^{\oplus}) \land (b^{' ⊖} \to b^{⊖})) \\ \land ((c^{' \oplus} \to c^{\oplus}) \land (c^{' ⊖} \to c^{⊖})) \end{matrix}$

To give the defining encoding function for the grounded semantics we use a similar technique as for the preferred semantic. Instead of the module for admissible interpretations we use complete semantics and require that the result is information minimal. A three valued interpretation v is preferred for an ADF D if for all $v^{'} \in adm (D)$ we have either that v and $v^{'}$ are incomparable w.r.t. $⩽_{i}$ , or that $v^{'} ⩽_{i} v$ . The grounded interpretation is the $⩽_{i}$ -minimal complete interpretation and thus all complete interpretations are comparable to the grounded interpretation. Therefore the encoding for the grounded semantics is slightly simpler than the one for preferred, where the check for comparability has to be included.
Proposition 3.16.
Given an ADF $D = (S, C)$ and a variable set copy $\bar{S}$ of S, let the function $E_{grd}$ return a QBF with free variables in ${\bar{S}}_{3}$ $E_{grd} [\bar{S}, \bar{C}] : = E_{com} [\bar{S}, \bar{C}] \land \forall {\bar{S}}_{3}^{″} (E_{com} [{\bar{S}}^{″}, {\bar{C}}^{″}] \to (({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{″})) .$ Then $E_{grd}$ is a defining encoding function for $grd$ .
Proof (sketch)
$E_{grd} [\bar{S}, \bar{C}]$ encodes the fact that the grounded interpretation of an ADF $D = (S, C)$ is the $⩽_{i}$ minimal complete interpretation of D. $E_{com} [\bar{S}, \bar{C}]$ encodes that the grounded interpretation is complete while $\forall {\bar{S}}_{3}^{″} (E_{com} [{\bar{S}}^{″}, {\bar{C}}^{″}] \to ({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{″}))$ encodes minimality. Coherence follows from Proposition 3.13 while soundness and completeness can be shown in a similar fashion to the proof of Proposition 3.14 also making use of Proposition 3.13, as well as Lemmas 2.1, 3.5 and 3.8.

Having established the encodings for the three valued semantics on ADFs we now proceed to the remaining two valued semantics. We begin with two valued models.
Proposition 3.17.
Given an ADF $D = (S, C = {φ_{s}}_{s \in S})$ and a variable set copy $\bar{S}$ of S, let the function $E_{\mod}$ return a QBF with free variables in $\bar{S}$ $E_{grd} [\bar{S}, \bar{C}] : = \underset{s \in S}{⋀} (\bar{s} \leftrightarrow {\bar{φ}}_{s}) .$ Then $E_{\mod}$ is a defining encoding function for $\mod$ .
Proof.
Let $D = (S, C = {φ_{s}}_{s \in S})$ be an ADF. For a two valued interpretation $\hat{v}$ it is the case that $\hat{v} ⊧ E_{\mod} [\bar{S}, \bar{C}] = ⋀_{s \in S} (\bar{s} \leftrightarrow {\bar{φ}}_{s})$ if and only if $\hat{v} ⊧ \bar{s} \leftrightarrow {\bar{φ}}_{s}$ for every $s \in S$ . This holds if and only if $\hat{v} (\bar{s}) = \hat{v} (\bar{φ_{s}})$ for every $s \in S$ . So given a two valued interpretation $\hat{v}$ such that $\hat{v} ⊧ E_{\mod} [\bar{S}, \bar{C}]$ , since $\hat{v} (\bar{s}) = \hat{v} (\bar{φ_{s}})$ for every $s \in S$ , also $v (s) = v (φ_{s})$ for every $s \in S$ and the interpretation v such that $\hat{v} ≅_{\bar{S}} v$ , that is, $v \in \mod (D)$ . On the other hand given an interpretation $v \in \mod (D)$ , any two valued interpretation $\hat{v}$ such that $\hat{v} ≅_{\bar{S}} v$ will satisfy that $\hat{v} (\bar{s}) = \hat{v} (\bar{φ_{s}})$ for every $s \in S$ and hence $\hat{v} ⊧ E_{\mod} [\bar{S}, \bar{C}]$ .

We provide the defining encoding for the stable semantics in Proposition 3.23. The encoding function maps every ADF $D = (S, C = {φ_{s}}_{s \in S})$ to a QBF consisting of three conjuncts. We first require that any model of the QBF correspond to a two valued model v of D. The second conjunct encodes that the statements mapped to t by v coincide with those mapped to t by the grounded interpretation of the reduct $D^{v}$ as defined in Definition 2.6. The last conjunct applies the defining encoding function of the grounded semantics to a modified version of D via a relatively simple syntactic trick, which essentially boils down to computing the grounded interpretation of the ADF $D_{}^{v} : = (S, C^{} : = {φ_{s}^{}}_{s \in S})$ with $φ_{s}^{} : = φ_{s}$ if $v (s) = t$ and $φ_{s}^{} : = ⊥$ if $v (s) = f$ . We prove in Lemma 3.21 that the grounded interpretation of $D^{v}$ and $D_{}^{v}$ are equal when restricting attention to the assignments to the variables in $E_{v} = {s \in S ∣ v (s) = t}$ . Before this we introduce some auxiliary terminology in Definitions 3.18 to 3.20.
Definition 3.18.
Let S be a set of statements. Then $U^{S}$ is the interpretation on S mapping each $s \in S$ to u .
Definition 3.19.
Let $D = (S, C)$ be an ADF and v be a two or three valued interpretation on S. Then $E_{v}^{D} : = {s ∣ s \in S and v (s) = t}$ .

When it is clear from the context to which ADF D we are referring we will more often than not drop the D from the notation $E_{v}^{D}$ as in the preceding paragraph, that is, write $E_{v}$ instead.
Definition 3.20.
Let v and $v^{'}$ be two or three valued interpretations on $S \cup T_{1}$ and $S \cup T_{2}$ , respectively for some sets S, $T_{1},$ and $T_{2}$ . Then
$v = ⇂_{S} v^{'}$ if $v (s) = v^{'} (s)$ for every $s \in S,$

$v <_{i} ⇂_{S} v^{'}$ if $v (s) <_{i} v^{'} (s)$ for every $s \in S,$ and

$v ⩽_{i} ⇂_{S} v^{'}$ if $v (s) ⩽_{i} v^{'} (s)$ for every $s \in S$ .

Lemma 3.21.
Let $D = (S, C = {φ_{s}}_{s \in S})$ be an ADF and v a three valued interpretation on S. Then, $grd (D_{}^{v}) = ⇂_{E_{v}} grd (D^{v})$ where $D_{}^{v} : = (S, C^{} : = {φ_{s}^{}}_{s \in S})$ with $φ_{s}^{} : = φ_{s}$ if $v (s) = t$ and $φ_{s}^{} : = ⊥$ if $v (s) = f$ .
Proof.
We prove by induction on $n ⩾ 0$ that $Γ_{D_{}^{v}}^{n} ⩽_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n}$ and $Γ_{D_{}^{v}}^{n + 1} ⩾_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n}$ . From this then the lemma follows since consider a $k ⩾ 0$ such that $Γ_{D_{}^{v}}^{k} = l.f.p. (Γ_{D_{}^{v}})$ and $Γ_{D^{v}}^{k} = l.f.p. (Γ_{D^{v}})$ . In that case, one has that $grd (D_{}^{v}) = l.f.p. (Γ_{D_{}^{v}}) = Γ_{D_{}^{v}}^{k} ⩽_{i} ⇂_{E_{v}} Γ_{D^{v}}^{k} = l.f.p. (Γ_{D^{v}}) = grd (D^{v})$ and $grd (D^{v}) = l.f.p. (Γ_{D^{v}}) = Γ_{D^{v}}^{k} ⩽_{i} ⇂_{E_{v}} Γ_{D_{}^{v}}^{k + 1} = Γ_{D_{}^{v}}^{k} = l.f.p. (Γ_{D_{}^{v}}) = grd (D_{}^{v})$ . In other words, $grd (D_{}^{v}) ⩽_{i} ⇂_{E_{v}} grd (D^{v})$ and $grd (D_{}^{v}) ⩾_{i} ⇂_{E_{v}} grd (D^{v})$ , hence $grd (D_{}^{v}) = ⇂_{E_{v}} grd (D^{v})$ .

The base case ( $n = 0$ ) of the inductive proof holds trivially since $Γ_{D_{}^{v}}^{0} = U^{S} = ⇂_{E_{v}} U^{E_{v}} = Γ_{D^{v}}^{0}$ and $Γ_{D_{}^{v}}^{1} ⩾_{i} ⇂_{E_{v}} Γ_{D^{v}}^{0} = U^{E_{v}}$ since $U^{E_{v}}$ is the $⩽_{i}$ least interpretation on $E_{V}$ .

Before proving the inductive step note first that $Γ_{D_{}^{v}}^{1} (s) = f$ for every $s \in S$ such that $v (s) = f$ (since for every $w \in {[U^{S}]}_{2}$ it is the case that $w (φ_{s}^{}) = w (⊥) = f$ ). Hence, since the characteristic operator is monotonic in fact $Γ_{D_{}^{v}}^{n} (s) = f$ and so also $w (s) = f$ for every $w \in {[Γ_{D_{}^{v}}^{n}]}_{2}$ holds for every $s \in S$ such that $v (s) = f$ and each $n > 0$ . A consequence of this is
Observation A: $w (φ_{s}) = w (φ_{s} [b / ⊥ : v (b) = f])$ for every $s \in E_{v}$ , $w \in {[Γ_{D_{}^{v}}^{n}]}_{2}$ and $n > 0$ .

A second fact that will be of use in the proof of the inductive step is
Observation B: if v and $v^{'}$ are two interpretations, $v ⩽_{i} ⇂_{S^{'}} v^{'}$ for some set $S^{'}$ , and ψ is a propositional formula with all variables that occur in ψ being in $S^{'}$ , then if for every $w \in {[v]}_{2}$ it is the case that $w (ψ) = x$ for $x \in {t, f}$ then also for every $w^{'} \in {[v^{'}]}_{2}$ it holds that $w^{'} (ψ) = x$ .

This is because if there exists some $w^{'} \in {[v^{'}]}_{2}$ such that $w^{'} (ψ) \neq x$ ( $x \in {t, f}$ ), then, since $v ⩽_{i} ⇂_{S^{'}} v^{'} ⩽_{i} w^{'}$ there also exists a $w \in {[v]}_{2}$ such that $w = ⇂_{S^{'}} w^{'}$ and therefore $w (ψ) \neq x$ which is a contradiction.

Assume now (induction hypothesis) that $Γ_{D_{}^{v}}^{n} ⩽_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n}$ and $Γ_{D_{}^{v}}^{n + 1} ⩽_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n}$ for $n > 0$ . We first prove that then also $Γ_{D_{}^{v}}^{n + 1} ⩽_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n + 1}$ . For this consider first that for an arbitrary $s \in E_{v}$ it is the case that $Γ_{D_{}^{v}}^{n + 1} (s) = t$ . This means that for every $w \in {[Γ_{D_{}^{v}}^{n}]}_{2}$ it holds that $w (φ_{s}^{}) = w (φ_{s}) = t$ . Because of Observation A this also means that for every $w \in {[Γ_{D_{}^{v}}^{n}]}_{2}$ it holds that $w (φ_{s} [b / ⊥ : v (b) = f]) = t$ . Now, since by induction hypothesis $Γ_{D_{}^{v}}^{n} ⩽_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n}$ , by Observation B this implies that also for every $w^{'} \in {[Γ_{D^{v}}^{n}]}_{2}$ it is the case that $w^{'} (φ_{s} [b / ⊥ : v (b) = f]) = t$ in which case $Γ_{D^{v}}^{n + 1} (s) = t$ . In the same manner one can prove that if $Γ_{D_{}^{v}}^{n + 1} (s) = f$ then also $Γ_{D^{v}}^{n + 1} (s) = f$ must be the case. Finally, if $Γ_{D_{}^{v}}^{n + 1} (s) = u$ then $Γ_{D_{}^{v}}^{n + 1} (s) ⩽_{i} Γ_{D^{v}}^{n + 1} (s)$ whatever the value of $Γ_{D^{v}}^{n + 1} (s)$ . Since $s \in E_{v}$ was arbitrary one can conclude that $Γ_{D_{}^{v}}^{n + 1} ⩽_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n + 1}$ .

To prove that $Γ_{D_{}^{v}}^{n + 2} ⩾_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n + 1}$ from the induction hypothesis assume now that for an arbitrary $s \in E_{v}$ it is the case that $Γ_{D^{v}}^{n + 1} (s) = t$ . This means that for every $w \in {[Γ_{D^{v}}^{n}]}_{2}$ it holds that $w (φ_{s} [b / ⊥ : v (b) = f]) = t$ . By the induction hypothesis $Γ_{D_{}^{v}}^{n + 1} ⩾_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n}$ , hence by Observation B also for every $w^{'} \in {[Γ_{D_{}^{v}}^{n + 1}]}_{2}$ it holds that $w^{'} (φ_{s} [b / ⊥ : v (b) = f]) = t$ . Finally, by Observation A one has that in fact for every $w^{'} \in {[Γ_{D_{}^{v}}^{n + 1}]}_{2}$ it is the case that $w^{'} (φ_{s}) = w^{'} (φ_{s}^{}) = t$ . Hence, $Γ_{D_{}^{v}}^{n + 2} (s) = t$ . In the same manner one can prove that if $Γ_{D^{v}}^{n + 1} (s) = f$ also $Γ_{D_{}^{v}}^{n + 2} (s) = f$ . Finally, if $Γ_{D^{v}}^{n + 1} (s) = u$ then $Γ_{D_{}^{v}}^{n + 2} (s) ⩾_{i} Γ_{D^{v}}^{n + 1} (s)$ whatever the value of $Γ_{D_{}^{v}}^{n + 2} (s)$ . Since $s \in E_{v}$ was arbitrary one can conclude that $Γ_{D_{}^{v}}^{n + 2} ⩾_{i} ⇂_{E_{v}} Γ_{D^{v}}^{n + 1}$ .

Before finally giving the defining encoding for the stable semantics we generalise the notation $φ [T / v (S)]$ for the case that T is a set of signed or unsigned variables representing a set of statements S and v is an interpretation on an ADF $D = (S, C)$ . We use this notation in the proof of Proposition 3.23 as well as when encoding the verification problem for an arbitrary ADF semantic in Proposition 3.25.
Definition 3.22.
Let ϕ be a QBF and $\bar{S}$ a variable set copy of a set of statements S. Then $φ [\bar{S} / v (S)]$ with v a two valued interpretation on S denotes the QBF $φ^{'}$ with $\bar{s}$ replaced for ⊤ in case $v (s) = t$ and $\bar{s}$ replaced for ⊥ in case $v (s) = f$ . $φ [{\bar{S}}_{3} / v (S)]$ with v a three (or two) valued interpretation on S denotes the QBF $φ^{'}$ where
${\bar{s}}^{\oplus}$ is replaced for ⊤ and ${\bar{s}}^{⊖}$ is replaced for ⊥ in case $v (s) = t;$

${\bar{s}}^{\oplus}$ is replaced for ⊥ and ${\bar{s}}^{⊖}$ is replaced for ⊤ in case $v (s) = f;$ and

${\bar{s}}^{\oplus}$ and ${\bar{s}}^{⊖}$ are replaced for ⊥ in case $v (s) = u$ .

In the defining encoding for the stable semantics given in Proposition 3.23, any priming applied to the modified acceptance conditions ${{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}$ (of an ADF $D = (S, {φ_{s}}_{s \in S})$ and w.r.t. a variable set copy $\bar{S}$ ) within the sub-module $E_{grd} [{\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}]$ is applied only to the acceptance condition ${\bar{φ}}_{s}^{'}$ and not to $\bar{s}$ for every $s \in S$ . So, for example, ${{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}^{″} = {{\bar{φ}}_{s}^{‴} \land \bar{s}}_{s \in S}$ . See Example 3.24 for how this works in practice.
Proposition 3.23.
Given an ADF $D = (S, C)$ and a variable set copy $\bar{S}$ of S, let the function $E_{stb}$ return a QBF with free variables in $\bar{S}$ $E_{stb} [\bar{S}, \bar{C}] : = E_{\mod} [\bar{S}, \bar{C}] \land \underset{s \in S}{⋀} (\bar{s} \leftrightarrow {\bar{s}}^{^{'} \oplus}) \land E_{grd} [{\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}] .$ Then $E_{stb}$ is a defining encoding function for $stb$ .
Proof.
Let $D = (S, C)$ be an ADF. In order to prove soundness consider a two valued interpretation $\hat{v}$ such that $\hat{v} ⊧ E_{stb} [\bar{S}, \bar{C}]$ . Then $\hat{v} ⊧ E_{\mod} [\bar{S}, \bar{C}]$ from which it follows via Proposition 3.17 that $v \in \mod (D)$ for the interpretation v such that $\hat{v} ≅_{\bar{S}} v$ . Now, it is also the case that $\hat{v} ⊧ E_{grd} [{\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}]$ and hence by Lemma 2.3 $\hat{v} ⊧ E_{grd} [{\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}] [\bar{S} / \hat{v} (\bar{S})]$ . Since $\hat{v} (\bar{s}) = v (s)$ for all $s \in S$ the latter is equivalent to $\hat{v} ⊧ E_{grd} [{\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}] [\bar{S} / v (S)]$ . From Proposition 3.16 it follows that $v^{'} = grd (D^{#})$ for the interpretation $v^{'}$ such that $\hat{v} ≅_{{\bar{S}}^{'}} v^{'}$ and the ADF $D^{#} = (S, {φ_{s}^{#}}_{s \in S})$ where $φ_{s}^{#} = φ_{s} \land ⊤$ if $v (s) = t$ and $φ_{s}^{#} = φ_{s} \land ⊥$ if $v (s) = f$ . Note that since $φ_{s} \land ⊤ \equiv φ_{s}$ and $φ_{s} \land ⊥ \equiv ⊥$ for any $s \in S$ the ADF $D^{#}$ is equivalent to the ADF $D_{}^{v} : = (S, C^{} = {φ_{s}^{}}_{s \in S})$ defined as in Lemma 3.21. Hence, $v^{'} = grd (D_{}^{v})$ . Finally, consider an arbitrary $s \in S$ such that $v (s) = t$ , that is, $s \in E_{v}$ . Since $\hat{v} ⊧ ⋀_{s \in S} (\bar{s} \leftrightarrow {\bar{s}}^{' \oplus})$ , in particular $\hat{v} ⊧ \bar{s} \leftrightarrow {\bar{s}}^{' \oplus}$ . Hence, given that $\hat{v} ≅_{\bar{S}} v$ and therefore $\hat{v} (\bar{s}) = t$ , it must also be the case that $\hat{v} ({\bar{s}}^{' \oplus}) = t$ . From this it follows that since $\hat{v} ≅_{{\bar{S}}^{'}} v^{'}$ also $v^{'} (s) = t$ and since $s \in E_{v}$ was arbitrary in fact $E_{v} \subseteq E_{v^{'}}$ . In the same manner from the fact that $\hat{v} ⊧ ⋀_{s \in S} (\bar{s} \leftrightarrow {\bar{s}}^{' \oplus})$ one can also conclude that $E_{v^{'}} \subseteq E_{v}$ and, hence, $E_{v} \subseteq E_{v^{'}}$ . Since $v^{'} = grd (D_{}^{v})$ from Lemma 3.21 it follows that $E_{v}^{D} = E_{v^{″}}^{D^{v}}$ where $v^{″} = grd (D^{v})$ .

To prove completeness, let $D = (S, C)$ be an ADF and v a two valued interpretation such that $v \in stb (D)$ . Then $v \in \mod (D)$ and $E_{v}^{D} = E_{v^{″}}^{D^{v}}$ for $v^{″} = grd (D^{v})$ . From Lemma 3.21 it follows that also $E_{v}^{D} = E_{v^{'}}^{D_{}^{v}}$ for $v^{″} = grd (D_{}^{v})$ . As has been argued for in the proof of soundness, the ADF $D_{}^{v}$ is equivalent to the ADF $D^{#}$ defined as above and hence $v^{'} = grd (D^{#})$ . Let $\hat{v}$ be a two valued interpretation such that $\hat{v} ≅_{\bar{S}} v$ and $\hat{v} ≅_{{\bar{S}}^{'}} v^{'}$ . Then since $v \in \mod (D)$ and $\hat{v} ≅_{\bar{S}} v$ it follows from Proposition 3.17 that $\hat{v} ⊧ E_{\mod} [\bar{S}, \bar{C}]$ . Also, since $v^{'} = grd (D^{#})$ , one has that $\hat{v} ⊧ E_{grd} [{\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}] [\bar{S} / v (S)] = E_{grd} [{\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}] [\bar{S} / \hat{v} (\bar{S})]$ . This by Lemma 2.3 is equivalent to $\hat{v} ⊧ E_{grd} [{\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}]$ . Finally, from the fact that $E_{v}^{D} = E_{v^{'}}^{D_{}^{v}}$ , $\hat{v} ≅_{\bar{S}} v$ , and $\hat{v} ≅_{{\bar{S}}^{'}} v^{'}$ it is easy to show that $\hat{v} (\bar{s}) = t$ if and only if $\hat{v} ({\bar{s}}^{' \oplus}) = t$ for each $s \in S$ and hence $\hat{v} ⊧ ⋀_{s \in S} (\bar{s} \leftrightarrow {\bar{s}}^{' \oplus})$ . In conclusion, $\hat{v} ⊧ E_{\mod} [\bar{S}, \bar{C}] \land ⋀_{s \in S} (\bar{s} \leftrightarrow {\bar{s}}^{' \oplus}) \land E_{grd} [{\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}] = E_{stb} [\bar{S}, \bar{C}]$ .
Example 3.24.
The following is a part of the encoding for the ADF $D = (S, C)$ from Example 2.7 w.r.t. the stable semantics (using $\bar{S} = S$ as variable set copy). $\begin{matrix} E_{stb} [\bar{S}, \bar{C}] & = E_{\mod} [S, C] \land E_{grd} [S^{'}, {φ_{s}^{'} \land s}_{s \in S}] \land (a \leftrightarrow a^{' \oplus}) \land (b \leftrightarrow b^{' \oplus}) \land (c \leftrightarrow c^{' \oplus}) \\ E_{\mod} [S, C] & = (a \leftrightarrow (b \lor \neg b)) \land (b \leftrightarrow b) \land (c \leftrightarrow (c \to b)) \\ V_{1} & = {a^{‴ \oplus}, a^{‴ ⊖}, b^{‴ \oplus}, b^{‴ ⊖}, c^{‴ \oplus}, c^{‴ ⊖}} \\ E_{grd} [S^{'}, {φ_{s}^{'} \land s}_{s \in S}] & = E_{com} [S^{'}, {φ_{s}^{'} \land s}_{s \in S}] \land \forall V_{1} (E_{com} [S^{‴}, {φ_{s}^{‴} \land s}_{s \in S}] \to (S_{3}^{'} ⩽_{i} S_{3}^{‴})) \\ V_{2} & = {a^{″}, b^{″}, c^{″}, a^{‴}, b^{‴}, c^{‴}} \\ E_{com} [S^{'}, {φ_{s}^{'} \land s}_{s \in S}] & = E_{adm} [S^{'}, {φ_{s}^{'} \land s}_{s \in S}] \land ((\neg a^{' \oplus} \land \neg a^{' ⊖}) \to \exists V_{2} ((S_{3}^{'} ⩽_{i} S^{″}) \\ \land (S_{3}^{'} ⩽_{i} S^{‴}) \land ((b^{″} \lor \neg b^{″}) \land a) \land \neg ((b^{‴} \lor \neg b^{‴}) \land a))) \land \\ ((\neg b^{' \oplus} \land \neg b^{' ⊖}) \to \exists V_{2} ((S_{3}^{'} ⩽_{i} S^{″}) \land (S_{3}^{'} ⩽_{i} S^{‴}) \land (b^{″} \land b) \\ \land \neg (b^{‴} \land b))) \land ((\neg c^{' \oplus} \land \neg c^{' ⊖}) \to \exists V_{2} ((S_{3}^{'} ⩽_{i} S^{″}) \land (S_{3}^{'} ⩽_{i} S^{‴}) \land \\ ((c^{″} \to b^{″}) \land c) \land \neg ((c^{‴} \to b^{‴}) \land c))) \\ E_{adm} [S^{'}, {φ_{s}^{'} \land s}_{s \in S}] & = coh [S^{'}] \land \forall {a^{'}, b^{'}, c^{'}} ((S_{3}^{'} ⩽_{i} S^{'}) \to (S_{3}^{'} ⩽_{i} {φ_{s}^{'} \land s}_{s \in S})) \\ S_{3}^{'} ⩽_{i} {φ_{s}^{'} \land s}_{s \in S} & = ((a^{' \oplus} \to ((b^{'} \lor \neg b^{'}) \land a)) \land (a^{' ⊖} \to \neg ((b^{'} \lor \neg b^{'}) \land a))) \land \\ ((b^{' \oplus} \to (b^{'} \land b)) \land (b^{' ⊖} \to \neg (b^{'} \land b))) \land \\ ((c^{' \oplus} \to ((c^{'} \to b^{'}) \land c)) \land (c^{' ⊖} \to \neg ((c^{'} \to b^{'}) \land c))) \\ \dots \end{matrix}$ Note in this example how $E_{grd} [S^{'}, {{\bar{φ}}_{s}^{'} \land s}_{s \in S}]$ and $E_{com} [S^{'}, {{\bar{φ}}_{s}^{'} \land s}_{s \in S}]$ are expanded without applying priming to any s within a modified acceptance condition of the form $φ_{s}^{'} \land s$ .

Having the defining encoding function for a semantics σ, encodings for the reasoning tasks we consider with respect to σ can be given in a generic manner as is condensed in Proposition 3.25.
Proposition 3.25.
Let $D = (S, C)$ be an ADF, $s_{} \in S,$ $σ \in {adm, com, prf, grd, \mod, stb},$ and v a three (or two) valued interpretation. If $σ \in {adm, com, prf, grd},$ then let $x \in {s_{}}^{\oplus}$ and $T = S_{3}$ . Otherwise if $σ \in {\mod, stb},$ then let $x = s_{}$ and $T = S$ . It holds that
${Cred}_{σ} (s_{}, D) = yes$ iff $\exists T (E_{σ} [S, C] \land x)$ is satisfiable;

${Skept}_{σ} (s_{}, D) = yes$ iff $\forall T (E_{σ} [S, C] \to x)$ is satisfiable; and

${Ver}_{σ} (v, D) = yes$ iff $E_{σ} [S, C] [T / v (S)]$ is satisfiable.

Proof.

Assume first that ${Cred}_{σ} (s_{}, D) = yes$ . This means that there exists an interpretation $v \in σ (D)$ such that $v (s_{}) = t$ . Let $\hat{v}$ be a two valued interpretation such that $\hat{v} ≅_{T} v$ . Then, since $E_{σ}$ is a defining encoding for σ, $\hat{v} ⊧ E_{σ} [S, C]$ . Also, since $v (s_{}) = t$ and $\hat{v} ≅_{T} v$ , it is the case that $\hat{v} ⊧ x$ . Hence $\hat{v} ⊧ E_{σ} [S, C] \land x$ and by Corollary 2.2 then $\exists T (E_{σ} [S, C] \land x)$ is satisfiable.

Assume now that $\exists T (E_{σ} [S, C] \land x)$ is satisfiable. Then by Corollary 2.2 there exists a two valued interpretation $\hat{v}$ such that $\hat{v} ⊧ E_{σ} [S, C] \land x$ . Let v be the three valued interpretation such that $\hat{v} ≅_{T} v$ . Then since $\hat{v} ⊧ E_{σ} [S, C]$ and $E_{σ}$ is a defining encoding for σ, $v \in σ (D)$ . Also, since $\hat{v} ⊧ x$ one has that $v (s_{}) = t$ . Hence ${Cred}_{σ} (s_{}, D) = yes$ .

Assume first that ${Skept}_{σ} (s_{}, D) = yes$ . This means that for every interpretation $v \in σ (D)$ it is the case that $v (s_{}) = t$ . Let $\hat{v}$ be a two valued interpretation such that $\hat{v} ⊧ E_{σ} [S, C]$ . In that case, since $E_{σ}$ is a defining encoding for σ, if $v^{'}$ is a three valued interpretation such that $\hat{v} ≅_{T} v^{'}$ , it holds that $v^{'} \in σ (D)$ . Hence $v^{'} (s_{}) = t$ and, therefore, $\hat{v} ⊧ x$ . As a consequence $\hat{v} ⊧ E_{σ} [S, C] \to x$ and, since $\hat{v}$ was arbitrary, by Corollary 2.2 $\forall T (E_{σ} [S, C] \to x)$ is satisfiable.

Assume now that $\forall T (E_{σ} [S, C] \to x)$ is satisfiable. Then by Corollary 2.2 for every two valued interpretation $\hat{v}$ it is the case that $\hat{v} ⊧ E_{σ} [S, C] \to x$ . Let v be any three valued interpretation such that $v \in σ (D)$ and ${\hat{v}}^{'}$ a two valued interpretation such that ${\hat{v}}^{'} ≅_{T} v$ . Then ${\hat{v}}^{'} ⊧ E_{σ} [S, C]$ and hence, since ${\hat{v}}^{'} ⊧ E_{σ} [S, C] \to x$ , also ${\hat{v}}^{'} ⊧ x$ . Therefore $v (s_{}) = t$ and, since v was arbitrary, it is the case that $v^{'} (s_{}) = t$ for any $v^{'} \in σ (D)$ , that is, ${Skept}_{σ} (s_{}, D) = yes$ .

Assume first that ${Ver}_{σ} (v, D) = yes$ . This means that $v \in σ (D)$ . Let $\hat{v}$ be a two valued interpretation such that $\hat{v} ≅_{T} v$ . Then, since $E_{σ}$ is a defining encoding for σ, $\hat{v} ⊧ E_{σ} [S, C]$ . By Lemma 2.3 this means that $E_{σ} [S, C] [T / \hat{v} (T)] = E_{σ} [S, C] [T / v (S)]$ is true (satisfiable).

Assume now that $E_{σ} [S, C] [T / v (S)]$ is satisfiable and let $\hat{v}$ be a two valued interpretation such that $\hat{v} ⊧ E_{σ} [S, C] [T / v (S)]$ . Note then that $\hat{v} [T / v (S)] ⊧ E_{σ} [S, C]$ where $\hat{v} [T / v (S)]$ is defined mirroring Definition 3.22. Also if $v^{'}$ is the three valued interpretation such that $\hat{v} [T / v (S)] ≅_{T} v^{'}$ then $v^{'} = v$ and since $E_{σ}$ is the defining encoding function for σ, $v \in σ (D)$ .

Many of the encodings shown above are adequate w.r.t. their complexity (see Table 2 for the complexity of the reasoning tasks)¹
1
We refer to the appendix for rewritings of all encodings (of non-trivial reasoning tasks) in such a manner that their structure reflects the complexity of the associated reasoning problems, that is, the encodings are transformed to PNF or, when they correspond to $D^{P}$ complete problems, are written in such a way that they mirror the structure of the SAT UNSAT problem.

. Since for any ADF $D = (S, C)$ and $s_{} \in S$ we have ${Cred}_{adm} (s_{}, D) = {Cred}_{com} (s_{}, D) = {Cred}_{prf} (s_{}, D)$ we can use the encodings for admissibility in these cases. Transforming $\exists T (E_{adm} [S, C] \land x)$ to PNF results in a formula of prefix type $Σ_{2}$ , that is, a QBF in a class of QBFs for which satisfiability is $Σ_{2}^{P}$ complete ( ${Cred}_{adm}$ is also $Σ_{2}^{P}$ complete). Note that, in fact, although $\exists T (E_{com} [S, C] \land x)$ results in a QBF with more variables per statement than the encoding for credulous reasoning w.r.t. admissible semantics it also respects the complexity of the reasoning task. We similarly arrive at QBFs in PNF which match the corresponding complexity for ${Skept}_{prf}$ , ${Cred}_{\mod}$ and ${Skept}_{\mod}$ . For instance, the QBF $\forall T (E_{prf} [S, C] \to x)$ can be transformed to a PNF with prefix type $Π_{3}$ . Skeptical acceptance w.r.t. admissible semantics is trivial. The encodings of ${Ver}_{adm} (v, D)$ and ${Ver}_{prf} (v, D)$ are also adequate, the first resulting in a formula with prefix type $Π_{1}$ when converted to PNF and the second with type $Π_{2}$ . The encodings for ${Ver}_{com} (v, D)$ and ${Ver}_{grd} (v, D)$ can also be considered ‘adequate’ in the sense that the encodings mirror the structure of the SAT UNSAT problem. Finally, ${Ver}_{\mod} (v, D)$ can be seen as an encoding of the verification problem for propositional logic which is inP.

For the remaining queries our encodings do not result in QBFs with a prefix type matching the complexity of the corresponding decision problem on ADFs. The reason for this is that the encodings for the grounded semantics, if translated to PNF, have a higher prefix type (third level) than the complexity of the corresponding decision problems would suggest. The encodings for the stable semantics in turn depend on the defining encoding function for the grounded semantics and are, hence, not adequate w.r.t. the complexity either. We give complexity sensitive encodings of all the reasoning tasks w.r.t. the grounded and stable semantics in Section 3.3, which requires us to deviate from the methodology we followed in this section. These are also a bit more involved than the more ‘natural’ encodings of these reasoning tasks given in this section, requiring more propositional variables per statement in the ADF. Finally since ${Skept}_{com} (s_{}, D) = {Skept}_{grd} (s_{}, D)$ , also skeptical acceptance w.r.t. complete semantics can be encoded with a lower prefix type than the one which results from using $\forall T (E_{com} [S, C] \to x)$ by using the encoding of ${Skept}_{grd} (s_{*}, D)$ we provide in Section 3.3.
3.3. Complexity sensitive encodings for the grounded and stable semantics

As already indicated, in this section we provide alternatives to those encodings from Section 3.2 which are not in a fragment of QSAT which matches the complexity of the reasoning task.

We consider first credulous and skeptical acceptance of statements with respect to the grounded semantics. One way of arriving at adequate encodings for these decision problems is by making use of a characterisation of grounded interpretations given by Strass Wallner (2014), for the statement of which we make use of the following definition:

Definition 3.10.
Let $D = (S, {φ_{s}}_{s \in S})$ be an ADF and v an interpretation. The following are some properties v can satisfy.
For each $s \in S$ such that $v (s) = t$ there exists an interpretation $w \in {[v]}_{2}$ for which $w (φ_{s}) = t$ .

For each $s \in S$ such that $v (s) = f$ there exists an interpretation $w \in {[v]}_{2}$ for which $w (φ_{s}) = f$ .

For each $s \in S$ such that $v (s) = u$ there exist interpretations $w_{1} \in {[v]}_{2}$ and $w_{2} \in {[v]}_{2}$ such that $w_{1} (φ_{s}) = t$ and $w_{2} (φ_{s}) = f$ .

The above mentioned characterisation of grounded interpretations is expressed in the following proposition by Strass and Wallner (2014):
Proposition 3.27.
Let D be an ADF. Then v is the grounded interpretation of D if and only if v is the $⩽_{i}$ least interpretation satisfying Properties 1–3 in Definition 3.26.

This characterisation leads to an alternative way of defining the encoding function for the grounded semantics as is expressed in the next proposition.
Proposition 3.28.
Given an ADF $D = (S, C = {φ_{s}}_{s \in S})$ and a variable set copy $\bar{S}$ of S, let the function $E_{grd}$ return a QBF with free variables in ${\bar{S}}_{3}$ $\begin{matrix} E_{grd} [\bar{S}, \bar{C}] & : = coh [\bar{S}] \land ψ \land (\forall {\bar{S}}_{3}^{'} ((coh [{\bar{S}}^{'}] \land χ) \to ({\bar{S}}_{3} ⩽_{i} {\bar{S}}_{3}^{'}))) \\ ψ & : = \underset{s \in S}{⋀} (({\bar{s}}^{\oplus} \to \exists \bar{S} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \land {\bar{φ}}_{s})) \land ({\bar{s}}^{⊖} \to \exists \bar{S} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \land \neg {\bar{φ}}_{s})) \land \\ ((\neg {\bar{s}}^{\oplus} \land \neg {\bar{s}}^{⊖}) \to \exists \bar{S} \cup {\bar{S}}^{'} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \land ({\bar{S}}_{3} ⩽_{i} {\bar{S}}^{'}) \land {\bar{φ}}_{s} \land \neg {\bar{φ}}_{s}^{'}))) \\ χ & : = (\underset{s \in S}{⋀} (({\bar{s}}^{' \oplus} \to \exists \bar{S} (({\bar{S}}_{3}^{'} ⩽_{i} \bar{S}) \land {\bar{φ}}_{s})) \land ({\bar{s}}^{' ⊖} \to \exists \bar{S} (({\bar{S}}_{3}^{'} ⩽_{i} \bar{S}) \land \neg {\bar{φ}}_{s})) \land \\ ((\neg {\bar{s}}^{' \oplus} \land \neg {\bar{s}}^{' ⊖}) \to \exists \bar{S} \cup {\bar{S}}^{'} (({\bar{S}}_{3}^{'} ⩽_{i} \bar{S}) \land ({\bar{S}}_{3}^{'} ⩽_{i} {\bar{S}}^{'}) \land {\bar{φ}}_{s} \land \neg {\bar{φ}}_{s}^{'})))) . \end{matrix}$

Then $E_{grd}$ is a defining encoding function for $grd$ .
Proof (sketch)
Given an ADF $D = (S, C = {φ_{s}}_{s \in S})$ , the proof involves showing that for any two valued interpretation $\hat{v}$ , $\hat{v} ⊧ E_{grd} [\bar{S}, \bar{C}]$ if and only if the interpretation v such that $\hat{v} ≅_{\bar{S}} v$ is the $⩽_{i}$ least interpretation satisfying Properties 1–3 in Definition 3.26. That $v \in grd (D)$ then follows from Proposition 3.27.

The proof can be fashioned after the proofs regarding defining encoding functions in Section 3.2 by using Lemmas 2.1, 3.5, 3.7, 3.8 and 3.9 in addition to Proposition 3.27.

For and ADF $D = (S, C)$ , $E_{grd} [S, C] [S_{3} / S]$ can be rewritten mirroring the structure of the SAT UNSAT problem as is shown in the appendix, thus reflecting the complexity of ${Ver}_{grd}$ which is $D^{P}$ complete. Giving complexity sensitive encodings for credulous and skeptical acceptance on the other hand requires to deviate from the template of Proposition 3.25 and rather make use of the characterisation of acceptance of statements with respect to the grounded semantics as expressed in the following immediate corollary of Proposition 3.27.
Corollary 3.29.
Let $D = (S, C)$ be an ADF, $s_{} \in S,$ and v the grounded interpretation of D. Then $v (s_{}) = x$ for $x \in {t, f}$ if and only if $w (s_{}) = x$ for every interpretation w that satisfies Properties 1–3 in Definition 3.26 w.r.t. D.
Proof.
Assume first that v is the grounded interpretation of D, $v (s_{}) = x$ for $x \in {t, f}$ and let w be an interpretation that satisfies Properties 1-3 in Definition 3.26. Then from Proposition 3.27 it follows that $v ⩽_{i} w$ and, hence also $v (s_{}) = x$ since t and f are the maximal elements of ${t, f, u}$ with respect to $⩽_{i}$ . The converse follows because v also satisfies Properties 1–3.

That $w (s_{}) = x$ for $x \in {t, f}$ and every w satisfying Properties 1–3 of Definition 3.26 for an ADF $D = (S, C = {φ_{s}}_{s \in S})$ can be encoded as in the next proposition.
Proposition 3.30.
Given an ADF $D = (S, C = {φ_{s}}_{s \in S})$ and a variable set copy $\bar{S}$ of S, let the function $A_{grd}$ return a closed QBF $\begin{matrix} A_{grd} (s_{}, \bar{S}, \bar{C}, x) & : = \forall {\bar{S}}_{3} ((coh [\bar{S}] \land ψ) \to t) \\ ψ & : = \underset{s \in S}{⋀} (({\bar{s}}^{\oplus} \to \exists \bar{S} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \land {\bar{φ}}_{s})) \land ({\bar{s}}^{⊖} \to \exists \bar{S} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \land \neg {\bar{φ}}_{s})) \land \\ ((\neg {\bar{s}}^{\oplus} \land \neg {\bar{s}}^{⊖}) \to \exists \bar{S} \cup {\bar{S}}^{'} (({\bar{S}}_{3} ⩽_{i} \bar{S}) \land ({\bar{S}}_{3} ⩽_{i} {\bar{S}}^{'}) \land {\bar{φ}}_{s} \land \neg {\bar{φ}}_{s}^{'}))), \end{matrix}$ where $t = {\bar{s_{}}}^{\oplus}$ if $x = t$ and $t = {\bar{s_{}}}^{⊖}$ if $x = f$ . Then, $A_{grd} (s_{}, \bar{S}, \bar{C}, x)$ with $x \in {t, f}$ is satisfiable if and only if $w (s_{}) = x$ for every interpretation w satisfying Properties 1–3 of Definition 3.26.
Proof (sketch)
The proof can be fashioned after the proofs regarding defining encoding functions in Section 3.2 by using Lemmas 2.1, 3.5, 3.7 and 3.9 as well as Corollary 2.2.

Then the following proposition gives adequate encodings w.r.t. their complexity for ${Skept}_{grd}$ and ${Ver}_{grd}$ (we remind the reader that ${Skept}_{grd}$ and ${Cred}_{grd}$ are equivalent since there exists only one grounded interpretation for any ADF).
Proposition 3.31.
Given an ADF $D = (S, C)$ and an $s_{} \in S$ let the function $S_{grd}$ return a closed QBF $S_{grd} (s_{}, S, C) : = A_{grd} (s_{}, S, C, t) .$ Then ${Skept}_{grd} (s_{}, D) = {Cred}_{grd} (s_{}, D) = yes$ if and only if $S_{grd} (s_{}, S, C)$ is satisfiable.
Proof.
This proposition follows directly from Proposition 3.30 and Corollary 3.29.

When converted to PNF the encodings which are returned by the function $S_{grd}$ are QBFs with prefix type $Π_{1}$ as is shown in the appendix, hence reflecting the complexity of ${Skept}_{grd} = {Cred}_{grd}$ ( $= {Skept}_{com}$ ) which is $coNP$ complete.

Corollary 3.29 can also be used to provide an alternative defining encoding function for the stable semantics as is expressed in Proposition 3.32. Given an ADF D, the encodings returned by this defining encoding function are based on the fact that verifying whether a two* valued interpretation v is equal to the grounded interpretation $v^{'}$ of the reduct $D^{v}$ is equivalent to checking whether each statement mapped to $x \in {t, f}$ is mapped to the same truth value x by all interpretations w satisfying Properties 1–3 of Definition 3.26 w.r.t. $D^{v}$ .
Proposition 3.32.
Given an ADF $D = (S, C = {φ_{s}}_{s \in S})$ and a variable set copy $\bar{S}$ of S, let the function $E_{stb}$ return a QBF with free variables in $\bar{S}$ $\begin{matrix} E_{stb} [\bar{S}, \bar{C}] : = \mod [\bar{S}, \bar{C}] \land & \underset{s \in S}{⋀} (\bar{s} \to A_{grd} (s, {\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}, t)) \land \\ \underset{s \in S}{⋀} (\neg \bar{s} \to A_{grd} (s, {\bar{S}}^{'}, {{\bar{φ}}_{s}^{'} \land \bar{s}}_{s \in S}, f)) . \end{matrix}$ Then $E_{stb}$ is a defining encoding function for $stb$ .
Proof (sketch)
The proof is similar to that of Proposition 3.23, using Propositions 3.17 and 3.30, Corollary 3.29 as well as Lemmas 2.3, 3.5 and 3.21.

Applying Proposition 3.25 using this alternative characterisation of the defining encoding function for the stable semantics gives complexity adequate encodings for verification (encodings of prefix type $Π_{1}$ ) and acceptance of statements (encodings of prefix type $Σ_{2}$ and $Π_{2}$ for credulous and skeptical acceptance, respectively). In conclusion, we have now provided complexity sensitive reductions to QSAT of all the reasoning tasks we set out to tackle in this work. We refer to the appendix for a summary of all the encodings written in such a manner that they reflect the complexity of the reasoning tasks.
4. Conclusion

We have presented encodings of several reasoning tasks defined on ADFs into the language of QBFs in a manner that is ‘adequate’ with respect to the complexity of the reasoning tasks. This allows for taking advantage of recent developments for QBF solvers and thereby tackling the high complexity of reasoning problems for ADFs.

An initial feasibility study of our encodings was conducted in Diller et al. (2014), comparing a prototype system QADF²

http://www.dbai.tuwien.ac.at/proj/adf/qadf/ http://www.dbai.tuwien.ac.at/proj/adf/qadf/

to the system DIAMOND by Ellmauthaler and Strass (2013, 2014). DIAMOND is the only other comparable ADF system known to us and is based on reductions to the language of Answer-Set Programming (ASP). The performance analysis reported on by Diller et al. (2014) suggests that our system is at the very least competitive with respect to DIAMOND (version 0.9 adapted by us to support reasoning about acceptance of statements) for the reasoning tasks we studied (credulous and skeptical acceptance with respect to the admissible and preferred semantics, respectively). Nonetheless, compared to the success of QBF solvers in other domains, the results indicate that there is room for improvement.

Thus, future work will focus mainly on tuning of the encodings and implementation to improve performance. In particular, it may be that QBF solvers are struggling to efficiently deal with the signed variables in our encodings, a concept we have borrowed from Arieli and Caminada (2013); this issue needs further investigation. Another point on our agenda is to specialise our encodings for ‘less complex’ ADFs (e.g. bipolar ADFs). Also, additional complexity in the structure of the encodings due to the Tseitin transformation that is required to transform the encodings to the prenex conjunctive normal form (PCNF) required by most QSAT solvers may be avoided by using a QSAT solver that does not require the input to be in PCNF. Finally we plan to investigate algorithms using recent advances in incremental QBF solving (Lonsing & Egly, 2014). Incremental algorithms can, for example, compute a preferred interpretation by incrementally computing admissible interpretations with increasing information until an information maximal interpretation is found. For AFs such an incremental approach has already been carried out and implementations based on incremental SAT showed a good performance (Cerutti, Dunne, Giacomin, & Vallati, 2013; Cerutti, Giacomin, Vallati, & Zanella, 2014; Dvořák, Järvisalo, Wallner, & Woltran, 2014). By utilising incremental QBF solving one can generalise the algorithms developed for AFs to ADFs and potentially inherit the good performance of this approach.

Footnotes

Disclosure statement

No potential conflict of interest was reported by the authors.

Funding

This research has been supported by the Austrian Science Fund (FWF) through projects I1102, W1255-N23 and S11403-N23.

Appendix. Summary of encodings

In this section we list those encodings we have provided in our work that are adequate with respect to the complexity of the reasoning tasks. We present them in such a manner that they reflect the complexity of the reasoning tasks, that is, they are either in PNF or mirror the structure of the SAT UNSAT problem which is prototypical for the complexity class $D^{P}$ . For this we transform the encodings given in Section 3 using renaming of variables and the following equivalences (denoted by ≡) for arbitrary QBFs ϕ, ψ and $p \in P$ not occurring free in ψ.

$\neg \exists p φ \equiv \forall p \neg φ,$

$\neg \forall p φ \equiv \exists p \neg φ,$

$(Q p φ) \land ψ \equiv Q p (φ \land ψ)$ for any $Q \in {\exists, \forall},$

$φ \land (Q p φ) \equiv Q p (φ \land ψ)$ for any $Q \in {\exists, \forall},$

$(\exists p φ) \to ψ \equiv \forall p (φ \to ψ),$

$(\forall p φ) \to ψ \equiv \exists p (φ \to ψ),$

$φ \to (Q p φ) \equiv Q p (φ \to ψ)$ for any $Q \in {\exists, \forall},$

In order to avoid excessive priming in the presentation of the encodings below we will often use alternative ‘base sets’ to the one given in Definition 3.1 (namely S) to generate the variable set copies of a set of statements S. Specifically, we will also consider sets $S^{j} : = {s^{j} ∣ s \in S}$ , $S^{j, k} : = {s^{j, k} ∣ s \in S}$ , $S^{j \nabla} : = {s^{j \nabla} ∣ s \in S}$ , $S^{j, k \nabla} : = {s^{j, k \nabla} ∣ s \in S}$ for any $j, k ⩾ 1$ and $\nabla \in {+, -}$ as base sets. $S^{1^{'}}$ , $S^{3 +^{″}}$ , $S^{2 -^{'}}$ and $S^{3, 2 -^{‴}}$ are then all examples of variable set copies that can be generated as in Definition 3.1. In the list of encodings below $D = (S = {s_{1}, \dots, s_{n}}, C = {φ_{s}}_{s \in S})$ is an ADF, v an interpretation on S and $s_{*} \in S$ . We also remind the reader that the notation $φ [S / v (S)]$ and $ψ [S_{3} / v (S)]$ we use in the encodings of the verification tasks has been introduced in Definition 3.22.

References

Arieli

, & Caminada

M.W.A.

(2013). A QBF-based formalization of abstract argumentation semantics. Journal of Applied Logic , 11, 229–252. doi: 10.1016/j.jal.2013.03.009

Baroni

, Cerutti

, Giacomin

, & Guida

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

Bench-Capon

T.J.M.

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

Benedetti

, & Mangassarian

(2008). QBF-based formal verification: Experience and perspectives. Journal on Satisfiability, Boolean Modeling and Computation , 5, 133–191.

Brewka

, Ellmauthaler

, Strass

, Wallner

J.P.

, & Woltran

(2013). Abstract dialectical frameworks revisited. In F. Rossi (Ed.), Proceedings of the 23rd international joint conference on artificial intelligence, IJCAI 2013 (pp. 803–809). Palo Alto, CA: AAAI Press / IJCAI.

Brewka

, Polberg

, & Woltran

(2014). Generalizations of dung frameworks and their role in formal argumentation. IEEE Intelligent Systems , 29, 30–38.

Brewka

, & Woltran

(2010). Abstract dialectical frameworks. In F. Lin, U. Sattler, & M. Truszczyński (Eds.), Proceedings of the twelfth international conference on principles of knowledge representation and reasoning, KR 2010 (pp. 102–111). Palo Alto, CA: AAAI Press.

Bryant

R.E.

, Lahiri

S.K.

, & Seshia

S.A.

(2003). Convergence testing in term-level bounded model checking. In D. Geist & E. Tronci (Eds.), Proceedings of the twelfth advanced research working conference on correct hardware design and verification methods, CHARME-2003, Vol. 2860 of Lecture notes in computer science (pp. 348–362). Berlin: Springer.

Büning

H.K.

, & Bubeck

(2009). Theory of quantified Boolean formulas. In A. Biere, M. Heule, H. van Maaren, & T. Walsh (Eds.), Handbook of satisfiability, Vol. 185 of Frontiers in artificial intelligence and applications (pp. 735–760). Amsterdam: IOS Press.

10.

Caminada

M.W.A.

, & Gabbay

D.M.

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

11.

Cayrol

, & Lagasquie-Schiex

(2005). On the acceptability of arguments in bipolar argumentation frameworks. In L. Godo (Ed.), Proceedings of the Eighth European conference on symbolic and quantitative approaches to reasoning with uncertainty, ECSQARU 2005, Vol. 3571 of Lecture notes in computer science (pp. 378–389). Berlin: Springer.

12.

Cerutti

, Dunne

P.E.

, Giacomin

, & Vallati

(2013). Computing preferred extensions in abstract argumentation: A SAT-based approach. In E. Black, S. Modgil, & N. Oren (Eds.), Proceedings of the second international workshop of theory and applications of formal argumentation, TAFA-2013, Vol. 8306 of Lecture notes in computer science (pp. 176–193). Berlin: Springer.

13.

Cerutti

, Giacomin

, Vallati

, & Zanella

(2014). An SCC recursive meta-algorithm for computing preferred labellings in abstract argumentation. In C. Baral, G.D. Giacomo, & T. Eiter (Eds.), Proceedings of the fourteenth international conference on principles of knowledge representation and reasoning, KR 2014. Palo Alto, CA: AAAI Press.

14.

Charwat

, Dvořák

, Gaggl

S.A.

, Wallner

J.P.

, & Woltran

(2015). Methods for solving reasoning problems in abstract argumentation – a survey. Artificial Intelligence , 220, 28–63. doi: 10.1016/j.artint.2014.11.008

15.

Diller

(2014). Solving reasoning problems on abstract dialectical frameworks via quantified Boolean formulas (Master's thesis, Vienna University of Technology, Institute of Information Systems).

16.

Diller

, Wallner

J.P.

, & Woltran

(2014). Reasoning in abstract dialectical frameworks using quantified Boolean formulas. In S. Parsons, N. Oren, C. Reed, & F. Cerutti (Eds.), Proceedings of the fifth international conference on computational models of argument, COMMA-2014, Vol. 266 of Frontiers in artificial intelligence and applications (pp. 241–252). Amsterdam: IOS Press.

17.

Dung

P.M.

(1995). On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and N-person games. Artificial Intelligence , 77, 321–357. doi: 10.1016/0004-3702(94)00041-X

18.

Dunne

P.E.

, & Bench-Capon

T.J.M.

(2002). Coherence in finite argument systems. Artificial Intelligence , 141, 187–203. doi: 10.1016/S0004-3702(02)00261-8

19.

Dvořák

, Järvisalo

, Wallner

J.P.

, & Woltran

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

20.

Egly

, Eiter

, Tompits

, & Woltran

(2000). Solving advanced reasoning tasks using quantified Boolean formulas. In H.A. Kautz & B.W. Porter (Eds.), Proceedings of the seventeenth national conference on artificial intelligence and twelfth conference on on innovative applications of artificial intelligence (AAAI/IAAI-2000) (pp. 417–422). Palo Alto, CA: AAAI Press / The MIT Press.

21.

Egly

, & Woltran

(2006). Reasoning in argumentation frameworks using quantified boolean formulas. In P.E. Dunne & T.J.M. Bench-Capon (Eds.), Proceedings of the first conference on computational models of argument, COMMA 2006, Vol. 144 of Frontiers in artificial intelligence and applications, Liverpool, (pp. 133–144).

22.

Ellmauthaler

, & Strass

(2013). The DIAMOND system for argumentation: Preliminary report. In M. Fink & Y. Lierler (Eds.), Proceedings of the sixth international workshop on answer set programming and other computing paradigms, ASPOCP 2013, Istanbul (pp. 97–108).

23.

Ellmauthaler

, & Strass

(2014). The DIAMOND system for computing with abstract dialectical frameworks. In S. Parsons, N. Oren, C. Reed, & F. Cerutti (Eds.), Proceedings of the fifth international conference on computational models of argument, COMMA-2014, Vol. 266 of Frontiers in artificial intelligence and applications (pp. 233–240). Amsterdam: IOS Press.

24.

Ferraris

, & Giunchiglia

(2000). Planning as satisfiability in nondeterministic domains. In H.A. Kautz & B.W. Porter (Eds.), Proceedings of the seventeenth national conference on artificial intelligence and twelfth conference on innovative applications of artificial intelligence, AAAI/IAAI-2000 (pp. 748–753). Palo Alto, CA: AAAI Press / The MIT Press.

25.

Franco

, & Martin

(2009). A history of satisfiability. In A. Biere, M. Heule, H. van Maaren, & T. Walsh (Eds.), Handbook of satisfiability, Vol. 185 of Frontiers in artificial intelligence and applications (pp. 3–74). Amsterdam: IOS Press.

26.

Giunchiglia

, Marin

, & Narizzano

(2009). Reasoning with quantified Boolean formulas. In A. Biere, M. Heule, H. van Maaren, & T. Walsh (Eds.), Handbook of satisfiability, Vol. 185 of Frontiers in artificial intelligence and applications (pp. 761–780). Amsterdam: IOS Press.

27.

Giunchiglia

, Narizzano

, & Tacchella

(2007). Quantifier structure in search-based procedures for QBFs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , 26, 497–507. doi: 10.1109/TCAD.2006.888264

28.

Ling

A.C.

, Singh

D.P.

, & Brown

S.D.

(2005). FPGA logic synthesis using quantified boolean satisfiability. In F. Bacchus & T. Walsh (Eds.), Proceedings of the eighth international conference on theory and applications of satisfiability testing, SAT 2005, Vol. 3569 of Lecture notes in computer science (pp. 444–450). Berlin: Springer.

29.

Lonsing

, & Egly

(2014). Incremental QBF solving. In B. O'Sullivan (Ed.), Principles and practice of constraint programming – Proceedings of the 20th international conference, CP 2014, Vol. 8656 of Lecture notes in computer science (pp. 514–530). Berlin: Springer.

30.

Lonsing

, & Seidl

(Eds.) (2013). Informal workshop report on the international workshop on quantified Boolean formulas 2013 .

31.

Mneimneh

M.N.

, & Sakallah

K.A.

(2003). Computing vertex eccentricity in exponentially large graphs: QBF formulation and solution. In E. Giunchiglia & A. Tacchella (Eds.), Proceedings of the sixth international conference on theory and applications of satisfiability testing (SAT-2003), Vol. 2919 of Lecture notes in computer science (pp. 411–425). Berlin: Springer.

32.

Rintanen

(1999). Constructing conditional plans by a theorem-prover. Journal of Artificial Intelligence Research , 10, 323–352.

33.

Strass

(2013). Approximating operators and semantics for abstract dialectical frameworks. Artificial Intelligence , 205, 39–70. doi: 10.1016/j.artint.2013.09.004

34.

Strass

, & Wallner

J.P.

(2014). Analyzing the computational complexity of abstract dialectical frameworks via approximation fixpoint theory. In C. Baral, G.D. Giacomo, & T. Eiter (Eds.), Proceedings of the 14th international conference on principles of knowledge representation and reasoning, KR 2014 (pp. 101–110). Palo Alto, CA: AAAI Press.

35.

Wallner

J. P.

(2014). Complexity results and algorithms for argumentation – Dung's frameworks and beyond (PhD thesis, Vienna University of Technology, Institute of Information Systems).