Paper deep dive
Beyond But-for Test: Counterfactual Explanation in Abstract Argumentation via Actual Causality (Extended Version)
Siyi Liu, Muyun Shao, Beishui Liao
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 7/5/2026, 5:36:48 AM
Summary
The paper introduces an intervention-based counterfactual reasoning framework for abstract argumentation (AA) to overcome the limitations of the traditional 'but-for' test. By encoding argument acceptance conditions as equations (inspired by Structural Equation Models) and utilizing the Halpern-Pearl definition of actual causality, the authors provide a method to handle complex argumentation structures like Preemption and Overdetermination. The framework allows for simultaneous changes to sets of arguments while keeping 'witness' arguments fixed, thereby providing more reliable and expressive counterfactual explanations in XAI.
Entities (9)
Relation Signals (4)
Siyi Liu → affiliatedwith → Zhejiang University
confidence 100% · Siyi Liu ... Zhejiang University, Hangzhou, China
Halpern-Pearl Definition → guides → Intervention-based Counterfactual Reasoning
confidence 90% · Guided by the refined counterfactual condition introduced in the Halpern-Pearl definition, our method goes beyond the but-for test
Structural Equation Models → underlies → Intervention-based Counterfactual Reasoning
confidence 90% · we build on the expressive framework of structural equation models (SEMs)
But-for Test → limitationof → Abstract Argumentation
confidence 80% · Existing approaches are limited to the but-for test and fail to accommodate more refined counterfactual conditions.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Counterfactual explanation in abstract argumentation calls for an answer to the what-if query: would the topic argument still be accepted if the status of certain other arguments were changed? Existing approaches are limited to the but-for test and fail to accommodate more refined counterfactual conditions. To overcome these limitations, we introduce an intervention-based counterfactual reasoning framework in abstract argumentation. Our approach encodes the acceptance conditions of arguments as equations, then defines an intervention operator that supports (1) changing sets of arguments simultaneously, and (2) fixing witness arguments to their actual labels. Guided by the refined counterfactual condition introduced in the Halpern-Pearl definition, our method goes beyond the but-for test, thereby correctly identifying causes in argumentation structures such as Preemption and Overdetermination. Through comparison, we show that our method surpasses prior methods in both expressiveness and reliability.
Tags
Links
- Source: https://arxiv.org/abs/2606.31080v1
- Canonical: https://arxiv.org/abs/2606.31080v1
Trouble viewing inline? Open PDF directly →
Full Text
89,532 characters extracted from source content.
Expand or collapse full text
Beyond But-for Test: Counterfactual Explanation in Abstract Argumentation via Actual Causality (Extended Version) Siyi Liu Muyun Shao Beishui Liao Corresponding Author: Beishui Liao, baiseliao@zju.edu.cn Zhejiang University, Hangzhou, China Abstract Counterfactual explanation in abstract argumentation calls for an answer to the what-if query: would the topic argument still be accepted if the status of certain other arguments were changed? Existing approaches are limited to the but-for test and fail to accommodate more refined counterfactual conditions. To overcome these limitations, we introduce an intervention-based counterfactual reasoning framework in abstract argumentation. Our approach encodes the acceptance conditions of arguments as equations, then defines an intervention operator that supports (1) changing sets of arguments simultaneously, and (2) fixing witness arguments to their actual labels. Guided by the refined counterfactual condition introduced in the Halpern-Pearl definition, our method goes beyond the but-for test, thereby correctly identifying causes in argumentation structures such as Preemption and Overdetermination. Through comparison, we show that our method surpasses prior methods in both expressiveness and reliability. keywords: Argumentation Causality AI , and 1 Introduction In the field of eXplainable AI (XAI), abstract argumentation (A) has been shown to have advantages in providing structured and verifiable explanations [13, 15, 30]. A formalises conflicts within an argumentation framework (AF) and selects acceptable arguments via semantics [14], which naturally supports answering the post-hoc explanatory question [3]: why is an argument accepted under specific semantics? Existing argument-based explanation methods answer this question by identifying sets of arguments that satisfy formal properties, such as Relevance [16, 21], Monotonicity [31], Sufficiency and Necessity [10, 8, 9]. In everyday reasoning, however, individuals rarely rely on static lists of reasons; they instinctively engage in counterfactual thinking, asking “what-if” questions to probe causes and dependencies [23, 11]. In A terms, this becomes a direct inquiry: Would the topic argument remain accepted if we were to change the acceptance status of one or more arguments suspected to be its causes? This calls for a counterfactual reasoning account in A. Early work addresses this via the most primitive form of counterfactual reasoning, the but-for test, which conducts a counterfactual analysis by asking whether the effect would have occurred without the cause. In A, this analysis is implemented by modifying the AF [28, 27, 29]. Sakama [28], for instance, defines two primitive updates: adding a new initial argument that attacks an accepted argument to render it rejected; and deleting all incoming attacks on a rejected argument to render it accepted. In essence, these operations ask whether changing a single argument’s status would change the acceptance of the topic argument. In the resulting counterfactual, only the suspected cause is altered, with no mechanism to hold other arguments fixed as witnesses. Consider Preemption (Fig. 1(a)), which illustrates the difficulty that arises when witnesses cannot be held fixed. ϵεωβαγη (a) ℱ1 F_1: Preemption ϵεωβαγηα K_α (b) Modified ℱ1 F_1 with α rejected by α K_α Figure 1: Counterexample to the but-for test in A. The status of each argument is visually encoded as: in=dark gray (accepted), out=cross-hatched (rejected), und=light gray (undecided). The dashed box encloses the newly introduced argument and the attack relation. These visual conventions are used throughout the paper. Example 1. Consider the AF ℱ1 F_1 in Fig. 1(a), where η is the accepted argument to be explained. α and β are initial and thus accepted. From each, an even-length path reaches η. However, only the “protecting” path from α is active, since α also attacks ϵε, keeping it rejected and thereby blocking the defensive path from β to η. Intuitively, α contributes to η’s acceptance, whereas β does not, leading to the conclusion that α should be qualified as a cause of η’s acceptance. However, rejecting α (by adding an attacker) does not alter η’s acceptance: with α out, it no longer keeps ϵε rejected, reactivating the defensive path from β via ω–ϵε–γ to η (Fig. 1(b)). The problem is that the counterfactual scenario does not keep ϵε fixed to its actual rejected status, allowing the alternative pathway to distort the counterfactual evaluation. To address the limitations of the but-for test highlighted above, we build on the expressive framework of structural equation models (SEMs) [24] and the Halpern–Pearl (HP) definition of actual causality [17, 18, 19]. We encode argument acceptance via equations and define an intervention operator that supports manipulating sets of arguments while keeping witness arguments fixed. Building on this, our approach yields a refined counterfactual condition that goes beyond the but‑for test and properly handles cases where the but‑for test fails, namely Preemption and Overdetermination. A detailed analysis of these cases is provided in Section 4. The structure of this paper is as follows. Section 2 recalls the necessary background. Section 3 introduces the acceptability model and the intervention operator. Section 4 defines the notion of actual cause via the refined counterfactual condition AC2mAC2^m and forms the basis for the counterfactual explanation method advocated in this paper. Section 5 presents the graphical representation for visualization. Section 6 compares prior methods. Section 7 concludes and outlines future work. All proofs of theorems and propositions are provided in the Appendix. 2 Preliminaries An argumentation framework (AF) is a directed graph ℱ=(,ℛ) F=( A, R), where A is a finite set of arguments and ℛ⊆× R A× A represents the attack relation [14]. The universe of AF is represented by the set ℱ UF, while the set of arguments that appear within ℱ UF is denoted as UA. For an AF ℱ=(,ℛ) F=( A, R) and α,β∈α,β∈ A, define α+=β∈∣(α,β)∈ℛα^+=\β∈ A (α,β)∈ R\ and α−=β∈∣(β,α)∈ℛα^-=\β∈ A (β,α)∈ R\. Given an AF ℱ=(,ℛ) F=( A, R), a set E⊆E A is conflict-free, denoted as E∈ℰcf(ℱ)E∈ E_cf( F) iff for all α,β∈Eα,β∈ E, (α,β)∉ℛ(α,β)∉ R. E defends an argument α∈α∈ A, iff for all β∈α−β∈α^-, there exists γ∈Eγ∈ E, s.t. (γ,β)∈ℛ(γ,β)∈ R. The characteristic function of an AF ℱ=(,ℛ) F=( A, R) is a function Γ s.t. for every E⊆AE A, we have Γℱ(E)=α∈∣Edefendsα _ F(E)=\α∈ A E~defends~α\. To characterize how an argument (in)directly defends another, we introduce the notion of directed and defense paths. Definition 1. Let ℱ=(,ℛ) F=( A, R) be an AF, and α,β∈α,β∈ A. A sequence P=(α0,⋯,αn)P=( _0,·s, _n) is a directed path from α to β iff α0=α _0=α, αn=β _n=β, and (αi−1,αi)∈ℛ( _i-1, _i)∈ R for all i∈1,⋯,ni∈\1,·s,n\; its length is n (number of edges). If such a path exists, α is also said to be relevant to β (by convention, each α is relevant to itself via a path of length 0). For a set S⊆S A, S is relevant for α if every β∈Sβ∈ S is relevant to α. A directed path from α to β is a defense path if its length is even. Furthermore, if there exists a directed path P=(α,γ,β)P=(α,γ,β) of length two, s.t. γ is distinct from α and β, we say that α directly defends β. The acceptability of an argument is prescribed by specific argumentation semantics [4]. Formally, a semantics σ assigns to each AF ℱ=(,ℛ) F=( A, R) a subset of 22 A, denoted as ℰσ(ℱ) E_σ( F). Classical semantics includes admissible, complete, grounded, preferred, and stable semantics (abbr. ad,co,gr,pr,stad,co,gr,pr,st). An extension under the semantics σ is called a σ-extension. While we focus on complete (coco) semantics as our baseline, we outline in Section. 3 how the formal framework for counterfactual explanation can be adapted to other semantics. Let ℱ=(,ℛ) F=( A, R) be an AF, and E∈ℰcf(ℱ)E∈ E_cf( F), E∈ℰco(ℱ)E∈ E_co( F) iff E defends all its elements (E∈ℰad(ℱ)E∈ E_ad( F)), and E=Γℱ(E)E= _ F(E). Argumentation semantics can be defined through two parallel methods: the above extension-based method, and the labelling-based method, which formulates semantics in terms of σ-labelling [12]. Definition 2. Given an AF ℱ=(,ℛ) F=( A, R), a labelling for ℱ F is a total function ℒ:↦ L: A , that assigns each argument a label from the set =,,V=\in,out,und\, denoted as ℒσ(ℱ) L_σ( F) for σ∈ad,co,gr,pr,stσ∈\ad,co,gr,pr,st\. Let (ℒ)in( L), (ℒ)out( L), and (ℒ)und( L) be the sets of arguments labelled in, out, and und respectively. We use the triple ⟨(ℒ),(ℒ),(ℒ)⟩ ( L),out( L),und( L) to represent the labelling ℒ L. A labelling ℒ L of ℱ=(,ℛ) F=( A, R) is said to be admissible (ℒ∈ℒad(ℱ) L∈ L_ad( F)) iff ∀α∈(ℒ)∪(ℒ)∀α ( L) ( L) it holds that: (i) ℒ(α)= L(α)=out iff ∃(β,α)∈ℛ∃(β,α)∈ R s.t. ℒ(β)= L(β)=in; and (i) ℒ(α)= L(α)=in iff ∀(β,α)∈ℛ∀(β,α)∈ R, ℒ(β)= L(β)=out. Moreover, ℒ L is a complete labelling (ℒ∈ℒco(ℱ) L∈ L_co( F)) iff conditions (i) and (i) hold for all arguments in A. 3 Intervention-based Counterfactual Reasoning in A 3.1 Acceptability Model and Intervention We start by defining a language of the logical system for reasoning about argument-label pairs. The atomic propositions are of the form (α)v(α), asserting that “argument α has the label v”. The set of logical connectives ¬,∧\ , \ forms an adequate set, where ¬(α) (α) is interpreted as “the label of α is not v”. The language further includes counterfactual formulas [ψ]φ[ψ] , where [ψ][ψ] is an intervention operator, read as “after intervening to make ψ true, φ holds”. Here, ψ, called a hypothesis, is a consistent conjunction of atomic propositions, ensured by the constraint that no argument receives two different labels. Definition 3 (Syntax). Given a universal set of arguments UA and the range of label V, with α ranging over UA and v ranging over V, the syntax of the language LL_ UA is defined recursively as follows: φ::=(α)∣¬φ∣φ∧φ∣[ψ]φ, ::=v(α) [ψ] , where in [ψ]φ[ψ] , the hypothesis ψ is defined by the grammar: ψ::=⊤∣(α)∣ψ∧ψ::= (α) ψ ψ, with the constraint that for any distinct atomic subformula (α1),(α2)∈(ψ)v_1( _1),v_2( _2)∈ Sub(ψ), α1≠α2 _1≠ _2, where (ψ) Sub(ψ) denotes the set of all atomic subformulas of ψ. A hypothesis ψ is called an atomic hypothesis if ψ=(α)ψ=v(α) for α∈α∈ UA and ∈v ; otherwise, it is a compound hypothesis. And for all (αi)∈(ψ)v_i( _i)∈ Sub(ψ), denote the set of αi _i by ψ A_ψ. We write L−L_ UA^- for the fragment of LL_ UA without counterfactual formulas. Given an AF ℱ F, there exists a unique acceptability model, denoted as ℳℱ M_ F, which is a set of acceptability equations. For any argument α in ℱ F, its equation fαf_α is a function from the labels of α’s attackers to the label of α. Definition 4 (Acceptability Model). Given an AF ℱ=(,ℛ) F=( A, R), its acceptability model ℳℱ=fα∈ M_ F=\f_α\_α∈ A is the unique set of functions, where each fαf_α is called an acceptability equation for α, defined as follows. For each α∈α∈ A. The function fαf_α takes as input an assignment of labels to each attacker β∈α−β∈α^-, denoted by (β)β∈α−(v_β)_β∈α^- with β∈v_β , and returns a label in V as follows: fα((β)β∈α−)=if ∀β∈α−:β=,if ∃β∈α−:β=,otherwise.f_α ((v_β)_β∈α^- )= casesin&if ∀β∈α^-:v_β=out,\\[1.0pt] out&if ∃β∈α^-:v_β=in,\\[1.0pt] und&otherwise. cases Our framework adopts the intervention‑based semantics of SEMs [24] to define counterfactual reasoning. An intervention modifies the model ℳℱ M_ F according to a hypothesis ψ, producing an intervened model ℳℱψ M_ F^ψ where the acceptability equation of each argument appearing in ψ is replaced by a constant function returning its stipulated label, while all other equations remain unchanged. Definition 5 (Intervention). Given an AF ℱ=(,ℛ) F=( A, R) and its acceptability model ℳℱ=fα∈ M_ F=\f_α\_α∈ A, let ψ=⋀i=1k(αi)ψ= _i=1^kv_i( _i) (with αi∈ _i∈ A and ∈v_i ) be a hypothesis. The intervened model ℳℱψ=fαψα∈ M_ F^ψ=\f_α^ψ\_α∈ A is defined by: for each α∈α∈ A, a function fαψf_α^ψ on the same domain as fαf_α: fαψ=,∃i∈1,⋯,k:α=αi,fαotherwise.f_α^ψ= casesv_i,&∃ i∈\1,·s,k\:α= _i,\\[1.0pt] f_α&otherwise. cases Recalled from Def. 2, a labelling ℒ L is a total function that assigns a label to each argument in an AF ℱ F. To unify non-intervened and intervened models, we have introduced ⊤ and let ℳℱ=ℳℱ⊤ M_ F= M_ F . A solution of an (intervened) model ℳℱ M_ F is a labelling that satisfies all its equations. Unlike classic SEMs, which are typically acyclic and yield a unique solution once the exogenous variables are fixed, an AF may contain cycles and thus admit multiple solutions, which correspond to the multiple coco-labellings. Definition 6 (Solution). Given an AF ℱ=(,ℛ) F=( A, R), and its acceptability model ℳℱ M_ F. A solution of the (intervened) model ℳℱψ M_ F^ψ is a labelling ℒ:↦ L: A , s.t. for all α∈α∈ A: ℒ(α)=fαψ((ℒ(β))β∈α−),wherefαψ∈ℳℱψ. L(α)=f_α^ψ (( L(β))_β∈α^- ),~where~f_α^ψ∈ M_ F^ψ. Example 2. Consider the AF ℱ2 F_2 in Fig. 2. For α whose only attacker is γ∈α−γ∈α^-, the acceptability equation fαf_α can be expressed as: γαβη Figure 2: ℱ2 F_2 with Even-Cycle fα=((),),((),),((),),f_α= \\, ((in),out ),\; ((out),in ),\; ((und),und )\, \, where each pair ((γ),α) ((v_γ),v_α ) denotes that input label γv_γ yields output label αv_α. Intervening with the hypothesis ψ=(α)ψ=out(α), the equation fαf_α is replaced by the constant function fαψf_α^ψ that always returns out. The unique solution of the intervened model ℳℱ2ψ M_ F_2^ψ is the labelling ℒ=⟨β,η,α,γ,∅⟩ L= \β,η\,\α,γ\, . The set of all labellings that are solutions of ℳℱψ M_ F^ψ is denoted as (ℳℱψ) Sol( M_ F^ψ). Without intervention, the solutions of the model ℳℱ M_ F coincide with the coco-labellings of the AF. Theorem 1. For any AF ℱ=(,ℛ) F=( A, R), and its acceptability model ℳℱ M_ F, it holds that (ℳℱ)=ℒco(ℱ) Sol( M_ F)= L_co( F). The solution of a model ℳℱψ M_ F^ψ (Def. 6) is tied to complete semantics but can extend to others (e.g., gr,pr,stgr,pr,st) by constraining the solution set (ℳℱψ) Sol( M_ F^ψ). For grounded semantics, the solution is restricted to the one where (ℒ)in( L) is minimal w.r.t. set-inclusion. In Ex. 2, the intervened model ℳℱ2ψ M_ F_2^ψ admits a unique solution ℒ L, which strictly satisfies set-inclusion minimality and thus represents the exact grounded solution. 3.2 Semantics: Base and Model-level Satisfaction Next, we define the semantics of this logical system. We introduce two levels of satisfaction: base satisfaction and model-level satisfaction. The base satisfaction relation (ℳ,ℒ)⊩φ( M, L) evaluates a formula φ∈L− ∈ L_ UA^- which is not a counterfactual formula, w.r.t. a specific solution ℒ L of a (possibly intervened) model ℳ M. Definition 7 (Base Satisfaction). Given an AF ℱ=(,ℛ) F=( A, R) and its acceptability model ℳℱ M_ F. Consider any (intervened) model ℳ=ℳℱψ M= M_ F^ψ and a solution ℒ L of ℳ M, the base satisfaction relation (ℳ,ℒ)⊩φ( M, L) for formula φ∈L− ∈ L_ UA^- is defined recursively: (ℳ,ℒ)⊩(α) ( M, L) (α) ⇔ℒ(α)=, L(α)=v, (ℳ,ℒ)⊩¬φ ( M, L) ⇔(ℳ,ℒ)⊮φ, ( M, L) , (ℳ,ℒ)⊩φ∧ψ ( M, L) ψ ⇔(ℳ,ℒ)⊩φ and (ℳ,ℒ)⊩ψ. ( M, L) and ( M, L) ψ. Model-level satisfaction lifts the base evaluation, considering either all (⊧∀ _∀) or some (⊧∃ _∃) of its solutions, and defines the meaning of counterfactual formulas. Definition 8 (Model-level Satisfaction). Let φ∈L ∈ L_ UA be a formula, ℱ=(,ℛ) F=( A, R) an AF, and ℳ=ℳℱψ M= M_ F^ψ any (intervened) acceptability model. Strong satisfaction (⊧∀ _∀) and weak satisfaction (⊧∃ _∃) are defined recursively over the structure of φ : For φ∈L−: ∈ L_ UA^-: ℳ⊧∀φ⇔∀ℒ∈(ℳ):(ℳ,ℒ)⊩φ, M _∀ ∀ L∈ Sol( M):\,( M, L) , ℳ⊧∃φ⇔∃ℒ∈(ℳ):(ℳ,ℒ)⊩φ. M _∃ ∃ L∈ Sol( M):\,( M, L) . For φ=[ψ]χ with ψ,χ∈L−: =[ψ]χ with ψ,χ∈ L_ UA^-: ℳ⊧∀[ψ]χ⇔ℳψ⊧∀χ, M _∀[ψ]χ M^ψ _∀χ, ℳ⊧∃[ψ]χ⇔ℳψ⊧∃χ. M _∃[ψ]χ M^ψ _∃χ. Example 3 (Cont. of Ex. 2). Recall ℱ2 F_2 in Fig. 2 and its unique coco-labelling ℒ∈ℒco(ℱ2) L∈ L_co( F_2) depicted therein. Base satisfaction gives (ℳℱ2,ℒ)⊩(α)( M_ F_2, L) (α). Consider two interventions: ψ1=(α) _1=out(α) and ψ2=(β) _2=out(β). • Under ψ1=(α) _1=out(α), ℳℱ2ψ1 M_ F_2 _1 has the unique solution ℒ1=⟨β,η,α,γ,∅⟩ L_1= \β,η\,\α,γ\, , where η labelled in. Thus, ℳℱ2⊧∀[(α)](η)⇔ℳℱ2(α)⊧∀(η) M_ F_2 _∀[out(α)]in(η) M_ F_2^out(α) _∀in(η). • Under ψ2=(β) _2=out(β), one of the solutions of ℳℱ2ψ2 M_ F_2 _2 is ℒ2=⟨∅,β,α,γ,η⟩ L_2= ,\β\,\α,γ,η\ , where η labelled und. Thus, ℳℱ2⊧∃[(β)](η)⇔ℳℱ2(β)⊧∃(η) M_ F_2 _∃[out(β)]out(η) M_ F_2^out(β) _∃out(η). 4 Counterfactual Explanation based on Actual Causality In general, an explanation strategy maps an AF ℱ F and a topic argument α in ℱ F to a set of explanations of a specific type. Here, we focus on the formula-based strategy. A formula‑based explanation method is a function F−Expl:ℱ×→2L−F-Expl: UF× UA→ 2^L_ UA^- associating with each AF ℱ=(,ℛ) F=( A, R) and α∈α∈ A a subset of L−L_ UA^-, denoted as F−Expl(ℱ,α)F-Expl( F,α). Each ψ∈F−Expl(ℱ,α)ψ -Expl( F,α) is called a formula‑based explanation. 4.1 From But-for Cause to Actual Causes To formalise “changing the cause(s)”, we introduce the set of modified hypotheses for the hypothesis ψ: those obtained by changing the label of at least one argument in ψ to a different label while keeping the other arguments fixed. Definition 9 (Modified Hypotheses). Let ψ=⋀i=1k(αi)ψ= _i=1^kv_i( _i) be a hypothesis. The set of modified hypotheses of ψ, denoted by (ψ) Mod(ψ), comprises all ψ′=⋀i=1k′(αi)ψ = _i=1^kv_i ( _i) s.t. there exists at least one index i∈1,…,ki∈\1,…,k\ with ′≠v_i _i. We consider two counterfactual conditions: the but‑for test BFTBFT (underlying graph‑modification, Ex. 1) and the modified condition AC2mAC2^m. A hypothesis passing BFTBFT is called a but‑for cause, and one passing AC2mAC2^m an actual cause. Both admit strong (∀) and weak (∃) versions, as an AF may admit multiple coco-labellings due to cycles. The but-for test (BFTBFT) applies only to an atomic hypothesis of the form (α)v(α) and involves no witness. It asks whether the effect would have occurred without the cause and, in the A setting, modifies the suspected argument’s label to either in or out. We define the restricted modification set /(ψ)⊆(ψ) Mod_in/out(ψ) Mod(ψ), which excludes modifications to und, following the graph‑modification approach of Sakama [28]. Definition 10 (But-for Cause). Let ℱ=(,ℛ) F=( A, R) be an AF, ℳℱ M_ F its acceptability model, α∈α∈ A the topic, and ℒ L a solution of ℳℱ M_ F. An atomic hypothesis ψ∈L−ψ∈ L_ UA^- is a but-for cause for (α)v(α) with (ℳ,ℒ)⊩ψ∧(α)( M, L) ψ (α), iff it passes the but-for test BFTqBFT_q, formally: ∃ψ′∈/(ψ):ℳℱ⊧q[ψ′]¬(α) for q∈∀,∃.∃ψ ∈ Mod_in/out(ψ): M_ F _q[ψ ] (α) for q∈\∀,∃\. Our definition of an actual cause in A preserves the three HP-conditions of actual causality [18, Def. 2.1]: Actuality requires the cause and effect to hold in the original labelling; Counterfactual Condition uses the modified version AC2mAC2^m adopted in this paper; 111In the original HP-definition, this condition is denoted by AC2(am)AC2(a^m) [18]. Minimality ensures that the cause contains no redundant parts. Definition 11 (Actual Cause). Let ℱ=(,ℛ) F=( A, R) be an AF and ℳℱ M_ F its acceptability model. Consider α∈α∈ A the topic, and ℒ L a solution of ℳℱ M_ F. A hypothesis ψ∈L−ψ∈ L_ UA^- is an actual cause for (α)v(α) iff it satisfies the following three conditions: Actuality (AC1AC1): (ℳℱ,ℒ)⊩ψ∧(α)( M_ F, L) ψ (α). Modified Counterfactual Condition (AC2mAC2^m): In Def. 12 below. Minimality (AC3AC3): Let ψ=⋀i=1k(αi)ψ= _i=1^kv_i( _i). Then for every proper sub-conjunction ψJ=⋀i∈J(αi) _J= _i∈ Jv_i( _i) (J⊊1,…,kJ \1,…,k\), ψJ _J fails to satisfy both AC1AC1 and AC2AC2. From Def. 10, a but-for cause trivially satisfies AC1AC1 and AC3AC3. The distinction between a but-for cause and an actual cause lies solely in the counterfactual condition. Proposition 1. Let ℳℱ M_ F be an acceptability model with a topic argument α. If hypothesis ψ is a but-for cause for (α)v(α), then ψ satisfies Actuality (AC1AC1) and Minimality (AC3AC3). AC2mAC2^m improves upon BFTBFT by allowing compound hypothesis and keeping witnesses fixed to their actual labels. It validates a counterfactual if there exist fixed witnesses that enable the intervention to alter the topic’s label. Analyzing the specific topological properties of such witnesses is left for future work. Definition 12 (Modified Counterfactual Condition (AC2mAC2^m)). Let ψ and χ be two hypotheses with ψ∩χ=∅ A_ψ∩ A_χ= , α∉χα∉ A_χ, and (ℳℱ,ℒ)⊩χ( M_ F, L) χ. We say ψ satisfies AC2qmAC2^m_q iff: ∃ψ′∈(ψ):ℳℱ⊧q[ψ′∧χ]¬(α) for q∈∀,∃.∃ψ ∈ Mod(ψ): M_ F _q[ψ χ] (α)~for~q∈\∀,∃\. Example 4 (But-for vs. Actual Cause). Recall the AF ℱ1 F_1 in Fig. 1(a) and its coco-labelling ℒ L depicted therein, where the topic argument η is labelled in. Let the suspected cause of (η)in(η) be the hypothesis ψ=(α)ψ=in(α). (α)in(α) fails the but-for test BFT∃BFT_∃: after intervening with (α)out(α), ℳℱ1(α) M_ F_1^out(α) has the unique solution ℒ1=⟨β,ϵ,η,α,ω,γ,∅⟩ L_1= \β,ε,η\,\α,ω,γ\, , in which η remains in. Hence, ¬(η) (η) does not hold, and (α)in(α) does not qualify as a but‑for cause. Yet (α)in(α) passes AC2∃mAC2^m_∃ with witness χ=(ϵ)χ=out(ε). Specifically, there exists a witness χ=(ϵ)χ=out(ε) fixed to its actual label in ℒ L, s.t. once we intervene with ψ1=(α)∈(ψ) _1=out(α)∈ Mod(ψ) while holding χ fixed, the compound hypothesis ψ2=(α)∧(ϵ) _2=out(α) (ε) is formed. The intervened model ℳℱ1ψ2 M_ F_1 _2 then yields the unique solution ℒ2=⟨β,γ,α,ω,ϵ,η,∅⟩ L_2= \β,γ\,\α,ω,ε,η\, , in which η is labelled out. Thus (α)in(α) is identified as an actual cause of (η)in(η), overcoming the counter-intuition of the but-for test illustrated in Ex. 1. Theorem 2 establishes that for both BFTBFT and AC2mAC2^m the strong variant implies the weak variant, while Theorem 3 shows that every but-for cause is also an actual cause. Together, they characterize the logical relationships among the counterfactual conditions. Theorem 2. Let ℳℱ M_ F be an acceptability model with a topic argument α. For any atomic hypothesis ψ∈L−ψ∈ L_ UA^-, if ψ is a but-for cause for (α)v(α) under BFT∀BFT_∀, then it is also a but-for cause for (α)v(α) under BFT∃BFT_∃. For any hypothesis ψ∈L−ψ∈ L_ UA^-, if ψ is an actual cause for (α)v(α) under AC2∀mAC2^m_∀, then it is also an actual cause for (α)v(α) under AC2∃mAC2^m_∃. Theorem 3. Let ℳℱ M_ F be an acceptability model with a topic argument α. For any atomic hypothesis ψ∈L−ψ∈ L_ UA^- and q∈∀,∃q∈\∀,∃\, if ψ is a but-for cause for (α)v(α) under BFTqBFT_q, then it is also an actual cause for (α)v(α) under AC2qmAC2^m_q. αωβ1 _1β2 _2η3 _3η1 _1η2 _2ϵεγ Figure 3: For Ex. 5 (ℱ3 F_3) Example 5. Consider the AF ℱ3 F_3 and its coco-labelling ℒ L in Fig. 3. Although α, β1 _1, and γ each have an even-length path to η1 _1, not all are actual causes: α’s defense is ”blocked” by β1 _1, whereas β1 _1 and γ are both necessary for η1 _1’s acceptance. First, test (γ)in(γ). Intervening with (γ)out(γ) yields a intervened model ℳℱ3(γ) M_ F_3^out(γ), one of whose solution is ℒ′=⟨ϵ,η2,β1,α,γ,η1,η3,β2,ω,∅⟩ L = \ε, _2, _1,α\,\γ, _1, _3, _2,ω\, , where η1 _1’s label becomes out. Hence, (γ)in(γ) is a but-for cause (and thus also satisfies AC2mAC2^m). Next, test (β1)in( _1). Under a but-for intervention (β1)out( _1) alone, the unique labelling is ℒ′=⟨α,β2,η1,γ,ω,β1,η3,η2,ϵ,∅⟩ L = \α, _2, _1,γ\,\ω, _1, _3, _2,ε\, , and η1 _1’s label remains. The blocked path from α is now active, preserving η1 _1’s acceptance. To prevent this, AC2mAC2^m also fixes β2 _2’s label to its original label out. In ℳℱ3(β1)∧(β2) M_ F_3^out( _1) ( _2), one solution is ℒ′=⟨α,γ,ω,β1,β2,ϵ,η1,η2,η3⟩ L = \α,γ\,\ω, _1, _2,ε\,\ _1, _2, _3\ , where η1 _1 is now labelled und. Thus, (β1)in( _1) qualifies as an actual cause under AC2mAC2^m, while the stricter but-for condition BFTBFT fails. 4.2 Counterfactual Explanation We now instantiate the formula-based explanation strategy F−ExplF-Expl with counterfactual explanation (CounterCounter) and but-for explanation (ButForButFor). The latter serves as a baseline to further justify the former as the appropriate instantiation. While the notion of actual cause (Def. 11) is independent of specific labels and accommodates any status of the topic argument (in, out, or und), we restrict our focus here to explaining its acceptance (in). This restriction is motivated by the fact that standard formal properties (e.g., Relevance, Existence) and the prevailing explanation methods compared in Section 6 are predominantly formulated for explaining accepted arguments. We adopt AC2mAC2^m for actual causes, and call the resulting method counterfactual explanation. Let (ℳℱ,ℒ,(α)) Act( M_ F, L,in(α)) be the set of hypotheses ψ∈L−ψ∈ L_ UA^- that satisfy AC2∃mAC2^m_∃ (the strong version AC2∀mAC2^m_∀ is left for future work) for (α)in(α) under the solution ℒ L of ℳℱ M_ F. Definition 13 (Counterfactual Explanation). Let ℱ=(,ℛ) F=( A, R) be an AF and ℳℱ M_ F its acceptability model. Consider α∈α∈ A the topic, ℒ L a solution of ℳℱ M_ F with ℒ(α)= L(α)=in. Then, Counter(ℱ,α)=⋃ℒ∈(ℳℱ)(ℳℱ,ℒ,(α)).Counter( F,α)= _ L∈ Sol( M_ F) Act( M_ F, L,in(α)). A basic requirement for any explanation is that the arguments it involves be relevant (recall Def. 1) to the topic. The following proposition confirms that our counterfactual explanation method satisfies the Relevance property. Proposition 2. Given an AF ℱ=(,ℛ) F=( A, R) and the topic α∈α∈ A. If the hypothesis ψ∈Counter(ℱ,α)ψ ( F,α), then for all αi∈ψ _i∈ A_ψ, it holds that αi _i is relevant to α. Monotonicity is a well-known property in argument-based explanation strategy [31]: if a set of arguments qualifies as an explanation, any superset should also be one. The counterfactual explanation method does not satisfy Monotonicity, as Minimality requires that no proper sub-conjunction of the cause satisfies Actuality (AC1AC1) and Modified Counterfactual Condition (AC2mAC2^m). Proposition 3. Given an AF ℱ=(,ℛ) F=( A, R) and the topic α∈α∈ A, for any hypotheses ψ,ψ′∈L−ψ,ψ ∈ L_ UA^- with ψ⊊ψ′ A_ψ A_ψ , if ψ∈Counter(ℱ,α)ψ ( F,α) then ψ′∉Counter(ℱ,α)ψ ( F,α). For comparison, we also define the but-for explanation. Let (ℳℱ,ℒ,(α)) BF( M_ F, L,in(α)) denote the set of all atomic hypotheses ψ∈L−ψ∈ L_ UA^- that satisfy BFT∃BFT_∃ for (α)in(α) under the solution ℒ L of ℳℱ M_ F. Consistent with the counterfactual explanation method, we restrict our focus to the weak version BFT∃BFT_∃. Then, ButFor(ℱ,α)=⋃ℒ∈(ℳℱ)(ℳℱ,ℒ,(α))ButFor( F,α)= _ L∈ Sol( M_ F) BF( M_ F, L,in(α)). The following proposition compares the two explanation methods w.r.t Non-trivial Explanation: the existence of an explanation that involves accepted arguments beyond the topic itself when the topic is a sink node. It shows that counterfactual explanation always provides such an explanation, whereas the but-for explanation may fail to do so. Proposition 4. Let ℱ=(,ℛ) F=( A, R) be an AF and α∈α∈ A the topic s.t. α−≠∅α^-≠ , α+=∅α^+= and ℒ(α)= L(α)=in for some ℒ∈ℒco(ℱ) L∈ L_co( F). 1. For any ℱ F and α satisfying the above conditions, there exists ψ∈Counter(ℱ,α)ψ ( F,α), s.t. (i) ψ∖α≠∅ A_ψ \α\≠ , and (i) for all β∈ψβ∈ A_ψ, ℒ(β)= L(β)=in. 2. There exists ℱ F and α satisfying the above conditions, s.t. for all ψ=(β)ψ=in(β), if ψ∈ButFor(ℱ,α)ψ ( F,α), then ψ∖α=∅ A_ψ \α\= . Example 6. Consider the AF ℱ4 F_4 in Fig. 4 and its unique coco-labelling ℒ L depicted therein. Let the topic be η labelled in. Although η is attacked by γ, it is accepted because both α and β defend it, each sufficient to protect η from γ’s attack. γαβη Figure 4: ℱ4 F_4: Overdetermination Neither (α)in(α) nor (β)in(β) passes the but-for test BFT∃BFT_∃. By contrast, the compound hypothesis ψ=(α)∧(β)ψ=in(α) (β) satisfies AC2∃mAC2^m_∃ and therefore belongs to Counter(ℱ4,η)Counter( F_4,η), providing a non-trivial explanation with ψ∖η≠∅ A_ψ \η\≠ . 5 Graph Mutilations of Intervention Following Pearl’s graph mutilations for interventions in causal networks [24, p. 23], we define a corresponding graph operation on AFs for each atomic hypothesis (α)v(α). These operations are illustrated in Fig. 5 and formalised in the following Def. 14. Notably, this section provides a graphical counterpart of the intervention (Def. 5). The core contribution of the intervention and AC2mAC2^m lies in distinguishing causes from witnesses, a capability absent from earlier graph‑modification approaches and essential for moving beyond the but‑for test, as demonstrated in Section 4. γαβη (a) ℱ2,(α) F_2,in(α) γαβη (b) ℱ2,(α) F_2,und(α) γαβηα K_α (c) ℱ2,(α) F_2,out(α) Figure 5: Atomic Mutilation of ℱ2 F_2 in Fig. 2. Symbols: dashed arrows == removed attacks, double arrows == newly introduced attacks, and double circles == newly introduced arguments. Definition 14 (Atomic Mutilation). Given an AF ℱ=(,ℛ) F=( A, R) and an atomic hypothesis (α)v(α) of ℱ F, three types of atomic mutilated ℱ F are defined as follows: • ℱ(α)=(∪α,ℛ∪(α,α)) F_out(α)= ( A∪\ K_α\,\; R∪\( K_α,α)\ ), • ℱ(α)=(,ℛ∖(β,α)∣β∈α−) F_in(α)= ( A,\; R \(β,α) β∈α^-\ ), • ℱ(α)=(,ℛ∪(α,α)∖(β,α)∣β∈α−) F_und(α)= ( A,\; R∪\(α,α)\ \(β,α) β∈α^-\ ). These atomic mutilations are not unique: ℱ(α) F_out(α) and ℱ(α) F_in(α) match Sakama [28], while ℱ(α) F_und(α) follows Rienstra [27]. Unlike their metaphysical interpretations, our intervention is purely instrumental for probing dependencies, treating the graph representation merely as a technical convenience. Any admissible formulation must respect two properties: Node Independence : In ℳℱ(α) M^v(α)_ F, the label of α no longer depends on its attackers. This is realized in the graph mutilation as follows: for ℱ(α) F_out(α), adding α K_α overrides all incoming attacks; for ℱ(α) F_in(α), incoming attacks are removed; for ℱ(α) F_und(α), incoming attacks are removed and a self‑attack is added. Status Uniqueness : The intervention fixes the label of α to v in ℳℱ(α) M^v(α)_ F. The same holds in the mutilated AF. The two properties discussed above jointly guarantee that the application of intervention hypotheses is order-invariant. Proposition 5. Let ℳℱ M_ F be an acceptability model and ψ=ψ1∧ψ2ψ= _1 _2 a compound hypothesis. Then, ℳℱψ=(ℳℱψ1)ψ2=(ℳℱψ2)ψ1 M^ψ_ F\;=\; ( M_ F _1 ) _2\;=\; ( M_ F _2 ) _1. This result also holds for framework mutilation. Based on this, we define mutilation of an AF by a compound hypothesis through the recursion of atomic mutilations. Definition 15 (Compound Mutilation). Let ℱ F be an AF and ψ∈L−ψ∈ L_ UA^- a hypothesis. The compound mutilated AF ℱψ F_ψ is defined recursively w.r.t the possible forms of ψ: • If ψ=(α)ψ=v(α), then ℱψ=ℱ(α) F_ψ= F_v(α), • If ψ=ψ1∧ψ2ψ= _1 _2, then ℱψ=(ℱψ1)ψ2=(ℱψ2)ψ1 F_ψ=( F_ _1)_ _2=( F_ _2)_ _1. We end this section by establishing a mapping from solutions of the intervened models to labellings of the mutilated AFs. Theorem 4. Let ℱ=(,ℛ) F=( A, R) be an AF, ℳℱ M_ F its acceptability model, and ψ∈L−ψ∈ L_ UA^- a hypothesis. For every ℒ∈(ℳℱψ) L∈ Sol( M_ F^ψ), there exists a labelling ℒ′ L of the mutilated AF ℱψ F_ψ s.t., for any argument α∈α∈ A, it holds that ℒ(α)=ℒ′(α) L(α)= L (α). 6 Discussion Most explanation methods in the literature are argument-based, defined as a function A−Expl:ℱ×→22A-Expl: UF× UA→ 2^2 A that returns sets of arguments as explanations. We recall four prominent instantiations RootσRoot_σ, SufSuf, NecNec, and Close−CountσClose-Count_σ below. Root Reason. Liao and Van Der Torre [22, Def. 14] introduce root reason. Given an AF ℱ=(,ℛ) F=( A, R), an extension E∈ℰσ(ℱ)E∈ E_σ( F), and a topic α∈Eα∈ E, let E¯=(γ,δ)∣γ,δ∈E,γ directly defends δ E=\(γ,δ) γ,δ∈ E,γ directly defends δ\ with transitive closure E¯+ E^+. An argument β∈Eβ∈ E is initial if it has no attackers in ℱ F, and self-explanatory if (β,β)∈E¯+(β,β)∈ E^+ (denoted EIE_I and ESE_S). Then, Rootσ(ℱ,α)=β∈E∣(β,α)∈E¯+,β∈EI∪ES|E∈ℰσ(ℱ),α∈E.Root_σ( F,α)= \\,\β∈ E (β,α)∈ E^+,\ β∈ E_I∪ E_S\ |E∈ E_σ( F),\ α∈ E\, \. Sufficient and Necessary Explanation. Borg and Bex [10, Def. 28] formalise sufficient and necessary explanations in A using the notion of relevance (Def. 1). A set S⊆S A is sufficient for α iff S is relevant for α, conflict-free, and defends S∪αS∪\α\. An argument β∈β∈ A is necessary for α iff β is relevant for α and, for every admissible set E∈ℰad(ℱ)E∈ E_ad( F), β∉Eβ∉ E implies α∉Eα∉ E. Then, Suf(ℱ,α) ( F,α) =S∪α|S is sufficient for α, = \\,S∪\α\ |S is sufficient for α\, \, Nec(ℱ,α) ( F,α) =α∪β∈∣β is necessary for α. = \\,\α\∪\β∈ A β is necessary for α\\, \. The next proposition relates counterfactual explanation to root reasons and sufficient explanation. When causes are restricted to initial or self‑explanatory arguments, counterfactual explanation is more precise than root reasons. When restricted to accepted arguments, it is more selective than the sufficient explanation. Proposition 6. Let ℱ=(,ℛ) F=( A, R) be an AF, α∈α∈ A the topic, and ℒ∈ℒco(ℱ) L∈ L_co( F) a coco-labelling with ℒ(α)= L(α)=in. Then, 1. For all ψ∈Counter(ℱ,α)ψ ( F,α) with ψ⊆(ℒ)I∪(ℒ)S A_ψ ( L)_I ( L)_S and (αi,α)∈(ℒ)¯+( _i,α)∈ in( L)^+ for all αi∈ψ _i∈ A_ψ, there exists E∈Rootco(ℱ,α)E _co( F,α) s.t. ψ⊆E A_ψ E. The converse does not hold. 2. For all ψ∈Counter(ℱ,α)ψ ( F,α) with ψ⊆(ℒ) A_ψ ( L), there exists E∈Suf(ℱ,α)E ( F,α) s.t. ψ⊆E A_ψ E. The converse does not hold: there exist E∈Suf(ℱ,α)E ( F,α) for which no such ψ satisfies ψ⊆E∖α A_ψ E \α\. Example 7 (Cont. of Ex. 2). Recall the AF ℱ2 F_2 in Fig. 2 and its unique coco-labelling ℒ L depicted therein, with η the topic argument. Rootco(ℱ2,η)=α,βRoot_co( F_2,η)=\\α,β\\, since α∈(ℒ)Sα ( L)_S and β∈(ℒ)Iβ ( L)_I, and both directly defend η. Suf(ℱ2,η)=α,β,η,α,η,β,ηSuf( F_2,η)=\\α,β,η\,\α,η\,\β,η\\, each S∖ηS \η\ for S∈Suf(ℱ2,η)S ( F_2,η) being conflict-free, relevant, and defending S∪ηS∪\η\. For counterfactual explanation, (β)in(β) is an actual cause, whereas (α)in(α) fails AC2∃mAC2^m_∃. First, after intervening with (α)out(α), ℳℱ2(α) M_ F_2^out(α) has the unique solution ℒ1=⟨β,η,α,γ,∅⟩ L_1= \β,η\,\α,γ\, , where η remains in. Second, after intervening with (α)und(α), ℳℱ2(α) M_ F_2^und(α) has the unique solution ℒ2=⟨β,η,γ,α⟩ L_2= \β,η\,\γ\,\α\ , with η still in. Third, no admissible witness can rescue (α)in(α): in both solutions, γ retains its original label out, so fixing any other arguments as witnesses does not alter the outcome. In contrast, ℳℱ2(β) M_ F_2^out(β) admits a solution ℒ3=⟨∅,β,α,γ,η⟩ L_3= ,\β\,\α,γ,η\ , where η is und. Hence (β)in(β) qualifies as an actual cause. Furthermore, Minimality excludes any ψ′ψ with ψ′⊋(β) A_ψ A_in(β); hence, ψ′∉Counter(ℱ2,η)ψ ( F_2,η). Thus, for ψ=(β)∈Counter(ℱ2,η)ψ=in(β) ( F_2,η), ψ=β A_ψ=β is a subset of every E∈Rootco(ℱ2,η)E _co( F_2,η) and every S∈Suf(ℱ2,η)S ( F_2,η), yet the converse fails. α1 _1α2 _2α3 _3α4 _4βγ1 _1γ2 _2ηϵε Figure 6: For Ex. 8 (ℱ5 F_5) Example 8. Consider the AF ℱ5 F_5 and the coco-labelling ℒ L in Fig. 6, with γ1 _1 as the topic argument. The set E=α1,α3,γ1E=\ _1, _3, _1\ is a sufficient explanation. And the set of in labelled arguments E′=(ℒ)E =in( L) is a root reason. ψ1=(α1) _1=in( _1), ψ2=(α3) _2=in( _3), and ψ3=(η)∧(ϵ) _3=in(η) (ε) are all actual causes. Moreover, ψi A_ _i is the subset of both E and E′E for i∈1,2,3i∈\1,2,3\. Closest-World-Based Counterfactual Explanation. In contrast to our intervention-based framework, Alfano et al. [2, Def. 1] introduce an alternative counterfactual explanation rooted in the closest-world semantics [20]. In this approach, a labelling ℒ L of an AF ℱ=(,ℛ) F=( A, R) is seen as the actual world and other σ-labellings as possible worlds. The similarity between two worlds is measured by the Hamming distance δ(ℒ,ℒ′)=|α∈∣ℒ(α)≠ℒ′(α)|δ( L, L )=|\α∈ A L(α)≠ L (α)\|. A labelling ℒ′ L is a counterfactual of ℒ L w.r.t. α iff: 1. ℒ(α)≠ℒ′(α) L(α)≠ L (α), and 2. there exists no ℒ′∈ℰσ(ℱ) L ∈ E_σ( F) s.t. ℒ(α)≠ℒ′(α) L(α)≠ L (α) and δ(ℒ,ℒ′)<δ(ℒ,ℒ′)δ( L, L )<δ( L, L ). The set of counterfactuals of ℒ L in an AF w.r.t. α is denoted as ℭσ(α,ℒ) CF^σ(α, L), and each such counterfactual labelling serves as an explanation for the topic’s acceptance. Then, Close−Countσ(ℱ,α)=(ℒ′)∣ℒ∈ℰσ(ℱ),α∈(ℒ),and∃ℒ′s.t.ℒ′∈ℭσ(α,ℒ).Close-Count_σ( F,α)= \in( L ) L∈ E_σ( F),α ( L),and~∃ L ~s.t.~ L ∈ CF^σ(α, L) \. Following the methodology of actual causality [5], human intuitions about causes can be formalised as structural principles on a given graph topology. While an exhaustive principle-based analysis is beyond the scope of this discussion, Fig. 1(a) (Preemption) and Fig. 4 (Overdetermination) instantiate the key structural patterns behind those principles. The next example compares our method with RootcoRoot_co, SufSuf, NecNec, and Close−CountcoClose-Count_co on these two structures. Example 9 (RootcoRoot_co, SufSuf, NecNec, Close−CountcoClose-Count_co vs. CounterCounter). Consider again the AFs ℱ1 F_1 (Preemption, Fig. 1(a)) and ℱ4 F_4 (Overdetermination, Fig. 4), each with the unique coco-labelling depicted therein. Let the topic be η in both AFs. Preemption (ℱ1 F_1): Rootco(ℱ1,η)=αRoot_co( F_1,η)=\\α\\, α,β,η∈Suf(ℱ1,η)\α,β,η\ ( F_1,η), Nec(ℱ1,η)=α,ηNec( F_1,η)=\\ \\α,η\\, Close−Countco(ℱ1,η)=∅Close-Count_co( F_1,η)= , (α)∈Counter(ℱ1,η)in(α) ( F_1,η) while (β)∉Counter(ℱ1,η)in(β) ( F_1,η). Overdetermination (ℱ4 F_4): Rootco(ℱ4,η)=α,βRoot_co( F_4,η)=\\α,β\\, α,η,β,η∈Suf(ℱ4,η)\α,η\,\β,η\ ( F_4,η), Nec(ℱ4,η)=ηNec( F_4,η)=\\η\\, Close−Countco(ℱ4,η)=∅Close-Count_co( F_4,η)= , (α)∧(β)∈Counter(ℱ4,η)in(α) (β) ( F_4,η) while (α),(β)∉Counter(ℱ4,η)in(α),in(β) ( F_4,η). Three observations follow. 1. RootcoRoot_co performs well in Preemption (singling out α) but fails in Overdetermination, as it cannot distinguish between the two symmetric defenders α and β. 2. NecNec is closer to CounterCounter than SufSuf is: in ℱ1 F_1, NecNec returns α,η\α,η\, whose non-topic element matches the actual cause (α)in(α); in ℱ4 F_4, NecNec returns η\η\, reflecting the absence of any single necessary argument, while CounterCounter captures joint necessity via (α)∧(β)in(α) (β). This confirms that CounterCounter merely tracks necessity, not sufficiency, which is a perspective largely overlooked in prior work. 3. Close−CountcoClose-Count_co fails to satisfy Existence, which is a foundational principle for any explanation method. Because both ℱ1 F_1 and ℱ4 F_4 admit only a unique coco-labelling, there are no alternative “possible worlds (counterfactual labellings)” where the status of η changes. Consequently, Close−CountcoClose-Count_co yields an empty set (∅ ) for both frameworks, which directly contradicts the intuitive premise that the acceptance of η has identifiable causes. 7 Conclusion and Future Work We introduce an intervention-based counterfactual reasoning framework in abstract argumentation and develop counterfactual explanations within this setting. By fixing witness arguments, our method overcomes the limitations of the but-for approach. We further show that the intervention operation can be visualized through graph mutilation, thereby improving our method’s explainability for human-aligned interaction. A comparison with existing argument-based explanation methods shows that our counterfactual explanation is more selective while maintaining connections to these approaches. Several research directions follow naturally. First, our method and existing approaches warrant a thorough principle-based analysis. This includes different paradigms of counterfactual reasoning, such as the non-intervention-based counterfactual explanation of Alfano et al. [2] rooted in closest-world semantics, and the post-hoc explanation proposed by Amgoud [3]. We plan to develop structural principles that describe specific graph patterns, thereby examining how these methods perform under those patterns. Second, the condition AC2mAC2^m is rooted in acyclic structural equation models. Although it fits well, we will explore counterfactual conditions that are more compatible with cyclic argumentation frameworks. The intervention-based counterfactual reasoning framework introduced in this paper offers an expressive logical language for this endeavor. Third, an analysis of the computational complexity and the development of algorithmic implementations for our framework remain crucial directions for practical deployment. Fourth, we plan to extend the approach to other semantics, and to extended frameworks (PAF, ADF) [1, 26], as well as structured frameworks (ASPIC+, ABA) [6, 25, 7]. Acknowledgements The authors are thankful to the anonymous reviewers for their helpful comments and suggestions. This work is supported by the National Natural Science Foundation of China (No. 62576309). References [1] G. Alfano, M. Calautti, S. Greco, F. Parisi, and I. Trubitsyna (2020) Explainable acceptance in probabilistic abstract argumentation: complexity and approximation. In Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR), p. 33–43. Cited by: §7. [2] G. Alfano, S. Greco, F. Parisi, and I. Trubitsyna (2024) Counterfactual and semifactual explanations in abstract argumentation: formal foundations, complexity and computation. In Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (KR), p. 14–26. Cited by: §6, §7. [3] L. Amgoud (2024) Post-hoc explanation of extension semantics. In 27th European Conference on Artificial Intelligence (ECAI), Frontiers in Artificial Intelligence and Applications, Vol. 392, p. 3276–3283. Cited by: §1, §7. [4] P. Baroni, M. Caminada, and M. Giacomin (2018) Abstract argumentation frameworks and their semantics. In Handbook of Formal Argumentation, p. 159–236. Cited by: §2. [5] S. Beckers and J. Vennekens (2018) A principled approach to defining actual causation. Synthese 195 (2), p. 835–862. Cited by: §6. [6] L. Bengel, L. Blümel, T. Rienstra, and M. Thimm (2022) Argumentation-based causal and counterfactual reasoning. In 1st International Workshop on Argumentation for eXplainable AI (ArgXAI, co-located with COMMA 22), CEUR Workshop Proceedings, Vol. 3209. Cited by: §7. [7] A. Bochman, F. Cerutti, and T. Rienstra (2025) Causation and argumentation. Journal of Applied Logics 12 (3), p. 713–786. Cited by: §7. [8] A. Borg and F. Bex (2021) A basic framework for explanations in argumentation. IEEE Intelligent Systems 36 (2), p. 25–35. Cited by: §1. [9] A. Borg and F. Bex (2021) Necessary and sufficient explanations for argumentation-based conclusions. In Symbolic and Quantitative Approaches to Reasoning with Uncertainty, ECSQARU 2021, Vol. 12897, p. 45–58. Cited by: §1. [10] A. Borg and F. Bex (2024) Minimality, necessity and sufficiency for argumentation and explanation. International Journal of Approximate Reasoning 168, p. 109143. Cited by: §1, §6. [11] R. M.J. Byrne (2019) Counterfactuals in explainable artificial intelligence (XAI): evidence from human reasoning. In Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI), p. 6276–6282. Cited by: §1. [12] M. Caminada and D. M. Gabbay (2009) A logical account of formal argumentation. Studia Logica 93 (2-3), p. 109–145. Cited by: §2. [13] K. Čyras, A. Rago, E. Albini, P. Baroni, and F. Toni (2021) Argumentative XAI: a survey. In Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI), p. 4392–4399. Cited by: §1. [14] P. M. Dung (1995) On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence 77 (2), p. 321–357. Cited by: §1, §2. [15] D. Engelmann, J. Damasio, A. R. Panisson, V. Mascardi, and R. H. Bordini (2022) Argumentation as a method for explainable AI : a systematic literature review. In 2022 17th Iberian Conference on Information Systems and Technologies (CISTI), p. 1–6. Cited by: §1. [16] X. Fan and F. Toni (2015) On computing explanations in argumentation. In Proceedings of the 29th AAAI Conference on Artificial Intelligence, 15, Vol. 29, p. 1496–1502. Cited by: §1. [17] J. Y. Halpern and J. Pearl (2005) Causes and explanations: a structural-model approach. Part I: Explanations. The British Journal for the Philosophy of Science 56 (4), p. 889–911. Cited by: §1. [18] J. Y. Halpern (2015) A modification of the halpern-pearl definition of causality. In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI), p. 3022–3033. Cited by: §1, §4.1, footnote 1. [19] J. Y. Halpern (2016) Actual causality. MIT Press. Cited by: §1. [20] D. Lewis (1973) Counterfactuals. Blackwell Publishing. Cited by: §6. [21] B. Liao and L. Van Der Torre (2020) Explanation semantics for abstract argumentation. In Proceedings of COMMA, p. 271–282. Cited by: §1. [22] B. Liao and L. Van Der Torre (2024) Attack-defense semantics of argumentation. In Proceedings of COMMA, p. 133–144. Cited by: §6. [23] T. Miller (2019) Explanation in artificial intelligence: insights from the social sciences. Artificial Intelligence 267, p. 1–38. Cited by: §1. [24] J. Pearl (2009) Causality: models, reasoning, and inference. Cambridge University Press. Cited by: §1, §3.1, §5. [25] G. Pisano, H. Prakken, G. Sartor, and R. Liepina (2025) Modelling cause-in-fact in legal cases through defeasible argumentation. In Proceedings of the 20th International Conference on Artificial Intelligence and Law (ICAIL), p. 268–277. Cited by: §7. [26] T. Rienstra, J.L.A. Heyninck, G. Kern-Isberner, K. Skiba, and M. Thimm (2022) Explaining argument acceptance in ADFs. In 1st International Workshop on Argumentation for eXplainable AI (ArgXAI, co-located with COMMA 22), CEUR Workshop Proceedings, Vol. 3209. Cited by: §7. [27] T. Rienstra (2014) Argumentation in flux (modelling change in the theory of argumentation). Ph.D. thesis, Université Montpellier I-Sciences et Techniques du Languedoc; Université du Luxembourg. Cited by: §1, §5. [28] C. Sakama (2014) Counterfactual reasoning in argumentation frameworks. In Proceedings of COMMA, p. 385–396. Cited by: §1, §4.1, §5. [29] C. Sakama (2018) Abduction in argumentation frameworks. Journal of Applied Non-Classical Logics 28 (2-3), p. 218–239. Cited by: §1. [30] R. Scheffers, F. Bex, and A. Borg (2024) Related explanations in formal argumentation, an empirical study. In Proceedings of COMMA, p. 265–276. Cited by: §1. [31] M. Ulbricht and J. P. Wallner (2021) Strong explanations in abstract argumentation. In Proceedings of the 35th AAAI Conference on Artificial Intelligence, 7, Vol. 35, p. 6496–6504. Cited by: §1, §4.2. Appendix: Proofs Proof of Theorem 1. Proof. (⇒ ) (ℳℱ)⊆ℒco(ℱ) Sol( M_ F) L_co( F): Let ℒ∈(ℳℱ) L∈ Sol( M_ F) be a solution of the acceptability model ℳℱ M_ F. Take an arbitrary argument α∈α∈ A. Since ℒ L satisfies every equation in ℳℱ M_ F, we have ℒ(α)=fα((ℒ(β)β∈α−)) L(α)=f_α (( L(β)_β∈α^-) ), where fαf_α is the acceptability equation of α. According to Def. 4, the output of the function fαf_α is completely determined by the labels of the attackers β∈α−β∈α^-. Now, examine the three possible cases for ℒ(α) L(α): Case 1 If ℒ(α)= L(α)=in, then by the equation, every attacker β∈α−β∈α^- must satisfy ℒ(β)= L(β)=out. Hence, condition (i) of a complete labelling holds for α. Case 2 If ℒ(α)= L(α)=out, then there exists β∈α−β∈α^- with ℒ(β)= L(β)=in. Thus, condition (i) of a complete labelling holds for α. Case 3 If ℒ(α)= L(α)=und, then it is neither the case that all are out nor that some attacker is in, which indicates that α must satisfy the condition (i) and (i) of a complete labelling. Since α was arbitrary, ℒ L satisfies the complete labelling conditions for every argument, i.e., ℒ∈ℒco(ℱ) L∈ L_co( F). Given that ℒ L is an arbitrary element of (ℳℱ) Sol( M_ F), we conclude that (ℳℱ)⊆ℒco(ℱ) Sol( M_ F) L_co( F). (⇐ ) ℒco(ℱ)⊆(ℳℱ) L_co( F) Sol( M_ F): Let ℒ∈ℒco(ℱ) L∈ L_co( F) be a complete labelling of ℱ F. For any α∈α∈ A, we show that ℒ(α)=fα((ℒ(β)β∈α−)) L(α)=f_α (( L(β)_β∈α^-) ): Case 1 If ℒ(α)= L(α)=in, then every attacker β∈α−β∈α^- is labelled out. According to Def. 4, fαf_α returns in in this situation. Case 2 If ℒ(α)= L(α)=out, then there exists an attacker β∈α−β∈α^- with ℒ(β)= L(β)=in. By Def. 4, fαf_α returns out. Case 3 If ℒ(α)= L(α)=und, then it is not true that all attackers are out and it is also not true that some attackers is inin. Hence, by Def. 4, fαf_α returns und. Thus, ℒ L satisfies the acceptability equation of α for all α∈α∈ A. Consequently, ℒ L is a solution of ℳℱ M_ F, i.e., ℒ∈(ℳℱ) L∈ Sol( M_ F). Given that ℒ L is an arbitrary element of ℒco(ℱ) L_co( F), we conclude that ℒco(ℱ)⊆(ℳℱ) L_co( F) Sol( M_ F) Therefore, (ℳℱ)=ℒco(ℱ) Sol( M_ F)= L_co( F) for every AF ℱ F. ∎ Proof of Theorem 2 Proof. Suppose that ψ is a but-for cause for (α)v(α) under BFT∀BFT_∀. It is a fundamental result in abstract argumentation that every argumentation framework admits at least one complete extension (specifically, the grounded extension is always a complete extension). Consequently, the set of complete extensions is strictly non-empty. In any non-empty domain, universal quantification logically entails existential quantification. Therefore, by Def. 8, ℳ⊧∀ϕ M _∀φ implies ℳ⊧∃ϕ M _∃φ for any arbitrary formula ϕφ. Hence, the counterfactual condition of BFT∀BFT_∀ directly entails the corresponding weak version BFT∃BFT_∃ for the same modified hypothesis ψ′ψ . By an identical line of reasoning, this implication strictly holds from AC2∀mAC2^m_∀ to AC2∃mAC2^m_∃. ∎ Proof of Theorem 3 Proof. Assume that ψ is an atomic hypothesis and that ψ is a but-for cause for (α)v(α) under BFTqBFT_q for some q∈∀,∃q∈\∀,∃\. By Def. 10, ∃ψ′∈/(ψ):ℳℱ⊧q[ψ′]¬(α) for q∈∀,∃.∃ψ ∈ Mod_in/out(ψ): M_ F _q[ψ ] (α) for q∈\∀,∃\. We now verify that ψ satisfies AC2qmAC2^m_q. Choose χ to be the empty conjunction, i.e., a tautology ⊤ . Trivially, (ℳℱ,ℒ)⊩χ( M_ F, L) χ holds for any solution ℒ L. Since ψ′∧χψ χ is logically equivalent to ψ′ψ , the intervened model ℳℱψ′∧χ M_ F^ψ χ is identical to ℳℱψ′ M_ F^ψ . Therefore, ∃ψ′∈/(ψ):ℳℱ⊧q[ψ′∧χ]¬(α)∃ψ ∈ Mod_in/out(ψ): M_ F _q[ψ χ] (α) holds as well. Note that /(ψ) Mod_in/out(ψ) is a subset of (ψ) Mod(ψ), it holds that ∃ψ′∈(ψ):ℳℱ⊧q[ψ′∧χ]¬(α).∃ψ ∈ Mod(ψ): M_ F _q[ψ χ] (α). Hence, ψ meets condition AC2qmAC2^m_q with the same ψ′ψ and the chosen χ=⊤χ= . Conditions AC1AC1 and AC3AC3 are already satisfied because (1) AC1AC1 is given in the condition of BFTqBFT_q where (ℳ,ℒ)⊩ψ∧(α)( M, L) ψ (α), and (2) ψ is an atomic hypothesis, which suggests that ψ is minimal w.r.t set inclusion. Consequently, ψ is an actual cause for (α)v(α) under AC2qmAC2^m_q. ∎ Proof of Theorem 4 Proof. Let ℒ∈(ℳℱψ) L∈ Sol( M^ψ_ F) be a solution of the intervened acceptability model ℳℱψ M^ψ_ F. Take an arbitrary argument α∈α∈ A. Since ℒ L satisfies every equation in ℳℱψ M^ψ_ F, we have ℒ(α)=fαψ((ℒ(β)β∈α−)) L(α)=f^ψ_α (( L(β)_β∈α^-) ) where fαψf^ψ_α is the intervened acceptability equation of α. We prove that ℒ L satisfies the complete labelling conditions for every argument α∈α∈ A. With additional arguments such as α K_α always labeled in, a complete labelling ℒ′ L of the modified AF ℱψ F_ψ could be construct from ℒ L. We prove this by cases. Case 1 For intervened arguments, which suggests there exists ∈v such that (α)∈(ψ)v(α)∈ Sub(ψ), therefore the equation fαψ=f^ψ_α=v. Now, we examine the three possible cases in the modified AF ℱψ F_ψ to show that in every complete labelling of ℱψ F_ψ, α is always labeled v: 1.1 If =v=out, then there is an additional initial argument α K_α attacks α. Given that α∉ K_α ∈ A, α K_α could not be intervened according to Def. 5. So α K_α is initial in ℱψ F_ψ, and α is attacked by an initial argument α K_α, so α is labeled out in every complete labelling of ℱψ F_ψ. 1.2 If =v=in, then all attacks from its parent nodes are removed from ℱψ F_ψ, which suggests α is now an initial argument in ℱψ F_ψ, this leads to the consequence that α is labeled in in every complete labelling of ℱψ F_ψ. 1.3 If =v=und, then all attacks from its parent nodes are removed from ℱψ F_ψ, and a new self-attack is introduced. In every complete labelling of ℱψ F_ψ, α could not be labeled in, since one of its attacker, α, is labeled in; α could not be labeled out either, because in that case all attackers of α are labeled out, which suggests α should be labeled in. So α could only be labeled und in every complete labelling of ℱψ F_ψ. Case 2 For non-intervened arguments, the intervened function fαψ=fαf^ψ_α=f_α, which suggests that the label of α is completely determined by the labels of the attackers β∈α−β∈α^-. Now, examine the three possible cases for ℒ(α) L(α): 2.1 If ℒ(α)= L(α)=in, then every attacker β∈α−β∈α^- must satisfy ℒ(β)= L(β)=out. Hence, condition (i) of a complete labelling holds for α; 2.2 If ℒ(α)= L(α)=out, then there exists β∈α−β∈α^- with ℒ(β)= L(β)=in. Thus, condition (i) of a complete labelling holds for α; 2.3 If ℒ(α)= L(α)=und, then it is neither the case that all are out nor that some attacker is in, which indicates that α must satisfy the condition (i) and (i) of a complete labelling. Since α was arbitrary, ℒ L satisfies the complete labelling conditions for every argument α∈α∈ A. With the additional arguments such as α K_α labeled in, a complete labelling ℒ′ L of modified AF ℱψ F_ψ could be constructed from ℒ L with ℒ(α)=ℒ′(α) L(α)= L (α) holds for α∈α∈ A. ∎ Proof of Proposition 1 Proof. Suppose ψ is a but-for cause for (α)v(α). By Def. 10, this implies that (ℳℱ,ℒ)⊩ψ∧(α)( M_ F, L) ψ (α). Consequently, ψ satisfies the Actuality (AC1AC1). Furthermore, the definition of but-for cause requires ψ to be an atomic hypothesis. As an atomic hypothesis, ψ possesses no proper sub-conjunctions. Therefore, ψ satisfies the Minimality (AC3AC3). ∎ Proof of Proposition 2 Proof. We proceed by case analysis on the structure of the hypothesis ψ. Case 1 Assume ψ is an atomic hypothesis, let ψ=′(β)ψ=v (β). Suppose, for the sake of contradiction, that the set of arguments ψ A_ψ contains at least one argument that is not relevant to α. Because ψ is atomic, β is the only element that is not relevant to α. Since the label of argument is only affected by its parents’ label, if changing the label of β would affect the label of α, then β should be an ancestor of α, which contradicts the fact that β is not relevant to α. Case 2 Assume ψ is a compound hypothesis. Suppose, for the sake of contradiction, that there exists β∈ψβ∈ A_ψ s.t. β is not relevant to α. Consider the proper sub-conjunction ψ′=⋀γ∈ψ∖β(γ)ψ = _γ∈ A_ψ \β\v(γ). If ψ is an actual cause of (α)v(α), then ψ satisfies AC3AC3, which suggests that the proper sub-conjunction ψ′ψ is not an actual cause of (α)v(α). Given that ψ′ψ is a proper sub-conjunction of ψ, if ψ satisfies AC1AC1, then ψ′ψ satisfies AC1AC1. Consequently, the reason ψ′ψ fails to be an actual cause is that it violates AC2AC2. Therefore, there exists no modified hypothesis of ψ′ψ that results in ¬(α) (α). However, because ψ is an actual cause of (α)v(α), there exists a modified hypothesis of ψ that causes ¬(α) (α). The only difference between these two hypotheses is ′(β)v (β). As established, changing the label of β can only affect the label of α if β is an ancestor of α, which contradicts the assumption that β is not relevant to α. ∎ Proof of Proposition 3 Proof. We proceed by contradiction. Suppose ψ′ψ is an actual cause of (α)v(α), then there exists a proper sub-conjunction ψ of ψ′ψ such that ψ is again an actual cause of (α)v(α). This contradicts the fact that ψ′ψ satisfies AC3AC3. ∎ Proof of Proposition 4 Proof. This proposition consists of two statements, which we prove respectively. Proof of 1. This is proved by constructing a hypothesis ψ that satisfies AC1AC1 and AC2∃mAC2^m_∃. Given that α−≠∅α^-≠ and ℒ(α)=in L(α)=in, for all γ∈α−γ∈α^-, it holds that ℒ(γ)=out L(γ)=out. For each γ∈α−γ∈α^-, there exists at least one parent η∈γ−η∈γ^- s.t ℒ(η)=in L(η)=in. Let γ∈α−γ∈α^- be a parent of α, let =η|ℒ(η)=in,η∈γ− C=\η~|~ L(η)=in,η∈γ^-\ be the set and ψ=⋀η∈in(η)ψ= _η∈ Cin(η) be the conjunction. This construction ensures that ψ satisfies AC1AC1. Then we prove that ψ satisfies AC2∃mAC2_∃^m. Let ψ′=⋀η∈out(η)ψ = _η∈ Cout(η). By Def. 9, ψ′ψ is a modified hypothesis of ψ. If the model is intervened by ψ′ψ , then ℒ(γ)≠out L(γ) since no parent of γ is labeled inin. This leads to the fact that ℒ(α)≠in L(α) . So ψ satisfies AC2∃mAC2_∃^m. The constructed ψ is a finite set since the model ℳ M is a finite model. By checking whether there exists a proper sub-conjunction of ψ that satisfies AC1AC1 and AC2∃mAC2_∃^m. If not, then ψ is the actual cause; if so, then again checking whether there exists a proper sub-conjunction. Within finite steps we could end with a ψ′ψ that is a proper sub-conjunction that satisfies AC3AC3, and the ψ′ψ is the actual cause. Proof of 2. The Overdetermination presented in Ex. 6 serves as a counterexample. ∎ Proof of Proposition 5 Proof. According to the restriction on hypotheses in Def. 3, for any atomic formulas (α1),(α2)∈(ψ)v_1( _1),v_2( _2)∈ Sub(ψ), we have α1≠α2 _1≠ _2. Therefore, for any atomic formula (α)∈(ψ)v(α)∈ Sub(ψ), if (α)∈(ψ1)v(α)∈ Sub( _1), then there does not exist any ′∈v such that ′(α)∈(ψ2)v (α)∈ Sub( _2). This shows that for any argument α, if a conjunct ψ1 _1 of ψ intervenes on αi _i, then there is no atomic formula related to αi _i in the other conjunct ψ2 _2. (Denoted as Sub-conclusion 1.) Based on this, we may assume that ψ=(α1)∧(α2)∧⋯∧(αn)ψ=v_1( _1) _2( _2) ·s _n( _n) is an intervention consisting of n (n≥2n≥ 2) atomic formulas. After an arbitrary partition, the two conjuncts are denoted as ψ1 _1 =(α1)∧(α2)∧⋯∧(αj), =v_1( _1) _2( _2) ·s _j( _j), ψ2 _2 =+(αj+1)∧⋯∧(αn), =v_j+1( _j+1) ·s _n( _n), where 1≤j<n1≤ j<n. For an acceptability model ℳℱ=fα∈ M_ F=\f_α\_α∈ A, by Def. 5, we have ℳℱψ=fαψα∈,fαψ=,∃i∈1,⋯,k:α=αi;fα,otherwise. M^ψ_ F=\f^ψ_α\_α∈ A, f_α^ψ= cases v_i,&∃ i∈\1,·s,k\:α= _i;\\[3.0pt] f_α,&otherwise. cases Next, we prove that ℳℱψ=(ℳℱψ1)ψ2=(ℳℱψ2)ψ1 M^ψ_ F=( M _1_ F) _2=( M _2_ F) _1, i.e., for any fα∈ℳℱf_α∈ M_ F, fαψ=(fαψ1)ψ2=(fαψ2)ψ1.f^ψ_α=(f _1_α) _2=(f _2_α) _1. We proceed by case analysis on an arbitrary argument α∈α∈ A. Case 1 For an argument α that does not appear in ψ, i.e., there is no v such that (α)∈(ψ)v(α)∈ Sub(ψ). By Def. 5, fαψ=fαf^ψ_α=f_α. Similarly, since ψ1 _1 and ψ2 _2 are conjuncts of ψ, from (α)∉(ψ)v(α)∉ Sub(ψ) we obtain (α)∉(ψ1)v(α)∉ Sub( _1) and (α)∉(ψ2)v(α)∉ Sub( _2). By Def. 5, (fαψ1)ψ2=fαψ2=fα(f _1_α) _2=f _2_α=f_α. Likewise, (fαψ2)ψ1=fα(f _2_α) _1=f_α. Case 2 For an argument α that appears in ψ1 _1, i.e., there exists v such that (α)∈(ψ1)v(α)∈ Sub( _1). By Def. 5, fαψ1=f _1_α=v. By Sub-conclusion 1, there is no ′v such that ′(α)∈(ψ2)v (α)∈ Sub( _2). Hence, (fαψ1)ψ2=fαψ1=(f _1_α) _2=f _1_α=v. Since ψ1 _1 is a conjunct of ψ and (α)∈(ψ1)v(α)∈ Sub( _1), we have (α)∈(ψ)v(α)∈ Sub(ψ). Then, fαψ=f^ψ_α=v. Thus, fαψ=(fαψ1)ψ2=f^ψ_α=(f _1_α) _2=v. Similarly, (fαψ2)ψ1=(f _2_α) _1=v. Case 3 For an argument α that appears in ψ2 _2, i.e., there exists v such that (α)∈(ψ2)v(α)∈ Sub( _2). By Sub-conclusion 1, there is no ′v such that ′(α)∈(ψ1)v (α)∈ Sub( _1). By Def. 5, fαψ1=fαf _1_α=f_α. Moreover, since (α)∈(ψ2)v(α)∈ Sub( _2), (fαψ1)ψ2=fαψ2=(f _1_α) _2=f _2_α=v. Because ψ2 _2 is a conjunct of ψ and (α)∈(ψ2)v(α)∈ Sub( _2), we have (α)∈(ψ)v(α)∈ Sub(ψ). Then, fαψ=f^ψ_α=v. Thus, fαψ=(fαψ1)ψ2=f^ψ_α=(f _1_α) _2=v. Similarly, (fαψ2)ψ1=(f _2_α) _1=v. In summary, for any argument α, we have fαψ=(fαψ1)ψ2=(fαψ2)ψ1.f^ψ_α=(f _1_α) _2=(f _2_α) _1. Given that ℳℱψ=fαψ M^ψ_ F=\f^ψ_α\, this results in ℳℱψ=(ℳℱψ1)ψ2=(ℳℱψ2)ψ1. M^ψ_ F=( M _1_ F) _2=( M _2_ F) _1. ∎ Proof of Proposition 6 Proof. This proposition consists of two statements, which we prove respectively. Proof of 1. Assume that ψ∈Counter(ℱ,α)ψ ( F,α) with ψ⊆(ℒ)I∪(ℒ)S A_ψ ( L)_I ( L)_S and (αi,α)∈(ℒ)¯+( _i,α)∈ in( L)^+ for all αi∈ψ _i∈ A_ψ. There exists a complete labelling ℒ∈ℒco(ℱ) L∈ L_co( F) s.t.: • ℒ(α)= L(α)=in; • ψ⊆E0 A_ψ E_0 with E0=(ℒ)E_0=in( L); • for every β∈ψβ∈ A_ψ, β∈E0I∪E0Sβ∈ E_0_I∪ E_0_S and (β,α)∈E¯+(β,α)∈ E^+. Now define: RE0:=β∈E0∣(β,α)∈E¯0+andβ∈E0I∪E0S,R_E_0:=\β∈ E_0 (β,α)∈ E_0^+~and~β∈ E_0_I∪ E_0_S\, which is exactly the root reason obtained from the complete extension E0E_0 according to the definition of Root Reasons. The condition above directly yields ψ⊆RE0 A_ψ R_E_0. Hence, the required root reason exists. The converse fails (counterexample). γ1 _1γ2 _2β1 _1β2 _2α Figure 7: ℱ6 F_6: V-Shape Consider the AF ℱ6 F_6 in Fig. 7 with the topic α. The set E=γ1,γ2E=\ _1, _2\ is the only root reason for α, while ψ1=(γ1) _1=in( _1), ψ2=(γ2) _2=in( _2) and ψ3=(α) _3=in(α) are the actual cause for (α)in(α). It is not the case that E⊆ψE A_ψ for i∈1,2,3i∈\1,2,3\. Proof of 2. Assume that ψ∈Counter(ℱ,α)ψ ( F,α) with ψ⊆(ℒ) A_ψ ( L). There exists a complete labelling ℒ∈ℒco(ℱ) L∈ L_co( F) s.t., ℒ(α)= L(α)=in and for every αi∈ψ _i∈ A_ψ, we have ℒ(αi)= L( _i)=in. Let E0∈ℰco(ℱ)E_0∈ E_co( F) with ψ⊆E0 A_ψ E_0 and α∈E0α∈ E_0, hence E0E_0 is admissible and conflict-free. Define: S=β∈E0∣βis relevant toαinℱ.S=\β∈ E_0 β~is relevant to~α~in~ F\. By Proposition 2, each argument in ψ A_ψ is relevant to α; therefore, ψ⊆S A_ψ S. We now show that S is sufficient for α. • Relevance: By construction, we know that every β∈Sβ∈ S is relevant for α. • Conflict-freeness: S⊆E0S E_0 and E0E_0 is conflict-free, so S is conflict-free. • Defence: Take any β∈S∪αβ∈ S∪\α\. – If β∈Sβ∈ S, then β∈E0β∈ E_0 and E0E_0 is admissible. For every attacker δ∈β−δ∈β^-, there exists γ∈E0γ∈ E_0 with (γ,δ)∈ℛ(γ,δ)∈ R. Because β is relevant to α, there exists a directed path from β to α. Extending this path via (δ,β)∈ℛ(δ,β)∈ R and (γ,δ)∈ℛ(γ,δ)∈ R yields a directed path from γ to α. Thus γ is relevant to α and consequently γ∈Sγ∈ S. – If β=αβ=α, the same argument applies. Therefore, every attacker of β is counter-attacked by an argument in S, i.e., S defends S∪αS∪\α\. Thus, S satisfied the three conditions, the set E=S∪αE=S∪\α\ belongs to Suf(ℱ,α)Suf( F,α). Since ψ⊆S⊆E0 A_ψ S E_0, the required sufficient explanation exists. Failure of the converse. Consider the AF in Fig. 4 with the topic η. The set α,η∈Suf(ℱ,η)\α,η\ ( F,η); similarly, β,η∈Suf(ℱ,η)\β,η\ ( F,η). Take the sufficient explanation E=α,ηE=\α,η\. There exists no ψ∈Counter(ℱ,α)ψ ( F,α) with ψ⊆(ℒ) A_ψ ( L) and ψ⊆E∖η A_ψ E \η\, because for the candidates ψ1=(α)∧(β) _1=in(α) (β) and ψ2=(η) _2=in(η), it holds that ψi⊈α A_ _i \α\ for i∈1,2i∈\1,2\. Hence the inclusion ψ⊆E∖η A_ψ E \η\ is impossible for this E. This demonstrates that the converse of the statement does not hold in general. ∎