You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Reasoning in abstract dialectical frameworks using quantified Boolean formulas

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.

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 ,, and ¬, denoting the logical conjunction, disjunction and negation, respectively. As for truth constants, we use ⊤ for the value true and :=¬ for false. QBFs additionally use the universal quantifier ∀ and the existential quantifier ∃. If ϕ is a (quantified) Boolean formula, then Qpφ is a QBF with Q{,} and pP. QBFs may be nested using the logical connectives. Further Qp1,p2,,pnφ or also QPφ with P={p1,p2,,pn} is a shorthand for Qp1Qp2,,Qpnφ . The order of variables in consecutive quantifiers of the same type does not matter. We define shorthands for (material) implication and equivalence: φφ:=¬φφ andφφ:=(φφ)(φφ).

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 vˆ:P{t,f} defines for each propositional variable a truth assignment. We sometimes explicitly highlight that a vˆ is defined on a set PP. The evaluation on atoms generalises as usual to arbitrary formulas: given a formula ϕ and an interpretation vˆ, then ϕ evaluates to true under vˆ (vˆ satisfies ϕ or vˆ is a model of ϕ, denoted by vˆφ) if one of the following holds, with pP and QBFs ψ, ψ1 andψ2.

  • φ=p and vˆ(p)=t;

  • φ=;

  • φ=¬ψ and ψ does not evaluate to true under vˆ;

  • φ=ψ1ψ2 and both ψ1 and ψ2 evaluate to true under vˆ;

  • φ=ψ1ψ2 and one of ψ1 and ψ2 evaluates to true under vˆ;

  • φ=pψ and one of ψ[p/] and ψ[p/] evaluates to true under vˆ;

  • φ=pψ and both ψ[p/] and ψ[p/] evaluate to true under vˆ.

We extend the evaluation function vˆ to formulas, that is, vˆ(φ) is the evaluation of ϕ under 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 vˆ and wˆ as well as a set of propositional variables P, vˆ[P/wˆ(P)] denotes the interpretation vˆ defined as:

  • vˆ(p):=wˆ(p) for pP.

  • vˆ(q):=wˆ(q) if qP and qP.

We will often use the simplified notation vˆ[p/x] with x{t,f} in the case that P={p} and 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 φ=Pψ (φ=Pψ), then vˆφ if and only if vˆ[P/wˆ(P)]ψ for some (all) interpretation(s) wˆ.

Corollary 2.2.

Let ψ be a closed QBF, and P a set of propositional variables. If φ=Pψ (φ=Pψ), then ϕ is true if and only if for some (all) interpretation(s) vˆ, vˆψ.

One final use of brackets as notational device we introduce for QBFs is φ[P/vˆ(P)] to denote the formula ϕ where every occurrence of any variable pP is replaced for ⊤ in case that vˆ(p)=t and replaced for ⊥ in the case that vˆ(p)=f. For φ[{p}/vˆ({p})] we use the simplified notation φ[p/vˆ(p)]. Another immediate result we make use of in this work is the following.

Lemma 2.3.

Let vˆ be an interpretation, ϕ a QBF, and pP. Then vˆφ if and only if vˆφ[p/vˆ(p)]. Also, if P are all the free variables of ϕ, then vˆφ if and only if for all interpretations wˆ it is the case thatwˆφ[P/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 Q1p1Q2p2,,Qnpnψ with piP and Qi{,} for 1in 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 Pφ (respectively, Pφ) is of type Πi+1 (respectively, Σi+1) fori0.

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: Σ0P=Π0P=P, Σi+1P=NPΣiP, Πi+1P=coNPΣiP for i0. In general, deciding whether a QBF ϕ is satisfiable is ΣkP complete if ϕ has prefix type Σk and otherwise if ϕ has prefix type Πk, then the problem is ΠkP complete (k1).

A language is in the complexity class DP if it is the intersection of a language in NP and a language in coNP. The canonical problem of DP 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 Cs specifying the conditions under which s can be accepted. Cs 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),

  • LS×S is a set of links,

  • C={Cs}sS is a set of total functions Cs:2parents(s){t,f}, one for each statement s. Cs is called acceptance condition of s.

We represent the acceptance conditions C as a collection {φs}sS 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)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 vˆ,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<it and u<if and no other pair in <i. The information ordering i extends in a straightforward way to interpretations v1,v2 over S in thatv1iv2 iff v1(s)iv2(s) for all sS.

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 viw. This means that all statements mapped to u by v are mapped to t orf by w. We denote by [v]2 the set of all two valued interpretations that extend v.

For an ADF D=(S,C), sS and a three valued interpretation v, the characteristic function ΓD(v)=v is given by

v(s)=t if w(φs)=t for all w[v]2,f if w(φs)=f for all w[v]2,u otherwise.
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 w1,w2[v]2, s.t. w1(φs)=t and w2(φ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 viΓD(v);

  • in com(D) if v=ΓD(v);

  • in grd(D) if vcom(D) and there is no wcom(D) with w<iv;

  • in prf(D) if vadm(D) and there is no wadm(D) with v<iw.

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 US mapping all statements sS of D to u. Then ΓD0:=US and ΓDi+1:=ΓD(ΓDi) fori0.

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}sS) if v(s)=v(φs) for all sS. Stable models are defined via a reduct.

Definition 2.6.

Let D=(S,L,C) be an ADF with C={φs}sS. A two-valued model v of D is a stable model of D iff Ev={sSv(s)=t} equals the statements set to true in the grounded interpretation of the reduced ADF Dv=(Ev,Lv,Cv), whereLv=L(Ev×Ev) and for sEv we set φsv=φs[b/:v(b)=f].

Example 2.7.

In Figure 1 we see an example ADF D=({a,b,c},C) with φa=b¬b, φb=b and φc=cb. The acceptance conditions are also shown below the statements.

Figure 1.

ADF example.

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 v8 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 v8, with the reduct of this model being Dv8=D. The grounded interpretation of D is v6, which is different than v8. Therefore v8 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σ(D). The corresponding decision problem is denoted by Credσ. If s is true in all vσ(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σ(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.

abc
v1uuuadm
v2ufuadm
v3utuadm
v4ttuadm
v5uttadm
v6tuuadm, com, grd
v7tfuadm, com, prf
v8tttadm, com, prf, mod

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

Table 2.

Complexity results for semantics of ADFs.

σadmcomprfgrdmodstb
CredσΣ2P-cΣ2P-cΣ2P-ccoNP-cNP-cΣ2P-c
SkeptσtrivialcoNP-cΠ3P-ccoNP-ccoNP-cΠ2P-c
VerσcoNP-cDP-cΠ2P-cDP-cin PcoNP-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. Skeptprf(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

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 σ{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:={ppP}.

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

The purpose of introducing the notation S¯ and 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 S¯ of propositional variables representing statements of some ADF the alphabet of QBFs also contains the set of signed variables corresponding to S¯.

Definition 3.2.

Let S¯ be a variable set copy of a set of statements S. Then S¯3:={s¯sS}{s¯sS} is the set of signed variables associated to S¯.

The intended meaning of s¯ is that s is accepted and s¯ that s is rejected under some interpretation. Intuitively, a statement is undecided if both s¯ and 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 s¯,s¯S¯3, we need to restrict attention to coherent interpretations for QBFs, which exclude the possibility for a model to satisfy both s¯ ands¯.

Definition 3.3.

Let S¯ be a variable set copy of a set of statements of S. A two valued interpretationvˆ is coherent on S¯3 if there is no sS such that vˆ(s¯)=t and vˆ(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 S¯ a variable set copy of S. A two valued interpretation vˆ on S¯ corresponds to a two valued interpretation v on S, denoted as vˆS¯v if v(s)=vˆ(s¯) for all sS. A coherent two valued interpretation vˆ on S¯3 corresponds to a three valued interpretation v on S, denoted as vˆS¯3v if the following three conditions are met:

  • v(s)=t if and only if vˆ(s¯)=t and vˆ(s¯)=f;

  • v(s)=f if and only if vˆ(s¯)=f and vˆ(s¯)=t; and

  • v(s)=u if and only if vˆ(s¯)=f and vˆ(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, S¯ and S¯¯ variable set copies of S, vˆ1 and vˆ2 two valued (QBF) interpretations, and v1 and v2 three or two valued interpretations on S.

  • (1) Assume that S¯3 and S¯¯3 are disjoint, v1ˆ is coherent on S¯3, v2ˆ is coherent on S¯¯3, v1ˆS¯3v1 and v2ˆS¯¯3v2. Then vˆ:=v1ˆ[S¯¯3/v2ˆ(S¯¯3)] is also coherent on each of S¯3 and S¯¯3, and it is also the case that vˆS¯3v1 and vˆS¯¯3v2.

  • (2) Assume that v1ˆ is coherent on S¯3, v1ˆS¯3v1 and v2ˆS¯¯v2. Then vˆ:=v1ˆ[S¯¯/v2ˆ(S¯¯)] is also coherent on S¯3 and it is also the case that vˆS¯3v1 and vˆS¯¯v2.

  • (3) Assume that v2ˆ is coherent on S¯¯3, v1ˆS¯v1 and v2ˆS¯¯3v2. Then vˆ:=v1ˆ[S¯¯3/v2ˆ(S¯¯3)] is also coherent on S¯¯3 and it is also the case that vˆS¯v1 and vˆS¯¯3v2.

  • (4) Assume that S¯ and S¯¯ are disjoint, v1ˆS¯v1 and v2ˆS¯¯v2. Then for vˆ:=v1ˆ[S¯¯3/v2ˆ(S¯¯3)] it is also the case that vˆS¯v1 and vˆS¯¯v2.

Proof (sketch)

Let T1=S¯3 and T2=S¯¯3 in item (1), T1=S¯3 and T2=S¯¯ in item (2), T1=S¯ and T2=S¯¯3 in item (3) and T1=S¯ and T2=S¯¯ in item (4). Then all these items follow from the fact that vˆ and v1ˆ as defined in each of the items agree on the variables in T1 while vˆ and vˆ2 agree on the variables in T2 (and that T1 and T2 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 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 (S¯3) or unsigned (S¯) variables standing for the statements of the ADFs, respectively. We thus write Eσ[(S¯,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 (σ{adm,com,prf,grd,mod,stb}), Eσ[(S¯,C¯)] must also be a QBF whose models are coherent on S¯3 in the sense of Definition 3.3.

Definition 3.6.

Let σ{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 S¯ of S it returns a QBF Eσ[(S¯,C¯)] with free variables in S¯3 if σ{adm,com,prf,grd} and in S¯ if σ{mod,stb}. Furthermore,

  • (1) (Coherence) If σ{adm,com,prf,grd}, then any two valued interpretation vˆ such that vˆEσ[S¯,C¯] is coherent on S¯3.

  • (2) (Soundness)

    • (a) If σ{adm,com,prf,grd} and vˆ is a two valued interpretation such that vˆEσ[S¯,C¯], then the three valued interpretation v on S such that vˆS¯3v is a σ interpretation of D.

    • (b) If σ{mod,stb} and vˆ is a two valued interpretation such that vˆEσ[S¯,C¯], then the two valued interpretation v on S such that vˆS¯v is a σ interpretation of D.

  • (3) (Completeness)

    • (a) If σ{adm,com,prf,grd} and v is a three valued σ interpretation of D, then for any two valued interpretation vˆ such that vˆS¯3v, it holds that vˆEσ[S¯,C¯].

    • (b) If σ{mod,stb} and v is a two valued σ interpretation of D, then for any two valued interpretation vˆ such that vˆS¯v, it holds that vˆEσ[S¯,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 S¯ of a set of statements S, the following formula ‘filters out’ interpretations which are not coherent on S¯3:

coh[S¯]:=sS¬(s¯s¯).

Lemma 3.7.

Let S¯ be a variable set copy of a set of statements S. A two valued interpretation vˆ is coherent on S¯3 if and only if vˆcoh[S¯].

Proof.

A two valued valuation vˆ is coherent on S¯3 according to Definition 3.3 if and only if there is no sS such that vˆ(s¯)=t and vˆ(s¯)=t. This is the case if and only if for each sS, vˆ¬(s¯s¯), that is,vˆsS¬(s¯s¯)=coh[S¯].

In order to encode the definitions of ADF semantics as QBFs we often need to express that v(s)iv(s) on all sS for two interpretations of an ADF D=(S,C). The formula

S¯3iS¯¯3:=sS((s¯s¯¯)(s¯s¯¯))
does precisely that assuming both v and v are three valued and using the variable set copies S¯ and 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, S¯ and S¯¯ disjoint variable set copies of S.

  • (1) Let vˆ be a two valued interpretation that is coherent on S¯3 and S¯¯3 such that vˆS¯3iS¯¯3. Then for three valued interpretations v, v on S such that vˆS¯3v and vˆS¯¯3v it is the case that viv.

  • (2) Let v and v be three valued interpretations on S such that viv. Then for any two valued interpretation vˆ such that vˆS¯3v and vˆS¯¯3v, it is the case that vˆS¯3iS¯¯3.

Proof.

  • (1) Let vˆ be a two valued interpretation that is coherent on S¯3 and S¯¯3 and assume that vˆS¯3iS¯¯3=sS((s¯s¯¯)(s¯s¯¯)). Let also v, v be three valued interpretations on S such that vˆS¯3v and vˆS¯¯3v. For an arbitrary sS, since vˆ(s¯s¯¯)(s¯s¯¯) and vˆS¯3v as well as vˆS¯¯3vif v(s)=t then vˆ(s¯)=t, hence vˆ(s¯¯)=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)iv(s) whatever the value of v(s). In conclusion, v(s)iv(s) and since sS was arbitrary viv.

  • (2) Let v and v be three valued interpretations on S such that viv and vˆ a two valued interpretation such that vˆS¯3v and vˆS¯¯3v. For an arbitrary sS, if v(s)=x{t,f} then also v(s)=x must be the case. Hence, it follows from Definition 3.4 that if vˆ(s¯)=t then also vˆ(s¯¯)=t and if vˆ(s¯)=t then vˆ(s¯¯)=t. Therefore vˆ(s¯s¯¯)(s¯s¯¯) and since sS was arbitrary vˆsS((s¯s¯¯)(s¯s¯¯))=S¯3iS¯¯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 S¯ and S¯¯ of S, there exist exactly two three valued interpretations v and v on S that correspond to a coherent two valued interpretation vˆ on S¯3 and S¯¯3, respectively, while for three valued interpretations v and v on S there exist (infinitely) many coherent two valued interpretations on S¯3 and S¯¯3 that correspond to v and v (all variables that are not in S¯3 and S¯¯3 can be assigned any truth value).

The formula below

S¯3iS¯¯:=sS((s¯s¯¯)(s¯¬s¯¯))
encodes that viv 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, S¯ and S¯¯ variable set copies of S.

  • (1) Let vˆ be a two valued interpretation that is coherent on the set of signed variables S¯3 and such that vˆS¯3iS¯¯. Then for the three and two valued interpretations v and v on S such that vˆS¯3v and vˆS¯¯v, it is the case that viv.

  • (2) Let v and v be three and two valued interpretations on S such that viv. Then for any two valued interpretation vˆ such that vˆS¯3v and vˆS¯¯v, it is the case that vˆS¯3iS¯¯.

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}sS) be an ADF and v a three valued interpretation on S. Then vadm(D) iff v(s)iw(φs) for all sS and w[v]2.

Proof.

Let v be a three valued interpretation such that vadm(D). For an arbitrary sS, if v(s)=x for x{t,f}, one has that v(s)iΓD(v)(s)iw(φs) for all w[v]2. If v(s)=u then v(s)iw(φs) whatever the value of w(φs) for all w[v]2. In conclusion, since sS was arbitrary v(s)iw(φs) for all sS and w[v]2.

Assume now that v(s)iw(φs) for all sS and w[v]2. For an arbitrary sS, assume first that w(φs)=t for all w[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[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[v]2, that is, there exist w,w[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 sS was arbitrary viΓ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}sS) and a variable set copy S¯ of S, let the function Eadm return a QBF with free variables in S¯3

Eadm[S¯,C¯]:=coh[S¯]S¯((S¯3iS¯)sS((s¯φ¯s)(s¯¬φ¯s))).
Then Eadm is a defining encoding function for adm.

Proof.

Coherence of Eadm follows from the fact that for any two valued interpretation vˆ such that vˆEadm[S¯,C¯] for an arbitrary ADF D=(S,C) it is also the case that vˆcoh[S¯] and, hence, according to Lemma 3.7, vˆ is coherent on S¯3.

In order to prove soundness assume that vˆ is a two valued interpretation, D=(S,C={φs}sS) an ADF, and vˆEadm[S¯,C¯]. Then, vˆS¯((S¯3iS¯)sS((s¯φ¯s)(s¯¬φ¯s))) which, by Lemma 2.1 implies that vˆ[S¯/w¯(S¯)](S¯3iS¯)sS((s¯φ¯s)(s¯¬φ¯s)) for any two valued interpretation w¯. In particular, zˆ(S¯3iS¯)sS((s¯φ¯s)(s¯¬φ¯s)) with zˆ:=vˆ[S¯/w¯(S¯)] for any two valued valuation wˆ such that wˆS¯w for some w[v]2. Now, by Lemma 3.5 zˆ is coherent on S¯3 and zˆS¯3v as well as zˆS¯w. Since w[v]2 it follows that viw and according to Lemma 3.9, zˆS¯3iS¯. Hence, also zˆsS((s¯φ¯s)(s¯¬φ¯s)) must be the case. Consider now an arbitrary sS and assume that v(s)=t. In that case, since zˆS¯3v, by Definition 3.4 zˆ(s¯)=t and, hence, since zˆs¯φs¯, also zˆφs¯ must be the case. Since zˆ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 zˆs¯¬φs¯, w(¬φs)=t holds, that is, w(φs)=f. Finally, if v(s)=u, then v(s)iw(φs) whatever the value of w(φs). In conclusion, v(s)iw(φs) and, since s and w are arbitrary, moreover v(s)iw(φs) for every sS and w[v]2. In conclusion, by Proposition 3.10 vadm(D) is the case.

To prove completeness, assume vadm(D) for an ADF D=(S,C={φs}sS). Consider a two valued interpretation vˆ such that vˆS¯3v. By Definition 3.4 and Lemma 3.7 then also vˆcoh[S¯]. Consider now an arbitrary two valued interpretation wˆ and assume that zˆS¯3iS¯ for zˆ:=vˆ[S¯/w¯(S¯)]. By Lemma 3.5 zˆ is also coherent on S¯3 while zˆS¯3v as well as zˆS¯w. Hence, according to Lemma 3.9, viw and since w is two valued this means that w[v]2. Since vadm(D) according to Proposition 3.10 this means that v(s)iw(φs) for all sS. Consider an arbitrary sS. If zˆ(s¯)=t, then since zˆ is coherent on S¯3 and zˆS¯3v it must be the case that v(s)=t. Hence, since v(s)iw(φs) also w(φs)=t must hold and, therefore, since zˆS¯w also zˆ(φs¯)=t must be the case. Therefore zˆs¯φs¯. In the same manner, from the assumption that zˆ(s¯)=t one arrives at zˆs¯¬φs¯. In conclusion, zˆ(s¯φs¯)(s¯¬φs¯) and since sS was arbitrary in fact zˆsS((s¯φ¯s)(s¯¬φ¯s)). Hence zˆ(S¯3iS¯)sS((s¯φ¯s)(s¯¬φ¯s)) and since wˆ in zˆ:=vˆ[S¯/wˆ(S¯)] was arbitrary according to Lemma 2.1 vˆS¯((S¯3iS¯)sS((s¯φ¯s)(s¯¬φ¯s))). Finally, it follows that vˆcoh[S¯]S¯((S¯3iS¯)sS((s¯φ¯s)(s¯¬φ¯s)))=Eadm[S¯,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 S¯=S as variable set copy). Here we use the abbreviation S3i{φs}sS:=sS((s¯φ¯s)(s¯¬φ¯s)) to express the conjunct at the end of the encoding presented in Proposition 3.11.

Eadm[S,C]=coh[S]{a,b,c}((S3iS)(S3i{φs}sS))coh[S]=¬(aa)¬(bb)¬(cc)S3iS=((aa)(a¬a))((bb)(b¬b))((cc)(c¬c))S3i{φs}sS=((a(b¬b))(a¬(b¬b)))((bb)(b¬b))((c(cb))(c¬(cb)))

Any interpretation mapping the free variables a and b to t and a, b, c, c to f satisfies Eadm[S,C] and corresponds to the interpretation v7adm(D) from Table 1.

The following proposition gives the defining encoding for the complete semantics. The first conjunct of Ecom[S¯,C¯] for some ADF D=(S,C={φs}sS) and variable set copy S¯ ensures that any model of Ecom[S¯,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 sS only if there exist w,w[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}sS) and a variable set copy S¯ of S, let the function Ecom return a QBF with free variables in S¯3

Ecom[S¯,C¯]:=Eadm[S¯,C¯]sS((¬s¯¬s¯)S¯S¯((S¯3iS¯)(S¯3iS¯)φs¯¬φs¯)).
Then Ecom 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}sS), vcom(D) if and only if (i) vadm(D) and (ii) v(s)=u is the case for some sS only if there exist w,w[v]2 such that w(φs)=t and w(φs)=t. Thatvcom(D) implies that v satisfies (i) and (ii) is immediate from the definition of complete interpretations. For the converse, (i), that is, viΓD(v), implies that v(s)=ΓD(v)(s) for sS such that v(s)=t andv(s)=f. On the other hand (ii), which spells out the conditions under which ΓD(v)(s)=u for some sS, implies that also v(s)=ΓD(v)(s) for sS such that v(s)=u.

Coherence follows directly from Proposition 3.11 and the fact that for any two valued interpretation vˆ such that vˆEcom[S¯,C¯] it is also the case that vˆEadm[S¯,C¯] for any ADF D=(S,C). Proof of soundness and completeness involves showing that for a two valued interpretationvˆ, vˆEcom[S¯,C¯] if and only if the three valued interpretation v such that vˆS¯3v satisfies (i) as defined above which is encoded via Eadm[S¯,C¯] and (ii) which is encoded via sS((¬s¯¬s¯)S¯S¯((S¯3iS¯)(S¯3iS¯)φ¯s¬φ¯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 allsS, 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 S¯ of S, let the function Eprf return a QBF with free variables in S¯3

Eprf[S¯,C¯]:=Eadm[S¯,C¯]S¯3(Eadm[S¯,C¯]((S¯3iS¯3)(S¯3iS¯3))).
Then Eprf is a defining encoding function for prf.

Proof.

Coherence of Eprf follows from the fact that for any two valued interpretation vˆ such that vˆEprf[S¯,C] for an arbitrary ADF D=(S,C) it is also the case that vˆEadm[S¯,C¯] and, hence, according to Proposition 3.11, vˆ is coherent on S¯3.

In order to prove soundness assume that vˆ is a two valued interpretation, D=(S,C) an ADF, and vˆEprf[S¯,C¯]. Then, also vˆEadm[S¯,C¯] and, hence, according to Proposition 3.11, any three valued interpretation v such that vˆS¯3v is an admissible interpretation of D. Assume that there exists vadm(D) such that v>iv. Now, since vˆEprf[S¯,C¯] it is also the case that vˆS¯3(Eadm[S¯,C¯]((S¯3iS¯3)(S¯3iS¯3))) and, hence, according to Lemma 2.1 vˆ[S¯3/w(S¯3)]Eadm[S¯,C¯]((S¯3iS¯3)(S¯3iS¯3)) for any interpretation wˆ. In particular, zˆEadm[S¯,C¯]((S¯3iS¯3)(S¯3iS¯3)) with zˆ:=vˆ[S¯3/vˆ(S¯3)] for any two valued valuation vˆ such that vˆS¯3v. Now, by Lemma 3.5 zˆS¯3v and zˆS¯3v. Since zˆS¯3v by Proposition 3.11vˆEadm[S¯,C¯]. Also, since v>iv, by Lemma 3.8, zˆS¯3iS¯3 and, hence, it must also be the case that zˆS¯3iS¯3 which, according to Lemma 3.8 contradicts the assumption that v>iv. Hence, there does not exist vadm(D) such that v>iv and v is therefore a preferred interpretation of D.

To prove completeness, assume vprf(D). Consider a two valued interpretation vˆ such that vˆS¯3v. Since vadm(D) by Proposition 3.11, vˆEadm[S¯,C¯]. Consider now an arbitrary two valued interpretation vˆ such that wˆEadm[S¯,C¯] for wˆ:=vˆ[S¯3/vˆ(S¯3)], that is, also vˆEadm[S¯,C¯]. By Proposition 3.11 this means that vadm(D) for the three valued interpretation v such that wˆS¯¯3v (and vˆS¯¯3v). Assume now that alsowˆS¯3iS¯3 but wˆS¯3iS¯3. Since by Lemma 3.5 also wˆS¯¯3v and hence wˆ is coherent on S¯3 in addition to S¯3, by Lemma 3.8 this implies that viv and viv, that is, v>iv, which is in contradiction withvprf(D). Hence wˆ(S¯3iS¯3)(S¯3iS¯3) and, therefore, wˆEadm[S¯,C¯]((S¯3iS¯3)(S¯3iS¯3)). Since vˆ in wˆ:=vˆ[S¯3/v¯(S¯3)] was arbitrary, by Lemma 2.1 this means that vˆS¯3(Eadm[S¯,C¯]((S¯3iS¯3)(S¯3iS¯3))). In conclusion we have vˆEadm[S¯,C¯]S¯3(Eadm[S¯,C¯]((S¯3iS¯3)(S¯3iS¯3)))=Eprf[S¯,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 S¯=S as variable set copy).

Eprf[S,C]=Eadm[S,C]{a,a,b,b,c,c}(Eadm[S,C]((S3iS3)(S3iS3)))Eadm[S,C]=coh[S]{a,b,c}((S3iS)(S3i{φs}sS))coh[S]=¬(aa)¬(bb)¬(cc)S3iS=((aa)(a¬a))((bb)(b¬b))((cc)(c¬c))S3i{φs}sS=((a(b¬b))(a¬(b¬b)))((bb)(b¬b))((c(cb))(c¬(cb)))Eadm[S,C]=coh[S]{a,b,c}((S3iS)(S3i{φs}sS))coh[S]=¬(aa)¬(bb)¬(cc)S3iS=((aa)(a¬a))((bb)(b¬b))((cc)(c¬c))S3i{φs}sS=((a(b¬b))(a¬(b¬b)))((bb)(b¬b))((c(cb))(c¬(cb)))S3iS3=((aa)(aa))((bb)(bb))((cc)(cc))S3iS3=((aa)(aa))((bb)(bb))((cc)(cc))

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 vadm(D) we have either that v and v are incomparable w.r.t. i, or that viv. 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 S¯ of S, let the function Egrd return a QBF with free variables in S¯3

Egrd[S¯,C¯]:=Ecom[S¯,C¯]S¯3(Ecom[S¯,C¯]((S¯3iS¯3)).
Then Egrd is a defining encoding function for grd.

Proof (sketch)

Egrd[S¯,C¯] encodes the fact that the grounded interpretation of an ADF D=(S,C) is the i minimal complete interpretation of D. Ecom[S¯,C¯] encodes that the grounded interpretation is complete while S¯3(Ecom[S¯,C¯](S¯3iS¯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}sS) and a variable set copy S¯ of S, let the function Emod return a QBF with free variables in S¯

Egrd[S¯,C¯]:=sS(s¯φ¯s).
Then Emod is a defining encoding function for mod.

Proof.

Let D=(S,C={φs}sS) be an ADF. For a two valued interpretation vˆ it is the case that vˆEmod[S¯,C¯]=sS(s¯φ¯s) if and only if vˆs¯φ¯s for every sS. This holds if and only if vˆ(s¯)=vˆ(φs¯) for every sS. So given a two valued interpretationvˆ such that vˆEmod[S¯,C¯], since vˆ(s¯)=vˆ(φs¯) for every sS, also v(s)=v(φs) for every sS and the interpretation v such that vˆS¯v, that is, vmod(D). On the other hand given an interpretation vmod(D), any two valued interpretationvˆ such that vˆS¯v will satisfy that vˆ(s¯)=vˆ(φs¯) for every sS and hence vˆEmod[S¯,C¯].

We provide the defining encoding for the stable semantics in Proposition 3.23. The encoding function maps every ADF D=(S,C={φs}sS) 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 Dv 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 Dv:=(S,C:={φs}sS) withφs:=φs if v(s)=t and φs:= if v(s)=f. We prove in Lemma 3.21 that the grounded interpretation of Dv and Dv are equal when restricting attention to the assignments to the variables in Ev={sSv(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 US is the interpretation on S mapping each sS to u.

Definition 3.19.

Let D=(S,C) be an ADF and v be a two or three valued interpretation on S. Then EvD:={ssS 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 EvD as in the preceding paragraph, that is, write Ev instead.

Definition 3.20.

Let v and v be two or three valued interpretations on ST1 and ST2, respectively for some sets S, T1, and T2. Then

  • v=Sv if v(s)=v(s) for every sS,

  • v<iSv if v(s)<iv(s) for every sS, and

  • viSv if v(s)iv(s) for every sS.

Lemma 3.21.

Let D=(S,C={φs}sS) be an ADF and v a three valued interpretation on S. Then, grd(Dv)=Evgrd(Dv) where Dv:=(S,C:={φs}sS) with φs:=φs if v(s)=t and φs:= if v(s)=f.

Proof.

We prove by induction on n0 that ΓDvniEvΓDvn and ΓDvn+1iEvΓDvn. From this then the lemma follows since consider a k0 such that ΓDvk=l.f.p. (ΓDv) and ΓDvk=l.f.p. (ΓDv). In that case, one has that grd(Dv)=l.f.p. (ΓDv)=ΓDvkiEvΓDvk=l.f.p. (ΓDv)=grd(Dv) and grd(Dv)=l.f.p. (ΓDv)=ΓDvkiEvΓDvk+1=ΓDvk=l.f.p. (ΓDv)=grd(Dv). In other words, grd(Dv)iEvgrd(Dv) and grd(Dv)iEvgrd(Dv), hence grd(Dv)=Evgrd(Dv).

The base case (n=0) of the inductive proof holds trivially since ΓDv0=US=EvUEv=ΓDv0 and ΓDv1iEvΓDv0=UEv since UEv is the i least interpretation on EV.

Before proving the inductive step note first that ΓDv1(s)=f for every sS such that v(s)=f (since for every w[US]2 it is the case that w(φs)=w()=f). Hence, since the characteristic operator is monotonic in fact ΓDvn(s)=f and so also w(s)=f for every w[ΓDvn]2 holds for every sS 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 sEv, w[ΓDvn]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, viSv for some set S, and ψ is a propositional formula with all variables that occur in ψ being in S, then if for every w[v]2 it is the case that w(ψ)=x for x{t,f} then also for every w[v]2 it holds that w(ψ)=x.

This is because if there exists some w[v]2 such that w(ψ)x (x{t,f}), then, since viSviw there also exists a w[v]2 such that w=Sw and therefore w(ψ)x which is a contradiction.

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

To prove that ΓDvn+2iEvΓDvn+1 from the induction hypothesis assume now that for an arbitrary sEv it is the case that ΓDvn+1(s)=t. This means that for every w[ΓDvn]2 it holds that w(φs[b/:v(b)=f])=t. By the induction hypothesis ΓDvn+1iEvΓDvn, hence by Observation B also for every w[ΓDvn+1]2 it holds that w(φs[b/:v(b)=f])=t. Finally, by Observation A one has that in fact for every w[ΓDvn+1]2 it is the case that w(φs)=w(φs)=t. Hence, ΓDvn+2(s)=t. In the same manner one can prove that if ΓDvn+1(s)=f also ΓDvn+2(s)=f. Finally, if ΓDvn+1(s)=u then ΓDvn+2(s)iΓDvn+1(s) whatever the value of ΓDvn+2(s). Since sEv was arbitrary one can conclude thatΓDvn+2iEvΓDvn+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 S¯ a variable set copy of a set of statements S. Then φ[S¯/v(S)] with v a two valued interpretation on S denotes the QBF φ with s¯ replaced for ⊤ in case v(s)=t and s¯ replaced for ⊥ in case v(s)=f. φ[S¯3/v(S)] with v a three (or two) valued interpretation on S denotes the QBF φ where

  • s¯ is replaced for ⊤ and s¯ is replaced for ⊥ in case v(s)=t;

  • s¯ is replaced for ⊥ and s¯ is replaced for ⊤ in case v(s)=f; and

  • s¯ and 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 {φ¯ss¯}sS (of an ADF D=(S,{φs}sS) and w.r.t. a variable set copy S¯) within the sub-module Egrd[S¯,{φ¯ss¯}sS] is applied only to the acceptance condition φ¯s and not to s¯ for every sS. So, for example, {φ¯ss¯}sS={φ¯ss¯}sS. See Example 3.24 for how this works in practice.

Proposition 3.23.

Given an ADF D=(S,C) and a variable set copy S¯ of S, let the function Estb return a QBF with free variables in S¯

Estb[S¯,C¯]:=Emod[S¯,C¯]sS(s¯s¯)Egrd[S¯,{φ¯ss¯}sS].
Then Estb is a defining encoding function for stb.

Proof.

Let D=(S,C) be an ADF. In order to prove soundness consider a two valued interpretationvˆ such that vˆEstb[S¯,C¯]. Then vˆEmod[S¯,C¯] from which it follows via Proposition 3.17 that vmod(D) for the interpretation v such that vˆS¯v. Now, it is also the case that vˆEgrd[S¯,{φ¯ss¯}sS] and hence by Lemma 2.3 vˆEgrd[S¯,{φ¯ss¯}sS][S¯/vˆ(S¯)]. Since vˆ(s¯)=v(s) for all sS the latter is equivalent to vˆEgrd[S¯,{φ¯ss¯}sS][S¯/v(S)]. From Proposition 3.16 it follows that v=grd(D#) for the interpretation v such that vˆS¯v and the ADF D#=(S,{φs#}sS) where φs#=φs if v(s)=t and φs#=φs ifv(s)=f. Note that since φsφs and φs for any sS the ADF D# is equivalent to the ADF Dv:=(S,C={φs}sS) defined as in Lemma 3.21. Hence, v=grd(Dv). Finally, consider an arbitrary sS such that v(s)=t, that is, sEv. Since vˆsS(s¯s¯), in particular vˆs¯s¯. Hence, given that vˆS¯v and therefore vˆ(s¯)=t, it must also be the case that vˆ(s¯)=t. From this it follows that since vˆS¯v also v(s)=t and since sEv was arbitrary in fact EvEv. In the same manner from the fact that vˆsS(s¯s¯) one can also conclude that EvEv and, hence, EvEv. Since v=grd(Dv) from Lemma 3.21 it follows that EvD=EvDv where v=grd(Dv).

To prove completeness, let D=(S,C) be an ADF and v a two valued interpretation such that vstb(D). Then vmod(D) and EvD=EvDv for v=grd(Dv). From Lemma 3.21 it follows that also EvD=EvDv for v=grd(Dv). As has been argued for in the proof of soundness, the ADF Dv is equivalent to the ADF D# defined as above and hence v=grd(D#). Let vˆ be a two valued interpretation such that vˆS¯v and vˆS¯v. Then since vmod(D) and vˆS¯v it follows from Proposition 3.17 that vˆEmod[S¯,C¯]. Also, since v=grd(D#), one has that vˆEgrd[S¯,{φ¯ss¯}sS][S¯/v(S)]=Egrd[S¯,{φ¯ss¯}sS][S¯/vˆ(S¯)]. This by Lemma 2.3 is equivalent to vˆEgrd[S¯,{φ¯ss¯}sS]. Finally, from the fact that EvD=EvDv, vˆS¯v, and vˆS¯v it is easy to show that vˆ(s¯)=t if and only if vˆ(s¯)=t for each sS and hence vˆsS(s¯s¯). In conclusion, vˆEmod[S¯,C¯]sS(s¯s¯)Egrd[S¯,{φ¯ss¯}sS]=Estb[S¯,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 S¯=S as variable set copy).

Estb[S¯,C¯]=Emod[S,C]Egrd[S,{φss}sS](aa)(bb)(cc)Emod[S,C]=(a(b¬b))(bb)(c(cb))V1={a,a,b,b,c,c}Egrd[S,{φss}sS]=Ecom[S,{φss}sS]V1(Ecom[S,{φss}sS](S3iS3))V2={a,b,c,a,b,c}Ecom[S,{φss}sS]=Eadm[S,{φss}sS]((¬a¬a)V2((S3iS)(S3iS)((b¬b)a)¬((b¬b)a)))((¬b¬b)V2((S3iS)(S3iS)(bb)¬(bb)))((¬c¬c)V2((S3iS)(S3iS)((cb)c)¬((cb)c)))Eadm[S,{φss}sS]=coh[S]{a,b,c}((S3iS)(S3i{φss}sS))S3i{φss}sS=((a((b¬b)a))(a¬((b¬b)a)))((b(bb))(b¬(bb)))((c((cb)c))(c¬((cb)c)))
Note in this example how Egrd[S,{φ¯ss}sS] and Ecom[S,{φ¯ss}sS] are expanded without applying priming to any s within a modified acceptance condition of the form φss.

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, sS, σ{adm,com,prf,grd,mod,stb}, and v a three (or two) valued interpretation. If σ{adm,com,prf,grd}, then let xs and T=S3. Otherwise if σ{mod,stb}, then let x=s and T=S. It holds that

  • (1) Credσ(s,D)=yes iff T(Eσ[S,C]x) is satisfiable;

  • (2) Skeptσ(s,D)=yes iff T(Eσ[S,C]x) is satisfiable; and

  • (3) Verσ(v,D)=yes iff Eσ[S,C][T/v(S)] is satisfiable.

Proof.

  • (1) Assume first that Credσ(s,D)=yes. This means that there exists an interpretation vσ(D) such that v(s)=t. Let vˆ be a two valued interpretation such that vˆTv. Then, since Eσ is a defining encoding for σ, vˆEσ[S,C]. Also, since v(s)=t and vˆTv, it is the case that vˆx. Hence vˆEσ[S,C]x and by Corollary 2.2 then T(Eσ[S,C]x) is satisfiable.

    Assume now that T(Eσ[S,C]x) is satisfiable. Then by Corollary 2.2 there exists a two valued interpretation vˆ such that vˆEσ[S,C]x. Let v be the three valued interpretation such that vˆTv. Then since vˆEσ[S,C] and Eσ is a defining encoding for σ, vσ(D). Also, since vˆx one has that v(s)=t. Hence Credσ(s,D)=yes.

  • (2) Assume first that Skeptσ(s,D)=yes. This means that for every interpretation vσ(D) it is the case that v(s)=t. Let vˆ be a two valued interpretation such that vˆEσ[S,C]. In that case, since Eσ is a defining encoding for σ, if v is a three valued interpretation such that vˆTv, it holds that vσ(D). Hence v(s)=t and, therefore, vˆx. As a consequence vˆEσ[S,C]x and, since vˆ was arbitrary, by Corollary 2.2 T(Eσ[S,C]x) is satisfiable.

    Assume now that T(Eσ[S,C]x) is satisfiable. Then by Corollary 2.2 for every two valued interpretation vˆ it is the case that vˆEσ[S,C]x. Let v be any three valued interpretation such that vσ(D) and vˆ a two valued interpretation such that vˆTv. Then vˆEσ[S,C] and hence, since vˆEσ[S,C]x, also vˆx. Therefore v(s)=t and, since v was arbitrary, it is the case that v(s)=t for any vσ(D), that is, Skeptσ(s,D)=yes.

  • (3) Assume first that Verσ(v,D)=yes. This means that vσ(D). Let vˆ be a two valued interpretation such that vˆTv. Then, since Eσ is a defining encoding for σ, vˆEσ[S,C]. By Lemma 2.3 this means that Eσ[S,C][T/vˆ(T)]=Eσ[S,C][T/v(S)] is true (satisfiable).

    Assume now that Eσ[S,C][T/v(S)] is satisfiable and let vˆ be a two valued interpretation such that vˆEσ[S,C][T/v(S)]. Note then that vˆ[T/v(S)]Eσ[S,C] where vˆ[T/v(S)] is defined mirroring Definition 3.22. Also if v is the three valued interpretation such that vˆ[T/v(S)]Tv then v=v and since Eσ is the defining encoding function for σ, vσ(D).

Many of the encodings shown above are adequate w.r.t. their complexity (see Table 2 for the complexity of the reasoning tasks)11. Since for any ADF D=(S,C) and sS we have Credadm(s,D)=Credcom(s,D)=Credprf(s,D) we can use the encodings for admissibility in these cases. Transforming T(Eadm[S,C]x) to PNF results in a formula of prefix type Σ2, that is, a QBF in a class of QBFs for which satisfiability is Σ2P complete (Credadm is also Σ2P complete). Note that, in fact, although T(Ecom[S,C]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 Skeptprf, Credmod and Skeptmod. For instance, the QBF T(Eprf[S,C]x) can be transformed to a PNF with prefix type Π3. Skeptical acceptance w.r.t. admissible semantics is trivial. The encodings of Veradm(v,D) and Verprf(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 Vercom(v,D) and Vergrd(v,D) can also be considered ‘adequate’ in the sense that the encodings mirror the structure of the SAT UNSAT problem. Finally, Vermod(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 Skeptcom(s,D)=Skeptgrd(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 T(Ecom[S,C]x) by using the encoding of Skeptgrd(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}sS) be an ADF and v an interpretation. The following are some properties v can satisfy.

  • (1) For each sS such that v(s)=t there exists an interpretation w[v]2 for which w(φs)=t.

  • (2) For each sS such that v(s)=f there exists an interpretation w[v]2 for which w(φs)=f.

  • (3) For each sS such that v(s)=u there exist interpretations w1[v]2 and w2[v]2 such that w1(φs)=t and w2(φ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}sS) and a variable set copy S¯ of S, let the function Egrd return a QBF with free variables in S¯3

Egrd[S¯,C¯]:=coh[S¯]ψ(S¯3((coh[S¯]χ)(S¯3iS¯3)))ψ:=sS((s¯S¯((S¯3iS¯)φ¯s))(s¯S¯((S¯3iS¯)¬φ¯s))((¬s¯¬s¯)S¯S¯((S¯3iS¯)(S¯3iS¯)φ¯s¬φ¯s)))χ:=(sS((s¯S¯((S¯3iS¯)φ¯s))(s¯S¯((S¯3iS¯)¬φ¯s))((¬s¯¬s¯)S¯S¯((S¯3iS¯)(S¯3iS¯)φ¯s¬φ¯s)))).

Then Egrd is a defining encoding function for grd.

Proof (sketch)

Given an ADF D=(S,C={φs}sS), the proof involves showing that for any two valued interpretation vˆ, vˆEgrd[S¯,C¯] if and only if the interpretation v such that vˆS¯v is the i least interpretation satisfying Properties 1–3 in Definition 3.26. That vgrd(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), Egrd[S,C][S3/S] can be rewritten mirroring the structure of the SAT UNSAT problem as is shown in the appendix, thus reflecting the complexity of Vergrd which is DP 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, sS, and v the grounded interpretation of D. Then v(s)=x for x{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{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 viw 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{t,f} and every w satisfying Properties 1–3 of Definition 3.26 for an ADF D=(S,C={φs}sS) can be encoded as in the next proposition.

Proposition 3.30.

Given an ADF D=(S,C={φs}sS) and a variable set copy S¯ of S, let the function Agrd return a closed QBF

Agrd(s,S¯,C¯,x):=S¯3((coh[S¯]ψ)t)ψ:=sS((s¯S¯((S¯3iS¯)φ¯s))(s¯S¯((S¯3iS¯)¬φ¯s))((¬s¯¬s¯)S¯S¯((S¯3iS¯)(S¯3iS¯)φ¯s¬φ¯s))),
where t=s¯ if x=t and t=s¯ if x=f. Then, Agrd(s,S¯,C¯,x) with x{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 Skeptgrd and Vergrd (we remind the reader that Skeptgrd and Credgrd are equivalent since there exists only one grounded interpretation for any ADF).

Proposition 3.31.

Given an ADF D=(S,C) and an sS let the function Sgrd return a closed QBF

Sgrd(s,S,C):=Agrd(s,S,C,t).
Then Skeptgrd(s,D)=Credgrd(s,D)=yes if and only if Sgrd(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 Sgrd are QBFs with prefix type Π1 as is shown in the appendix, hence reflecting the complexity of Skeptgrd=Credgrd (=Skeptcom) which iscoNP 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 Dv is equivalent to checking whether each statement mapped to x{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.Dv.

Proposition 3.32.

Given an ADF D=(S,C={φs}sS) and a variable set copy S¯ of S, let the function Estb return a QBF with free variables in S¯

Estb[S¯,C¯]:=mod[S¯,C¯]sS(s¯Agrd(s,S¯,{φ¯ss¯}sS,t))sS(¬s¯Agrd(s,S¯,{φ¯ss¯}sS,f)).
Then Estb 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 QADF22 to the system DIAMOND by Ellmauthaler and Strass (20132014). 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.

Notes

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 DP complete problems, are written in such a way that they mirror the structure of the SAT UNSAT problem.

Disclosure statement

No potential conflict of interest was reported by the authors.

References