Revisiting Unrestricted Rebut and Preferences in Structured Argumentation.

1 Introduction

Structured argumentation offers a formal method for defeasible reasoning. Many approaches distinguish between strict and defeasible inference rules. Unlike strict rules, a defeasible rule warrants the truth of its conclusion only provisionally: it is retracted in case good counter-arguments are encountered. Different types of argumentative attacks can be distinguished. E.g., if an argument a concludes the contrary of an argument b it is said to rebut b. In many formalisms, such as ASPIC+ [Modgil and Prakken, 2013; 2014], rebut is restricted in such a way that an argument b cannot be rebutted if its conclusion is obtained by a strict rule. In [Caminada et al., 2014], it has been argued that especially in dialectical contexts unrestricted rebut is more natural. As a consequence, the system ASPIC- has been proposed in which rebut is unrestricted.

In [Caminada and Amgoud, 2007] several rationality postulates have been proposed. E.g., the output of an argumentation system should be consistent and closed under the strict rules. For multi-extension semantics (e.g., preferred and stable semantics), ASPIC- violates these postulates unlike ASPIC+ (given some restrictions) [Prakken, 2011]. Thus, unrestricted rebut can lead to undesired behaviour and one has to be careful when devising systems utilizing it. The situation is different for the single-extension grounded semantics where both ASPIC+ and ASPIC- are well-behaved relative to the postulates in [Caminada and Amgoud, 2007].

∗We thank M. Beirlaen, M. Caminada and the anonymous reviewers for helpful comments. Our research is supported by the Alexander von Humboldt-Foundation.

However, as shown in this article, ASPIC- does not satisfy other standards such as Crash-Resistance and NonInterference. Ideally, a reasoning system should not lose consequences if irrelevant information is added to the knowledge base. As demonstrated in [Wu, 2012] for ASPIC, the lack of Crash-Resistance and Non-Interference is especially threatening if the underlying strict rules are domain-independent. This is typically the case if the strict rules are induced by an underlying logic such as classical logic (in short, CL). Given an inconsistent knowledge base and strict rules such as logical explosion, for any formula an argument with a contrary conclusion can be constructed.

So far, there are not many results that establish CrashResistance and Non-Interference for systems in the ASPICfamily. An exception is [Wu, 2012] where Crash-Resistance is established for ASPIC Lite, where priorities over defeasible rules are not taken into account. In [Grooters and Prakken, 2016] a systemwith restricted rebut is introduced that avoids logical explosion by using a sub-classical logic as a base logic. For any completeness-based semantics a weakened version of Crash-resistance and Closure are shown for total pre-orders expressing priority relations between the defeasible rules. For multi-extension semantics a counter-example for full Crash-Resistance is provided.

For approaches with unrestricted rebut, to the best of our knowledge, there have been no investigations into CrashResistance or Irrelevance. This paper therefore answers the following pertinent question: is it possible to define a framework for structured argumentation that gives a sensible output when the strict rules are domain-independent? We will answer this question positively by defining the system ASPIC⊖. We consider total pre-orders expressing priority relations between the defeasible rules. To the best of our knowledge, this is the first such result for frameworks in the ASPIC-family.

2 The ASPIC-family

A well-known, general and popular family of frameworks for structured argumentation is the ASPIC-family. In ASPIC arguments are constructed using an argumentation system. 1

1 In this paper we will, due to spatial restrictions, omit several features of the original ASPIC+ framework of [Prakken, 2011], such as defeasible premises, issues, undercutting and undermining attacks.

Definition 1. An Argumentation System (AS) is a tuple AS = (L, S,D,K, ,⩽) consisting of:

• a formal language L
• a set of strict rules S ⊆ 2L ×L of the form A1, . . . , An → B
• a set of defeasible rules D ⊆ 2L × L of the form A1, . . . , An ⇒ B.
• an S-consistent 2 set of strict premises K ⊆ L.
• a contrariness function from L to L. 3
• a preorder ⩽ over D.

A1, . . . ,An are called the antecedents and B is called the consequent of A1, . . . , An → B resp. A1, . . . , An ⇒ B.

Definition 2. Let AS = (L, S,D,K, ,⩽) be an argumentation system. An argument a is one of the following:

• a = 〈A〉 where A ∈ K conc(a) = A, Sub(a) = {a}, DefR(a) = ∅
• a = 〈a1, . . . , an → B〉 where a1, . . . an (with n ⩾ 0) are arguments s.t. there is a strict rule conc(a1), . . . conc(an) → B ∈ S conc(a) = B, Sub(a) = {a} ∪ ⋃ni=1 Sub(ai), and DefR(a) = ⋃ni=1 DefR(ai).
• a = 〈a1, . . . , an ⇒ B〉 where a1, . . . an (with n ⩾ 0) are arguments s.t. there is a defeasible rule conc(a1), . . . conc(an) ⇒ B ∈ D conc(a) = B, Sub(a) = {a} ∪ ⋃ni=1 Sub(ai), DefR(a) = {conc(a1), . . . conc(an) ⇒ B} ∪ ⋃ni=1 DefR(ai).

By Arg(AS) we denote the set of arguments that can be built from AS. An argument a will be called defeasible if DefR(a) ̸= ∅ and strict otherwise. We lift DefR to sets of arguments as usual: DefR({a1, . . . , an}) = ⋃ni=1 DefR(ai).

Example 1. The paradigmatic example for generating a set of strict rules SCL by an underlying logic is to use CL: A1, . . . ,An → A ∈ SCL iff {A1, . . . ,An} ⊢CL A. Contrariness is defined by A = ¬A. We will use this system as a guiding example throughout this paper.

Let AS1 = (L, SCL,D1 = {⊤ ⇒2 ¬p ∨ ¬q, ⊤ ⇒1 p, p ⇒1 q}, ∅, ,⩽). In this and the following examples, the natural numbers in the subscripts of ⇒ are used to express the priority ordering over D, i.e. (A1, . . . ,An ⇒i B) ⩽ (A′1 , . . . ,A′m ⇒j B′ ) iff i ⩽ j. Here are some arguments in Arg(AS1):

a1: ⊤⇒2 ¬p ∨¬q a2: ⊤⇒1 p a3: a2 ⇒1 q a4: a1, a2 →¬q a5: a2, a3 → p ∧ q a6: a1, a3 →¬p

2K is S-inconsistent iff there is a derivation from K using S for A and A (for some A ∈ L). K is S-consistent if it is not Sinconsistent.

3 In the context of ASPIC+ usually associates formulas with a set of contrary formulas. To simplify the presentation we opt here for the simpler variant where each formula is associated with a unique contrary formula.

2.1 Attacks and Defeats

Definition 3. Where a, b ∈ Arg(AS), a unrestrictedly rebuts b (in symbols: aUrReb) iff conc(a) = conc(b) and b is defeasible.

Definition 4. Where a, b ∈ Arg(AS), a restrictedly rebuts (in symbols: aReReb) b = 〈b1, . . . , bn ⇒ B〉 iff conc(a) = B.

It is clear that for any arguments a and b, if aReReb then aUrReb. The other direction does not hold in general, as witnessed by the fact that in Example 1, where a′2 = a2 → ¬¬p, we have a2UrRea6 but not a2ReRea6.

When two arguments conflict, one of the arguments may defeat the other due to its higher priority. To account for defeat via priorities, we lift our order ⩽ on D to an order on arguments via the weakest link lifting(see e.g. [Modgil and Prakken, 2013]): where a, b ∈ Arg(AS), a ⪯ b iff DefR(b) = ∅ or ∃α ∈ DefR(a) s.t. ∀β ∈ DefR(b): α ⩽ β.

Definition 5. Where a, b ∈ Arg(AS) and Att ∈ {ReRe, UrRe}: a defeats b iff there is a c ∈ Sub(b) s.t. aAttc and c ⪯ a. We write (a, b) ∈ Att⪯(Arg(AS)).

Where Arg(AS) is clear from the context, we will often just write Att⪯ instead of Att⪯(Arg(AS)).

2.2 Grounded Semantics

Definition 6. Where Att ∈ {ReRe, UrRe}, an argumentation framework (AF) for an argumentation theory AS is the pair (Arg(AS), Att⪯(Arg(AS))).

Given an AF, we can apply Dung's acceptability semantics [Dung, 1995] for evaluating arguments.

Definition 7. Let AF = (Arg(AS), Att⪯) be an AF, A ⊆ Arg(AS) and a ∈ Arg(AS). a is acceptable w.r.t. A (or, A defends a) iff for all b s.t. (b, a) ∈ Att⪯ there is a c ∈ A s.t. (c, b) ∈ Att⪯. We write Acc(A) for the set of all acceptable arguments w.r.t. A. A is conflict-free iff there are no a, b ∈ A s.t. (a, b) ∈ Att⪯. A is a complete extension iff it is conflictfree and Acc(A) = A. The minimal complete extension is the grounded extension, written G(AF ).

Remark 1. The grounded extension has the following fixed point characterization: G(AF) = ⋃i≥0 Gi where G0 = Acc(∅) and Gi+1 = Acc(Gi) (i ≥ 0).

We define a consequence relation based on the grounded extension for AFs as follows.

Definition 8. Where AF = (Arg(AS), Att⪯) is an AF for AS. AS |∼ Att⪯ A iff there is an argument a ∈ G(AF) with conc(a) = A.

3 Rationality Postulates

In [Caminada and Amgoud, 2007; Caminada et al., 2011] desirable properties for argumentation-based consequence relations |∼ are defined:

Postulate 1. |∼ satisfies Direct Consistency if for no argumentation system AS, AS |∼A and AS |∼A (for some A ∈ L).

Postulate 2. |∼ satisfies Closure if for every argumentation system AS, if AS |∼Ai for 1 ⩽ i ⩽ n and B follows via the strict rules of AS from {A1, . . . , An} then AS |∼B.

Postulate 3. |∼ satisfies Indirect Consistency if for no argumentation system AS with strict rules S, there are A1, . . . , An s.t. AS |∼Ai for 1 ⩽ i ⩽ n and {A1, . . . , An} is S-inconsistent.

Where ∆ ⊆ L, let Atoms(∆) be the set of all atoms occurring in ∆.

Postulate 4. |∼ satisfies Non-Interference if for any two argumentation systems AS = (L, S,D,K, ,⩽) and AS′ = (L, S,D′ ,K′ , ,⩽′ ), where K ∪ K′ is S-consistent, (Atoms(D) ∪ Atoms(K)) ∩ (Atoms(D′ ) ∪ Atoms(K′ )) = ∅, we have: AS′ |∼A iff AS+ |∼A where AS+ = (L, S, D ∪ D′ ,K ∪ K′ , ,≤+) and Atoms(A) ⊆ Atoms(AS′ ) (where ≤+ is such that ≤ [≤′ ] is the restriction of ≤+ to D × D [D′ × D′ ]). 4

4 ASPIC-, Non-Interference, and Closure: a Dilemma

In [Caminada et al., 2014] it is shown that |∼ UrRe , the consequence relation associated with ASPIC- under the grounded semantics, satisfies Closure and both Consistency postulates. However, if the strict rules are defined on the basis of CL (see Ex. 1) there are counterexamples to Non-Interference.

Example 2. Let AS2 = (L, SCL,D2 = {⊤⇒ p}, ∅, ,D2× D2) and AS3 = (L, SCL,D3 = {⊤ ⇒ p,⊤ ⇒ s,⊤ ⇒ ¬s}, ∅, ,D3 ×D3), where SCL and are defined as in Ex. 1. Note that a = ⊤ ⇒ p ∈ G((Arg(AS2), UrRe)) but since b = 〈⊤ ⇒ s〉, 〈⊤ ⇒ ¬s〉 → ¬p ∈ Arg(AS3) and b defeats a, a ̸∈ G((Arg(AS3), UrRe)).

A solution to problems of this kind has been proposed in [Wu, 2012] for ASPIC+ (so using restricted rebut) and for trivial preference orderings over the defeasible rules (so where ≤ = D × D). Non-Interference is ensured there by filtering out inconsistent arguments like b in Ex. 2, i.e., arguments with inconsistent support sets.

A first proposal to ensure Non-Interference for |∼ UrRe would be thus to filter out inconsistent arguments. However, in ASPIC- frameworks with a non-trivial priority ordering this leads to violations of Closure as shown in the following example:

Example 3 (Ex. 1 continued). Suppose the inconsistent a6 is removed from the AS while the consistent arguments a1, a2, a3, a4, a5 remain. Since a5 ⪯ a1 while a1 ̸⪯ a5, with a1 the argument a5 can be defeated but not vice versa. Thus, a1 is in the grounded extension G while a5 /∈ G. Moreover, the potential defeater a6 of a2 is removed, thus a2 ∈ G. However, a3 and a4 keep each other out of the grounded extension. Hence, we get the consequences ¬p∨¬q and p while ¬q does not follow.

4 A related rationality standard is Crash Resistance. It follows from Non-Interference under some very weak criteria on the strict rule base (cf. [Caminada et al., 2011]).

We analyse this example as follows: a1 = ⊤ ⇒2 ¬p ∨ ¬q offers a strong reason against the reasoning path taken by a3 = 〈⊤ ⇒1 p〉 ⇒1 q since it expresses that at least one of the two conclusions of the two subarguments a2 = ⊤ ⇒1 q and a3 has to be false. In other words, someone arguing for a3 is committed to both p and q while someone arguing for a1 expresses that this commitment is mistaken. In view of this, one would expect a1 to defeat a3. Consequently, since a1 is in the grounded extension, it would defend a4 = a1, a2 ⇒1 ¬q from its attacker a3. Thus, also a4 would be grounded and we would get Closure.

Our analysis motivates to generalize Unrestricted Rebut to allow for attacks like the one of a1 on a3 as follows: a attacks b in (the conclusions of) some of its subarguments b1, . . . , bn iff conc(a) expresses that conc(b1), . . . , conc(bn) cannot all hold at the same time. We will do so in the next section.

5 Generalizing Rebut: ASPIC⊖

We will now define ASPIC⊖, a framework for structured argumentation that satisfies all four rationality postulates above while allowing for unrestricted rebut. Recall that we faced the following dilemma in Section 4. Unrestricted rebut leads to a violation of Non-Interference (see Ex. 2). While removing inconsistent arguments from AFs remedies this shortcoming it gives rise to a violation of Closure (see Ex. 3). We will now show that we can have our cake and eat it: inspired by our analysis of Ex. 3 we propose a generalization of unrestricted rebut which allows for an argument to attack another one if its conclusion claims that a subset of the commitments of the attacked argument are not tenable together.

To formalize this idea we introduce two notational conventions. First, we assume that a lifting of the contrariness operator : L→L to (finite) sets of formulas : ℘fin(L)\∅ →L is available. For instance, one may express {A1, . . . ,An} by means of disjunction ∨ni=1 Ai or by means of conjunction ∧ni=1 Ai. Second, we define C(a) =df {conc(b) | b ∈ Sub(a)} to be the set of the conclusions of subarguments of a.

Definition 9. Where a, b ∈ Arg(AS) : a gen-rebuts b (in symbols: aGeReb) iff b is defeasible and conc(a) = ∆ for some ∆ ⊆ C(b).

Definition 10. (a, b) ∈ GeRe⪯ iff there is a c ∈ Sub(b) s.t. aGeRec and c ⪯ a.

Clearly, if aUeReb then aGeReb while the other direction does not hold in general.

The consequence relation for generalized rebuttal |∼ GeRe is defined as in Definition 8.

In Example 3, note that now a1 defeats a3 and consequently, AS |∼ GeRe¬p. In fact, as is shown in the next section all four rationality postulates hold for |∼ GeRe given some requirements on the strict rules that are met by many potential base logics or domain dependent rule bases.

6 Rationality Standards and ASPIC⊖

When proving the rationality postulates for ASPIC⊖, we will suppose that the set of strict rules S of a given AS satisfies Transposition (T), Resolution (R) and Cut (C) (where ∆′ ⊆ ∆ and Θ′ ⊆ Θ are finite sets of formulas):

• T: (∆\∆′ ) ∪Θ′ → (Θ \Θ′ ) ∪∆′ if ∆→Θ.
• R: ∆∪∆∪Θ→Θ.
• C: ∆∪Θ→A if ∆∪ {D} →A and Θ→D.

We suppose that there is a conjunction symbol in the language that works in the usual way: e.g., ∆ → A iff ∧ ∆ → A; ∆ → ∧ ∆ and ∧ ∆ → A where A ∈ ∆ are available rules.

The generality of these requirements ensure that our framework can be instantiated by a broad class of rule bases. For example, a wide variety of Tarski consequence relations, such as CL, intuitionistic logic and many modal logics, can be used to generate a set of strict rules. Likewise, closing a set of domain specific rules under the properties defined above generates such a strict rule base. Note that Transposition was already required in e.g. [Prakken, 2011] and [Caminada et al., 2014].

Example 4. For the instantiation SCL in terms of CL proposed in Ex. 1 the requirements read:

• T: If A1, . . . ,An → ¬B1 ∨ . . . ∨ ¬Bm ∈ SCL then A1, . . . , Al, Bk, . . . , Bm → ¬Al+1∨. . .∨¬An∨¬B1∨ . . . ∨ ¬Bk-1 ∈ SCL.
• R: A1, . . . , An, ¬A1 ∨ . . . ∨ ¬An ∨ ¬B1 ∨ . . . ∨ ¬Bm → ¬B1 ∨ . . . ∨ ¬Bm ∈ SCL.
• C: If A1, . . . ,An →A∈SCL andB1, . . . ,Bm →Ai∈SCL then A1,.., Ai-1, Ai+1,.., An, B1,.., Bm→A∈SCL.

As noted in Section 4, Non-Interference fails for unrestricted rebut in the presence of inconsistent arguments. In contrast, for generalized rebut they are harmless as the grounded extension attacks them:

Fact 1. Where AS = (L, S,D,K, ,≤), AF = (Arg(AS), GeRe⪯), S is closed under T and C, and b ∈ Arg(AS) is S-inconsistent (i.e., C(b) is S-inconsistent), b is defeated by 〈→ C(b)〉 ∈ G0(AF ).

Proof. Since b is inconsistent, ∃A ∈ L s.t. C(b) → A, C(b) → A ∈ S. By T, A → C(b) ∈ S. By C, C(b) → C(b) ∈ S. By T, a = 〈→ C(b)〉 ∈ Arg(AS). As a has no attackers, a ∈ G0(AF).

The four rationality standards hold for |∼ GeRe :

Theorem 1. |∼ GeRe satisfies Direct Consistency, Closure, Indirect Consistency and Non-Interference for any AS = (L, S,D,K, ,≤) such that S is closed under T, R and C and ≤ is a total preorder.

Proof. Direct Consistency follows from G(AF) being conflict-free. Closure follows from Lemma 2 (proven below). Indirect Consistency is a corollary of Direct Consistency and Closure. Non-Interference follows with Fact 5 and Lemmas 3 and 4 (proven below). We show one direction. Suppose AS′ |∼ GeReA. Thus, ∃a ∈ G(AF ′ ) s.t. conc(a) = A. By Fact 5, cut(a) ∈ G(AF ′ ). By Lemma 3, cut(a) ∈ G(AF +). Thus AS+ |∼ GeReA.

The following proofs are for a given AF with underlying argumentation system AS = (L, S,D,K, ,≤) that satisfies the requirements of Theorem 1. In order to avoid clutter, we will in the following sometimes write a1, . . . , an instead of {conc(a1), . . . , conc(an)}. Furthermore, we will say a defeats b in {b1, . . . , bn} if a defeats b and conc(a) = b1, . . . , bn for b1, . . . , bn ∈ Sub(b).

Some proofs of the following auxiliary results are omitted due to space restrictions:

Proof. We show the inductive step (k ⇒ k + 1) of the inductive proof. Suppose b defeats a′ in some ∆. If a′ /∈ ∆ then b defeats a and is thus defeated by Gk. Else by Fact 2 b′ = 〈b → (∆∪ {a}) \ {a′ }〉 defeats a. Thus, some c ∈ Gk defeats b′ in some Λ. If b′ /∈ Λ, c′ also defeats b. Otherwise with Fact 2 c′ = 〈c → (Λ ∪ {b}) \ {b′ }〉 defeats b.

• Fact 3. 1. If b = 〈b1, . . . , bn → B〉 and Gk defeats b then it also defeats b in some ∆ for which b /∈ ∆.
• If a ∈ Gk, b = 〈a1, . . . , an → A〉 ∈ Arg(AS) where a1, . . . , an ∈ Sub(a), then b ∈ Gk.
• Where a ∈ G and a attacks b then G defeats b.

Proof. Ad 1. Suppose c ∈ Gk defeats b in ∆ and b ∈ ∆. By Fact 2 and Lemma 1 c′ = 〈c → (∆ ∪ {b1, . . . , bn}) \ {b}〉 ∈ Gk. Clearly, c′ defeats b. Ad 2. Suppose some c defeats b in ∆. If b /∈ ∆ then c also defeats a and thus Gk-1 defeats b. Else by Fact 2 c′ = 〈c → ∆∪ {a1, . . . , an}) \ {b}〉 defeats a. Again, Gk-1 defeats c′ and by item 1 it also defeats b. Ad 3. Omitted due to space.

Proof. We prove this by an induction on π(a) = n + ∑ni=1 κ(ai) where κ(ai) is the minimal j for which ai ∈ Gj . We show the inductive step. We first consider defeaters b of a in some ∆ where a /∈ ∆. Let ∆i = ∆ ∩ Sub(ai) where 1 ≤ i ≤ n. Suppose first that some ∆i = ∅. Wlog suppose ∆1 ∪ . . . ∪∆k = ∅ while each ∆j ̸= ∅ where k < j ≤ n. Let dj = 〈∆j → ∧ ∆j〉. By Fact 3.2 dj ∈ Gκ(aj). By the IH, d′ = 〈dk+1, . . . , dn → c〉 ∈ G. Since d′ attacks c, by Fact 3.3, G defeats c.

Suppose now that for every 1 ≤ i ≤ n, ∆i ̸= ∅. Suppose wlog that a1 ∈ min⪯({a1, . . . , an}). Thus, c′ = 〈c,∆2, . . . ,∆n → ∆1〉 defeats a1. Hence, there is a e ∈ Gκ(a1)-1 that defeats c′ in some Λ. By Fact 3.1 we can assume that c′ /∈ Λ. Let Λj = Λ ∩ Sub(aj) for each 2 ≤ j ≤ n and Λc = Λ ∩ Sub(c). Let lj = 〈Λj → ∧ Λj〉 if Λj ̸= ∅ and otherwise lj is the empty string. By Fact 3.2, lj ∈ Gκ(aj) whenever Λj ̸= ∅. Let e′ = 〈e, l2, . . . , ln → Λc〉. By the IH, e′ ∈ G. Since e′ attacks c, G defeats c by Fact 3.3.

Consider a b defeating a in ∆ s.t. A ∈ ∆. By Fact 2 we have b′ = 〈b → (∆∪ {a1, . . . , an}) \ {a}〉 defeating a. Above we have shown that G defeats b′ . By Fact 3.1 G defeats b.

Remark 2. Any argument a ∈ Arg(AS) can be transformed into an argument cut(a) such that: any argument b ∈ Sub(cut(a)) of the form b = 〈b1, . . . , bn → B〉 is such that each bi is either of the form 〈Bi〉 or of the form 〈b′1 , . . . , b′m ⇒ Bi〉, DefR(cut(a)) = DefR(a), and C(cut(a)) ⊆ C(a).

The way to achieve this is to apply C "as much as possible". That means for any subargument b = 〈b1, . . . , bn → B〉 of a for which some bi is of the form 〈b′1 , . . . , b′m → Bi〉 we replace b in a by b′ = 〈b1, . . . , bi-1, b′1 , . . . , b′m, bi+1, . . . , bn → B〉.

Fact 4. If b is S-consistent and b′ = 〈b → B〉 ∈ Arg(AS), then b′ is S-consistent.

Fact 5. If a ∈ G(AF) then also cut(a) ∈ G(AF).

In the remainder of this section, let AS = (L, S,D,K, ,≤ ), AS′ = (L, S,D′ ,K′ , ,≤′ ), and AS+ = (S,D ∪D′ ,K ∪ K′ , ,≤+) be as in Postulate 4 where AF, AF ′ and AF + are the corresponding argumentation frameworks.

Fact 6. Where a ∈ Arg(AS+)\Arg(AS′ ) is S-consistent and Atoms(conc(a)) ⊆ Atoms(K′ ∪D′ ), there is a c ∈ Arg(AS′ ) for which C(c) ⊆ C(a), DefR(c) = DefR(a) ∩ D′ and conc(c) = conc(a).

Lemma 3. cut(a) ∈ G(AF +) if cut(a) ∈ G(AF ′ ).

Proof. Let a′ = cut(a). We prove by induction that if a′ ∈ Gi(AF ′ ) then a′ ∈ G(AF +). We show the inductive step. Let a′ ∈ Gi+1(AF ′ ). By Fact 1, a′ is S-consistent. Suppose some b ∈ Arg(AS+) defeats a′ in {a1, . . . , an}. If b is Sinconsistent it is, by Fact 1, attacked by G0(AF +) and hence a′ is defended from b. Suppose now b is S-consistent.

If Atoms(conc(a′ )) ̸⊆ Atoms(AS′ ) then a′ is of the form a′ = 〈c1, . . . , cm → A〉. If now additionally a′ = ai for some 1 ≤ i ≤ n, say wlog a′ = a1, let b′ = 〈b → c1, . . . , cm, a2, . . . , an〉 which is in Arg(AS+) by Fact 2.

Else let b′ = b. By Fact 4, b′ is S-consistent. By Fact 6, there is a c ∈ Arg(AS′ ) s.t. b′ ⪯′ c, C(c) ⊆ C(b), and conc(c) = conc(b′ ). Since c defeats a′ and a′ ∈ Gi+1(AF ′ ) there is a d ∈ Gi(AF ′ ) that defeats c in some {d1, . . . , dk}. By the inductive hypothesis d ∈ G(AF +). Since C(c) ⊆ C(b′ ), d also defeats b′ . If conc(b′ ) is not among conc(d1), . . . , conc(dk), d defeats b and hence defends a from b. Otherwise suppose wlog, conc(d1) = conc(b′ ). By Fact 2, d′ = 〈d → b, d2, . . . , dk〉 ∈ Arg(AS′ ). By Lemma 1, d′ ∈ Gi(AF ′ ). Since d′ defeats b it defends a′ . Altogether we have shown that a′ is defended by G(AF +) and thus a′ ∈ G(AF +).

Lemma 4. Where Atoms(conc(a)) ⊆ Atoms(D′ ∪ K′ ), if a ∈ Gi(AF +) then there is an a′ ∈ Gi(AF ′ ) with conc(a′ ) = conc(a), C(a′ ) ⊆ C(a) and DefR(a′ ) = DefR(a) ∩ D′ .

The proof is similar to the one of Lemma 3.

7 FutureWork

In future research we plan to investigate how to overcome some of the restrictions imposed on the framework of this paper. This includes, among others, to study non-total orders on the priorities for the defeasible rules and other lifting principles such as last link, to combine generalized rebut with other attack rules such as undercut, and to study variants of generalized rebut. Generalized rebut in its current form allows for attacks that some may deem counter-intuitive. E.g., given the arguments a = 〈⊤ ⇒3 p〉 ⇒1 q and b = ⊤ ⇒2 ¬p, we have b GeRe⪯ a simply since a ⪯ b. Of course, c = ⊤ ⇒3 p defeats b and defends a, as desired. Nevertheless, on intuitive grounds one may consider b defeating a as counter-intuitive since the subargument c of a (the conclusion of which b attacks) is stronger than b. An alternative would thus be to define a gen-rebuts b in the conclusions of subarguments b1, . . . , bn of b iff (I) conc(a) = {conc(b1), . . . , conc(bn)} and (II) bi ⪯ a for all (or some) 1 ≤ i ≤ n. We will investigate such variants in the future. This variant also turns out more promising when studying other lifting principles such as last link.