Reasoning by Cases in Structured Argumentation

TL;DR

This paper extends the ASPIC+ framework for structured argumentation to incorporate reasoning by cases, enabling defeasible arguments with disjunctive conclusions and highlighting the complexities of defeasible reasoning with disjunctive information.

Contribution

It introduces a novel extension to ASPIC+ for reasoning by cases, providing a formal approach to handle disjunctive information in defeasible argumentation.

Findings

Different results from other non-monotonic logic approaches

Formalization of reasoning with disjunctive information is complex

Raises new questions about defeasible reasoning subtleties

Abstract

We extend the $ASPIC^+$ framework for structured argumentation so as to allow applications of the reasoning by cases inference scheme for defeasible arguments. Given an argument with conclusion `$A$ or $B$', an argument based on $A$ with conclusion $C$, and an argument based on $B$ with conclusion $C$, we allow the construction of an argument with conclusion $C$. We show how our framework leads to different results than other approaches in non-monotonic logic for dealing with disjunctive information, such as disjunctive default theory or approaches based on the OR-rule (which allows to derive a defeasible rule `If ($A$ or $B$) then $C$', given two defeasible rules `If $A$ then $C$' and `If $B$ then $C$'). We raise new questions regarding the subtleties of reasoning defeasibly with disjunctive information, and show that its formalization is more intricate than one would presume.

Equations

$${\phi }_1\vee \dots \vee {\phi }_n,{\phi }_1\supset \psi ,\dots ,{\phi }_n\supset \psi ⊢\psi$$

$${\phi }_1\vee \dots \vee {\phi }_n,{\phi }_1\Rightarrow \psi ,\dots ,{\phi }_n\Rightarrow \psi \mid \sim \psi$$

$$\begin{array}[]{l@{\ \ \ \ \ \ \ \ }l}A_{0}=\langle\langle\top\rangle\Rightarrow p\rangle&A_{2}=\langle A_{0},A_{1}\rightarrow\lnot s\rangle\\[4.30554pt] A_{1}=\langle A_{0}\Rightarrow\lnot p\rangle&A_{3}=\langle\langle\top\rangle\Rightarrow s\rangle\\ \end{array}$$

$$\begin{gathered} \mathtt{Att}(\mathrm{AT})\subseteq (\mathtt{Arg}(\mathrm{AT})\times \mathtt{Arg}(\mathrm{AT})) \\ \cup (\mathtt{Arg}(\mathrm{AT})\times \mathtt{HArg}(\mathrm{AT})) \\ \cup (\mathtt{HArg}(\mathrm{AT})\times \mathtt{HArg}(\mathrm{AT})) \end{gathered}$$

$$\mathrm{SAF}\mid \sim \varphi \text{mbox}iff{\mathrm{SAF}}^{\prime }\mid \sim \varphi .$$

$$\frac{\varphi :{\psi }_1,\dots ,{\psi }_n}{{\gamma }_1\mid \dots \mid {\gamma }_m}$$

$${\Delta }_3=\left\{\frac{p:q\vee r}{q\mid r},\frac{q:s}{s},\frac{s:v}{v},\frac{r:v}{v},\frac{t:\neg s}{\neg s},p,t\right\}$$

$$\frac{\psi \Rightarrow \varphi {\psi }^{\prime }\Rightarrow \varphi }{\psi \vee {\psi }^{\prime }\Rightarrow \varphi }[\mathrm{OR}]$$

$$\frac{\psi \Rightarrow \varphi {\psi }^{\prime }\Rightarrow {\varphi }^{\prime }}{\psi \vee {\psi }^{\prime }\Rightarrow \varphi \vee {\varphi }^{\prime }}[\mathrm{gOR}]$$

$$A_3=⟨⟨⟨p\Rightarrow q\vee r⟩\Rightarrow s\vee v⟩\Rightarrow v\vee v⟩\to v$$

$$†A_1,\dots ,†A_{n^{\prime }-1},†B_1,\dots ,†B_{k-1}⊢\neg †B_k$$

$$†A_1,\dots ,†A_{n^{\prime }-1},†B_1,\dots ,†B_{k-1}⊬\perp$$

$$†A_1,\dots ,†A_{n^{\prime }-1},†B_1,\dots ,†B_{k-1}⊢\neg \mathtt{Conc}(B_k)$$

$$†A_1,\dots ,†A_{n^{\prime }-1},†B_1,\dots ,†B_{k-1}⊢\neg \mathtt{Conc}(B_{j_i})$$

Full text

1 Introduction

When formulated in terms of the material implication connective ‘$\supset$’, the pattern of reasoning by cases is valid in classical logic:

[TABLE]

Many formalisms of non-monotonic logic likewise allow defeasible applications of reasoning by cases, where a formula ‘$\varphi\Rightarrow\psi$’ reads ‘If $\varphi$, then normally/usually/probably $\psi$’:

[TABLE]

In the context of formal argumentation, it is natural to include a more general argumentative version of the RBC rule. Relative to a knowledge base this rule would allow the construction of an rbc- argument $C$ with conclusion $\psi$ given (i) an argument $A$ with the disjunctive conclusion $\varphi_{1}\vee\ldots\vee\varphi_{n}$, and (ii) for each $i\in\{1,\ldots,n\}$, an argument $B_{i}$ with conclusion $\psi$ based on an extended knowledge base including $\varphi_{i}$. To the best of our knowledge, no such rule has yet been introduced and studied in the context of formal argumentation. The aim of this paper is to do exactly this, and to investigate the nature of ‘argumentation by cases’.

For defining rbc-arguments and attacks on rbc-arguments, we will extend the $ASPIC^{+}$ framework [8]. $ASPIC^{+}$ is a framework for instantiating abstract argumentation frameworks as conceptualized by Dung [4]. We introduce abstract argumentation frameworks in Section 2, and define our formalism in Section 3. Our approach is limited in at least two ways. First, we do not allow for nested or iterated rbc-arguments. Second, we do not yet take into account priorities assigned to arguments, nor do we include undercutting attacks. The removal of these limitations is left for future work.

The present approach raises new questions regarding the nature of arguing by cases. For instance, what happens if in the rbc-argument $C$ one of the arguments $B_{i}$ is rebutted by an independent argument? Is this a sufficient condition for rejecting argument $C$? After all, there are $n-1$ other defeasible ‘paths’ leading to $C$’s conclusion. Our formalism implements a cautious rationale according to which a successful rebut on one of its paths is indeed sufficient for rejecting an rbc-argument. In Section 4 we show how this approach leads to intuitive outcomes different from those obtained by other formalisms in non-monotonic logic.

2 Abstract argumentation

A Dung-style abstract argumentation framework (AF) is a pair $({\tt Arg},\tt{Att})$ where ${\tt Arg}$ is a set of arguments and $\tt{Att}\subseteq{\tt Arg}\times{\tt Arg}$ is a binary relation of attack. Relative to an AF, Dung defines a number of extensions – subsets of ${\tt Arg}$ – on the basis of which we can evaluate the arguments in ${\tt Arg}$.

Definition 1** (Defense).**

A set of arguments $\mathcal{X}$ defends an argument $A$ iff every attacker of $A$ is attacked by some $B\in\mathcal{X}$.

Definition 2** (Extensions).**

Let $({\tt Arg},{\tt Att})$ be an AF. If $\mathcal{E}\subseteq{\tt Arg}$ is conflict-free, i.e. there are no $A,B\in\mathcal{E}$ for which $(A,B)\in{\tt Att}$, then (i) $\mathcal{E}$ is a complete extension iff $A\in\mathcal{E}$ whenever $\mathcal{E}$ defends $A$; (ii) $\mathcal{E}$ is a preferred extension iff it is a set inclusion maximal complete extension; and (iii) $\mathcal{E}$ is the grounded extension iff it is the set inclusion minimal complete extension.

Dung [4] showed that for every AF there is a unique grounded extension. On Dung’s abstract approach from [4], arguments are basic units of analysis the internal structure of which is not represented. In what follows we will instantiate abstract arguments by allowing for the representation of their internal logical structure.

3 Argumentation by cases

In this section we define structured argumentation frameworks (SAFs) for reasoning by cases. Our point of departure is an instantiation of the $ASPIC^{+}$ framework (without priorities, without defeasible premises and without undercuts).

We adjust $ASPIC^{+}$ in the following ways. (i) We define a new type of argument called an rbc-argument (see point 4 in Definition 4). By means of rbc-arguments, we can argue by cases in an argumentation formalism (Section 3.1). (ii) We generalize the attack relation so as to include argumentation by cases, using the concept of a hypothetical argument (Section 3.2), and we define a logical consequence relation for the resulting SAFs (Section 3.3). We briefly discuss the meta-theoretical properties of our framework (Section 3.4).

3.1 Arguments

We illustrate our framework using the propositional fragment of classical logic ($\mathbf{CL}$) as our core logic. We denote the consequence relation of $\mathbf{CL}$ by $\vdash$. To obtain the formal language $\mathcal{L}$ of $\mathbf{CL}$, we close a denumerable stock $\mathcal{P}=\{p,q,r,\ldots\}$ of propositional letters under the usual $\mathbf{CL}$-connectives $\neg,\vee,\wedge,\supset,\equiv$. We also add the verum constant $\top$ and the falsum constant $\bot$ to $\mathcal{L}$. For reasons of transparency we will sometimes use subscripted letters $p_{1},p_{2},q_{1},q_{2},\ldots$ as names for propositional letters.

Definition 3** (Argumentation theory).**

An argumentation theory (AT) is a triple ${\rm AT}=(\mathcal{L},\mathcal{R},\mathcal{F})$ where:

• •

$\mathcal{L}$* is our formal language defined above;*

• •

$\mathcal{R}=\mathcal{S}\cup\mathcal{D}$* is a set of strict ($\mathcal{S}$) and defeasible ($\mathcal{D}$) inference rules of the form $\varphi_{1},\ldots,\varphi_{n}\rightarrow\psi$ and $\varphi_{1},\ldots,\varphi_{n}\Rightarrow\psi$ respectively (where $\varphi_{1},\ldots,\varphi_{n},\psi\in\mathcal{L}$); and*

• •

$\mathcal{F}\subseteq\mathcal{L}$* is a $\mathbf{CL}$-consistent knowledge base.111$\mathcal{F}\subseteq\mathcal{L}$ is $\mathbf{CL}$-consistent iff $\mathcal{F}\not\vdash\bot$.*

We assume in addition that $\varphi_{1},\ldots,\varphi_{n}\rightarrow\psi\in\mathcal{S}$ iff $\{\varphi_{1},\ldots,\varphi_{n}\}\vdash\psi$. Since we keep $\mathcal{L}$ and $\mathcal{S}$ fixed, we will in the remainder refer to ATs as pairs $(\mathcal{D,F})$.

Definition 4** (Arguments).**

Given an argumentation theory ${\rm AT}=(\mathcal{D},\mathcal{F})$, the set of arguments ${\tt Arg}^{\bot}({\rm AT})$ contains:

$A=\langle\phi\rangle$* where $\phi\in\mathcal{F}$*

• •

${\tt Conc}(A)=\phi$**

• •

${\tt Sub}(A)=\{A\}$**

• •

${\tt HSub}(A)=\emptyset$** 2. 2.

$A=\langle A_{1},\ldots,A_{n}\rightarrow\phi\rangle$* where $A_{1},\ldots,A_{n}\in{\tt Arg}^{\bot}({\rm AT})$ and ${\tt Conc}(A_{1}),\ldots,{\tt Conc}(A_{n})\rightarrow\phi\in\mathcal{S}$*

• •

${\tt Conc}(A)=\phi$**

• •

${\tt Sub}(A)=\{A\}\cup{\tt Sub}(A_{1})\cup\ldots\cup{\tt Sub}(A_{n})$**

• •

${\tt HSub}(A)={\tt HSub}(A_{1})\cup\ldots\cup{\tt HSub}(A_{n})$** 3. 3.

$A=\langle A_{1},\ldots,A_{n}\Rightarrow\phi\rangle$* where $A_{1},\ldots,A_{n}\in{\tt Arg}^{\bot}({\rm AT})$ and ${\tt Conc}(A_{1}),\ldots,{\tt Conc}(A_{n})\Rightarrow\phi\in\mathcal{D}$*

• •

${\tt Conc}(A)=\phi$**

• •

${\tt Sub}(A)=\{A\}\cup{\tt Sub}(A_{1})\cup\ldots\cup{\tt Sub}(A_{n})$**

• •

${\tt HSub}(A)={\tt HSub}(A_{1})\cup\ldots\cup{\tt HSub}(A_{n})$** 4. 4.

$A=\langle A_{1},[A_{2}],\ldots,[A_{n}]\leadsto\phi\rangle$* where $n\geq 3$*

• •

$\phi=\bigvee\{{\tt Conc}(A_{2}),\ldots,{\tt Conc}(A_{n})\}$,

• •

${\tt Conc}(A_{1})=\bigvee_{i=2}^{n}\psi_{i}$, $A_{i}\in{\tt Arg}^{\bot}((\mathcal{D},\mathcal{F}\cup\{\psi_{i}\}))$,

• •

and ${\tt HSub}(A_{i})=\emptyset$ for all $2\leq i\leq n$.

We have:

• •

${\tt Conc}(A)=\phi$**

• •

${\tt Sub}(A)=\{A\}\cup{\tt Sub}(A_{1})$**

• •

${\tt HSub}(A)={\tt HSub}(A_{1})\cup\{(A_{2},\psi_{2}),\ldots,(A_{n},\psi_{n})\}$**

Definition 4 departs in two respects from the way arguments are usually defined in $ASPIC^{+}$. First, there is a new class of arguments constructed by means of rule 4: these arguments are called rbc-arguments. They correspond to applications of the reasoning by cases scheme outlined in Section 1.

Example 1**.**

Let $\mathcal{D}=\{\top\Rightarrow p\vee q;\>\>p\Rightarrow p_{1};\>\>p_{1}\Rightarrow p_{2};\>\>p_{2}\Rightarrow r;\>\>q\Rightarrow q_{1};\>\>q_{1}\Rightarrow r\}$ and ${\rm AT}=(\mathcal{D},\{\top\})$. The following are arguments in ${\tt Arg}^{\bot}({\rm AT})$:

• $A_{1}=\langle\langle\top\rangle\Rightarrow p\vee q\rangle$**
• $A_{2}=\langle A_{1},[\langle\langle\langle p\rangle\Rightarrow p_{1}\rangle\Rightarrow p_{2}\rangle\Rightarrow r],[\langle\langle q\rangle\Rightarrow q_{1}\rangle\Rightarrow r]\leadsto r\rangle$**
• $A_{3}=\langle A_{1},[\langle p\rangle\Rightarrow p_{1}],[\langle q\rangle\Rightarrow q_{1}]\leadsto p_{1}\vee q_{1}\rangle$**

$A_{2}$ and $A_{3}$ are rbc-arguments constructed on the basis of the ‘cases’ $p$ and $q$ in the disjunctive conclusion of $A_{1}$. Argument $A_{2}$ concludes that $r$, while $A_{3}$ concludes that $p_{1}\vee q_{1}$.

The second novel feature of Definition 4 is that we not only keep track of an argument $A$’s conclusion (${\tt Conc}(A)$) and its sub-arguments (${\tt Sub}(A)$), but also of its hypothetical sub-arguments (${\tt HSub}(A)$). These are pairs consisting of an argument $B$ and a formula $\phi$, where $B$ is constructible on the basis of the extended AT obtained by adding $\phi$ to the knowledge base of the original AT. For instance, {\tt HSub}(A_{2})=\bigl{\{}\bigl{(}\langle\langle\langle\langle p\rangle\Rightarrow p_{1}\rangle\Rightarrow p_{2}\rangle\Rightarrow r\rangle,p\bigr{)},\bigl{(}\langle\langle\langle q\rangle\Rightarrow q_{1}\rangle\Rightarrow r\rangle,q\bigr{)}\bigr{\}}.

$A_{2}$’s hypothetical sub-argument $(\langle\langle\langle\langle p\rangle\Rightarrow p_{1}\rangle\Rightarrow p_{2}\rangle\Rightarrow r\rangle,p)$ contains the argument $\langle\langle\langle\langle p\rangle\Rightarrow p_{1}\rangle\Rightarrow p_{2}\rangle\Rightarrow r\rangle$ constructible on the basis of the AT $(\mathcal{D},\{\top,p\})$.

Remark 1**.**

If one is interested in reducing the size of ${\tt Arg}^{\bot}({\rm AT})$, one may only allow for minimal disjunctions when generating arguments of type 4. More precisely, where $A_{1}$ is of the form $\langle B_{1},\ldots,B_{m}\rightarrow\bigvee_{i=1}^{n}\psi_{i}\rangle$ or $\langle B_{1},\ldots,B_{m}\Rightarrow\bigvee_{i=1}^{n}\psi_{i}\rangle$, $A=\langle A_{1},[A_{2}],\ldots,[A_{n}]\leadsto\phi\rangle\in{\tt Arg}^{\bot}({\rm AT})$ only if there is no $\bigvee_{j\in J}\psi_{j}$ where $J\subset\{2,\ldots,n\}$ for which ${\tt Conc}(B_{1}),\ldots,{\tt Conc}(B_{m})\rightarrow\bigvee_{j\in J}\psi_{j}\in\mathcal{S}$.

Definition 4 allows for the construction of arguments containing sub-arguments the conclusions of which are jointly inconsistent, such as arguments $A_{1}$ and $A_{2}$ in the following example, both of which rely on both $p$ and $\neg p$ in their construction.

Example 2**.**

Let ${\rm AT}=(\{\top\Rightarrow s,\top\Rightarrow p,p\Rightarrow\lnot p\},\{\top\})$.

[TABLE]

When $\mathbf{CL}$ is used as the underlying logic, inconsistent arguments like $A_{1}$ and $A_{2}$ may contaminate our formalism by blocking intuitively acceptable arguments like $A_{3}$. (This is because the conclusions of $A_{2}$ and $A_{3}$ are conflicting, causing $A_{2}$ to attack and exclude $A_{3}$, cfr. infra.) Contamination problems of this kind have been studied and tackled in $ASPIC^{+}$ [3, 10]. We can avoid them by filtering out inconsistent arguments.

Definition 5**.**

We define $\dagger A$ for an argument $A$ recursively as follows:

• •

$\dagger\langle\phi\rangle=\phi$**

• •

$\dagger A=\phi\wedge\dagger B_{1}\wedge\ldots\wedge\dagger B_{n}$* where $A=\langle B_{1},\ldots,B_{n}\rightarrow\phi\rangle$*

• •

$\dagger A=\phi\wedge\dagger B_{1}\wedge\ldots\wedge\dagger B_{n}$* where $A=\langle B_{1},\ldots,B_{n}\Rightarrow\phi\rangle$*

• •

$\dagger A=\phi\wedge\dagger B_{1}\wedge(\dagger B_{2}\vee\ldots\vee\dagger B_{n})$* where $A=\langle B_{1},[B_{2}],\ldots[B_{n}]\leadsto\phi\rangle$.*

Definition 6**.**

An argument $A$ is inconsistent iff $\dagger A\vdash\bot$. Otherwise $A$ is consistent. Relative to ${\rm AT}=(\mathcal{D},\mathcal{F})$, ${\tt Arg}({\rm AT})$ is ${\tt Arg}^{\bot}({\rm AT})$ without inconsistent arguments.

For arguments without occurrences of $\leadsto$ our definition of inconsistent arguments is equivalent to that of [10]. In the remainder we will focus on the set ${\tt Arg}({\rm AT})$ rather than ${\tt Arg}^{\bot}({\rm AT})$, avoiding contamination problems.

3.2 Attacks

In $ASPIC^{+}$, attacks are defined in terms of a generic contrariness operator. We define them in terms of ‘$\neg$’, so that arguments the conclusions of which are classical contradictories attack each other. We have to be careful when defining argumentative attacks when rbc-arguments are involved, since we must take into account the hypothetical sub-arguments of an rbc-argument. New questions arise here. For instance, an argument’s hypothetical sub-argument may conflict with a non-hypothetical argument.

Example 3**.**

Let ${\rm AT}=(\mathcal{D,F})$, with $\mathcal{D}=\{p\Rightarrow q\vee r;\ q\Rightarrow s;\ s\Rightarrow v;\ r\Rightarrow v;\ t\Rightarrow\lnot s\}$ and $\mathcal{F}=\{p,t\}$.

• A_{1}=\bigl{\langle}\langle\langle p\rangle\Rightarrow q\lor r\rangle,[\langle\langle q\rangle\Rightarrow s\rangle\Rightarrow v],[\langle r\rangle\Rightarrow v]\leadsto v\bigr{\rangle}**
• A_{2}=\bigl{\langle}\langle t\rangle\Rightarrow\lnot s\bigr{\rangle}**

In Example 3, the non-hypothetical argument $A_{2}$ is in conflict with the argument $\langle\langle q\rangle\Rightarrow s\rangle\Rightarrow v$, which belongs to $A_{1}$’s hypothetical sub-argument $(\langle\langle\langle q\rangle\Rightarrow s\rangle\Rightarrow v\rangle,q)$. The desirable outcome in this example is that $A_{2}$ attacks $A_{1}$, but not vice versa.

As a further illustration, consider the following scenario.

Example 4**.**

${\rm AT}=(\mathcal{D},\mathcal{F})$, with $\mathcal{D}=\{p\Rightarrow(q\lor r);\ q\Rightarrow s_{1};\ s_{1}\Rightarrow s_{2};\ s_{2}\Rightarrow v;\ r\Rightarrow v;\ q\Rightarrow\lnot s_{1}\}$ and $\mathcal{F}=\{p\}$.

• $A_{0}=\langle\langle p\rangle\Rightarrow q\vee r\rangle$**
• $A_{1}=\langle A_{0},[\langle\langle\langle q\rangle\Rightarrow s_{1}\rangle\Rightarrow s_{2}\rangle\Rightarrow v],[\langle r\rangle\Rightarrow v]\leadsto v\rangle$**

The following argument is constructible on the basis of the extended theory ${\rm AT}^{\prime}=(\mathcal{D},\mathcal{F}\cup\{q\})$:

• $A_{2}=$* $\langle\langle q\rangle\Rightarrow\neg s_{1}\rangle$.*

$A_{1}$ contains the intermediate conclusion $s_{2}$ based on the assumption $q$. However, $A_{2}$ concludes that $\neg s_{2}$ on the basis of the same assumption, $q$. The desirable outcome in this example is to let $A_{1}$ and $A_{2}$ attack each other, since these arguments were both constructed on the basis of our knowledge base plus the assumption that $q$, and since their conclusions are contradictories.

To handle examples like these, we introduce the set ${\tt HArg}(\mathcal{D},\mathcal{F})$ of all arguments that can be constructed on the basis of some disjunct used in the construction of an rbc-argument in ${\tt Arg}(\mathcal{D},\mathcal{F})$.

Where $A$ is an argument and $\phi$ a formula, $\pi_{1}(A,\phi)=A$ and $\pi_{2}(A,\phi)=\phi$. We lift the definition as usual: where $i\in\{1,2\}$, $\pi_{i}(\Delta)=\{\pi_{i}(A,\phi)\mid(A,\phi)\in\Delta\}$.

Where $\phi\in\mathcal{L}\setminus\mathcal{F}$, ${\rm AT}=(\mathcal{D},\mathcal{F})$ and ${\rm AT}^{\prime}=(\mathcal{D},\mathcal{F}\cup\{\phi\})$, we denote ${\tt Arg}({\rm AT}^{\prime})\setminus{\tt Arg}({\rm AT})$ by ${\tt Arg}^{\phi}({\rm AT})$.

Definition 7** (Hypothetical Arguments).**

Where ${\rm AT}=(\mathcal{D},\mathcal{F})$, ${\tt HArg}({\rm AT})$ is the set of all $A\in{\tt Arg}^{\phi}({\rm AT})$ such that $\phi\in\pi_{2}({\tt HSub}(B))$ for some $B\in{\tt Arg}({\rm AT})$.

Definition 8** (Attacks, Rebuts).**

For a given theory ${\rm AT}$, we define a direct attack relation

[TABLE]

as follows: $A$ directly attacks $B$ iff $B$ is of the form $\langle\ldots\Rightarrow{\tt Conc}(B)\rangle$, (${\tt Conc}(A)=\neg{\tt Conc}(B)$ or ${\tt Conc}(B)=\neg{\tt Conc}(A)$), and

• •

$A\in{\tt Arg}({\rm AT})$* and $B\in{\tt Arg}({\rm AT})$ or*

• •

$A\in{\tt Arg}({\rm AT})$* and $B\in{\tt HArg}({\rm AT})$ or*

• •

$A\in{\tt Arg}^{\phi}({\rm AT})$* and $B\in{\tt Arg}^{\phi}({\rm AT})$ for some $\phi\in\mathcal{L}\setminus\mathcal{F}$.*

We lift the definition recursively in the following way: $A$ attacks $B$ if $A$ directly attacks $B$ or it attacks some $C\in({\tt Sub}(B)\setminus\{B\})\cup\bigcup\mathfrak{\pi}_{1}({\tt HSub}(B))$.

For an argument $A$ to directly attack an argument $B$, the following requirements need to be fulfilled: The conclusion of $A$ conflicts with the conclusion of $B$ and (either $A$ is non-hypothetical, or $A$ and $B$ are hypothetical arguments based on the same assumption $\phi$).

To illustrate how this works, reconsider our examples. In Example 3, $\langle\langle q\rangle\Rightarrow s\rangle\in{\sf HArg}({\rm AT})$ and $A_{2}$ directly attacks $\langle\langle q\rangle\Rightarrow s\rangle$, so $A_{2}$ attacks $A_{1}$ (but not vice versa). In Example 4 the arguments $\langle\langle q\rangle\Rightarrow s_{1}\rangle$ and $A_{2}$ are in ${\tt Arg}^{q}({\rm AT})$, so these arguments directly attack each other. Consequently, $A_{2}$ also attacks $A_{1}$.

3.3 Consequence relations

Definition 9**.**

The structured argumentation framework (in short, SAF) defined by the theory ${\rm AT}$ is the pair $({\tt Arg}({\rm AT})\cup{\tt HArg}({\rm AT}),{\tt Att}({\rm AT}))$.

Given a SAF, we can use the argumentation semantics from Section 2 to define consequence relations:

Definition 10**.**

Let ${\rm SAF}=({\tt Arg}({\rm AT})\cup{\tt HArg}({\rm AT})$, ${\tt Att}({\rm AT}))$, let ${\sf sem}\in\{\sf Cmp,\sf Prf,\sf Grd\}$, and let ${\sf Cmp}({\rm SAF})$, ${\sf Prf}({\rm SAF})$, and ${\sf Grd}({\rm SAF})$ denote the sets of ${\rm SAF}$’s complete extensions, ${\rm SAF}$’s preferred extensions, and ${\rm SAF}$’s grounded extension respectively.

• •

${\rm SAF}\mathop{\mid\!\sim}^{\cap}_{\sf sem}\phi$* iff for every $\mathcal{B}\in{\sf sem}({\rm SAF})$ there is an $A\in\mathcal{B}\cap{\tt Arg}({\rm AT})$ with ${\rm conc}(A)=\phi$.*

• •

${\rm SAF}\mathop{\mid\!\sim}^{\Cap}_{\sf sem}\phi$* iff there is a $\mathcal{B}\in\bigcap{\sf sem}({\rm SAF})\cap{\tt Arg}({\rm AT})$ with ${\rm conc}(A)=\phi$.*

Since the grounded extension is unique both definitions coincide for ${\sf sem}={\sf Grd}$.

Relative to a theory ${\rm AT}$, the ‘virtual’ arguments in ${\tt HArg}({\rm AT})$ are capable of attacking arguments in ${\tt Arg}({\rm AT})$ (in their hypothetical subarguments), and consequently of preventing the derivability of conclusions of arguments in ${\tt Arg}({\rm AT})$. However, the conclusions of virtual arguments are never themselves derivable from AT.

3.4 Rationality postulates

In [2, 3] several postulates were proposed to evaluate formalisms for structured argumentation. In the present context these postulates read as follows. Given a SAF $({\tt Arg}({\rm AT})\cup{\tt HArg}({\rm AT}),{\tt Att}({\rm AT}))$ where $\mathcal{E}\in{\sf Cmp}({\rm SAF})$:222The proofs of these properties are to be found in the technical appendix as indicated below, except for te proof of non-interference which we omit due to space restrictions. The authors in [2] distinguish between direct and indirect consistency: in our framework these definitions are equivalent since our strict rules are closed under $\mathsf{CL}$.

1. Sub-argument closure: where $A\in\mathcal{E}$, ${\tt Sub}(A)\subseteq\mathcal{E}$ (immediate in view of Theorem 1)
2. Closure under strict rules: where $A_{1},\ldots,A_{n}\in\mathcal{E}\cap{\tt Arg}({\rm AT})$ and ${\rm Conc}(A_{1}),\ldots,{\rm Conc}(A_{n})\vdash B$ also $\langle A_{1},\ldots,A_{n}\rightarrow B\rangle\in\mathcal{E}\cap{\tt Arg}({\rm AT})$ (see Theorem 2),
3. Consistency: $\{{\rm Conc}(A)\mid A\in\mathcal{E}\cap{\tt Arg}({\rm AT})\}$ is consistent (see Theorem 3),
4. Non-interference: Let ${\sf Atoms}(\mathcal{F})$ [${\sf Atoms}(\mathcal{D})$] be the set of all atoms occurring in $\mathcal{F}$ [$\mathcal{D}$]. Where ${\rm AT}=(\mathcal{D},\mathcal{F})$, ${\rm AT}^{\prime}=(\mathcal{D}\cup\mathcal{D}^{\prime},\mathcal{F}\cup\mathcal{F}^{\prime})$, ${\rm SAF}=({\tt Arg}({\rm AT})\cup{\tt HArg}({\rm AT}),{\tt Att}({\rm AT}))$, ${\rm SAF}^{\prime}=({\tt Arg}({\rm AT}^{\prime})\cup{\tt HArg}({\rm AT}),{\tt Att}({\rm AT}^{\prime}))$, ${\mathop{\mid\!\sim}}\in\{{\mathop{\mid\!\sim}_{\sf Grd}^{\cap}}$, ${\mathop{\mid\!\sim}_{\sf Grd}^{\Cap}}$, ${\mathop{\mid\!\sim}_{\sf Prf}^{\cap}}$, ${\mathop{\mid\!\sim}_{\sf Prf}^{\Cap}}\}$, ${\sf Atoms}(\phi)\subseteq{\sf Atoms}(\mathcal{D})\cup{\sf Atoms}(\mathcal{F})$, and $({\sf Atoms}(\mathcal{D})\cup{\sf Atoms}(\mathcal{F}))\cap({\sf Atoms}(\mathcal{D}^{\prime})\cup{\sf Atoms}(\mathcal{F}^{\prime}))=\emptyset$, we have:

[TABLE]

The property of non-interference can be used to show that the present framework avoids contamination problems of the kind discussed in Section 3.1 (see [3, 10]).

4 Related work

4.1 Disjunctive Defaults

In [5] a generalization of default logic, disjunctive default logic, is proposed that is more apt to deal with disjunctions than Reiter’s original approach. For instance, given the default theory with $p\vee q$ and the defaults $p\Rightarrow r$ and $q\Rightarrow r$, $r$ is not a default consequence in Reiter’s approach since the only extension of this theory is $Cn(p\vee q)$. In disjunctive default logic, an alternative disjunction $\mid$ is available: $p\mid q$ enforces that $p$ or $q$ is in any extension of the theory. So, for the default theory consisting of $p\mid q$, and the defaults $p\Rightarrow r$ and $q\Rightarrow r$ we have two extensions, $Cn(\{p,r\})$ and $Cn(\{q,r\})$. Now $r$ is a skeptical consequence. Default consequents can also make use of $\mid$: a disjunctive default is of the form:

[TABLE]

where $\phi$ is the prerequisite, $\psi_{1},\ldots,\psi_{n}$ are justifications, and $\gamma_{1},\ldots,\gamma_{m}$ are consequents of the default. A set of formulas $\Xi$ is an extension of a disjunctive default theory consisting of the disjunctive defaults in $\Delta$ (we here follow the convention in [5] according to which ’facts’ are considered as disjunctive defaults with empty prerequisite and empty justification) if it satisfies the following requirements: (i) for any $\frac{\phi:\psi_{1},\ldots,\psi_{n}}{\gamma_{1}\mid\ldots\mid\gamma_{m}}\in\Delta$, if $\phi\in\Xi$ and $\neg\psi_{1},\ldots,\neg\psi_{n}\notin\Xi$ then $\gamma_{i}\in\Xi$ for some $1\leq i\leq m$, (ii) $Cn(\Xi)=\Xi$, and (iii) $\Xi$ is minimal with properties (i) and (ii).333This definition in [5] is suboptimal in that it gives undesired results: e.g. for the theory $\Delta=\{\frac{\top~{}:~{}\neg p}{\neg p}\}$ also $Cn(p)$ will form an extension. The problem can easily be fixed though by defining extensions analogous to Reiter.

We compare our approach to disjunctive default logic by thinking of $\Rightarrow$ as a default conditional: $\psi\Rightarrow\phi$ encodes the normal default $\frac{\psi:\phi}{\phi}$. We start our comparison with the example given above. Let $\Delta_{1}=\{p\mid q,p\Rightarrow r,q\Rightarrow r\}$. $\Delta_{1}$ has two extensions, $Cn(\{p,r\})$ and $Cn(\{q,r\})$ and so $r$ is a skeptical consequence. This outcome corresponds to our approach for the theory ${\rm AT}_{1}=(\{p\Rightarrow r,q\Rightarrow r\},\{p\vee q\})$: the argument $\langle\langle p\vee q\rangle,[\langle p\rangle\Rightarrow r],[\langle q\rangle\Rightarrow r]\leadsto r\rangle$ is in all complete extensions of ${\rm AT}_{1}$.

Next, consider Poole’s broken arm example [9]. Let $l$ be “having a left broken arm”, $r$ “having a right broken arm”, $w$ “writing legibly”. On our approach, the theory ${\rm AT}_{\rm arm}=(\{w\Rightarrow\neg r\},\{l\vee r,w\})$ gives rise to the argument $\langle\langle\langle w\rangle\Rightarrow\neg r\rangle,\langle l\vee r\rangle\rightarrow l\rangle$, which is in all complete extensions of ${\rm AT}_{\rm arm}$. In contrast, the disjunctive default theory $\Delta_{\rm arm}=\{l\mid r,w,w\Rightarrow\neg r\}$ has two extensions $Cn(\{l,w,\neg r\})$ and $Cn(\{r,w\})$. Since $l\notin Cn(\{r,w\})$, $l$ is not a skeptical consequence in disjunctive default logic.

Finally, reconsider the AT from Example 3. There are various ways in which we can translate this AT into a disjunctive default theory, e.g.444Our discussion also applies if we translate $p\Rightarrow q\vee r$ by $\frac{p~{}:~{}q\wedge r}{q\mid r}$.

[TABLE]

For $\Delta_{3}$ we have the extensions $Cn(\{p,t,q,s,v\})$, $Cn(\{p,t,q,\neg s\})$, and $Cn(\{p,t,\neg s,r,v\})$, so $v$ is not a skeptical consequence. This corresponds to our approach in which the argument $A_{1}$ from Example 3 is excluded due to the attack by $A_{2}$. However, on our approach $A_{2}$ is in all complete extensions, so contrary to disjunctive default logic we obtain $\neg s$ as a skeptical consequence.

4.2 The OR meta-rule

A different approach for dealing with disjunctive information is to allow for inference rules that produce new conditionals from given conditionals. We, for instance, find the following rule in system P [6] and in several Input/Output logics [7]:

[TABLE]

One could define an $ASPIC^{+}$-like system where arguments are constructed as in rules 1–3 in Definition 4, and in which the defeasible rules are closed under OR. For instance, given ${\rm AT}_{1}$ from Section 4.1 this allows to derive $p\vee q\Rightarrow r$ from $p\Rightarrow r$ and $q\Rightarrow r$, so that we can construct the argument $\langle p\vee q\rangle\Rightarrow r$ and obtain $r$ as a consequence.

Adding OR is not sufficient to always get the intuitive outcome. Let ${\rm AT}_{4}=(\{p\Rightarrow q\vee r,q\Rightarrow s,s\Rightarrow v,r\Rightarrow u,u\Rightarrow v\},\{p\})$. One would want to build an argument for $v$, but we cannot put OR to much use (except for deriving $s\vee u\Rightarrow v$). We would have to combine OR with e.g. right-weakening (RW: $\frac{\psi\vdash\phi~{}~{}\psi^{\prime}\Rightarrow\psi}{\psi^{\prime}\Rightarrow\phi}$), or generalize OR to

[TABLE]

in order to produce $q\vee r\Rightarrow s\vee u$. Since also $s\vee u\Rightarrow v\vee v$ can be derived, we now have the means to construct the argument $\langle\langle\langle p\Rightarrow q\vee r\rangle\Rightarrow s\vee u\rangle\Rightarrow v\vee v\rangle\rightarrow v$. In many systems of nonmonotonic logic, e.g. in system P and in many Input/Output logics, OR and RW are available (and thus gOR is a derived rule). We now contrast our approach with such (g)OR-based approaches.

A striking difference concerns the handling of Example 3. In the gOR-based system we can construct:

[TABLE]

This argument is not attacked by the argument $t\Rightarrow\neg s$. An alternative argument for $v$ is given by $\langle t\Rightarrow\neg s\rangle,\langle\langle p\Rightarrow q\vee r\rangle\Rightarrow s\vee v\rangle\rightarrow v$. Recall that neither in our approach nor in disjunctive default logic $v$ is a skeptical consequence. Even if we add $\neg r$ to the knowledge base $\mathcal{F}$ in Example 3, $v$ remains derivable in the gOR-based approach since $A_{3}$ remains unchallenged. This is counter-intuitive: both the argumentative path via $q\Rightarrow s\Rightarrow v$ and the path via $r\Rightarrow v$ are barred in view of the unchallenged arguments $t\Rightarrow\neg s$ and $\neg r$. An advantage of using the reasoning-by-cases rule 4 in Definition 4 is that it provides more fine-grained ways of tracking commitments in sub-arguments. This enables us to block the undesired consequence $v$ in this example.555An additional advantage is that argument strength can be tracked in a more fine-grained way when using RbC in contrast to OR-based approaches. See also Section 5.

5 Conclusion and outlook

The ideas developed in this paper offer many interesting avenues for further work, partially consisting of the removal of the limitations assumed in this paper. For example, we did not consider nested rbc-arguments or various components that can be modelled in the ASPIC+-framework such as defeasible premises, undermining or undercut attacks. We also plan to present a less cautious variation of this framework where an attack on an rbc-argument $A,[B_{1}],\ldots,[B_{n}]\leadsto\psi$ succeeds only if each of the $B_{i}$’s is attacked. In addition we will investigate prioritized default rules in this framework. Here too, new questions arise. Consider, for instance, an argument $\langle p\vee q\rangle,[\langle\langle p\rangle\Rightarrow s\rangle\Rightarrow t],[\langle q\rangle\Rightarrow t]\leadsto t$. If in addition there is an argument $\langle\top\rangle\Rightarrow\neg s$ which is preferred over $\langle p\rangle\Rightarrow s$, then it seems intuitive to let the former attack the latter argument. But what if the hypothetical argument $\langle p\rangle\Rightarrow s$ has a higher degree of priority than the non-hypothetical $\langle\top\rangle\Rightarrow\neg s$? Should we decide in favor of the highest priority assigned, or should we never let a hypothetical argument attack a non-hypothetical one? More generally, how do we lift the priorities assigned to the (hypothetical and non-hypothetical) constituents of an rbc-argument? Difficult questions like these will have to be answered in order to resolve conflicts between prioritized rbc-arguments.

In future work we also plan to investigate the use of an ordered disjunction $\overleftarrow{\lor}$ (see, e.g., [1]). For instance, a rule $p\Rightarrow q\overleftarrow{\lor}r$ can be read as: ‘If $p$ then plausibly $q$ or $r$, where $q$ is more plausible than $r$’. This is especially interesting when measures of argument strength are considered and when thinking about defeat of rbc-arguments based on ordered disjunctions such as $\langle\langle q\overleftarrow{\lor}r\rangle,[q\Rightarrow s],[r\Rightarrow s]\leadsto s\rangle$.

APPENDIX

For the meta-proofs below it will be sometimes useful to speak about sub-arguments in the following stronger sense. ${\tt Sub}^{\prime}(\langle A_{1},[A_{2}],\ldots,[A_{n}]\leadsto\phi\rangle)$ consists of ${\tt Sub}^{\prime}(A_{1})$ and $\langle A_{1},[A_{2}^{\prime}],\ldots,[A_{n}^{\prime}]\leadsto\bigvee\{{\tt Conc}(A_{i}^{\prime})\mid 2\leq i\leq n\}\rangle$ for every $A_{i}^{\prime}\in{\tt Sub}(A_{i})$ where $2\leq i\leq n$. For other types of arguments $A$ (see Def. 3, items 1-3), the definition of ${\tt Sub}^{\prime}(A)$ is the same as the definition of ${\tt Sub}(A)$. Note that for any argument $A$, ${\tt Sub}(A)\subseteq{\tt Sub}^{\prime}(A)$. In the following results, if not specified further, ${\rm SAF}$ is a structured argumentation framework based on the arbitrary argumentation theory ${\rm AT}$. The next theorem is a strong form of sub-argument closure:

Theorem 1**.**

If $\mathcal{E}\in{\sf Cmp}({\rm SAF})$ and $A\in\mathcal{E}$, ${\tt Sub}^{\prime}(A)\subseteq\mathcal{E}$.

Proof.

Let $B\in{\tt Sub}^{\prime}(A)$. It is easy to see that every attacker $C$ of $B$ attacks $A$. Since $\mathcal{E}$ is complete, it defends $A$ and hence also $B$. Again, since $\mathcal{E}$ is complete, $B\in\mathcal{E}$. ∎

Definition 11**.**

Where ${\tt Sub}^{\prime}(A)=\{A_{1},\ldots,A_{n}\}$, let $\hat{A}=\langle A_{1},\ldots,A_{n}\rightarrow\bigwedge_{i=1}^{n}{\tt Conc}(A_{i})\rangle$.

Lemma 1**.**

(1) $A$ and $\hat{A}$ have the same attackers in ${\rm SAF}$; (2) $\vdash\dagger A\equiv\dagger\hat{A}$; (3) Where $\mathcal{E}\in{\sf Cmp}({\rm SAF})$, (3.1) if $A\in\mathcal{E}$, $\hat{A}\in\mathcal{E}$; (3.2) if $\langle A_{1},\ldots,A_{n}\rightarrow\phi\rangle\in\mathcal{E}$ and ${\tt Conc}(\hat{A_{1}}),\ldots,{\tt Conc}(\hat{A_{n}})\vdash\psi$, $\langle\hat{A_{1}},\ldots,\hat{A_{n}}\rightarrow\psi\rangle\in\mathcal{E}$.

Proof.

(1) follows due to the fact that the set of defeasible conclusions of $A$ is the same as the set of defeasible conclusions of $\hat{A}$. (2) follows by simple $\mathsf{CL}$-manipulations in view of Definition 5. For (3.1) note that, by (1), if some $B$ attacks $\hat{A}$ then it also attacks $A$. Since $\mathcal{E}$ is complete, $\hat{A}$ is defended and thus in $\mathcal{E}$. The proof of (3.2) is similar to (3.1) and left to the reader. ∎

Theorem 2** (Closure under strict rules).**

Where $A_{1},\ldots,A_{n}\in\mathcal{E}\cap{\tt Arg}({\rm AT})$ and $\mathcal{E}\in{\sf Cmp}({\rm SAF})$: $\langle A_{1},\ldots,A_{n}\rightarrow\phi\rangle\in\mathcal{E}\cap{\tt Arg}({\rm AT})$ if ${\tt Conc}(A_{1}),\ldots,{\tt Conc}(A_{n})\vdash\phi$.

Proof.

Let ${\rm AT}=(\mathcal{D},\mathcal{F})$. We show the statement by an induction over $s=\sum_{i=1}^{n}\#A_{i}$ where $\#B$ is the number of rules from $\mathcal{D}$ and ${\cal S}$ applied in $B$. We have to show two things: (i) $A\in{\tt Arg}({\rm AT})$ and (ii) $A\in\mathcal{E}$.

($s=0$) Then $A$ has the form $\langle\langle\phi_{1}\rangle,\ldots,\langle\phi_{n}\rangle\rightarrow\phi\rangle$. Thus, $\phi_{1},\ldots,\phi_{n}\in\mathcal{F}$ and $\phi_{1},\ldots,\phi_{n}\vdash\phi$. Since we assume our knowledge base to be consistent, $\{\phi_{1},\ldots,\phi_{n},\phi\}$ is consistent and hence $A\in{\tt Arg}({\rm AT})$. Since $A$ has no attackers and $\mathcal{E}$ is complete, $A\in\mathcal{E}$.

($s{\Rightarrow}s{+}1$) We first show (i). Assume for a contradiction that $A\in{\tt Arg}^{\bot}({\rm AT})\setminus{\tt Arg}({\rm AT})$. This means that $\dagger A_{1},\ldots,\dagger A_{n},\phi\vdash\bot$. Since ${\tt Conc}(A_{1}),\ldots,{\tt Conc}(A_{n})\vdash\phi$ this implies by transitivity that $\dagger A_{1},\ldots,\dagger A_{n}\vdash\bot$. Let $n^{\prime}$ be minimal such that $1\leq n^{\prime}\leq n$ and $\dagger A_{1},\ldots,\dagger A_{n^{\prime}}\vdash\bot$. By the induction hypothesis, $\sum_{i=1}^{n^{\prime}{-}1}\#A_{i}\leq s<\sum_{i=1}^{n^{\prime}}\#A_{i}$ which implies $\#A_{n^{\prime}}\geq 1$. Let $\langle B_{1},\ldots,B_{m}\rangle$ be a list of ${\tt Sub}^{\prime}(A_{n^{\prime}})$ ordered in such a way that for all $1\leq i<j\leq m$ we have $B_{j}\notin{\tt Sub}^{\prime}(B_{i})$ and ${\tt Sub}^{\prime}(B_{j})\subseteq\{B_{1},\ldots,B_{j}\}$. Take a minimal $k$ such that $1\leq k\leq m$ and $\dagger A_{1},\ldots,\dagger A_{n^{\prime}-1},\dagger B_{1},\ldots,\dagger B_{k}\vdash\bot$. Then,

[TABLE]

(3) follows by simple $\mathsf{CL}$-manipulations in view of (1) and since $\dagger B_{k}=\dagger B_{j_{1}}\wedge\ldots\wedge\dagger B_{j_{o}}\wedge{\tt Conc}(B_{k})$. We distinguish the following cases concerning the form of $B_{k}$:

$B_{k}=\langle B_{j_{1}},\ldots,B_{j_{o}}\twoheadrightarrow\phi_{k}\rangle$ where $\{B_{j_{1}},\ldots,B_{j_{o}}\}\subseteq\{B_{1},\ldots,B_{k-1}\}$ and ${\twoheadrightarrow}\in\{{\rightarrow},{\Rightarrow}\}$, or 2. 2.

$B_{k}=\langle B_{j_{1}},[B_{j_{2}}],\ldots,[B_{j_{o}}]\leadsto\phi_{k}\rangle$ where for each $B_{j_{2}}^{\prime}\in{\tt Sub}^{\prime}(B_{j_{2}})$, …, each $B_{j_{o}}^{\prime}\in{\tt Sub}^{\prime}(B_{j_{o}})$ s.t. $\{B_{j_{2}}^{\prime},\ldots,B_{j_{o}}^{\prime}\}\neq\{B_{j_{2}},\ldots,B_{j_{o}}\}$, $\langle B_{j_{1}},[B_{j_{2}}^{\prime}],\ldots,[B_{j_{o}}^{\prime}]\leadsto\bigvee\{{\tt Conc}(B_{j_{i}}^{\prime}\mid j_{2}\leq i\leq j_{o}\})\rangle\in\{B_{1},\ldots,B_{k-1}\}$

Consider case 1 with ${\twoheadrightarrow}={\Rightarrow}$ (the case ${\twoheadrightarrow}={\rightarrow}$ is left to the reader). By the inductive hypothesis, (3), Theorem 1 and Lemma 1, $A^{\prime}=\langle\hat{A_{1}},\ldots,\hat{A_{n-1}},\hat{B_{1}},\ldots,\hat{B_{k-1}}\rightarrow\neg{\tt Conc}(B_{k})\rangle\in\mathcal{E}$. However, since also $B_{k}\in\mathcal{E}$ and $A^{\prime}$ attacks $B_{k}$, this is a contradiction to the conflict-freeness of $\mathcal{E}$.

We now sketch the proof for case 2. By some basic $\mathsf{CL}$-manipulations it can be shown that for all $j_{2}\leq i\leq j_{o}$

[TABLE]

We distinguish two cases: (a) for all $j_{2}\leq i\leq l_{o}$, $B_{j_{i}}$ is of the form $\langle\ldots\rightarrow{\tt Conc}(B_{j_{i}})\rangle$ and (b) there is a $j_{2}\leq l\leq j_{o}$ for which $B_{j_{l}}$ is of the form $\langle\ldots\Rightarrow{\tt Conc}(B_{j_{l}})\rangle$. In case (a), $\dagger A_{1},\ldots,\dagger A_{n^{\prime}-1},\dagger B_{1},\ldots,\dagger B_{k-1}\vdash\bigvee\{{\tt Conc}(B_{j_{i}})\mid j_{2}\leq i\leq j_{o}\}$, which with (4) contradicts (2). In case (b), the argument $C=\langle\hat{A_{1}},\ldots,\hat{A_{n^{\prime}-1}},\hat{B_{1}},\ldots,\hat{B_{k-1}}\rightarrow\neg{\tt Conc}(B_{j_{l}})\rangle$ attacks $B_{k}$ in its hypothetical subargument $B_{j_{l}}$. By the inductive hypothesis, (3), Theorem 1, and Lemma 1, $C\in\mathcal{E}$. This contradicts the conflict-freeness of $\mathcal{E}$ and completes the proof of claim (i).

Suppose that some $C\in{\tt Arg}({\rm AT})\cup{\tt HArg}({\rm AT})$ attacks $A$. Clearly, $C$ attacks some $A_{i}$ (where $1\leq i\leq n$). Since, by Theorem 1, $A_{i}\in\mathcal{E}$, some $D\in\mathcal{E}$ attacks $C$. Altogether this shows that $\mathcal{E}$ defends $A$ and since $\mathcal{E}$ is complete, $A\in\mathcal{E}$. This is claim (ii). ∎

Theorem 3** (Consistency).**

Where $\mathcal{E}\in{\sf Cmp}({\rm AT})$ and $A_{1},\ldots,A_{n}\in\mathcal{E}\cap{\tt Arg}({\rm AT})$, $\{{\tt Conc}(A_{1}),\ldots,{\tt Conc}(A_{n})\}$ is consistent.

Proof.

By Theorem 2, $A=\langle A_{1},\ldots,A_{n}\rightarrow\top\rangle\in\mathcal{E}\cap{\tt Arg}({\rm AT})$ which implies that $\{{\tt Conc}(A_{1}),\ldots,{\tt Conc}(A_{n})\}$ is consistent since otherwise $\dagger A\vdash\bot$. ∎