A key ingredient of computational argumentation in AI is the generation of arguments in favor or against claims under scrutiny. In this paper we look at the complexity of the argument generation procedure in the prominent structured formalism of assumption-based argumentation (ABA). We show several results connecting expressivity of ABA fragments and number of constructed arguments. First, for several NP-hard fragments of ABA, the number of generated arguments is not bounded polynomially. Even under equivalent rewritings of the given ABA framework there are situations where one cannot avoid an exponential blow-up. We establish a weaker notion of equivalence under which this blow-up can be avoided. As a general tool for analyzing ABA frameworks and resulting arguments and their conflicts, we extend results regarding dependency graphs of ABA frameworks, from which one can infer structural properties on the induced attacks among arguments.
assess the instantiated AF. Thus, many typical research
questions can be answered out of the box after converting
Computational models of argumentation are a central ap- the knowledge base. Moreover, since AFs are directed
proach within non-monotonic reasoning [
In the present paper, we will focus on ABA [
Constructing an AF corresponding to a given knowl- knowledge base, we would make the conditions under
edge base has several advantages. From a technical point which can be derived (i.e. what satisfying assignments
of view, there is an abundance of research concerned with to the formula exist) visible; indeed, among others, the
AFs (see [
′2 ′1
1 2
′2 2 We can now directly read off that e.g. {1, 2} (see 3) constitutes a satisfying assignment to since both 1 and 2 (and thus ) can be derived. We can also see that {1, ′1} would in principle infer as well, but this set of literals does not correspond to a well-defined (partial) assignment; we can not set 1 to true and false simultaneously. We thus see that constructing the arguments helps visualizing the information encoded in the knowledge base and makes certain relations explicit. Indeed, simply inspecting all arguments deriving suffices to decide whether there is a satisfying assignment to our formula.
However, since checking satisfiability of a given
CNFformula is the prototypical NP-complete problem, we
expect that this procedure must come with computational
cost elsewhere. Indeed, many structured argumentation
formalisms (including ABA) suffer from the drawback
that the knowledge base gives rise to exponentially many
(or even an infinite amount of) arguments [
by an ABA knowledge base large in size, but reasoning is easy? Although this idea is appealing in principle, the answer turns out to be negative in general: Even if we reduce our attention to the class of AFs induced by ABA knowledge bases, reasoning is still intractable in general. Nonetheless, we expect an underlying trade-off between size and complexity which is worth to be investigated. As a high level observation we expect an ideal ABA knowledge base to • induce a large AF, but with reasoning being simple, or • a concise AF, in which reasoning is potentially hard.
If the former is the case, then the instantiation procedure can help displaying relationships encoded within the knowledge base, as it was the case for our CNF formula from above. If on the other hand the latter case occurs, then the constructed AF is efficient and easy to capture visibly. In this paper, we will investigate this trade-off and examine the relationship between size and complexity of the induced AF. Most notably, we will show that each ABA framework can be transferred in a way that either reasoning becomes easy (Theorem 32) or the AF is of polynomial size (Proposition 28), but reaching both goals simultaneously is not possible in general (Theorem 32).
In doing so, our goal is also contributing to a general
formal understanding under which conditions a
knowledge base induces large AFs and which techniques might
help avoiding this blow-up. For carrying out reasoning
on ABA via using AFs, both the size of the resulting
AF and complexity of the resulting AF can pose
barriers to (automated) argumentative reasoning. On the one
hand size and complexity of AFs are direct challenges
for solvers [
The main contributions of the paper can be summarized as follows.
• We first deal with the case of infinite instantiated AFs and show that one can restrict attention to ifnite cores. • We relate bounds on the given ABA instance to (i) size bounds and computability of the constructed AF and (ii) complexity of reasoning. • We show that each ABA framework can be rewritten in a way that reasoning in the induced AF is tractable, while credulous acceptance of a target conclusion is preserved. • We present, for a fairly large class of ABA frameworks, a general transformation procedure to obtain a translated ABA framework which is equivalent under projection and has a polynomial-sized AF. We present an impossibility result suggesting that the notion of equivalence cannot be strengthened to full equivalence. • We extend the notion of dependency graphs on ABA frameworks (see, e.g., Craven and Toni, 2016) to a general tool for investigating ABA frameworks able to check structural properties inducing milder complexity, such as acyclic or odd-cycle free AFs.
We recall preliminaries for assumption-based
argumentation (ABA) [
The first ingredient of ABA is that of a deductive system (ℒ, ℛ), with ℒ a formal language and ℛ a set of inference rules over ℒ. In this work we assume that ℒ is a set of atoms. A rule ∈ ℛ is of the form ← 1, . . . , with ∈ ℒ. A shorthand for the head of a rule is defined by ℎ() = {}, and for the (possibly empty) body via () = {1, . . . , }. An ABA framework contains a deductive system and specifies which atoms are assumptions and what are contraries of assumptions. Definition 1. An ABA framework is a tuple = does not attack itself. Set defends assumption set (ℒ, ℛ, , ), where (ℒ, ℛ) is a deductive system, ⊆ ℒ ⊆ in iff for all ⊆ that attack it holds that a non-empty set of assumptions, and a function map- attacks . ping assumptions ∈ to atoms ∈ ℒ (the contrary function).
In this paper, we focus on the central semantical concept of admissibility.
(i) flat, i.e., for each rule ∈ ℛ it holds that ℎ() ∈/ Definition 4. Let = (ℒ, ℛ, , ) be an ABA frame(no assumptions can be derived), (ii) ℒ, ℛ, and () work. A set of assumptions ⊆ is admissible iff is for each ∈ is finite, and (iii) each rule in ℛ is stated conflict-free and defends itself. explicitly (given as input). We move on to tree-based arguments.
Semantics of ABA frameworks can be defined on subsets of the assumptions or via translation to arguments Definition 5. Let = (ℒ, ℛ, , ) be an ABA frameand attacks. Below, we recall both notions. work, and ( ⊢ ) and ( ⊢ ) two tree-based argu
Arguments in an ABA framework = (ℒ, ℛ, , ) ments based on . Tree-based argument ( ⊢ ) attacks are based on proof trees (derivations). Due to our focus on ( ⊢ ) if there is an assumption ∈ s.t. = . computational aspects, we will in later sections consider a different representation of arguments, hence we refer Collecting all tree-based arguments and attacks based to arguments based directly on proof trees as “tree-based on an ABA results in an argumentation framework correarguments”. Formally, a tree-based argument, denoted by sponding to the given ABA. ⊢ℛ , with ⊆ and ∈ ℒ based on is defined Definition 6. Let = (ℒ, ℛ, , ) be an ABA frameas a finite labeled rooted tree s.t. the root is labeled with work. The pair (A, R) is called the argumentation frame, each leaf is labeled by an assumption ∈ or a work (AF) corresponding to if A is the set of all treededicated symbol ⊤ ∈/ ℒ s.t. the set of all labels of leaves based arguments based on , and R is the set of all is , and each internal node is labeled with ℎ() of a attacks based on . rule ∈ ℛ s.t. the set of labels of children of this node is equal to () or ⊤ if the body is empty. Moreover, Below we recall the analogous notions of conflictif ∈ , then {} ⊢ℛ is also a tree-based argument freeness, defense and admissibility in AFs. (special case without using any derivation rules). In brief, a tree-based argument represents a derivation using rules Definition 7. Let be an ABA framework, = (A, R) in ℛ to derive starting from assumptions in . We say the corresponding AF, and ⊆ A a set of tree-based that is the claim of the tree-based argument. We remark arguments of . The set is conflict-free (in ) if there that there can be multiple tree-based arguments with the are no arguments ( ⊢ ), ( ⊢ ) ∈ s.t. ( ⊢ same set of assumptions and claim. ) attacks ( ⊢ ). A conflict-free set defends an
Given an ABA framework = (ℒ, ℛ, , ), deriv- argument ( ⊢ ) (in ) if for each argument ( ⊢ ) ∈ ability for a set of assumptions ⊆ is defined via A that attacks ( ⊢ ) it holds that there is an argument Th() = { | there is a tree-based argument ′ ⊢ℛ ( ⊢ ) ∈ s.t. ( ⊢ ) attacks ( ⊢ ). Moreover, , ′ ⊆ }. That is, Th() contains all atoms that is admissible (in ) if it is conflict-free and defends itself. can be derived (via tree-based arguments) using assumptions in . We omit subscripts and ℛ if clear from the context.
We now recall conflicts, admissible sets, and subsequently the corresponding definitions on tree-based arguments.
cl () = { | ( ⊢ ) ∈ } for a set of treebased arguments , and assumptions via asms () = ⋃︀(⊢)∈ .
To clearly distinguish semantics, we say that ⊆ is an admissible assumption set (or an adm-assumption Definition 2. Let = (ℒ, ℛ, , ) be an ABA frame- set) and that a set of tree-based arguments is an admiswork, and , ⊆ be two sets of assumptions. Assump- sible extension (or adm-extension for short). We refer tion set attacks assumption set in if ∈ Th() to all adm-assumption sets of via adm(), and to for some ∈ . all adm-extensions of an AF by adm( ). There is a direct correspondence between semantics via assumption
In words, an assumption set attacks assumption set sets and sets of tree-based arguments (see, e.g., Cˇyras if it is possible to derive from the contrary of some et al., 2018). assumption in .
Proposition 8. Let = (ℒ, ℛ, , ) be an ABA framework and = (A, R) the corresponding AF.
Definition 3. Let = (ℒ, ℛ, , ) be an ABA framework. An assumption set ⊆ is conflict-free in iff • If ∈ adm() then {( ⊢ ) | ⊆ , ( ⊢ ) is a tree-based argument in } ∈ adm( ), and • if ∈ adm( ) then asms () ∈ adm().
and = . There are infinitely (countably) many treebased arguments based on (via chaining rules arbitrary many times), and argument {} ⊢ is attacked by all tree-based arguments concluding (of which there are infinitely many). 1 ← 2 ← 1; 1 ← 2; ← ′2; 2 ← 1, 2.
′1; It holds that each ⊆ is admissible whenever {, ′} ̸⊆ for ∈ {1, 2} (no “complementary literals”). Moreover, the literal is credulously accepted under admissibility, since, e.g. {1, 2} is admissible and ∈ Th({1, 2}).
In general it can be the case that an AF corresponding to a given ABA is not finite. We first recall some basic properties of such (possibly) infinite corresponding AFs.
We say that an AF = (A, R) is infinite if A is innfiite.
An AF is finitary [
An important reasoning task on ABA and AFs is credulous reasoning under admissibility. An atom is cred- This leads to the simple observation stated next. That ulously accepted under admissibility in an ABA iff there are countably many tree-based arguments can be there is an adm-assumption-set s.t. ∈ Th(). For a seen since one can write (for a given ABA) each argument given AF (A, R) and ∈ A, it holds that is credulously as a string over a restricted alphabet. accepted under admissibility in iff there is an adm- Observation 11. Given an ABA framework, the correextension containing . We remark that credulous sponding AF can be (countably) infinite and non-finitary. acceptance of tree-based arguments in a given AF can be directly generalized to ask for acceptance of claims of Nevertheless, as one can see intuitively in the example, tree-based arguments, i.e., asking whether there is some AFs corresponding to an ABA framework can be “cut adm-extension containing some tree-based argument down” to a finite core by removing “duplicates” of arwith claim . guments. This observation is sometimes assumed to be
Complexity results for reasoning in ABA and AFs were folklore in the research community and stated for other
established (see, e.g., Dvorˇák and Dunne, 2018, for an forms of structured argumentation [
If one is not interested in the actual derivation of a claim, Example 10. Let = (ℒ, ℛ, , ) be an ABA frame- representing an argument as a pair (, ) narrows down work with = {, }, ℒ = {, } ∪ , four rules the argument to the information required in order to con( ← ), ( ← ), ( ← ), and ( ← ), and = struct the corresponding AF (the core) and perform the
Definition 12. Let = (ℒ, ℛ, , ) be an ABA framework. Let A = {(, ) | there is a tree-based argument ( ⊢ ) in }. An argument (, ) attacks an argument (, ) (in ) if ∃ ∈ s.t. = , with R being the set of all such attacks.
The AF = (A, R) is called the core of .
Claims and assumptions of a set of arguments ⊆ A are defined similarly as for tree-based arguments: cl () = { | (, ) ∈ } and asms () = ⋃︀(,)∈ . Given an ABA its corresponding AF and core ′, in addition to the core being finite it follows directly that • for each tree-based argument ( ⊢ ) there is an
argument (, ) and vice versa, and thus • has an admissible set of tree-based arguments with cl () = and asms () = iff ′ has an admissible set of arguments ′, cl (′) = and asms (′) = . standard reasoning tasks. To some extent surprising per- 4.1. Bounds and Complexity of haps, we can find a complexity-theoretic result supporting Reasoning the intuition that the core is a more efficient representation: while deciding whether a proof tree constitutes a tree-based argument for a given ABA is immediate, it is NP -hard to decide whether a pair (, ) occurs in the core.
Proposition 13. It is NP-hard to decide whether there is a proof tree from a given set of assumptions to a given claim.
Proof. Let = 1 ∧· · ·∧ be a Boolean formula in conjunctive normal form over vocabulary = {1, . . . , } with = {1, . . . , } the set of clauses. We construct an ABA framework with = , atoms together with literals over and {1 , . . . , }, and the following rules (note that “¬” is a symbol in ABA and has no meaning attached to the negation sign):
← { ¬ ← { ← ← and ← ¬ 1 , . . . , ∈ | ∈ }, and ∈ |¬ ∈ } for each ∈
for each ∈ Contraries are assigned to literals not appearing in any rules (for the task of argument construction, contraries are not relevant). It can be shown that (, ) is an argument of the resulting ABA framework iff is satisfiable.
that it is harder to compute the core compared to a corresponding AF, since one can directly extract the core from the corresponding AF. Rather, Proposition 13 formalizes that skipping computation of the proof trees in order to construct the core is a hard task in general.
From now on, we restrict our attention to cores, and assume that, for a given ABA, we operate exclusively on a core, unless explicitly mentioned otherwise.
In this section we study the impact of bounding certain parts of the input ABA on the complexity of reasoning and size of cores (and corresponding AFs in cases). We consider bounds on derivation-depth and bodies of rules.
When investigating size of cores, we make use of the following definition. Given an ABA the size of (||) is the length of a (direct) string representation of . Let be a set of ABA frameworks. We say that the cores of are polynomially bounded if there is a polynomial s.t. (||) ≥ | A| for all ∈ with = (A, R) the core of . We will see below that the cores of the set of all ABA frameworks are not polynomially bounded.
First, we consider bounds on (i) the depth of chaining rules and (ii) the size of bodies of rules. We show that restricting derivation-depth or rule-size does not yield milder complexity regarding credulous reasoning under admissibility.
Formally, an ABA is bounded by -derivation-depth if each proof tree of has height at most (i.e., the longest path from assumptions to claim is at most ). A rule of the form ← 1, . . . , is bounded by if ≤ ; an ABA is rule-size bounded by if each rule in is bounded by .
In order to show that bounding derivation-depth is intractable, we reduce the Boolean Satisfiability Problem via the following reduction: Reduction 14. Let = 1 ∧ · · · ∧ be a Boolean formula in conjunctive normal form (CNF) over clauses = {1, . . . , } and Boolean variables = {1, . . . , }. Define ′ = {′ | ∈ }. Construct = (ℒ, ℛ, , ) by • ℒ = ∪ ′ ∪ ∪ {}, • = ∪ ′, • = ′ and ′ = for each ∈ , and • let the set of rules be composed of ← 1, . . . , , and ← with = and ∈ or = ′ and ¬ ∈ .
The resulting ABA framework is bounded by 2derivation-depth as each proof tree has height at most 2. We observe that the presented reduction formalizes our introductory example: Example 15. Given the CNF-formula = (1 ∨ ¬2) ∧ (¬1 ∨ 2) from the introduction. Following Reduction 14, we obtain an ABA framework = (ℒ, ℛ, , ) which contains the assumptions = {1, 2, ′1, ′2} and the rules ← 1, 2 and • 1 ←
as • 2 ← 1, 1 ← ′1, 2 ← ′2 (since 1, ¬2 ∈ 1) as well 2 (since ′1, 2 ∈ 2) Moreover, the ABA framework assigns symmetric contraries, i.e., = ′ and ′ = for ∈ {1, 2}. The resulting framework indeed coincides with the introductory example (cf. Example 9).
accepted under admissible semantics in the ABA framework iff the formula is satisfiable.
Observe that tree-based arguments in the corresponding AF in Reduction 14 have derivation-depth of at most 2. We obtain that credulous reasoning is NP -complete
On the other hand, we observe that the computational hardness in symmetric ABAs stems entirely from the construction of arguments: indeed, constructing the cores results in AFs with ||/2 many even cycles of length 2 (a cycle for every assumption and its negation) satisfying that all arguments with claim ∈/ have only incoming attacks. For an example we refer to Figure 1. Credulous reasoning under admissibility in such AFs is decidable in time polynomial in the number of arguments, since it sufcfies to check if there exists an argument having the queried claim that is not attacked by both arguments in a 2-cycle. (1) = ∑︀=− 01 via induction over .
For = 1, we have (1) = .
Now assume the statement holds true for rule depth − 1.
(1) = · ( − 1(1)) = · (∑︀=− 02 ) = · (∑︀− 2 )
=0 = ∑︀=− 01 .
We thus obtain that the number of all possible trees constructible from is bounded by · with = ∑︀− 1 .
=0
Intuitively, exponentiality of the number of tree-based new argument. Therefore, after at most |A| + 1 iterations arguments stems from , and thus from derivation-depth we are done. Each iteration visits |ℛ| rules. Consider one and rule-size. Moreover, it is clear that the result extends particular rule . For each body literal, we need to search to the number of arguments in the cores of derivation- through at most |A| arguments. Since |()| ≤ , depth and rule-size bounded ABA frameworks. Bounding this is in (|A|). In order to decide whether or not the both parameters thus yields polynomially bounded cores. induced argument ⊢ ℎ() needs to be added, we again search through the at most |A| already constructed Corollary 20. The cores of the set of ABA frameworks arguments and compare. In summary, we visit rules at which are both derivation-depth and rule-size bounded by most (|A| + 1) · |ℛ| times and thereby, we can perform some constant are polynomially bounded. the necessary computations in time in 1(|A|+1).
Bounding derivation-depth or rule-size individually, however, does not yield cores that are polynomially bounded.
Proposition 21. The cores of ABA frameworks which are derivation-depth bounded by some constant are not polynomially bounded. Likewise, the cores of rule-size bounded ABA frameworks are not polynomially bounded.
As the reader might have noticed, having polynomially bounded cores does not (directly) imply the existence of a polynomial-time algorithm that can actually obtain the core in question. We show that for ABA frameworks which are rule-size bounded an algorithm can be obtained that enumerates arguments in polynomial-time regarding size of input and number of arguments. This can be achieved by a direct algorithm: for each rule with () = {1, . . . , } and already computed (tree-based) arguments { 1, . . . , } loop through each -sized subset of { 1, . . . , } and check whether cl () = (). If so, attach it to a potential new argument concluding ℎ(). If this argument is fresh, add it to the output. If ≤ for a constant , this search is bounded polynomially by the given ABA and size of core. Theorem 22. The cores of ABA frameworks whose rulesize is bounded by a constant can be constructed in polynomial time w.r.t. the size of the given ABA and core. Proof. Consider the following brute-force procedure. • loop through each rule ∈ ℛ as long as new arguments are added.
– given () = {1, . . . , }, for each subset 1, . . . , of the already constructed arguments s.t. cl () = * if the corresponding argument ⊢ ℎ() is not yet constructed, add it to the list; * otherwise break; By definition, this algorithm constructs the correct arguments in . The outer loop over each rule can be left once there was one iteration which did not induce any
Corollary 23. The cores of the set of rule-size and derivation-depth bounded ABA frameworks can be computed in polynomial time in size of the given ABA framework.
condition of rule-size boundedness in Theorem 22 can
be dropped; we conjecture that the condition is required.
In any case, Theorem 22 also yields the result that
enumerating arguments in the core of a rule-size bounded
ABA framework has incremental polynomial time
complexity [
We saw that ABA frameworks may yield a core not polynomially bounded, but with polynomial-time reasoning (under the credulous view and admissibility), e.g., when looking at Reduction 14. In this section we look at possibility results and an impossibility result of transforming a given ABA to another ABA framework whose core is polynomially bounded or allows for polynomial-time reasoning.
Recall that one of our main goals was to formalize the idea that one could construct ABA frameworks in a way that the induced AF might be large, but yields tractable reasoning in return. As we already mentioned, the ABA framework constructed in the motivating example corresponds to applying Reduction 14. Our intuition is that the ABA frameworks constructed according to this reduction indeed yield AFs with tractable reasoning (though in the potential exponential size of the AF). This intuition can be confirmed as follows: First, observe hat Reduction 14 The transformation is defined as follows. Intuitively, for yields symmetric ABA frameworks (by definition). Thus each conclusion derivable from a given ABA framework by Proposition 18 stating that reasoning in symmetric AFs , we introduce fresh assumptions (’ is derivable’) is indeed tractable, we obtain the desired outcome. and (’ is not derivable’) that simulate derivations.
However, this only states that a certain class of ABA The resulting ABA framework ′ contains only rules frameworks possesses this property. We would like to go with assumptions in the body, each of which gives rise one step further and transform an arbitrary given ABA to exactly one tree-based argument. Since no rule in ′ framework s.t. the corresponding AF behaves this way. It contains non-assumptions, each proof tree is of height 1. turns out that this can be achieved indeed, at least if we restrict our attention to some target conclusion, say ∈ ℒ. Definition 26. Let = (ℒ, ℛ, , ) be a non-circular The underlying idea is surprisingly simple: Suppose we ABA framework such that each ∈ ℒ is in Th(). We want to transform the ABA framework . Since the SAT define ′ = (ℒ′, ℛ′, ′, ′) as the AF-sensitive ABA problem is NP-complete, we can in polynomial time con- framework of as follows. For each ∈ ℒ ∖ struct a formula which is satisfiable iff is credulously • let and be two fresh assumptions, with accepted in . Now, our Reduction 14 translates into • = and = in ′. an ABA framework with the behavior we wish to obtain.
All these steps can be performed in polynomial time. This yields the following main theorem. • under admissibility, is credulously accepted in
iff is credulously accepted in ′, • reasoning in the corresponding AF is tractable
in the size of .
Now we turn our attention to the opposite direction: We present a general polynomial-time procedure which under mild conditions transforms a given ABA framework s.t. (i) the translated framework is equivalent under projection to and (ii) the core of the translated ABA framework is polynomially bounded. That is, this time we do not try to obtain an AF with tractable reasoning, but we wish to prevent the exponential blow-up which might be caused from the instantiation procedure.
We take the definition of circular tree-based arguments (proof trees) from Craven and Toni (2016).
Definition 25. A tree-based argument is circular if there is a path from a leaf to the root which contains two distinct vertices with the same label. An ABA framework is circular if there is a circular tree-based argument for this framework.
We remark that ABA frameworks obtained from Reduction 14 are non-circular and all atoms are derivable (independently of whether the underlying formula is satisifable).
Example 27. Consider an ABA framework (ℒ, ℛ, , ) with assumptions = {, }, rules ℛ: = 1 : ← ; 2 : ← ; 3 : ← ; and contraries = and = . In , both {} and {} are admissible as they symmetrically attack each other.
Following Definition 26, we obtain the corresponding ABA ′ = (ℒ′, ℛ′, ′, ′) with assumptions , , and additional assumptions , , , , , ; and rules ℛ′: 1′ : ← ; 2′ : ← ; 3′ : ← .
The assumption is defended by each assumption set that derives (since is attacked by which is in turn attacked by all assumption sets that derive ). Consequently, {, } is admissible since it derives and and thus defeats the attackers and . Likewise, {, } is admissible in ′ as it defends itself against the attack from and .
outcome to the initial set of assumptions yields the original extensions. This is not a coincidence, as we show next: admissible assumption sets and derivations are preserved when projecting to of the original ABA framework.
Proposition 28. Let = (ℒ, ℛ, , ) be a non-circular ABA framework such that each ∈ ℒ is in Th() and ′ the AF-sensitive ABA framework of . It holds that • if ∈ adm(), then there is an ′ ∈ adm(′) with = ′ ∩ and Thℛ() = Thℛ′ (′)∩ℒ, and Proposition 29. Let be the set of all non-circular ABA frameworks with all atoms derivable, and ′ the set of AF-sensitive ABA frameworks from . It holds that the cores of ′ are polynomially bounded.
Proof. Suppose that such an algorithm exists. Let = 1 ∧ · · · ∧ be a Boolean formula in CNF over clauses = {1, . . . , } and Boolean variables = {1, . . . , }. Let be the ABA framework obtained from Reduction 14, and let ′ = () be the outcome of the algorithm. Note that ′ can be constructed in time polynomial w.r.t. size of . By Reduction 14 and second Theorem 31. There is some polynomial such that each non-circular ABA framework = (ℒ, ℛ, , ) with ℒ ⊆ Th() can be transformed in polynomial time into an ABA framework ′ where Example 30. Let us consider again our ABA framework from Example 15. Applying the above construction, we obtain an ABA ′ with additional assumptions (1), item, it holds that is satisfiable iff there is an admissible (1), (2), (2); moreover, we replace rule ← assumption set with ∈ Thℛ′ (). 1, 2 with the rule ← (1), (2). The resulting AF Each admissible assumption-set in satisfies ⊆ is given in Figure 2. ∪ {′ | ∈ }, moreover, does not contain both and ′ for any ∈ Also note that each conflict-free
We can now gather our results to infer our desired theo- assumption-set is admissible since Reduction 14 yields a rem. Due to Proposition 29 the AF-sensitive ABA frame- symmetric ABA framework. work induces an AF with polynomial size and Proposi- By the first item, ′ has the same admissible assumption 28 ensures that applying this constructions preserves tion sets as ′. It holds that there is an argument (, ) in admissible reasoning under projection. Combining these ′ and does not contain both and ′ for any ∈ insights yields the following central result. iff is credulously accepted under admissible semantics in ′ iff is credulously accepted under admissible semantics in iff is satisfiable. Thus, if one finds an argument (, ) for ′ without “complementary literals” (i.e., without any ∈ s.t. both and ′ are in ) we • if ∈ adm(), then there is an ′ ∈ adm(′)
with = ′ ∩ and Thℛ() = Thℛ′ (′)∩ℒ, • if ′ ∈ adm(′), then ′ ∩ ∈ adm() and
Thℛ() ⊇ Thℛ′ (′) ∩ ℒ, and • the size of the AF corresponding to ′ is bounded
by (|′|). Then the dependency graph G is given as follows.
a path (cycle) is the number of edges labeled “− ”. The relation between paths in G and the core of is very close as formalized in the following lemma.
Lemma 35. Let be an ABA framework with core =
(A, R) and dependency graph G. If (, ) ∈ R, then
there is a path of length one from cl ( ) to cl ( ) in G.
We look at dependencies induced by the rules of a given
ABA framework, inspired by dependency graphs in logic
programming, and related but different to the dependency
graph notion existing for ABA [
Definition 33. The dependency graph G = (, , ) for a given ABA = (ℒ, ℛ, , ) is an edge-labelled graph with • = ℒ is the set of vertices, • edge = (, ) ∈ iff i) there is some rule ∈ ℛ with ∈ () and ℎ() = {}, in this case () = +; or ii) ∈ and = , in this case, () = − .
Example 34. Let = (ℒ, ℛ, , ) be an ABA framework with = {, , , , }, distinct contraries = ¯ for each ∈ and the following rules:
Proposition 36. Let be an ABA framework with core and dependency graph G. i) If G is acyclic, then so is . ii) If G is odd-cycle free, then so is .
Proposition 39. Let = (ℒ, ℛ, , ) be an ABA The observation can be extended to the following result. framework, = (A, R) be the core and G the dependency graph. For each ∈ ℒ let () = { ∈ | has a path in G to }. Then |A| ≤ || + ∑︀∈ℒ∖ 2|()|.
The above proposition does not hold for even cycles.
As a counter-example consider the even-cycle free dependency graph of Example 34. In contrast, the core possesses an even cycle. Vice versa, given a cycle in the dependency graph, we can construct a cycle of the same length in .
Proposition 37. Let = (ℒ, ℛ, , ) be an ABA framework such that each ∈ ℒ is in Th(), be the core and G the dependency graph. If 1, . . . , is a cycle in G, then there is a cycle of the same length in .
Proof. For 2 ≤ ≤ let be an assumption. By construction of G, − 1 = . Since is trim, there is an argument 1 with conclusion cl (1) = − 1. Now let be minimal s.t. < and is an assumption.
Again since is trim, there is also an argument 2 with cl (2) = − 1 = . Observe that 2 is attacked by arguments with conclusion − 1. Thus, we have an attack from 1 to , 2 in . In G, the length of the path − 1, . . . − 1 equals one since by choice of we have {− 1, . . . − 1}∩ = {}. If we continue analogously we find a cycle in having the same length as our cycle 1, . . . , .
The dependency graph can be utilized to obtain approximations for several bounds we considered throughout this paper.
Proposition 38. Let = (ℒ, ℛ, , ) be an ABA framework and G = (, , ) the dependency graph. i) For the rule size of we have ≤ max∈ |{′ ∈ | (′, ) ∈ }|. ii) If G is acyclic, then the derivationdepth of is bounded by the size of the longest path (counting “+” labels) in G.
the core than our previously established term 2|| · |ℒ ∖ | .
Acknowledgments