On Independence and SCC-Recursiveness in Assumption-Based Argumentation

1 Introduction

The ability to recognize and manage (in)dependence is crucial in symbolic reasoning at large [Darwiche and Pearl, 1994; Darwiche, 1997; Lang et al., 2002; Rienstra et al., 2020]. It plays an essential role in causal reasoning [Pearl, 2009], e. g., in probabilistic models, where (in)dependence between variables is built into graphical representations such as Bayesian networks [Geiger et al., 1990]. The ability to determine independence contributes to the explainability [Halpern and Pearl, 2001] and trustworthiness [Belle et al., 2024] of reasoning systems, while also improving efficiency by empowering breaking problems down so that they can be managed more effectively.

In this paper, we study conditional independence in computational argumentation, which captures how different parts of the argumentative information can be logically separated. Two prominent areas therein are abstract argumentation, coined by the seminal paper of Dung (1995), and structured argumentation, as overviewed by Besnard et al. (2014b). Unlike abstract argumentation, where arguments are considered abstract, structured argumentation frameworks focus on the structure of the arguments, enabling a finer-grained analysis of the arguments and relations. Assumption-based argumentation (ABA) [Bondarenko et al., 1997; ˇCyras et al., 2018] is a well-known form of structured argumentation, whose building blocks are assumptions (defeasible elements) and inference rules. We illustrate this with the following example.

Example 1.1. Alice, Bob, and Carol plan a tandem trip; we consider assumptions a (Alice cycles), b (Bob cycles), and c (Carol cycles) for each of our protagonists. Naturally, only two of them cycle at the same time, that is, not all our assumptions can be true at once. We capture the relations between our assumptions with inference rules; e. g., "if Bob and Carol cycle then Alice does not" is captured by the rule (a ← b, c), here, a is the contrary of a. Crucially, if the weather is bad (d) nobody can cycle. On the bright side, then there is no need to water the plants (w) outside. Also, Alice thinks about bringing her book (k), but if she cycles, it might be too heavy. 1

ABA has been broadly studied computationally [Toni, 2013; Cyras et al., 2021a; Craven and Toni, 2016; Lehtonen et al., 2024a; Lehtonen et al., 2024b]. ABA is also widely applicable, e.g., in healthcare [Cyras et al., 2021b], to provide explanations [Cyras et al., 2021a], for causal discovery [Russo et al., 2024], and planning [Fan, 2018]. In all these settings, a good understanding of independence between various components in ABA frameworks (ABAFs) is crucial. However, to date the study of independence within ABA remains underexplored. Actually, with the notable exception of the conditional independence analysis in abstract argumentation [Rienstra et al., 2020], the topic has been largely neglected in the computational argumentation literature so far.

Turning our attention to ABA, we address the following question: under what conditions are two (sets of) assumptions independent from each other, relative to a (potentially empty) set of assumptions that is considered prior knowledge? In other words, does the choice of truth values for one set of assumptions restrict the available choices for the truth values of another set, given the truth values for a third set are fixed?

Example 1.2 (Example 1.1 cont.). Let us find out if Alice and Bob influence each other's cycling activities. First, are a and b (unconditionally) independent of each other? The answer to that question is positive: knowing that Alice cycles does not give us any information about Bob, Alice could cycle with either Bob or Carol; similarly, if Alice does not cycle we do not know whether Bob cycles; either Bob and Carol cycle together or the weather could have ruined their trip. In contrast, a and b depend on each other, given c: knowing that Carol cycles implies that one of the other two cycles as well.

1 A formalization is given in Example 3.2.

Identifying conditional independence in ABA is computationally challenging, as we will show. To alleviate the high computational complexity we exploit the structure of ABA and explore SCC-recursiveness for ABAFs. Rienstra et al. (2020) demonstrate the advantages of SCC-recursiveness for efficiently checking conditional independence between arguments, based on the SCCs of an abstract argumentation framework (AF) [Dung, 1995]. Despite these considerable computational advantages, SCC-recursiveness has not received attention in the context of structured argumentation so far. In the scope of our independence studies for ABA, we tackle this issue and propose an SCC-recursive schema for ABA semantics alongside sound independence checks for assumptions in ABAFs.

Overall, we make the following contributions, for a wellstudied fragment of ABA whereby assumptions cannot be inferred (known as flat ABA) and where assumptions, their contraries and any sentences in inference rules are atomic.

• We introduce conditional independence in ABA and study its properties. We analyze its computational complexity and reveal the close relation of independence in ABAFs and AFs. We also settle the complexity of the corresponding decision problems for AFs. Section 4
• We introduce sound and poly-time methods for checking independence in ABA via two different routes:
• applying the approach by Rienstra et al. (2020) to a suitable AF instantiation for ABAFs; Section 5.1
• exploiting the structure of the ABAF directly, based on the SCCs of the so-called dependency graph [Rapberger et al., 2022]. Section 5.3
• To facilitate route (2), we introduce SCC-recursiveness for ABA and show that all semantics under consideration satisfy this property. Section 5.2

Due to space restrictions, we focus on complete-based semantics; analogous results for admissible semantics, alongside with proofs and further discussions are included in an extended version found online (DOI 10.5281/zenodo.15470789, https://zenodo.org/records/15470789).

2 RelatedWork

To address the challenges of computationally demanding dependency models, researchers [Verma and Pearl, 1988; Rienstra et al., 2020] have proposed sound (but potentially incomplete) Directed Acyclic Graph (DAG) representations to check independence. In the context of computational argumentation, Rienstra et al. (2020) identify a way to transform AFs into DAGs, based on their SCCs, to express (some) dependencies between arguments. Our study of the relation between SCCs in ABA and independence is inspired by this work. However, differently from their work, we focus on structured argumentation in the form of ABA.

Heyninck (2023) proposes a generic framework for studying independence in approximation fixpoint theory, applicable to any logic with fixpoint semantics, including logic programs under partial stable models and well-founded model semantics. Since the latter are instances of ABA in general, and of the restricted form of ABA we consider, the resulting framework in [Heyninck, 2023] is applicable to our setting, too. That being said, our focus lies on the relation to abstract argumentation, and the relation between independence and SCCs (which we newly introduce in this paper for ABA).

Some works use reasoning with independence information to perform causal discovery with ABA [Russo et al., 2024] or paradigms related to ABA, such as ASP [Zhalama et al., 2019]. This line of work is orthogonal to ours, as we focus on studying independence in ABA, rather than using ABA for ascertaining independence for causal discovery. Another work [Besnard et al., 2014a] defines an approach to reasoning about causes via argumentation, which, like in our case, is structured but built on classical logic and including ontologies. It does not consider independence in argumentation.

3 Background

A directed graph is a pair G = (V,E) where V is a set of vertices and E ⊆ V 2 . A (un)directed path p is a sequence v1 . . . vn, vi ∈ V , vi ̸= vj, i ̸= j, with (vi, vi+1) ∈ E (or (vi+1, vi) ∈ E); a cycle is a sequence vnv1 . . . vn where v1 . . . vn is a directed path. G is a directed acyclic graph (DAG) if it contains no directed cycles. For a vertex set U ⊆ V , PAG(U) = {w ∈ V | (w, u) ∈ E, u ∈ U} \ U are the parents of U, ANG(U) = {w ∈ V | ∃u ∈ U, p = (w, ..., u) directed path} \ U the ancestors of U. We say v ∈ V is a descendant of U, if U ∩ ANG({v}) ̸= ∅. We denote by DDG(v) the set of all descendants and by NDG(v) the set of all non-descendants and non-parents of U.

3.1 Assumption-based Argumentation

We recall assumption-based argumentation (ABA) [ ˇCyras et al., 2018]. We assume a deductive system (L,R), where L is a formal language, i. e., a set of sentences, and R is a set of inference rules over L. A rule r ∈ R has the form a0 ← a1, . . . , an with ai ∈ L. We write head(r) = a0 and body(r) = {a1, . . . , an} for the possibly empty body of r.

Definition 3.1. An ABA framework (ABAF) is a tuple (L,R,A, ) with a deductive system (L,R), a non-empty set A ⊆ L of assumptions, and contrary function : A→L.

Unless otherwise specified, we assume a unique contrary ac for each assumption a ∈ A. We write a to denote ac.

Example 3.2. We formalise the introductory Example 1.1 as ABAF D with assumptions {a, b, c, d, w, k}, their contraries, and inference rules, (v ← d), (d ← v) for v ∈ {a, b, c}, and

Below, we fix an arbitrary ABAF D = (L,R,A, ). A sentence p ∈ L is tree-derivable from assumptions A ⊆ A and rules R ⊆ R, denoted by A ⊢R p (tree-derivation), if there is a finite rooted labelled tree T such that the root is labelled with p, the set of labels for the leaves of T is equal to A or A ∪ {⊤}, and there is a surjective mapping from the set of internal nodes to R, satisfying that for each internal node v, there is r ∈ R, s.t. v is labelled with head(r), and the set of all successor nodes corresponds to body(r) or ⊤ if body(r) = ∅. We say p is derivable (in D) iff there is a tree-derivation A ⊢R p, A ⊆ A, R ⊆ R. We call A ⊢ p an (ABA) argument if there is R ⊆ R s.t. A ⊢R p. Arguments of the form {a} ⊢ a, a ∈ A are assumption arguments, arguments with R ̸= ∅ rule-based arguments. Each assumption argument is unique; we identify assumption arguments with their assumptions.

By ThD(A) = {p | ∃A ⊢ p} we denote the set of all claims derivable from assumptions A in D. We let A = {a | a ∈ A}. The set A attacks B ⊆ A if there is A′ ⊆ A, b ∈ B s.t. A′ ⊢ b. A is conflict-free if it does not attack itself; A is admissible if it is conflict-free and defends itself.

A semantics σ is a function assigning ABAF a set of σlabellings. We recall complete, grounded, preferred, and stable semantics (abbr. co, gr, pr, st) [Schulz and Toni, 2017].

Definition 3.3. A labelling is a (partial) function λ : A → L, L = {in, out, und}. For A ⊆ A, we let λA : A → L denote a partial labelling of A; λ|A denotes the restriction of λ to A. For lab ∈ L, lab(λ) = {x ∈ A | λ(x) = lab}.

Definition 3.4. λ : A → L is a complete labelling (abbr. colabelling) of an ABAFD = (L,A,R, ) iff for each a ∈ A,

• λ(a)=in iff for all B⊢a, there is b∈B s.t. λ(b)=out;
• λ(a)=out iff there is B⊢a s.t. λ(b)=in for all b∈B.

A co-labelling λ is grounded iff und(λ) is ⊆-maximal among all co-labellings of F; preferred iff in(λ) is ⊆-maximal among all co-labellings of F; and stable iff und(λ) = ∅.

For semantics σ, the set Λσ denotes the set of all σlabellings of ABAF D. For A ⊆ A, we say λA is σcompatible with D if there is λ ∈ Λσ(D) s.t. λ|A = λA.

Assumption 3.5. We focus on ABAFs which are flat, i. e., for each rule r ∈ R, head(r) /∈ A (no assumption can be derived, and finite, i. e., L, R, A are finite; moreover, each sentence in s ∈ L is atomic and derivable, i. e., there is A ⊆ A s.t. A ⊢ s, and each rule is stated explicitly (given as input).

ABAFs and Abstract Argumentation An argumentation framework (AF) [Dung, 1995] is a directed graph F = (A, R) where A ⊆ U are arguments and R ⊆ A2 are attacks. We fix a non-finite set U of arguments. For x, y ∈ A, if (x, y) ∈ R we say x attacks y; E ⊆ A defends x if it attacks each attacker of x; E is conflict-free if it does not attack itself; and admissible if it is conflict-free and defends all x ∈ E.

We recall labelling-based complete, grounded, preferred, and stable semantics (abbr. co, gr, pr, st) for AFs, following [Caminada and Pigozzi, 2011]. Analogous to ABAFs, a labelling is a function λ : A → L (cf. Definition 3.3).

Definition 3.6. A labelling λ : A → L is a complete labelling (abbr. co-labelling) of an AF F = (A, R) iff for each x ∈ A,

• λ(x) = in iff λ(y) = out for every attacker y of x;
• λ(x) = out iff λ(y) = in for some attacker y of x.

A co-labelling λ is grounded iff und(λ) is ⊆-maximal among all co-labellings of F; preferred iff in(λ) is ⊆-maximal among all co-labellings of F; and stable iff und(λ) = ∅.

We use Λσ, analogous to ABAFs (cf. below Definition 3.4). ABAFs are closely related to AFs [ ˇCyras et al., 2018].

Definition 3.7. The associated AF FD = (A, R) of an ABAF D=(L,R,A, ) is given by A = {A ⊢ p | ∃R ⊆ R : A ⊢R p} and attack relation (A ⊢ p, A′ ⊢ p′ ) ∈ R iff p ∈ A′ .

The translation preserves the semantics [Schulz and Toni, 2017], the correspondence is 1:1 for all considered semantics.

Proposition 3.8. Let D be an ABAF with AF FD, σ ∈ {gr, co, pr , st}. If λ ∈ Λσ(D) then ({A ⊢ p | A ∈ in(λ)}, {A ⊢ p | ∃a ∈ A : a ∈ out(λ)}, {A ⊢ p | ∃a ∈ A : a ∈ und(λ),A ∩ out(λ) = ∅}) ∈ Λσ(F); if λ ∈ Λσ(F) then (in(λ|A), out(λ|A), und(λ|A)) ∈ Λσ(D).

Each AF induces an ABAF by associating assumptions and arguments [Toni, 2012]. The translation preserves semantics.

Definition 3.9. For an AF F = (A, R), we define the ABAF DF =(L,A,R, ) s.t. A = A, and a ← b ∈ R iff (b, a)∈R.

Proposition 3.10. Let F be an AF, DF its associated ABAF, and σ ∈ {co, pr , gr , st}. Then, Λσ(F ) = Λσ(DF ).

3.2 Conditional Independence

A dependency model I over a set of variables V is a ternary relation over disjoint subsets of V . We write X⊥IY | Z iff (X, Y,Z) ∈ I and say X and Y are independent, given Z [Pearl and Paz, 1986]. We drop I if clear from context.

We recall semi-graphoid axioms [Pearl, 2009]:

Symmetry A⊥B | C ⇒ B⊥A | C

Decomposition A⊥B ∪B′ | C ⇒ A⊥B | C

Weak Union A⊥B ∪B′ | C ⇒ A⊥B | C ∪B′

Contraction A⊥B | C ∧ A⊥B′ | C∪B ⇒ A⊥B∪B′ | C

For a DAG, the notion of d-separation introduces a dependency model which is a semi-graphoid; also, checking d-separation is in P [Darwiche, 2009]. A node v = vi in path v1 . . . vn is a collider iff (vi-1, vi), (vi+1, vi)∈E.

Definition 3.11. Let G=(V,E) be aDAGandA,B,C ⊆ V . Then, A and B are d-separated, given C (A⊥dB | C) in G, iff for all undirected paths p between A and B, it holds that p contains a collider v s.t. ({v} ∪ DDG(v)) ∩ C = ∅ or C ∩ {v ∈ p | v is not a collider} ̸= ∅.

Rienstra et al. [2020] introduce independence for AFs.

Definition 3.12. For an AF F = A, R, semantics σ and disjoint sets A, B, C ⊆ A we say A is σ-independent of B, given C in F, written A⊥σB | C, iff, for all λ1, λ2 ∈ Λσ(F), if λ1|C = λ2|C then there is some λ3 ∈ Λσ(F) s.t. λ3|A = λ1|A, λ3|B = λ2|B and λ3|C = λ1|C = λ2|C.

4 Independence in ABA

We investigate a semantical notion of conditional independence between assumptions. Similar to [Rienstra et al., 2020; Darwiche, 1997], we base our notion on the acceptance status of assumptions. Intuitively, two sets of assumptions A and B are independent of each other, given a third set C, if coming to know the acceptance status of A in addition to knowing the acceptance status of C does not influence the acceptance status of B.

Definition 4.1. Let D = (L,R,A, ) be an ABAF, σ be a semantics, and let A,B,C ⊆ A be disjoint sets of assumptions. Then A is σ-independent of B, given C in D, written A⊥σB | C, iff, for all labellings λ1, λ2 ∈ Λσ(D), if λ1|C = λ2|C then there is some labelling λ3 ∈ Λσ(D) s.t. λ3|A = λ1|A, λ3|B = λ2|B and λ3|C = λ1|C = λ2|C.

We drop σ and write A⊥B | C, if clear from context. By Iσ we denote the corresponding dependency model.

Example 4.2. The ABAF D from Example 3.2 has five colabellings; four of them are preferred and stable:

We can infer several (in)dependencies here.

• The assumptions a and b are σ-independent wrt. ∅ for σ ∈ {pr, st}. For this, we identify the labels which are individually assigned to a and b under σ and verify that each combination of them is realized under σ.
• a and b are not co-independent, though: assigning a the label in and b the label und is individually possible, but there is no labelling with λ(a) = in and λ(b) = und.
• When conditioning on {d}, the assumptions a and b are dependent under pr and st semantics. If λ(d) = out, then a and b can be individually out, but not together.

Our first central result sheds light on the close connection between assumption independence and independence between arguments (cf. [Rienstra et al., 2020]). We show that two sets of assumptions A, B are independent, given C, iff their corresponding assumption arguments are. Below, we identify assumption argument {a} ⊢ a with assumption a.

Proposition 4.3. Let D = (L,R,A, ) be an ABAF, FD its corresponding AF, and let σ ∈ {co, gr, pr, st}. Then, for all A, B, C ⊆ A, we have A⊥σB |C in D iff A⊥σB |C in FD.

Example 4.4. Consider the ABAF from Example 4.2. We obtain an AF FD (cf. Fig. 1) with assumption arguments xv : {v} ⊢ v, v ∈ {a, b, c, d, w, k} and rule-based arguments

We have (x, y) ∈ R iff x = A ⊢ p, y = B ⊢ q, and for some b ∈ B : b = p.

By Proposition 4.3 we can use the AF labellings to check for independence between assumptions; e.g., since xk and xa are pr-dependent in FD, k and a are pr-dependent in D.

As a consequence, we can transfer results from the AF literature [Rienstra et al., 2020] to our setting. We so obtain that our independence notion for ABA is a semi-graphoid.

Proposition 4.5. σ-independence in ABA is a semi-graphoid.

Since each AF induces an ABAF [Toni, 2012] we can transfer ABA independence results to AFs as well.

Proposition 4.6. Let F = (A, R) be an AF, DF its associated ABAF, and σ ∈ {co, gr, pr, st}. Then, for all A,B,C ⊆A, we have A⊥σB |C in F iff A⊥σB |C in DF .

In what follows, we assume an arbitrary but fixed ABAF D = (L,R,A, ). First, note that under gr semantics, all sets are independent since the gr-labelling is unique. Next, we show that two assumption sets are independent when conditioned on a set that uniquely defines one of them.

Definition 4.7. Assumption set A ⊆ A σ-defines B ⊆ A iff for all partial σ-compatible labellings λA of A, there is a unique labelling λB which is σ-compatible with D.

Proposition 4.8. Let A, B, C ⊆ A be disjoint sets of assumptions. If C σ-defines B then A⊥σB | C.

As a corollary, we obtain that conditional independence is downwards closed wrt. set inclusion.

Corollary 4.9. A⊥σB | C implies A′⊥σB′ | C for any semantics σ and for all A′ ⊆ A, B′ ⊆ B.

In contrast to d-separation in DAGs (cf. Def. 3.11), it is, however, not possible check independence between sets of assumptions by looking at the pairwise independence of their members. In Example 3.2, for instance, the singletons a, b, c are pairwise st -independent while {a, b} and {c} are not.

We conclude by showing that deciding independence can be computationally hard. In addition, we identify the complexity of the corresponding decision problem for AFs.

Proposition 4.10. Let C denote the class of AFs/flat ABAFs. Deciding σ-independence in C is ΠP2 -complete for σ ∈ {co, st} and ΠP3 -complete for σ = pr .

5 SCC-driven Independence Checks

The goal of this section is to establish sound and computationally efficient criteria for checking independence for ABAFs. First, we make use of the close connection between AFs and ABAFs and apply the d-graph method for AFs by [Rienstra et al., 2020] to ABAFs (Section 5.1). It turns out, however, that the applicability of the approach is limited due to the specific structure of the instantiated AF. For the second approach, we first define and investigate SCC-recursiveness for ABA based on the dependency graph [Rapberger et al., 2022] in Section 5.2. Next, in Section 5.3, we show that the SCC-Markov condition [Rienstra et al., 2020] is satisfied by universal and SCC-recursive ABA semantics, thereby providing the prerequisites for an independence check in ABAFs.

In each of these sections, SCCs will play an important part.

Definition 5.1. Let G = (V,E) be a directed graph, N ⊆ V . N is a strongly connected component (SCC) of G iff for all u, v ∈ N there is a path from u to v and N is ⊆-maximal with this property. SCC(G) denotes the set of all SCCs in G.

The SCCs of G induce a DAG CG = (SCC (G), {(S, T ) | S ⊆ PAG(T)}. We call an SCC an initial SCC if it has no parents and a terminal SCC if it has no children in CG.

5.1 AF-Based d-Graph Approach for ABA

Rienstra et al. [2020] develop a sound method to check independence in polynomial time: they transform a given AF into a DAG where each node corresponds to an argument or an SCC and, for a given SCC node, outgoing arcs encode membership and incoming arcs its parents in the AF. We restate their definition of the d-graph below.

Definition 5.2. Given a directed graph Q = (V,E), the dgraph GQ = (Vd,Ed) is a DAG with Vd = V ∪ {s | S ∈ SCC(F)}; and (u, v) ∈ Ed iff (i) v ∈ V , u ∈ SCC(F) and v ∈ u or (ii) u ∈ V , v ∈ SCC(F) and u ∈ PAG(v).

This seems promising at first sight: by Proposition 4.3, we can instantiate an ABAF and use the d-graph approach on the AF to check for independence in ABAFs. Below, we identify assumptions with their corresponding nodes in the d-graph.

Theorem 5.3. Let D = (L,R,A, ) be an ABAF, FD the corresponding AF, GFD the d-graph resulting from FD, and let σ ∈ {pr, co}. Then, for disjoint sets A,B,C ⊆ A of assumptions, A⊥dB | C in GFD implies A⊥σB | C in D.

Example 5.4. Let D = (L,L,R, ) with A = {a, b, c, d}, contraries a = b, d = c, c = d, and rule (b ← a, d). The resulting AF FD is given in Fig. 2 (top, with x = {a, d} ⊢ b). It contains three SCCs, S1 = {a}, S2 = {b, x}, S3 = {c, d}. From the d-graph approach, we obtain a DAG (cf. Fig. 2, bottom). We can use the DAG to identify independencies between assumptions, e.g., since b cuts the path between a and c, we infer {a}⊥σ{c} | {d}, σ ∈ {pr, co}, in the ABAF.

To avoid the exponential blow-up of the AF instantiation, we can utilize the poly-sized, polynomial-time computable, and (under projection) semantics-preserving AF-sensitive instantiation ([Lehtonen et al., 2023], cf. Def. D.5 )

Proposition 5.5. Checking independence in ABA using the d-graph approach on its AF-sensitive instantiation is in P.

Note that we require an SCC-structure which is informative enough. The SCCs that contain assumption arguments are however often either terminal or initial SCCs (cf. Proposition D.2). In an ABAF with separated contraries, i. e., if A∩A = ∅, conditioning on a set C cannot make assumption sets independent if they are not independent already.

Proposition 5.6. Let D=(L,A,R, ) be an ABAF, A∩A = ∅, FD its corresponding AF, and GFD the resulting d-graph, Then, for all disjoint sets A,B,C ⊆ A, if A ̸ ⊥ID B | C in GFD thenA ̸ ⊥dB|C ′ inGFD for all assumption sets C ′ ⊇C.

Indeed, in case of our initial example not much can be said.

Example 5.7. In the associated AF FD of the ABAF D from Example 4.2, all assumptions are terminal SCCs. The resulting d-graph GFD is a DAG where all nodes that correspond to assumptions are connected with collider-free paths. So we cannot use assumptions to d-separate each other.

In the next two subsections, we propose a native SCCbased method for ABAFs that circumvents the AF instantiation by exploiting the attack structure of the ABAF directly.

5.2 SCC-Recursiveness for ABA

We explore the notion of SCC-recursiveness in ABA. In our context, we first need to clarify what the SCCs of an ABAF are. For this, we make use of the dependency graph [Rapberger et al., 2022].

Definition 5.8. The dependency graph PD = (V,E, l) for an ABAF D = (L,R,A, ) is an edge-labelled graph with V = L; and edge e = (s, t) ∈ E iff (i) there is some rule r ∈ R with s ∈ body(r) and head(r) = {t}, in this case l(e) = +; or (ii) t ∈ A and t = s, in this case, l(e) = -.

Example 5.9. Let D = (L,R,A, ) be an ABAF with A = {t1, t2, t3, s1, s2, s3, s4}, and the following rules:

Then the dependency graph PD is given in Fig. 3.

Definition 5.10. Let D = (L,R,A, ) be an ABAF with dependency graph PD. The SCCs of D are given by

For S, T ∈ SCC(D), T is a parent of S iff there is a directed path T1 . . . Tn of SCCs from T to S in CPD s.t. T1 = T, Tn = S and Ti = ∅ for i /∈ {1, n}.

Let us delve into the concepts needed to understand SCCrecursiveness in ABA. SCC-recursive semantics can be computed locally, starting from the initial SCCs. In what follows, we will go through such a recursion step by step, using Example 5.9, and introduce all required concepts along the way.

Example 5.11 (Ex. 5.9, cont.). Our ABAF D from before has two SCCs: S = {s1, s2, s3, s4} and T = {t1, t2, t3}.

In the first step, we compute all σ-labellings for the single initial SCC T . If a given SCC has no parents, the computation amounts to evoking a so-called base function that returns all its σ-labellings. Let σ = co. We obtain two labellings λ1 and λ2 with λ1(ti) = und, i ≤ 3, and λ2(t1) = in, λ2(t2) = out, λ2(t3) = und. We continue with labelling λ=λ2.

When computing the labellings for a non-initial SCC, the first step is to partition its elements based on the incoming arcs of the parent SCCs. In contrast to AFs, we can have attacks where the attacking assumption set consists both of assumptions from the parent and the current SCC, similar as in SCC-recursiveness for SETAFs [Nielsen and Parsons, 2006], cf. [K¨onig et al., 2022; Dvor´ak et al., 2024]. Before coming up with a suitable partition of the assumptions in a given SCC, we will first partition the rules accordingly.

Definition 5.12. Let D = (L,R,A, ) be an ABAF, A ⊆ A an assumption set and λ : A → L a labelling. A rule r∈R is

deactivated, r ∈ Rd(λ) iff λ(ai) = out

for some assumption ai ∈ body(r) ∩ A

semi-active, r ∈ Rs(λ) iff λ(ai) = und

for some assumption ai ∈ body(r) ∩ A and r /∈ Rd(λ)

active, r∈Ra(λ) iff r is neither deactivated nor semi-active.

We omit λ and write Rs, Ra if it does not cause confusion.

Example 5.13 (Ex. 5.9, cont.). We move on to compute S, based on the information we got from T . Labelling λ deactivates rules with (the out-labelled) t2 in the body (first row); it renders non-deactivated rules using t3 semi-active (second row); the rest is active (last row).

We are ready to define the partition of S into defeated, provisionally defeated, and undefeated assumptions.

Definition 5.14. Let D = (L,R,A, ) be an ABAF, S ∈ SCC(D), λ : PAD(S) → L a labelling, and Ra,Rs sets of active and semi-active rules. An assumption a ∈ S is

defeated, a ∈ def D(S, λ,Ra,Rs) iff in(λ) ⊢Ra a

provisionally defeated, a ∈ prdef D(S, λ,Ra,Rs) iff a is not defeated and A \ (S ∪ out(λ)) ⊢Ra∪Rs a

undefeated, a ∈ undef D(S, λ,Ra,Rs) iff a is neither defeated nor provisionally defeated

These sets can be considered a pre-selection for a labelling on S. We define a provisional labelling λp on S ∪ PAD(S).

Definition 5.15. Let D = (L,R,A, ) be an ABAF, S ∈ SCC(D), λ : PAD(S) → L a labelling, and Ra,Rs sets of (semi-)active rules. We define the partial provisional labelling λp(S, λ, Ra, Rs) : S ∪ PAD(S) → L by

Example 5.16 (Ex. 5.9, cont.). In D, the assumption s2 is defeated, s4 is provisionally defeated, and {s1, s3} are undefeated. We use this partition of S to extend λ: the so-obtained provisional labelling λp is given by out(λp) = {s2, t2}, und(λp) = {s4, t3}, and in(λp) = {t1, s1, s3}.

The restriction D↓λp S , which we compute using λp to carry out the recursion on the given SCC S, contains only the provisionally defeated and undefeated assumptions of S; to compute our new rule set, we first update Ra and Rs to get rid of rules that use defeated assumptions from S.

Definition 5.17. Let D = (L,R,A, ) be an ABAF and λp(S, λ,Ra,Rs) a provisional labelling for an SCC S ∈ SCC(D), and (semi-)active rule sets Rup a ,Rup s . We define

where Rup s = ((Ra(λp) \Rup a )∪Rs(λp))∩(Ra ∪Rs) and Rup a = Ra(λp) ∩Ra are the updated sets of semi-active and active rules, respectively; and

• the restricted rule sets to S, λp are Rs↓λp S =R′ \Ra↓λp S and Ra↓λp S ={head(r) ← body(r) \ (A\S) | r∈Rup a }.

Example 5.18 (Ex. 5.9, cont.). RestrictionD↓λp S has assumptions s1, s3, s4. To compute R′ , we first update our rule sets:

Now, R′ contains the updated (semi-)active rules where all for the restriction irrelevant assumptions, i. e., assumptions not contained in {s1, s3, s4}, are removed from the bodies:

Without further knowledge about which of the rules are semi-active, we could wrongly conclude s3 can be accepted because s4 is attacked by a fact (i. e., by ∅). However, the rule (s4 ←) is semi-active, thus it cannot be counted as a successful attack against s4. We remember the restricted rule sets Rs↓λp S and Ra↓λp S for the next recursion step.

D↓λp S has three SCCs: S1 = {s1}, S2 = {s3}, S3 = {s4}. Again, we start with the initial SCCs. Taking Rs into account, we obtain label und for s3 and s4, in for s1, out for s2. Together with λ, we thus get a co-labelling for D.

We are ready to state our definition for SCC-recursiveness. We use a function GF(D,E,Ra,Rs), that takes as parameters an ABAF D, a set of candidate assumptions E, sets of (semi-)active rules Rs, Ra to compute a set of labellings on D. A semantics σ is SCC-recursive if GF can be computed locally on each SCC with a σ-specific base function BF .

Definition 5.19. A semantics σ satisfies SCC-recursiveness if there exists a local function BFσ(D,E,Ra,Rs) such that for every ABAF D = (L,R,A, ) we have λ ∈ Λσ(D) iff λ ∈ GFσ(D, A, R, ∅) where λ ∈ GFσ(D, E, Ra, Rs) iff

• if |SCC(D)| = 1, λ ∈ BFσ(D,E,Ra,Rs)
• otherwise, for each S ∈ SCC(D), λ|S = λ′ for some λ′ ∈ GFσ(D↓λp S , in(λp),Ra ↓λp S ,Rs ↓λp S ) on D↓λp S , and λ(s) = out for s ∈ S \ D↓λp S , for the partial provisional labelling λp(S, λ|PAD(S),Ra,Rs).

We give our main result of this subsection. The σ-specific base functions are given at the end of Appendix E.

Theorem 5.20. Each ABA semantics σ ∈ {co, pr, st, gr} satisfies SCC-recursiveness.

5.3 Direct d-Graph Approach for ABA

We propose a sound method to determine conditional independence that does not rely on the AF instantiation. The idea is to apply the d-graph approach to the SCCs of the dependency graph of an ABAF instead of the associated AF.

Definition 5.21. The d-graph of an ABAF D = (L,R,A, ) is GD=GPD the d-graph wrt. its dependency graph PD.

Example 5.22. Consider an ABAF D with assumptions a, b, c and rules (a ← a), (b ← a), (c ← b). Each assumption has its own SCC in PD, thus, GD is a chain (cf. Fig. 4).

For the check, we now first compute the dependency graph PD of the ABAF D, then build the d-graph GD based on the SCCs of PD, and, finally, use the d-separation criterion in GD to check independence between sets of assumptions. To show soundness of the approach, we recall the crucial SCC-Markov property [Rienstra et al., 2020].

Definition 5.23. A dependency model I satisfies the SCCMarkov condition wrt. graph G iff, for all S ∈ SCC(G), S⊥INDG(S) | PAG(S).

We call σ an SCC-Markovian semantics if Iσ satisfies the SCC-Markov condition wrt. PD. To guarantee this, we require σ to be SCC-recursive, universal (Λσ(D) ̸= ∅ for all D), and admissible (in(λ) is admissible for all λ∈Λσ(D)). We provide a counterpart of [Rienstra et al., 2020, Thm. 2].

Theorem 5.24. If σ is SCC-recursive, admissible, and universal, then Iσ satisfies the SCC-Markov condition.

Since co, gr , and pr are admissible, universal, and, by Theorem 5.20, also SCC-recursive, we conclude the following.

We show that the native ABA d-graph approach is sound: we can indeed use the d-separation criterion in d-graph GD to check independence for SCC-Markovian ABA semantics.

Theorem 5.26. Let D = (L,R,A, ) be an ABAF and σ be SCC-Markovian. Then, for disjoint sets A,B,C ⊆ A of assumptions, A⊥dB | C in GD implies A⊥σB | C in D.

The approach is in P since constructing PD is linear in the size of D. Thus, we can check for σ-independence between assumptions in polynomial time for all except st semantics.

As it turns out, the native d-graph approach for ABAFs reveals different independencies than the AF-approach.

Example 5.27. All assumptions of the d-graph GFD of AF FD for ABAF D from Example 5.22 are in terminal SCCs (cf. Fig. 5). In GFD , we cannot say if a and c are independent, given b, since they are connected by a collider-free path not containing b. In contrast, b separates a and c in GD (cf. Fig. 4). So, from GD we can conclude a⊥σc | b for all semantics σ which satisfy the conditions in Theorem 5.24.

As for AFs, all elements in the same SCC are dependent. As a result, we can only determine independence between assumptions from different SCCs. Thus, just like the AFapproach, the native ABA-approach is incomplete, i.e., not all independencies can be identified. That being said, the ABA d-graph approach still gives us information the AF-approach cannot procure, specifically for ABAFs with separated contraries. Finally, let us head back to our introductory example.

Example 5.28. In the d-graph GD for the ABAFD from Example 3.2, assumption d separates every undirected path from w to, e.g., a. Therefore a⊥σw | d in D for σ ∈ {co, pr , gr}.

6 Summary and Conclusion

We have conducted a comprehensive study of a semantical notion for conditional independence between assumptions in flat ABA, including satisfaction of semi-graphoid axioms, results on computational complexity and two methods for a sound check of independence in polynomial time, the latter based on our novel notion of SCC-recursiveness for ABA. The proposed independence model is based on three-valued labellings, a choice which was motivated by promising results for a similar notion in the setting of abstract argumentation [Rienstra et al., 2020]. Other concepts of independence between assumptions are feasible, though. In particular, defining independence wrt. joint acceptability of assumptions instead proved to be a well-behaved notion in a preliminary analysis which is beyond the scope of this paper. Diametric to this future work direction, ABA frameworks offer rich structural aspects, and investigating independence between literals, rules and independence in dynamic settings, also for nonflat ABA, are natural next steps. Specifically, our approach could empower enforcement methods as well as repairing and forgetting research [Rapberger and Ulbricht, 2023; Rapberger and Ulbricht, 2024; Berthold et al., 2023] by enabling the decomposition of global reasoning tasks into local reasoning tasks in smaller instances. The high computational complexity of deciding independence may prove challenging for these studies. Overcoming the limitations of the proposed checks when handling ABAFs with large SCCs we consider an interesting albeit possibly challenging research objective. Lastly, the adaptation of our results to other closely related structured argumentation formalisms such as ASPIC+ [Modgil and Prakken, 2013] or defeasible logic programming [Garc´ıa and Simari, 2004] would be worth investigating.

Ethical Statement

There are no ethical issues.

Acknowledgments

The research reported here was partially supported by the Deutsche Forschungsgemeinschaft (grant 550735820), by ERC under the EU's Horizon 2020 research and innovation programme (grant agreement no. 101020934, ADIX), and by J.P. Morgan and the Royal Academy of Engineering under the Research Chairs and Senior Research Fellowships scheme (grant agreement no. RCSRF2021\11\45).