Assumption-Based Argumentation (ABA) is a well-established rule-based formalism for modelling and reasoning in non-monotonic settings, with a wide range of applications. However, the high computational complexity of core reasoning tasks in ABA poses a significant challenge for its applicability in practice. This issue is further exacerbated when ABA frameworks (ABAFs) are instantiated into graph-based argumentation formalisms, such as Dung's Argumentation Frameworks (AFs) and Argumentation Frameworks with Collective Attacks (SETAFs). In the context of non-monotonic reasoning, a key strategy to address computational intractability is to optimise reasoning over a given knowledge base through divide-and-conquer algorithms. A paradigmatic example of this approach is splitting, where extensions of a given framework are computed incrementally, i.e. restricting the search space to sub-frameworks only, and then combining the obtained results. This approach has been successfully applied to SETAFs in the literature. Furthermore, a parametrised version has been introduced for AFs under stable semantics. However, the exponential growth produced by the instantiation process might undermine the usefulness of splitting on the argument graphs induced by ABAFs. For this reason, there is a need for splitting-based algorithms tailored for ABA. To address this issue, our work investigates the concept of splitting for ABAFs under common semantics. Furthermore, we generalise splitting to its parametrised version both for SETAFs and ABAFs.
Computational models of argumentation in AI [
Although ABA is a well-established formalism to perform non-monotonic reasoning, with applications
in medical decision-making, explainable AI and, more recently, causal discovery [
In the context of non-monotonic reasoning, one prominent strategy to address computational
intractability is to optimise reasoning over a given knowledge base through divide-and-conquer algorithms.
A paradigmatic example of this approach is splitting, originally developed for answer-set programming
[
© 2025 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
can invalidate the usefulness of splitting. This motivates the need for splitting techniques that operate
directly on ABAFs. To this end, this paper makes the following contributions:
• We begin by reviewing existing notions of splitting for AFs (Section 2) and SETAFs (Section 3).
• We then introduce a novel notion of ABA splitting in Section 4, along with the syntactic
adjustments required to establish a splitting theorem, which we prove under standard argumentation
semantics.
• In Section 5, we extend our results to the more general framework of parameterised splitting [
Assumption-Based Argumentation We recall here the basic concepts of assumption-based
argumentation (ABA) [
For a set of assumptions, ⊆ we use to indicate the set of contraries of . Conversely, we define the partial function : ℒ ↦→ assigning an assumption to its contrary ∈ such that () = if = . This generalises to sets of contraries as before. For a set of rules , we fix ℎ() = {ℎ() | ∈ }, () = {() | ∈ }. Further we use () = { ∈ ℒ | ∈ , () ∈ or ∈ }. In what follows, we read () as ({}). For a rule ∈ ℛ, we say that is: a fact if () = ∅; a loop-rule is = ℎ() and ∈ (). A sentence ∈ ℒ is tree-derivable from ⊆ and rules ⊆ ℛ , denoted by ⊢ , if there is a finite rooted labelled tree where: the root of is labelled with ; the set of labels for the leaves of is equal to or ∪ {⊤}; and for every inner node of there is a rule ∈ such that is labelled with ℎ(), and every successor of is labelled with ∈ () or ⊤ if () = ∅. We sometimes write ⊢ instead of ⊢ if it does not cause confusion. Moreover, we call ℎ() = { ∈ ℒ | ⊢ } the theory of w.r.t. the ABAF . Throughout the paper, we assume that ABAFs do not contain dummy rules, whose body is not derivable from any set of assumptions.
Definition 2. Let = (ℒ, ℛ, , ) be an ABAF. A set ⊆ attacks ⊆ if ′ ⊢ for some ′ ⊆ and ∈ . A set is conflict-free in an ABAF ( ∈ cf()) if it does not attack itself; defends if it attacks each attacker of ; is admissible ( ∈ adm()) if it is conflict-free and defends itself.
We say a set of assumptions attacks an assumption if attacks the singleton {}. In this paper, we assume ABAFs to be flat, unless specified otherwise. We call an ABAF flat if every set of assumptions is closed (i.e. ⊢ implies ∈ ) and non-flat otherwise. We next recall definitions for grounded, complete, preferred, and stable ABA semantics (abbr. grd, com, pref, stb).
Definition 3. Let be an ABAF and let ∈ adm(). ∈ com() if contains every assumption
set it defends; ∈ grd() if is ⊆ -minimal in com(); ∈ pref() if is ⊆ -maximal in com();
∈ stb() if attacks each {} ⊆ ∖ . We call () the set of -extensions of the ABAF .
SETAF Instantiation König et al. [
Definition 4. A SETAF is a pair = (, ) where is a finite set of arguments, and ⊆ 2 × is the attack relation. For an attack (, ℎ) ∈ we call the tail and ℎ the head of the attack. We write (, ℎ) to denote the set-attack ({}, ℎ). For ⊆ , we say attacks an argument ∈ if there is an attack (, ) ∈ with ⊆ . Moreover, for a set ⊆ we say that attacks if attacks some ∈ . We use + = { | attacks } and define the range of w.r.t. as ⊕ = ∪ + .
Every ABAF = (ℒ, ℛ, , ) can be instantiated as the SETAF = (, ) by setting
= and (, ) ∈ if ⊢ [
Example 1. Consider an ABAF = (ℒ, ℛ, , ) with assumptions = {, , , }, ℒ = ∪ ∪ {} and rules ℛ = { ← , ; ← ; ← ; ← }. The induced SETAF is = ({, , , }, {({, }, ), (, ), (, )}).
Notice that such mapping is many-to-one. Indeed, we lose when instantiating the first two rules
into ({, }, ). For this reason, SETAFs can be seen – syntactically – as a fragment of flat ABAFs.
Splitting We now recall Baumann’s splitting approach for AFs [
The reduct is designed to take care of arguments attacked by the extension . Further, to account for the propagation of undecided arguments w.r.t. , a further modification is needed: self-attacks are propagated from 1 to arguments in 2.
Definition 6. Let (1, 2, 3) be a splitting for an AF and an extension of 1. Moreover, take 2′ = (′2, 2′) as the (, 3)-reduct of 2 and as the set of undecided arguments w.r.t. . The ( , 3)-modification of 2 is defined as ,3 (2′) = (′2, 2′ ∪ {(, ) | ∃ ∈ : (, ) ∈ 3}).
Using these definitions, Baumann [
Theorem 1 ([
1. If 1 ∈ (1) and 2 ∈ (,3 (2′)), then 1 ∪ 2 ∈ ( ). 2. If ∈ ( ), then ∩ 1 ∈ (1) and ∩ 2 ∈ (,3 (2′)).
Later, this idea has been generalised by relaxing the strict separation requirement, which significantly
narrows the applicability of splitting, introducing so-called parametrised splitting [
Definition 7. Let = (, ) be a SETAF, 1 = (1, 1) and 2 = (2, 2) two sub-frameworks of such that 1∩2 = ∅, = 1∪2 and = 1∪2∪3 with 3 ⊆ ︀( (21 ∖{∅})∪22 )︀ × 2. We call a splitting of the triple (1, 2, 3). Moreover, we call 3 the set of links wrt (1, 2, 3) and say that a link is undecided if no argument in its tail is defeated, but at least one is undecided.
As for AFs, the general idea is to compute extensions of as a combination of extensions of 1
and 2. Due to the links from 1 to 2 we have to modify 2 according to the extension(s) of
1 to account for the prior accepted and rejected arguments. Following Baumann [
{( ∩ ′2, ℎ) | (, ℎ) ∈ 3, ∩ ′2 ̸= ∅, ℎ ∈ ′2, ∩ 1 ⊆ 1, ∩ (1)+3 = ∅}.
When dealing with undecidedness, what guides our intuition towards a certain modification is not the status of the arguments in 1, but rather the status of the links. Hence, we decide to slightly tweak the original definition and base our notion solely on the undecided links.
Definition 9 (Undecided Links). Given a splitting (1, 2, 3) for a SETAF and an extension 1 ∈ 1 we define the set of undecided links w.r.t. 1 as: 31 = {(, ℎ) ∈ 3 | ∩ (1)1∪3 = ∅ and ∃ ∈ : ∈ 1 ∖ (1)⊕1 }.
+
In what follows, we define the modification , which is applied on the reduct, and accounts for the efects of the undecided links. In particular, we add to 2 one self-attacking argument which also partially attacks the target for each undecided attack in 3.
Definition 10 (Modification) . Let (1, 2, 3) be a splitting for a SETAF and 1 an extension of 1. Take 2′ as the (1, 3)-reduct of 2 and 31 as the set of undecided links w.r.t. 1. We denote with 13 (2′) the 31 -modification (or simply modification) of 2′ s.t.:
13 (2′) = (′2, 2′ ∪ {(( ∩ ′2) ∪ {ℎ}, ℎ) | (, ℎ) ∈ 31 , ℎ ∈ ′2}).
Before we present the splitting theorem we illustrate Definitions 8–10 in the following example. Example 2. In (a) we have a SETAF with a splitting that separates the arguments 1 = {, , , } from 2 = {, , , , }. We see that 1 = {} is admissible in the left part of the splitting. In (b) we see the reduct w.r.t. the set {}, where and are defeated by (as {}+1 = {, }) and is undecided. This reduct contains from the right part all arguments except , which is defeated by (as {}+3 = {}). We see that most attacks are removed from the right part, but (, ) persists (since it is in 2 and all involved arguments remain), and the attack ({, }, ) is changed to (, ). The attack ({, }, ) is removed since is defeated. The attack ({, }, ) is also removed, as is undecided (i.e., {, } ∩ 1 ⊈ 1). However, in (c) we see that the latter case is important for the modification: the attack ({, }, ) is an undecided link, which means in the modification we introduce the attack ({, }, ). Now, since {, } is admissible, we obtain {, , } as an admissible set for .
(a) SETAF (b) ({}, 3)-reduct (c) {3}-modification
Having these notions at hand, we now establish the adequacy of the splitting technique for SETAFs.
We start by establishing that (a) conflict-freeness of the sub-frameworks 1 and 2 carries over to
the whole SETAF , and (b) conflict-free sets of induce conflict-free subsets in 1 and 2′.
Proposition 1 (Buraglio et al. [
1. If 1 ∈ cf(1) and 2 ∈ cf(2⋆), then 1 ∪ 2 ∈ cf( ). 2. If ∈ cf( ), then ∩ 1 ∈ cf(1) and ∩ 2 ∈ cf(2′).
Finally, we are ready to characterize the splitting algorithm by generalising the splitting theorem for SETAFs under the standard Dung semantics.
Theorem 2 (Buraglio et al. [
1. If 1 ∈ (1) and 2 ∈ (︀ 13 (2′))︀ , then 1 ∪ 2 ∈ ( ). 2. If ∈ ( ), then ∩ 1 ∈ (1) and ∩ 2 ∈ (︀ ∩1 (2′))︀ . 3
While the existing instantiation procedure from ABA frameworks to SETAFs provides a
foundation for defining splitting, attempting to directly replicate the SETAF-style idea of splitting among
assumptions fails to yield a natural notion of splitting. This disconnect stems from a fundamental
structural diference: in SETAFs, attacks are primitive, whereas in ABA, they are derived from the
underlying deductive system (ℒ, ℛ). As a result, naively mimicking SETAF-style splitting in ABA
would require (i) arbitrarily partitioning the assumption set into 1 and 2, and (ii) computing attacks
as derivations from assumptions in 1 to those in 2. However, splitting should be possible solely by
inspecting the knowledge base at hand. Moreover, while instantiating ABAFs into SETAFs has been
shown useful in specific contexts [
In this section we present splitting results for ABAFs. The rule-set of an ABAF is split into a bottom and a top part whenever no assumption occurs in the bottom part whose contrary is derived by some rule in the top. This ensures that the assumptions in the bottom can be evaluated independently of what can be deduced by inspecting the top part. We capture this intuition via the notion of splitting set: Definition 11. Given an ABAF = (ℒ, ℛ, , ), a set ⊆ ℒ is a splitting set (or simply a splitting) of if = () and for all ∈ ℛ, ℎ() ∈ implies () ⊆ .
A splitting set partitions the deductive system into two sub-systems (ℒ1,ℛ1) and (ℒ2,ℛ2), called the ‘bottom’ and ‘top’. In particular, we have (i) ℒ1 = and ℛ1 = { ∈ ℛ | ℎ() ∈ } and (ii) ℒ2 = ℒ ∖ and ℛ2 = { ∈ ℛ | ℎ() ∈/ }. These induce respectively two sub-frameworks 1 = (ℒ1, ℛ1, 1, 1) and 2 = (ℒ2, ℛ2, 2, 2) with = ℒ ∩ and the contrary function defined over .
Example 3. Consider the ABAF = (ℒ, ℛ, , ) corresponding to the SETAF of Example 2, where = {, , , , , , , , }, ℒ = ∪ ∪ {, }, and the rule-set ℛ consists of the following:
Take the set = {, , , , , , , , }. It can be easily checked that is a splitting set of , through which we obtain two sub-systems (ℒ1, ℛ1) and (ℒ2,ℛ2) with ℛ1 (bottom) and ℛ2 (top) are exactly the second line and the first line of rules in ℛ. Moreover, ℒ1 = and ℒ2 = ℒ ∖ .
Notice that some atoms contained in ℒ1 (but not in ℒ2) may occur in the body of some rule in ℛ2 ( and in Example 3). This intermediate mismatch will be resolved later by the notion of reduct. Moreover, their occurrence in the top rules does not afect the acceptance status of such atoms. In fact, a first sanity check, we observe that our notion of splitting prevents building attacks from assumptions of 2 towards assumptions of 1 using top-rules in ℛ2. This is ensured by the fact that contraries of assumptions occurring in the bottom part are not derived via rules in the top part (via construction of ℛ2). As a result, assumptions in 1 are attacked only via rules in ℛ1 by assumptions in 1. Thus, no attack generated from 2 (by means of rules in ℛ2) is directed towards 1.
Proposition 2. Let be an ABAF and a set of literals that splits into 1 and 2. For every derivation ⊢ with ∈ 1, it holds that ⊆ ℛ 1 and ⊆ 1.
The attacks of the bottom part can be extended in a conservative way: whatever happens in the second sub-framework does not afect the acceptability status of assumptions in 1. Thus, to compute incrementally an extension of an ABAF , we can first select an extension of 1 and later modify 2 according to the information contained in . Consequently, we can evaluate the modified framework 2 and augment its extensions with . Again, we follow the approach of Baumann and appeal to the notions of reduct and modification to realise the modification of 2 in a two-step process. First, we propagate all the information we get from a -extension of 1 to ensure that rules which are in contrast with are removed. The outcome is called the -reduct of 2.
Definition 12. Let = (ℒ, ℛ, , ) be an ABAF, a set that splits into two sub-frameworks 1 and 2 and a -extension of 1. We call 2 = (ℒ2, ℛ2 , 2, 2) the -reduct (or simply reduct) of 2, where ℛ2 is obtained by deleting: • each rule ∈ ℛ2 with () ∩ ̸⊆ Th1 (); • all literals in Th1 () from the remaining rules.
As we anticipated, all and only the atoms occurring in the rule-set of the reduct are contained in ℒ2. Therefore, the reduct can be evaluated in complete isolation from 1. In the second step, we modify the reduct to propagate the information about assumptions (or their contraries) which are not contained in Th1 (). We call these assumptions undecided, as they are not in nor their contrary is derivable from it (i.e. are not attacked by ). Then, the set of undecided assumptions of 1 w.r.t. is UA1 () = { ∈ 1 | ∈/ and ∈/ Th1 ()}. Since their status can be transmitted to other assumptions via rules, we need to introduce the concept of undecided theory of 1, capturing all statements derivable from a set of undecided (and not defeated) assumptions.
Definition 13. Let = (ℒ, ℛ, , ) be an ABAF and ∈ (). The undecided theory of w.r.t. is
UT() = { ∈ ℒ | ∃ ⊆ s.t. ⊢ , ∩ UA() ̸= ∅, ∩ ℎ() = ∅}.
Rules in 2 whose body contain elements of UT1 () might carry over undecidedness from 1. However, this scenario could be overwritten by the presence of incompatible sentences w.r.t , captured by IS1 () = ℎ1 (ℛ+1 ) ∪ , where ℛ+1 = { ∈ 1 | ⊢ , ⊆ ℛ 1}. Hence, a set of sentences from 1 will carry undecidedness to sentences in 2 if and only if (i) none of its elements is incompatible and (ii) at least one of its elements is in the undecided theory w.r.t. the previously selected extension. This concept mirrors the notion of undecided links for SETAFs.
We are now in the position to formally define the modification of 2 . First, we expand the set of sentences with a fresh assumption and corresponding contrary. Further, we introduce (i) a loop-rule for and (ii) a modified version of every rule with some undecided (but no incompatible) sentence in the body. In particular, we expand their body with , after projecting to ℒ2.
Definition 14. Let be an ABAF, a set that splits into two sub-frameworks 1 and 2 and an extension of 1. Let 2′ be the -reduct of 2. We use 1 (2′) = 2⋆ = (ℒ⋆2, ℛ2, 2, ⋆) to denote ⋆ ⋆ the -modification (or simply modification) of 2′ such that 2⋆ = 2′ if UA1 () = ∅, and otherwise: ℒ⋆2 = ℒ2 ∪ {, }; ℛ⋆2 = ℛ′2 ∪ { ← } ∪ {ℎ() ←
(() ∩ ℒ2) ∪ {} | ∈ ℛ2, () ∩ IS1 () = ∅, () ∩ UT1 () ̸= ∅}.
Example 4. Consider again the ABAF = (ℒ, ℛ, , ) from Example 3 and splitting set = {, , , , , , , , }. We know that {} ∈ pref(1). Therefore, the {}-reduct of 2 is 2{} = (ℒ2, ℛ{2}, 2, 2), where the rule-set ℛ2
{} is: Moreover, the set of undecided assumptions is UA1 ({}) = {} and UT1 ({}) = {, , }. We then {} such that: compute the modification by expanding the set of sentences with {, } and ℛ2 It is easy to see that {, } ∈ pref(1 (2′)), and retrieve {, , }, as for Example 2.
We can now prove that our procedure preserves conflict-free sets under incremental computation as well as projection to sub-frameworks, similarly to Section 3.
Proposition 3. Let be a splitting set for an ABAF into 1 and 2.
1. if 1 ∈ cf(1) and 2 ∈ cf(11 (21 )), then 1 ∪ 2 ∈ cf().
2. if ∈ cf(), then 1 = ∩ 1 ∈ cf(1) and 2 = ∩ 2 ∈ cf(21 ).
Proof. For notational convenience, let = 1 ∪ 2 and let 2′ = (ℒ2, ℛ′2, 2, 2) be the reduct of 2 w.r.t. 1 = ∩ 1. (1.) To prove the statement we need to show that there is no ∈ 1 ∪ 2 and and ∈ ℛ such that 1 ∪ 2 ⊢ . Towards contradiction, assume there is indeed such an . Thus either (i) ∈ 1 or (ii) ∈ 2. Assume (i) is true, that is ∃ ∈ 1 such that 1 ∪ 2 ⊢ and ∈ ℛ. From Proposition 2, we know that 2 = ∅ and ⊆ ℛ 1. Thus, 1 ⊢ , in contradiction with 1 ∈ cf(1). Assume now that (ii) is true, i.e. ∃ ∈ 2 and ∈ ℛ such that 1 ∪ 2 ⊢ . Hence, there is a tree-derivation from 1 ∪ 2 ∪ {⊤} rooted in and a non-empty set of rules 2 = ∩ ℛ2. For each rule ∈ 2, there are three possible outcomes when computing 11 (21 ) = 2⋆: (a) does not get removed when computing the reduct; (b) gets removed and later added in the modification; (c) gets removed for good. Assume (a) is the case. If a rule is not removed when computing the reduct, it is modified into a rule ′ ∈ ℛ′2 such that (′) = () ∖ ℎ1 (1) and ℎ(′) = ℎ(). Thus, (′) consists of elements of 2 or atoms derivable from it. Therefore, 2 ⊢ℛ21 and consequently 2 ⊢ℛ2⋆ (more rules). Finally, we get ∈/ cf(2⋆), contradicting our hypothesis. Assume now (b) is the case. By definition of derivation, this means that 2 derives in 2⋆ only if ∈ 2. However, this contradicts conflict-freeness of 2 in the modification. Finally, consider case (c). Since gets removed, but not added in the modification, we infer that () ∩ IS1 (1) ̸= ∅. Hence, either + ) ∩ () ̸= ∅. However, since 1 ∈ cf(1), this means that either 1 ∩ () ̸= ∅ or ℎ1 ((1)ℛ1 is a dummy rule or that ∃ ∈ () ∩ 1 ̸⊆ 1. Thus, in both cases 1 ∪ 2 ̸⊢ , contradicting our assumption.
(2.) Suppose now that ∈ cf(). From this we derive that ∩ 1 ∈ cf(1) (subset of a conflictfree set). We now show that ∩ 2 ∈ cf(2′). Towards contradiction, assume ∩ 2 ∈/ cf(2′). There is an ∈ ∩ 2 such that ∩ 2 ⊢ℛ′2 . By definition of reduct, we know that each ′ ∈ ℛ′2 is obtained from a corresponding rule ∈ ℛ2 such that () ⊆ (′) ∪ ℎ1 ( ∩ 1). Therefore, ( ∩ 1) ∪ ( ∩ 2) ⊢ℛ1∪ℛ2 . By definition of splitting, we know that ℛ = ℛ1 ∪ ℛ2 and = ( ∩ 1) ∪ ( ∩ 2), deriving ⊢ℛ , and finally ∈/ cf(). Contradiction.
We prove our algorithm is adequate with respect to most common semantics. Due to space constraints we present proof details only for stable and admissible semantics, which are prototypical for the others. Theorem 3. Let be a splitting set for an ABAF into 1 and 2 and = {stb, adm, com, pref, grd}. 1. if 1 ∈ (1) and 2 ∈ (11 (21 )), then 1 ∪ 2 ∈ (). 2. if ∈ (), then 1 = ∩ 1 ∈ (1) and 2 = ∩ 2 ∈ (11 (21 )). ⋆ Proof. (stable). First notice that from 1 ∈ stb(1), we get 1 (1) = ∅, and consequently ′2 = 2.
(1.) From Proposition 3 together with the hypotheses that 1 ∈ stb(1) and 2 ∈ stb(2⋆), we know that 1 ∪ 2 ∈ cf(). Thus, for any ∈ ∖ , we show that ∈ + , i.e. ⊢ for some ⊆ ℛ . We proceed by cases. Let ∈ 1. From hypothesis we know that 1 ⊢1 for some 1 ⊆ ℛ 1 which immediately implies ∈ +1 . Let ∈ 2. From hypothesis, we know that 2 ⊢2 for some 2 ⊆ ℛ ′2. Thus, for each rule ′ ∈ ℛ′2 there is a rule ∈ ℛ2 such that () ⊆ () ∪ ℎ1 (1). Hence, it follows directly that 1 ∪ 2 = ⊢ for some ⊆ ℛ 1 ∪ ℛ2 = ℛ.
(2.) Assume ∈ stb(). From this we know that ∪ ℛ+ = ℛ⊕ = = 1 ∪ 2. We first prove that 1 = ∩ 1 ∈ stb(1). From Proposition 3 we know ∩ 1 ∈ cf(1). Moreover, from Proposition 2, we know that any set of assumptions which is not entirely contained in 1 attacks ∈ 1 via rules in ℛ1, therefore we get ∩ 1 ⊢1 for all ∈ 1 ∖ for some 1 ⊆ ℛ 1. Hence, 1 ∈ stb(1). We know turn to prove 2 = ∩ 2 ∈ stb(2′). We know conflict-freeness holds from Proposition 3. Hence, we only need to show that for every ∈ ′2 ∖ 2, 2 ⊢2′ for some 2′ ⊆ ℛ ′2. Since ⊢ in , we have two possibilities: (a) 1 = ∅ or (b) 1 ̸= ∅. If (a) holds, we get ⊆ ℛ 2 and = 2 ⊢ where 2 ⊆ ′2 and ∈ ′2. Thus, 2 ⊢ holds for some ⊆ ℛ ′2. If (b) holds, 1 ∪ 2 ⊢ in . Therefore, each rule ∈ ∩ ℛ2 has a corresponding rule ′ ∈ ℛ′2 such that (′) = () ∖ ℎ1 (1). Since 1 ∪ 2 ∈ cf() by hypothesis, we know that ℎ1 (1) ∩ 2 = ∅. Hence, ( ∖ 1) ⊢2′ where 2′ ⊆ ℛ ′2. In both cases we have + 2 ∪ (2)ℛ′2 = ′2, concluding 2 ∈ stb(2′).
(admissible). (1.) Since admissibility implies confict-freeness from Proposition 3, we know that = 1 ∪ 2 ∈ cf(). Thus we only need to show that defends itself in , i.e. for all ∈ , if ⊢ , then ′ ⊢ for some ∈ and ′ ⊆ . If ∈ 1, we know that is defended by 1 in 1 from hypothesis. Thus, from Proposition 2, we can deduce that 1 ∈ adm(). Consider now an assumption ∈ 2 and some ⊆ such that ⊢ and ⊆ ℛ . If ∩ ℎ1 (1) ̸= ∅, then 1 defends against in . If ∩ ℎ1 (1) = ∅, this means that ⊆ 2 and ⊢ in 2′ ( is attacked in the reduct) or ∪ ⊢ in 2⋆ ( is attacked in the modification). In both cases, since 2 is conflict-free and defends in 2⋆, there is a ′ ⊆ 2 such that ′ ⊢ with ∈ . We distinguish two cases: either (i) ′ ⊢ already in 2, in which case is defended by in , or (ii) there is some ′′ ⊃ ′ such that ′′ ⊢ in and ′′ ∩ 1 ⊆ 1. Thus, since ⊆ 1 ∪ 2, is defended by 1 ∪ 2 in . In any case is defended in by , i.e. ∈ adm().
(2.) By Proposition 3, we get 1 ∈ cf(1) and 2 ∈ cf(2′). First, we know that 1 ∈ adm(1) because defends itself in and 1 is not attacked by a subset of 2 (Proposition 2). It remains to prove that 2 ∈ adm(2⋆). Take an assumption ∈ 2 such that ⊢ in 2⋆. Each such derivation corresponds to exactly one derivation ′ ⊢ with ⊆ ℛ . There are two cases: either (i) ′ = ⊆ 2 and ⊆ ℛ 2 or (ii) ′ ⊃ ∖ {} where ′ ∖ ⊆ 1 (assumptions deleted from simplified rules in the reduct). From both (i) and (ii) we deduce that ′ ∩ ℎ1 (1) = ∅: for (i) because it would entail ̸⊆ 2; for (ii) because otherwise ̸⊢ in 2⋆. Nonetheless, since defends in , in case (i) there is a counter-attack ′′ ⊢ℛ2 such that ′′ ⊆ and ∈ ( ∖ {}). In case (ii), the same holds but ∈ ( ′ ∖ {, }). If ′′ ∩ 1 = ∅, we know that {} ⊆ ′2 and together with the fact that ′′ ⊆ , we derive ′′ ⊆ ∩ ′2 = 2. Hence, ′′ defends from in 2⋆. If ′′ ∩ 1 ̸= ∅, then ′′ ∩ 1 ⊆ 1. Therefore, from ′′ ⊆ we get ′′ ∩ ′2 ⊢ℛ′2 , which defends against in 2⋆. Thus is always defended in 2⋆, as desired.
We now introduce a more general version of splitting for ABAFs and SETAFs, called parametrised
splitting [
We first introduce a parametrised version of splitting for ABA. In contrast with the previous notion, we allow some contraries of assumptions occurring in bodies of ℛ1 to appear as the heads of rules in ℛ2. The concept of a splitting set is then generalised accordingly in the following way: Definition 15. For any ABAF = (ℒ, ℛ, , ), a set ⊆ ℒ is a called quasi-splitting of if = () and for all ∈ ℛ, ℎ() ∈ implies () ∖ ⊆ . Let ← = { ∈ ∖ | ∃, ′ ∈ ℛ : ∈ () ∩ , ℎ() ∈ , ℎ(′) = , ̸= ′}. We call : • -splitting of , if |← | = ; • (proper) splitting of , if |← | = 0.
As before, the rule-set is split into a bottom and top part, depending on the rule-head respectively being or not in . As a result, ← is the set of assumptions in the bottom whose contrary is derived in the top. We call ← the set of vulnerabilities with respect to , since it contains assumptions that are attacked by . Whenever |← | ̸= 0, there are some heads in ℛ2 whose corresponding assumption may appear in bodies of ℛ1. Therefore, the notion of splitting of Definition 11 corresponds to a 0-splitting.
To account for elements of ← , the ABAFs 1 and 2 induced by the chosen splitting set are constructed in a slightly diferent way than before. In particular, we fix 1 and 2 as before, but let ℒ1 = ∪ ← ∪ ← . Moreover, since contraries in ← may be derived by top rules, the status of their corresponding assumptions in the bottom depends on rules in the top. Consequently 1 cannot be evaluated in complete isolation from the rest, in contrast with proper splitting.
For computing extension of the sub-framework 1, we first need to modify the ABAF. First, we modify the rules by removing body-atoms not in ℒ1. Indeed, these atoms occur in ℒ2 and are unattacked in , therefore they can be disregarded when evaluating 1. Further, we proceed by adding: (i) a fresh assumption ′ (and its contrary ′) for each ∈ ← ; (ii) rules which encode the choice for or against the presence of each assumption ∈ ← in the extension. In this way, we store at the object level the meta-information regarding our choices on each ∈ ← .
Definition 16. Let = (ℒ, ℛ, , ) be an ABAF, ⊆ ℒ be a quasi-splitting of inducing the sub-frameworks 1 and 2. Moreover, let ← be the set of vulnerabilities of 1 with respect to and (ℛ1)↓ℒ1 = {ℎ() ← () ∩ ℒ1 | ∈ ℛ1}. We construct ⌞1⌟ = (⌞ℒ1⌟, ⌞ℛ1⌟, ⌞1⌟, ) as the ABAF obtained from 1 by letting: • ⌞ℒ1⌟ = ℒ1 ∪ {′, ′ | ∈ ← }; • ⌞ℛ1⌟ = (ℛ1)↓ℒ1 ∪ { ← ′, ′ ← | ∈ ← }.
Intuitively, the additional rules allow us to choose whether we want to accept an extension of ⌞1⌟ containing or one that does not. After this choice, we can safely compute the -reduct of 2, as for proper splitting. In this way, we propagate the meta-information to which we committed by means of our choice. A further modification of 2 is now needed to make sure that our hypothesis regarding is ensured: we add a fact-rule ← or a loop-rule ← , depending on whether the previously chosen extension contains or ′. These represent a form of (positive and negative) constraints in ABA. Definition 17. Let = (ℒ, ℛ, , ) be an ABAF, a quasi-splitting of into 1 and 2. Moreover, let ← be the set of vulnerabilities with respect to and 2 the -reduct of 2 for some ∈ (⌞1⌟). We denote with ⌜2⌝ = (ℒ2, ⌜ℛ2⌝, 2, 2) the ABAF obtained augmenting ℛ2 with: { ←|
∈ ∩ ← } ∪ { ← | ′ ∈ }.
Notice that such modification might make the ABAF ⌜2⌝ non-flat, as (∅) = { | ∈ ∩ ← }. For stable semantics, however, this does not result in a higher complexity for the same reasoning tasks. Example 5. Consider the ABAF = (ℒ, ℛ, , ) where = {, , , }, ℒ = ∪ ∪ {}, and rule-set ℛ as follows: ← ← ← , ← First notice that = {, } and ′ = {, , } are stable extensions in . Now let = {, , , , } be a quasi-splitting of and ← = {} the set of vulnerabilities w.rt. . We get ⌞ℒ1⌟ = ∪{}∪{}∪{′, ′} and ⌞ℛ1⌟ such that: ← ← , ← ′ ← ← ′
We derive two stable extensions 1 = {} and 1′ = {′, , }. Now consider 2 with ℒ2 = ℒ ∖ = {, , , }. For the former we get ⌜21 ⌝ with ⌜ℛ21 ⌝ = ∅ ∪ { ←} from which we derive 2 = {, } as a stable extension. For the latter we get ⌜21′ ⌝ with ⌜ℛ21 ⌝ = { ←} ∪ { ← } from which we derive 2′ = {} as a stable extension. We then obtain = (1 ∩ ) ∪ 2 and ′ = (1′ ∩ ) ∪ 2′. Theorem 4. For an ABAF = (ℒ, ℛ, , ) and a quasi-splitting ⊆ ℒ of : 1. if 1 ∈ stb(⌞1⌟) and 2 ∈ stb(⌜21 ⌝), then (1 ∩ ) ∪ 2 ∈ stb(). 2. if ∈ stb(), then there is a set ⊆ { ′ | ∈ ← } such that 1 = ( ∩ ) ∪ ∈ stb(⌞1⌟) and 2 = ∩ 2 ∈ stb(⌜21 ⌝).
Proof. In what follows, for notational convenience, let = 1 ∪ 2 and let 2′ = (ℒ2, ℛ′2, 2, 2) be the reduct of 2 w.r.t. 1 = ( ∩ ) ∪ .
(1.) To prove the statement we need to show (1 ∩ ) ∪ 2 ∈ cf() and ((1 ∩ ) ∪ 2)⊕ℛ = . We start with conflict-freeness. Since 1 ∈ cf(⌞1⌟), then 1 ∩ ∈ cf(⌞1⌟) (less assumptions) and 1 ∩ ∈ cf(1) (less attacks). Since ℒ1 = ℒ ∩ , ℛ1 = { ∈ ℛ | ℎ() ∈ }, we can derive 1 ∩ ∈ cf(). Consider now 2 ∈ stb(⌜2′⌝). Since being stable implies conflictfreeness we immediately get 2 ∈ cf(⌜2′⌝). Again, since ℛ′2 ⊆ ⌜ℛ′2⌝, we obtain 2 ∈ cf(2′). Furthermore, Proposition 3 for proper splittings, together with 1 ∩ ∈ cf(1) and 2 ∈ cf(2′), entail (1 ∩ ) ∪ 2 ̸⊢ for any ∈ 2 and ⊆ ℛ . It only remains to consider possible attacks from 2 to 1 ∩ in . Suppose that there are ⊆ 2 and ∈ 1 ∩ such that ⊢ for some ⊆ ℛ . First, notice that since ⊆ 2, we get () ∩ = ∅ ⊆ ℎ1 (1), and thus ⊆ ℛ ′2. Moreover, ∈ ← so that ⌜ℛ′2⌝ = ℛ′2 ∪ { ←} . Therefore, ⊢ and ⊢ for some ⊆ ⌜ℛ′2⌝, i.e. 2 is either not conflict-free or not closed in ⌜2′⌝.
We now show that ((1 ∩ ) ∪ 2)⊕ℛ = . Towards contradiction, consider an assumption ∈/ ((1 ∩ ) ∪ 2)⊕ℛ. Assume ∈ . By hypothesis, 1 ∈ stb(⌞1⌟), i.e. either ∈ 1 or 1 ⊢ for some ⊆ ⌞ℛ1⌟. From our assumption, we get ∈/ (1 ∩ )⊕ℛ, that is (i) ∈/ 1 ∩ and (ii) 1 ∩ ̸⊢ for any ⊆ ℛ . If (i) holds, we immediately derive 1 ⊢ for some ⊆ ⌞ℛ1⌟. Consider now our assumption (ii). Because ∈ we know that every rule of is contained in ℛ1. For the same reason such rules are in ⌞ℛ1⌟ ( ∈/ ← ). Therefore, 1 ∩ ̸⊢ for any ⊆ ⌞ℛ1⌟ in contradiction with our hypothesis. Assume now ∈ ∖ . By hypothesis we know either ∈ 2 or 2 ⊢ for so m⊆ℛe . ⊆As⌜bℛef′2o⌝r.eF,rforommt h(ie) aasnsduomuprtihoynp, owtheegseist we∈/d(eri2v)e⊕ℛ,t2ha⊢tis(im)us∈/t ho2ldanfodr (sioi)me2̸⊢ ⊆ ⌜fℛor′2⌝a.nIyf ∈ ← , there are two possibilities: ∈ 1 ∖ or ∈/ 1 ∖ . In the first scenario, ⌜ℛ′2⌝ = ℛ′2 ∪ { ←} . Again, 2 ⊢ and 2 ⊢ for some ⊆ ⌜ℛ′2⌝, in contradiction with the fact that 2 is a stable extension of ⌜2′⌝. If ∈/ 1 ∖ , then ′ ∈ 1, which means ⌜ℛ′2⌝ = ℛ′2 ∪ { ← }. Since ∈/ 2, the loop-rule ← is not in , therefore ⊆ ℛ ′2. Thus, for each rule ′ ∈ ℛ′2 there is a rule ∈ ℛ2 such that () ⊆ () ∪ ℎ1 (1). Hence, it follows directly that (1 ∩ ) ∪ 2 ⊢ for some ⊆ ℛ 1 ∪ ℛ2 = ℛ. If ∈/ ← , then ∈/ 1. If 2 ⊢ for some ⊆ ⌜ℛ′2⌝, it is not because { ← } ⊆ ⌜ℛ′2⌝. Thus ⊆ ℛ ′2. As before, for each rule ′ ∈ ℛ′2 there is exactly one rule ∈ ℛ2 such that () ⊆ (′) ∪ ℎ1 (1 ∩ ). As a result, in the entire rule-set ℛ we obtain (1 ∩ ) ∪ 2 ⊢ is a derivation in . This contradicts our assumption.
(2.) First we get ∈ cf() and thus ∩ ∈ cf(1) (less attacks). Now let = 1 ∖ ( ∩ )⊕ℛ. Since ∈ stb(), it attacks every other assumption. Hence, we can infer that assumptions in are contained in 1 and attacked by ∩2 in , that is ⊆ ℛ+ ∖( ∩)⊕ℛ = ( ∩2)+ℛ. Therefore there is a rule ∈ ℛ2 with ℎ() = for each ∈ , meaning that = ← . Now let = {′ | ∈ }. Thus ⌜ℛ′2⌝ contains a pair of rule { ← ′, ′ ← } for each ∈ . Consequently, conflict-freeness of ( ∩ ) ∪ is ensured since ∈/ ∩ for all ∈ . Moreover, attacks every ∈ in ⌞1⌟, making ( ∩ ) ∪ stable.
It now remains to show 2 = ∩2 ∈ stb(⌜2′⌝). As before, we know that ∩2 ∈ cf(2) since is conflict-free in (less assumptions), and ∩ 2 ∈ cf(2′) because ℎ2′ ( ∩ 2) ⊆ ℎ2 ( ∩ 2) (less rules and attacks). Consider now the modified framework ⌜2′⌝ wrt ( ∩ ) ∪ . By construction, ∩ 2 ∈/ cf(⌜2′⌝) only if ∈ ∩ ( ∩ 2). Recall that ⊆ ( ∩ 2)+ℛ. Thus, ∩ 2 ∈/ cf(). By contradiction, we derive that ∩ 2 is conflict free in ⌜2′⌝. We now show that 2 ⊢ for all ∈ 2 ∖ 2 and some ⊆ ⌜ℛ′2⌝. Towards contradiction, we assume there is an ∈ 2 ∖ 2 such that 2 ̸⊢ , i.e. ∈/ ℎ⌜2′⌝(2). Therefore, since ∈/ 2, we get ∈/ ℎ2′ (2). Hence, before the reduct is applied, it holds that ( ∩ ) ∪ 2 ̸⊢ with ⊆ ℛ 2. Since no rule ∈ ℛ1 is such that ℎ() = , we derive ( ∩ ) ∪ 2 ̸⊢ in , in contradiction with out hypothesis. Finally, we ensure that (2) = 2 in ⌜2′⌝. Assume the contrary holds. Since 2′ is flat, that means { ←} ⊆ ⌜ℛ′2⌝ and ∈/ 2. These facts respectively entail ∈ 1 and 2 ⊢ (from previous paragraph). This contradicts the conflict-freeness of . Thus, 2 is conflict-free, closed and attacks every other assumption.
In this section we investigate a notion of parametrised splitting for SETAFs, which generalises the one
for AFs [
Definition 18. Let = (, ) be a SETAF, 1 = (1, 1) and 2 = (2, 2) two subframeworks of such that 1 ∩ 2 = ∅ and = 1 ∪ 2. We call a quasi-splitting of the tuple (1, 2, 3← , 3→) with 3→ ⊆ ︀( (21 ∖ {∅}) ∪ 22 )︀ × 2, 3← ⊆ ︀( (22 ∖ {∅}) ∪ 21 )︀ × 1 and = 1 ∪ 2 ∪ 3. Moreover, we say that 3← and 3→ are the set of incoming and outgoing links w.r.t. the splitting. The splitting (1, 2, 3← , 3→) is called: • the -splitting of , if |3← | = ; • (proper) splitting of , if |3← | = 0.
While the idea of quasi-splitting is carried out in a conceptually similar manner than for ABAFs, the concrete modifications that we require are fairly diferent. In particular, we start by augmenting 1 with fresh arguments that encode meta-information regarding incoming links. For each of these, we introduce symmetric attacks to force a choice between the target of the incoming link and the new one. Definition 19. Let = (, ) be a SETAF, (1, 2, 3← , 3→) be a quasi-splitting of inducing the sub-frameworks 1 and 2. We construct ⌞1⌟ = (⌞1⌟, ⌞1⌟) as the SETAF obtained from 1 by letting: • ⌞1⌟ = 1 ∪ {′ | ∈ +3← }; • ⌞1⌟ = 1 ∪ {({}, ′), ({′} ∪ ( ∩ 1), ) | (, ) ∈ 3← }.
We call a conditional extension of 1 if it is a stable extension of ⌞1⌟.
As for proper splitting, 1 is used to compute the reduct of 2. Further, in this setting the the meta-information in 1 plays a role. In particular, if ∈/ 1 and is not attacked by 1 ∩ 1, then it must be attacked externally.
Definition 20. Let be a SETAF and (1, 2, 3← , 3→) be a quasi-splitting of . Moreover, let 1 be a conditional extension of 1. We call 11 = { ∈ 1 ∖ 1 | ∈/ (1 ∩ 1)} + the set of externally attacked arguments in 1 w.r.t. 1.
Next, we introduce a modification of 21 that takes into account information regarding incoming links. First, we add set-self-attacks to make coflicting those sets of arguments attacking 1 via 3← . Further, for each of these externally attacked arguments, we introduce a self-attacking argument attacked by the remaining part of an incoming link.
Definition 21. Let be a SETAF and (1, 2, 3← , 3→) be a quasi-splitting of . Moreover, let 1 be a conditional extension of 1 and 11 = { ∈ 1 ∖ 1 | ∈/ (1 ∩ 1)+}. We denote with ⌜21 ⌝ = (⌜21 ⌝, ⌜21 ⌝) the SETAF where: ⌜21 ⌝ =21 ∪ { | ∈ 11 }; ⌜21 ⌝ =21 ∪ {( , ) | ∈ ⊆ 21 , ( , 1) ∈ 3← } ∪
{, ), ( , ) | ∈ 11 , ⊆ 21 , ∃ ′ ⊇ s.t. ( ′, ) ∈ 3← }.
Example 6. Consider the SETAF = (, ) where = {, , , } and = {(, ), ({, }, ), (, )} and its quasi-splitting as depicted below (a). We have two possible stable extensions = {, } and ′ = {, , }. After modification, the first sub-framework ⌞1⌟ (b) has two stable extensions: 1 = {′, } and 1′ = {}. These yield two diferent modifications ⌜21 ⌝ (c) and ⌜21′ ⌝ (d), with respect to 11 = {} and 11′ = ∅. Consequently, their only stable extensions are 2 = {} and 2′ = {, } respectively.
(a) ′ (b) ⌞1⌟ ′ (c) ⌜21 ⌝ ′
1′ (d) ⌜2 ⌝
Towards proving the splitting theorem, we adapt a useful lemma from [
Proof. Suppose ∈ stb( ) such that (i) and (ii) hold. Since ⊆ and (i) holds, we get ∈ cf( ′). Moreover, from (ii) we derive that ⊕( ′) = ⊕( ) ∪ = ∪ , deriving ∈ stb( ′). Assume ∈ stb( ′). Since every is self-attacking, we know that ⊆ . Thus ∈ cf( ) (less attacks). Further, ⊕( ′) = ∪ from hypothesis, and ⊕( ) = ⊕( ′) ∖ = ( ∪ ) ∖ = , proving that ∈ stb( ). We now show (i) and (ii). For (i) notice that for all ⊆ ℬ , we have ̸⊆ because is conflict-free in ′. For (ii), each is the set of sets attacking the corresponding ∈ . Therefore, at least one of such attacking sets ∈ is guaranteed to be in since ⊕( ′) = ∪ .
Notice that the SETAFs and ′ in the lemma above corresponds exactly to 21 and ⌜21 ⌝, where ℬ is the set of sets attacking 1 and each the set of sets attacking each ∈ 11 . The lemma is thus utilised to show the following parametrised splitting theorem focusing on 21 only. Theorem 5. Let be a SETAF and (1, 2, 3← , 3→) be a quasi-splitting of . Moreover, let ⌞1⌟ and ⌜2′⌝ = ⌜21 ⌝ be as per Definitions 19 and 21.
1. If 1 ∈ stb(⌞1⌟) and 2 ∈ stb(⌜2′⌝), then (1 ∩ 1) ∪ 2 ∈ stb( ). 2. If ∈ stb( ), then there is a set ⊆ { ′ | ∈ +3← } such that 1 = (∩1)∪ ∈ stb(⌞1⌟) and 2 = ∩ 2 ∈ stb(⌜2′⌝).
Proof. (1.) We first prove conflict-freeness. From hypothesis, 1 ∈ cf(⌞1⌟) implies ∩ 1 ∈ cf(1) since ∩ 1 ⊆ 1 and 1 ⊆ ⌞1⌟. Thus, ∩ 1 ∈ cf( ) because 1 = ∩ (21 × 1). From the fact that 2 ∈ stb(⌜2′⌝) together with Lemma 1, we know that 2 ∈ stb(2′), and thus 2 ∈ cf( ). We now consider possible attacks from 1 ∩ 1 to 2 and viceversa. Clearly, (1 ∩ 1, 2) ∈/ + since 1 ∩ 1 ⊆ 1 and 2 ⊆ ′2 (recall ′2 = 2 ∖ (1)3← ). Assume towards contradiction that (2, 1 ∩ 1) ∈ , i.e. (, ) ∈ 3← for some ⊆ 2 ⊆ ′2 and ∈ 1 ∩ 1. If this is the case, then by construction of ⌜2′⌝ we have (, ) ∈ ⌜2′⌝ for some ∈ , violating the coflict-freeness of 2 in ⌜2′⌝. Hence, (1 ∩ 1) ∪ 2 ∈ cf( ). We show that ((1 ∩ 1) ∪ 2)⊕ = 1 ∪ 2 = by contradiction. Assume ∈/ ((1 ∩ 1) ∪ 2)⊕. If ∈ 1, we deduce that ∈ 11 . As before, given that 2 ∈ stb(⌜2′⌝), it holds that 2 ∈ stb(2′) via Lemma 1, and (2, ) ∈ ⌜2′⌝. Therefore, 2 attacks via 3← in , contradicting our assumption. If ∈ 2, together with our assumption, we get ∈ ′2 (elements in 1 ∖ 1 do not attack arguments in 2). Again, since 2 ∈ stb(⌜2′⌝), it holds that 2 ∈ stb(2′) via Lemma 1. Thus, ∈ (2)⊕, contradicting our assumption. Therefore, ((1 ∩ 1) ∪ 2)⊕ = and (1 ∩ 1) ∪ 2 ∈ stb( ).
(2.) We first show that ( ∩ 1) ∪ ∈ stb(⌞1⌟). Let = {1, . . . , } = 1 ∖ ( ∩ 1)⊕ and + = {′ | ∈ }. Since ∈ stb( ), it follows that ⊆ (2). Hence, by construction of ⌞1⌟, we derive that ( ∩ 1) ∪ ∈ stb(⌞1⌟). Consider now 2. From ∈ stb( ), we get 2 ∈ stb(2′) because each ∈ ′2 is attacked by 2 in . Moreover, since is conflict-free in , there is no ⊆ 2 such that (, 1) ∈ 3← (2 satisfies (i)). Notice that = 11 , i.e. each ∈ is in 1 and externally attacked. Recall that ⊆ (2)+. Therefore, there is some ′ ⊆ 2 such that ( ′, ) for each ∈ 11 . By construction of ⌜2′⌝, a fresh argument () = is introduced for each ∈ along with ( ′, ) (2 satisfies (ii)). Thus Lemma 1 applies, concluding 2 ∈ stb(⌜2′⌝).
In this paper, we have presented a modification-based approach to splitting assumption-based
argumentation frameworks. In particular, we have shown that 1. if one computes an extension 1 in 1, then
applies the reduct and modification, and obtains an extension 2 of the remaining sub-framework, their
set-union is an extension of the whole framework. This characterises the incremental computation of
the extension by evaluating the two sub-frameworks. Conversely, we show that 2. if we project an
arbitrary extension of the whole framework to its sub-frameworks, we obtain extensions 1 for 1
and 2 for the (1)-modified version of 2. Since this is bound to specific structure of the underlying
ABAF, we have considered a more general variant of splitting called parametrised splitting inspired by
Baumann et al. [
This work has been supported by the European Union’s Horizon 2020 research and innovation programme (under grant agreement 101034440).
Declaration on Generative AI The author(s) have not employed any Generative AI tools.