Sage Journals: Discover world-class research

Abstract

Dialectical proof procedures in assumption-based argumentation are in general sound but not complete with respect to both the credulous and skeptical semantics (due to non-terminating loops). This raises the question of whether we could describe exactly what such procedures compute.

In a previous paper, we introduce infinite arguments to represent possibly non-terminating computations and present dialectical proof procedures that are both sound and complete with respect to the credulous semantics of assumption-based argumentation with infinite arguments.

In this paper, we study whether and under what conditions dialectical proof procedures are both sound and complete with respect to the grounded semantics of assumption-based argumentation with infinite arguments. We introduce the class of ω-grounded and finitary-defensible argumentation frameworks and show that finitary assumption-based argumentation is ω-grounded and finitary-defensible. We then present dialectical procedures that are sound and complete wrt finitary assumption-based argumentation.

Keywords

Dialectical proof procedure infinite argument grounded semantics soundness and completeness

1. .Introduction

Dialectical proof procedures for assumption-based argumentation ([12,13,15,17–19,22,24,32,33]) could be viewed as an integration of the dialectical procedures of abstract argumentation ([8,20,21,26,34,35]) with the process of argument constructions where the latter could get into a non-terminating loop leading to the incompleteness wrt both credulous and skeptical semantics.

A natural question here is: Can we give a precise semantical characterization of what dialectical proof procedures compute?

Representing possibly non-terminating loops as infinite arguments, we present dialectical proof procedures in [31], that are sound and complete wrt credulous semantics. Continuing this line of research, in this paper we present dialectical procedures that are sound and complete with respect to the grounded semantics.

A detailed analysis of the need for infinite arguments in understanding the semantics of dialectical proof procedures is given in [31].

To illustrate how some practical systems of dialectical procedures (like SWI-Prolog ([36])) handle infinite arguments, we analyze the working of SWI-Prolog on two examples taken from [31] below.1

\begin{aligned} F_{1} : r : a \leftarrow n o t_α r^{'} : α \leftarrow f (0) r_{n} : f (n) \leftarrow f (n + 1), n ⩾ 0 \\ t : β \leftarrow \\ F_{2} : r : a \leftarrow n o t_α r^{″} : α \leftarrow n o t_β, f (0) r_{n} : f (n) \leftarrow f (n + 1), n ⩾ 0 \\ t : β \leftarrow \end{aligned}

The behaviors of $F_{1}$ and $F_{2}$ could be explained by the proof trees (viewed arguments) in Fig. 1.

Fig. 1.

Arguments of $F_{1}$ and $F_{2}$ .

SWI-prolog does not deliver any answer to the queries $\leftarrow a$ ? and “ $\leftarrow α$ ?” because of infinite recursion in executing α.2

How could we interpret the outputs of SWI-prolog declaratively?

SWI-prolog could not overcome the non-termination of the process to construct an argument supporting α due to the “infinite-loop” represented by infinite argument $C_{1}$ .

We could interpret this observation as indicating that infinite arguments (representing “infinite-loop”) do not support their conclusions the way finite arguments do.

We could also say that the failure of SWI-prolog to deliver any answer to the query “ $\leftarrow a$ ?” is due to the non-acceptability of argument A. It implies that though infinite argument $C_{1}$ can not support its conclusion, it could still attack argument A.

SWI-prolog delivers respectively the answers “True”, “False”, “True” to the queries $\leftarrow a$ ?, “ $\leftarrow α$ ?” and “ $\leftarrow β$ ?” wrt program $F_{2}$ .3 The answer to “ $\leftarrow α$ ?” is false because the only argument supporting it is $C_{2}$ that is based on assumption $n o t_β$ that is attacked by argument B. We could hence say that infinite arguments are attacked the same way finite arguments are attacked.

These observations suggest that infinite arguments still attack (or are attacked by) other arguments as finite arguments do though they do not support their own conclusions.

To capture this peculiar character of infinite arguments, [31] views infinite arguments as self-attacking arguments.

In [31], two proof procedures for credulous semantics are presented. In one, proof trees are constructed explicitly. A filtering mechanism to memorizing the attacked assumptions of both proponent and opponent is employed to prevent each player from constructing the same proof trees twice. The other procedure is simply a flattening of the first. The filtering mechanism in these procedures can not be applied for grounded semantics. The following example illustrates this point.

Example 1.

Consider the argumentation framework $F$ represented by the simple logic program:

\begin{aligned} r : p \leftarrow n o t_q t : q \leftarrow n o t_p \end{aligned}

To support p, the proof procedures in [31] would correctly deliver argument P (See Fig. 2).

The proponent first constructs argument P to support p. The opponent responds by constructing argument Q to attack P at assumption $n o t_q$ . The filtering mechanism memorizes assumption $n o t_q$ after the opponent attacks it and does not allow the opponent to attack it again. The procedures hence stop and deliver P as an admissible argument supporting p.

As the grounded extension of $F$ is empty, procedures for grounded extension need to drop this filtering mechanism.

Fig. 2.

Illustration of Example 1.

A consequence of dropping the filtering mechanism in the procedures for credulous semantics in [31] is that an argument could be constructed repeatedly many times at different stages in the computation. To distinguish between these distinct “copies” of the same argument, we consider them together with their histories.

The grounded extension of an argumentation framework $A F = (A r, a t t)$ coincides with the least fixed point of the characteristic function $F_{A F}$ . It hence follows that the grounded extension of $A F$ contains the set $F_{A F}^{ω} (\emptyset) = \cup {F_{A F}^{i} (\emptyset) | i is a natural number}$ .4

To check whether an argument A is groundedly accepted, a dialectical proof procedure would compute the defenders of A (i.e. arguments attacking those attacking A) and then check whether such defenders could also be defended and so on. In cases where there are infinitely many arguments attacking A, such process may not succeed.

Example 2.

Let $A F = (A r, a t t)$ with $A r = {B, A_{0}, A_{1}, . . ., A_{i}, A_{i + 1}, . . .}$ and $a t t = {(A_{2 k + 1}, B) | k ⩾ 0} \cup {(A_{k}, A_{k + 1}) | k ⩾ 0}$ . (A graphical illustration of this argumentation framework is in Fig. 3).

It is easy to see that for each natural number $⩾ 1$ : $F_{A F}^{i} (\emptyset) = {A_{0}, A_{2}, . . ., A_{2 (i - 1)}}$ . Hence $F^{ω} (\emptyset) = \cup {F_{A F}^{i} (\emptyset) | i is a natural number} = {A_{0}, A_{2}, . . ., A_{2 i}, . . .}$ .

The grounded extension of $A F$ is: $F_{A F} (F_{A F}^{ω} (\emptyset)) = F_{A F}^{ω} (\emptyset) \cup {B}$ .

To check whether B is groundedly accepted, a dialectical procedure would need to compute the infinite set ${A_{2 k + 1} | k ⩾ 0}$ of arguments attacking B and find the infinite set ${A_{2 k} | k ⩾ 0}$ of defenders of B. In general, no dialectical proof procedures could carry out such task successfully.

Fig. 3.

An argumentation framework that is not ω-grounded.

To address this issue, we introduce the class of ω-grounded argumentation frameworks where the grounded extension is “computed” after at most ω steps, i.e. the grounded extension of $A F$ coincides with $F_{A F}^{ω} (\emptyset) = \cup {F_{A F}^{i} (\emptyset) | i is a natural number}$ . We then present several key results:

We show that an argumentation framework is ω-grounded iff it is finitary defensible (i.e. all minimal defences of non-selfattacking arguments are finite);

We show that finitary assumption-based argumentation frameworks (see Definition 1) with infinite arguments are finitary defensible;

We present two dialectical proof procedures that are both sound and complete wrt finitary assumption-based frameworks with infinite arguments where in the first procedure, proof trees together with their histories are fully and explicitly represented to shed light on the construction process of arguments and counter arguments during a derivation and hence providing key insights into the soundness and completeness of the procedure. We then present another procedure that is simply the result of flattening the first where most of the data structures representing the proof tree structures of the arguments are striped away. Consequently, the second procedure is both sound and complete but with much simpler data structure and hence much more amenable to possible implementation.

The rest of this paper is organized as follows. In Section 2, we recall the basic notions of abstract and assumption-based argumentation as well as the machinery of infinite arguments. Section 3 proposes the concept of ω-groundedness of argumentation framework and show that finitary assumption-based argument systems are ω-grounded. We then present a dialectical proof procedure wrt grounded semantics in Section 4. The soundness and completeness of the grounded proof procedure are discussed in Section 5 –6. Further we present the flatten version of the proof procedure in Section 7. We conclude and discuss possible expansions of our works in Section 8.

2. .Preliminaries: Argumentation with infinite arguments

In this section, we recall key basic concepts of abstract argumentation from [16] and [14] and infinite arguments together with some illustrating examples in assumption-based argumentation from [31] and [30].

2.1. .Abstract argumentation

Following [14,16], an argumentation framework is a pair $A F = (A r, a t t)$ where $A r$ is a set of arguments, and $a t t \subseteq A r \times A r$ so that $(X, Y) \in a t t$ specifies that X attacks Y. A set of arguments S attacks an argument X if some argument in S attacks X. S attacks another set of arguments $S^{'}$ if S attacks some argument in $S^{'}$ . Moreover we say that S defends X iff S attacks all arguments attacking X. We also say that an argument X is defensible if it is defended by some set of arguments.

A set $S \subseteq A r$ is said to be

conflict-free iff S does not attack itself; and

admissible iff S is conflict-free and S defends each argument in S; and

a preferred extension if S is maximally (wt set inclusion) admissible;5 and

a complete extension if S is admissible and contains each argument it defends.

The characteristic function of AF, denoted by $F_{A F}$ , is defined by

\begin{aligned} F_{A F} : 2^{A r} \to 2^{A r} \end{aligned}

where

\begin{aligned} F_{A F} (S) = {X \in A r | S defends X} \end{aligned}

It is straightforward to see that $F_{A F}$ is monotonic (wrt set inclusion). Since $2^{A r}$ is a complete partial order (wrt set inclusion),6 $F_{A F}$ has a least fixed point.7

The grounded extension of $A F$ denoted by ${G E}_{A F}$ , is defined as the least fixed point of $F_{A F}$ .8

As the set of complete extensions of $A F$ is a complete semilattice ([16]),9 the grounded extension coincides with the least complete extension of $A F$ .

2.2. .Assumption-based argumentation

Given a logical language $L$ , a standard assumption-based argumentation (ABA) framework ([6]) is a triple $F = (R, A, $ \bar{} $)$ where $R$ is a set of inference rules of the form $l_{0} \leftarrow l_{1}, . . . l_{n}$ ( $n ⩾ 0$ and $l_{0}, . . ., l_{n} \in L$ ), and $A \subseteq L$ is a set of assumptions, and $$ \bar{} $$ is a (total) one-one mapping from $A$ into $L ∖ A$ , where $\bar{x}$ is referred to as the contrary of x, and assumptions in $A$ do not appear in the heads of rules.

Remark 1.
In non-standard ABA frameworks ([24]), the contrary $\bar{α}$ of an assumption α could be a set. Such non-standard frameworks could be translated into equivalent standard ones by introducing a new atom $α^{'}$ for each assumption α and i) define $α^{'}$ as the contrary of α; and ii) for each $δ \in \bar{α}$ , add a new rule: $α^{'} \leftarrow δ$ to $R$ .
Remark 2.
Logic programming is a well-known instance of standard ABA where the contrary of a negation-as-failure assumption $n o t_p$ is p.
Remark 3.
For each rule r of the form $l_{0} \leftarrow l_{1}, . . . l_{n}$ , $l_{0}$ and the set ${l_{1}, . . ., l_{n}}$ are referred respectively as the head and the body of r and denoted by $h d (r)$ , $b d (r)$ .

Further the set of assumptions (resp non-assumptions) appearing in the body of r is denoted by $A s s (r)$ (resp. $N A s s (r)$ ).
Definition 1 Finitary ABA

An ABA framework $F = (R, A, $ \bar{} $)$ is finitary if for each sentence $δ \in L$ , the set of rules with head δ is finite.10

Convention 1.
From now on until the end of the paper,
we restrict our consideration to standard finitary ABA. Hence whenever we refer to an ABA framework, we mean a standard finitary one; and

if not otherwise mentioned, we assume an arbitrary but fixed finitary standard assumption-based argumentation framework $F = (R, A, $ \bar{} $)$ .

Definition 2 Partial Proof

Given an ABA $F$ , a partial proof supporting $σ_{0}$ (wrt $F$ ) is a finite sequence of the form

\begin{aligned} (r o o t, σ_{0}) . (r_{1}, σ_{1}) . . . . (r_{n}, σ_{n}) \end{aligned}

where

r_{i} \in R

i ⩾ 1

such that

σ_{i - 1} = h d (r_{i})

and

σ_{i} \in b d (r_{i})

. If

b d (r_{i}) = \emptyset

then

σ_{i} = t r u e

Example 3.
Let’s consider an argumentation framework $F_{2}$ in the introduction.
$\begin{aligned} F_{2} : r : a \leftarrow n o t_α r^{″} : α \leftarrow n o t_β, f (0) r_{n} : f (n) \leftarrow f (n + 1), n ⩾ 0 \\ t : β \leftarrow \end{aligned}$

Some partial proofs supporting a and α are described below and illustrated in Fig. 4.
$\begin{aligned} ψ = (r o o t, a) \\ ψ^{'} = (r o o t, a) . (r, n o t_α) \\ p_{0} = (r o o t, α) \\ p_{1}^{^{'}} = (r o o t, α) . (r^{″}, n o t_β) \\ p_{1} = (r o o t, α) . (r^{″}, f (0)) \\ p_{2} = (r o o t, α) . (r^{″}, f (0)) . (r_{0}, f (1)) \\ . . . \\ p_{n + 1} = (r o o t, α) . (r^{″}, f (0)) . (r_{0}, f (1)) . . . (r_{n - 1}, f (n)) \end{aligned}$

Fig. 4.
A graphical representation of partial proofs of Example 3.

Fig. 5.
Some proof trees of $F_{2}$ .

We next define partial proof trees where we identify the nodes in such trees with the partial proofs representing the unique paths from the root to them.
Definition 3 Partial Proof Trees

A partial proof tree (or just proof tree for simplification) T for a sentence $σ_{0}$ wrt $F$ is a non-empty set of partial proofs supporting $σ_{0}$ wrt $F$ such that for each partial proof

\begin{aligned} p \equiv (r o o t, σ_{0}) . (r_{1}, σ_{1}) . . . . (r_{n}, σ_{n}), n > 0 \end{aligned}

from T, the following properties hold:

The partial proof $p^{'} \equiv (r o o t, σ_{0}) . (r_{1}, σ_{1}) . . . . (r_{n - 1}, σ_{n - 1})$ also belongs to T and is referred to as the unique parent of p whereas p is referred to as a child of $p^{'}$ ;

Every partial proof of the form $p^{'} . (r_{n}, σ^{'})$ with $σ^{'} \in b d (r_{n})$ , also belongs to T and is a child of $p^{'}$ ;

$p^{'}$ has no other children.

σ_{0}

is often referred to as the conclusion of T, denoted by

C l (T)

while the partial proof

(r o o t, σ_{0})

is referred to as the root of T.

An example of partial proof trees is given in Fig. 5.

Remark 4.
For convenience, we often refer to a partial proof tree without mentioning its conclusion if there is no possibility for misunderstanding.
Notation 1 Nodes in Partial Proof Trees

Abusing the notation for convenience, we often refer to a partial proof $(r o o t, σ_{0}) . (r_{1}, σ_{1}) . . . . (r_{n}, σ_{n})$ in a partial proof tree T as a node labeled by $σ_{n}$ in T.

Notation 2.
Let T be a partial proof tree and S be a set of partial proof trees,
A node N in T is said to be a leaf of T if N has no children.

A leaf N of T is said to be final if N is labeled by $t r u e$ or by an assumption. N is non-final if it is not final.

The support of T, denoted by $S p (T)$ , is the set of all sentences labeling the leaves of T and different from $t r u e$ .

The set of all assumptions appearing in T is denoted by $A s s (T)$ .

The set of all assumptions appearing in partial proof trees in S is denoted by $A s s (S)$ .

The set of conclusions of partial proof trees in S is denoted by $C l (S)$ .

Considering Fig. 5, the partial proof $(r o o t, α) . (r^{″}, f (0))$ is a leaf node of $T_{r_{0}}$ while, $(r o o t, α) . (r^{″}, f (0)) . . . (r_{n - 1}, f (n))$ is a leaf node of $T_{r_{n}}$ .

Further, the support of $T_{r_{0}}$ , i.e. $S p (T_{r_{0}})$ , is ${n o t_β, f (0)}$ and $A s s (T_{r_{0}})$ is ${n o t_β}$ .
Definition 4 Arguments

A partial proof tree T is a full proof tree if all leaves of T are final.

An argument for α is a full proof tree for α.

The set of all arguments wrt the ABA framework $F$ is denoted by ${A r}_{F}$ .

Convention 2.
For short, we often simply say, proof trees instead of partial proof trees if there is no possibility of confusion.

When a player in a dialectical computation is attempting to construct an argument, the attempt may not terminate. Declaratively, we model a non-terminating attempt to construct an argument as an attempt to construct an infinite argument.

As infinite arguments do not provide support for their conclusions, they can not be accepted as an admissible argument. We model this intuition as self-attacks of infinite arguments.
Definition 5 Attacks

An argument A attacks an argument B iff one of the following conditions holds:

(1)
The conclusion of A is the contrary of some assumption in the support of B.
(2)
A and B are identical and infinite.

The attack relation between arguments in ${A r}_{F}$ is denoted by ${a t t}_{F}$ . Define
$\begin{aligned} {A F}_{F} = ({A r}_{F}, {a t t}_{F}) \end{aligned}$

Due to the fact that the infinite arguments always attack themselves, the following lemma holds obviously.
Lemma 1.
Let $S \subseteq {A r}_{F}$ be admissible wrt ${A F}_{F} = ({A r}_{F}, {a t t}_{F})$ . Then S contains only finite arguments.
Notation 3.
Let T, $T^{'}$ be proof trees and N be a non-final leaf node in T labeled by a non-assumption σ.11
$T^{'}$ is an immediate expansion of T at N if there is a rule r of the form $σ \leftarrow b_{1}, . . ., b_{m}$ such that $T^{'} = T \cup {N . (r, b_{1}), . . ., N . (r, b_{m})}$ .

Note that if $m = 0$ , $T^{'} = T \cup {N . (r, t r u e)}$ .12

We write $T^{'} = exp (T, N, r)$ .

We say $T^{'}$ is an immediate expansion of T if $T^{'}$ is an immediate expansion of T at some leaf node N of T.

We define
$\begin{aligned} CE (T, N) = {\exp (T, N, r^{'}) | r^{'} is a rule s.t . h d (r^{'}) = σ} . \end{aligned}$

Considering Fig. 5, $T_{r_{1}} = \exp (T_{r_{0}}, N, r_{0})$ where N is $(r o o t, α) . (r^{″}, f (0))$ .

Further the set of all immediate expansion of $T_{r_{0}}$ at node N, i.e. $C E (T_{r_{0}}, N)$ , is ${T_{r_{1}}}$ .
Notation 4.
Let $T_{0}$ , $T_{1}$ be proof trees for $σ_{0}$ .
We say T, $T^{'}$ are compatible iff $T \cup T^{'}$ is also a proof tree.

We say $T_{0}$ is a prefix of $T_{1}$ iff $T_{0} \subseteq T_{1}$ .13^,14

We say $T_{0}$ is a proper prefix of $T_{1}$ if $T_{0}$ is a prefix of $T_{1}$ and $T_{0} \neq T_{1}$ .

Considering Fig. 5, $T_{r_{0}}$ is a prefix of $T_{r_{1}}$ .
Remark 5.
It is worthwhile to note that two proof trees could be compatible without being in a prefix-relationship as illustrated below (see Fig. 6).

Consider an assumption-based framework with three rules:
$\begin{aligned} r_{1} : a \leftarrow b, c; \\ r_{2} : b \leftarrow; \\ r_{3} : c \leftarrow . \end{aligned}$

Consider two proof trees:
$\begin{aligned} T_{0} = {p_{0}, p_{1}, p_{2}, p_{3}}, T_{1} = {p_{0}, p_{1}, p_{2}, p_{4}} where \\ p_{0} = (r o o t, a), p_{1} = (r o o t, a) . (r_{1}, b), p_{2} = (r o o t, a) . (r_{1}, c) and \\ p_{3} = (r o o t, a) . (r_{1}, b) . (r_{2}, t r u e), p_{4} = (r o o t, a) . (r_{1}, c) . (r_{3}, t r u e) . \\ T_{0}, T_{1} are compatible but neither is a prefix of the other . \end{aligned}$

Fig. 6.
Two compatible proof trees.
Lemma 2.
Let $T_{0}$ , $T_{1}$ be proof trees. The following statements hold: (1)
If $T_{1}$ is an immediate expansion of $T_{0}$ then $T_{0}$ is a proper prefix of $T_{1}$ .
(2)
Suppose $T_{0}$ is a prefix of $T_{1}$ . It holds that (a)
the roots of $T_{0}$ , $T_{1}$ coincide; and
(b)
if N is a node in $T_{0}$ then the parent and children (if exist) of N in $T_{0}$ are respectively also the parent and children of N in $T_{1}$ .

Proof.
Obvious.
Lemma 3.
Let T be an argument, $T_{0}$ be a proof tree such that $T_{0}$ is a proper prefix of T. Furthermore, let N be a leaf node in $T_{0}$ such that $C E (T_{0}, N) \neq \emptyset$ . Then there is an unique $T_{1} \in C E (T_{0}, N)$ such that $T_{1}$ is a prefix of T.

$T_{1}$ is often simply denoted by $e x p (T_{0}, N, T)$ .

We also define $e x p (T_{0}, T) = {\exp (T_{0}, N, T) | N i s a n o n - f i n a l l e a f n o d e o f T_{0}}$ . 15
Proof.
Lemma 3 in [31] proves the existence of $T_{1}$ . The uniqueness of $T_{1}$ should be obvious.
Definition 6.
An increasing sequence of proof trees $T_{0} \subseteq T_{1} \subseteq . . . T_{i} \subseteq . . .$ is said to be fair if for each $T_{i}$ , for each non-final leaf node $N \in T_{i}$ there is a node $M \in T_{j}$ , $j > i$ , such that N is a proper prefix of M.
Lemma 4.
Let $s q \equiv T_{0} \subseteq T_{1} \subseteq . . . T_{i} \subseteq . . .$ be an increasing sequence of proof trees. The following statements hold: (1)
$T_{0} \cup T_{1} \cup . . . T_{i} \cup . . .$ is a proof tree.
(2)
If the sequence $s q$ is fair then $T_{0} \cup T_{1} \cup . . . T_{i} \cup . . .$ is an argument.

Proof.
This is Lemma 4 in [31].
Notation 5.
Let T be a proof tree and $N \equiv (r o o t, σ_{0}) . (r_{1}, σ_{1}) . . . . (r_{i}, σ_{i})$ be a node in T.

The height of N in T, denoted by $h (N, T)$ , is defined by $h (N, T) = i$ .16

The minimum of the heights of the non-final leaf nodes in T are denoted by $h i (T)$ , i.e. $h i (T) = min {h (N, T) | N is a non-final leaf node in T}$
3. .ω-Groundedness of argumentation frameworks

We first introduce the notion of ω-grounded argumentation frameworks. We then show that finitary ABA frameworks are ω-grounded.

3.1. .ω-Grounded argumentation frameworks

Let $A F = (A r, a t t)$ be an argumentation framework.

Definition 7 ω-Groundedness

An argumentation framework $A F$ is ω-grounded if its grounded extension ${G E}_{A F}$ can be “computed” after at most ω steps, i.e.

\begin{aligned} G E_{A F} = F_{A F}^{ω} (\emptyset) = ⋃_{i = 0}^{\infty} F_{A F}^{i} (\emptyset) \end{aligned}

It should be obvious that the argumentation framework in Fig. 1 is not ω-grounded.

We give now a sufficient condition for ω-groundedness.

Let $D$ be a set of sets of arguments (i.e $D \subseteq 2^{A r}$ ). $D$ is said to be directed iff for all $S, S^{'} \in D$ , $S \cup S^{'} \in D$ .17

Note that the least upper bound of $D$ , $l u b (D)$ , is $l u b (D) = \cup D$ .

Definition 8 Admissibility Continuity

A function $Φ : 2^{A r} \to 2^{A r}$ is said to be admissibility-continuous (or just ad-continuous for short) if for each directed set of admissible sets $D$

\begin{aligned} l u b {Φ (S) | S \in D} = Φ (l u b (D)) \end{aligned}

Lemma 5.
If the characteristic function $F_{A F}$ is ad-continuous then $A F$ is ω-grounded.
Proof.
Suppose $F_{A F}$ is ad-continuous. Let $D = {F_{A F}^{i} (\emptyset) | i is a natural number}$ . $D$ is obviously directed and $l u b (D) = F_{A F}^{ω} (\emptyset) = ⋃_{i = 0}^{\infty} F_{A F}^{i} (\emptyset)$ .

Since $F_{A F}$ is ad-continuous, $F_{A F}^{ω} (\emptyset) = ⋃_{i = 0}^{\infty} F_{A F}^{i} (\emptyset) = l u b {F_{A F} (S) | S \in D} = F_{A F} (l u b (D)) = F_{A F} (F_{A F}^{ω} (\emptyset))$ . Therefore $F_{A F}^{ω} (\emptyset)$ coincides with the grounded extension of $A F$ .
Definition 9.
A set S of arguments is said to be a minimal defense of an argument A if S defends A and no proper subset of S defends A.
Definition 10 Finitary Defensible

A defensible argument A is finitary-defensible iff all minimal defenses of A are finite.18

An argumentation framework $A F$ is said to be finitary-defensible if all defensible arguments in $A F$ that are not self-attacking19 are finitary defensible.

Theorem 1 Finitary Defensibility implies ad-Continuity

Let $A F$ be a finitary-defensible argumentation framework. Then $F_{A F}$ is ad-continuous and hence $A F$ is ω-grounded.

Proof.
Let $A F$ be a finitary-defensible argumentation framework, $D$ be a directed set of admissible sets of arguments. We show that $l u b {F_{A F} (S) | S \in D} = F_{A F} (l u b (D))$ .

It is obvious that for each $S \in D$ : $S \subseteq l u b (D)$ . Since $F_{A F}$ is monotonic, it holds for each $S \in D$ : $F_{A F} (S) \subseteq F_{A F} (l u b (D))$ . Therefore $l u b {F_{A F} (S) | S \in D} \subseteq F_{A F} (l u b (D))$ .

It remains to show that $l u b {F_{A F} (S) | S \in D} \supseteq F_{A F} (l u b (D))$ .

Let $A \in F_{A F} (l u b (D))$ . Hence $l u b (D)$ is a defense of A. Since $D$ is a set of admissible sets of arguments, $l u b (D) = \cup D$ is also admissible. Therefore $F_{A F} (l u b (D))$ is admissible. Thus A is not self-attacking. Since $A F$ is a finitary-defensible, there is a finite minimal defense $M \subseteq l u b (D)$ of A. Hence for each $X \in M$ there is $S_{X} \in D$ such that $X \in S_{X}$ . Since $M$ is finite, $S^{'} = \cup {S_{X} | X \in M} \in D$ . Thus $A \in F_{A F} (S^{'}) \subseteq l u b {F_{A F} (S) | S \in D}$ .

From Lemma 5, it follows immediately that $A F$ is ω-grounded.

3.2. .Finitary ABA frameworks are finitary-defensible and ω-grounded

We present a novel insight into the semantic structure of finitary ABA systems by showing that finitary ABA frameworks are finitary-defensible and hence ω-grounded. We begin with a lemma stating that finite arguments of finitary ABA framework are finitary-defensible.

Lemma 6 Finite Arguments are Finitary Defensible

Let $F$ be a finitary ABA framework. Then defensible finite arguments in ${A F}_{F}$ are finitary-defensible.

Proof.
Let B be a defensible finite argument in ${A r}_{F}$ .

Let S be a minimal defense of B wrt ${A F}_{F} = ({A r}_{F}, {a t t}_{F})$ . We show that S is finite.

Suppose the contrary that S is infinite. Hence $S = {D_{1}, . . ., D_{i}, . . .}$ . Let $S_{i} = {D_{1}, . . ., D_{i}}$ .

Because S is a minimal defense of B, it follows that the set $A \subseteq {A r}_{F}$ of attacks against B is infinite (if $A$ is finite, pick for each $X \in A$ , an argument $D_{X} \in S$ s.t. $D_{X}$ attacks X. Hence the set ${D_{X} | X \in A} \subset S$ is a finite defense of B (wrt ${A F}_{F}$ ). Contradiction to the fact that S is a infinite minimal defense of B).

Let ${P A}_{n}$ be the set of balanced proof trees of height n20 that are prefixes of arguments in $A$ and ${P A N}_{n}$ are those elements in ${P A}_{n}$ that are not attacked by S.

Further let ${F A}_{n}$ be the set of the full arguments of height n in $A$ .21

Since $F$ is finitary, both ${P A}_{n}$ and ${F A}_{n}$ are finite22 and so are ${P A N}_{n}$ .
We first show that for each n, ${P A N}_{n} \neq \emptyset$ . Suppose the contrary that there is n such that ${P A N}_{n} = \emptyset$ , i.e. each partial argument in ${P A}_{n}$ is attacked by S. Since ${P A}_{n}$ is finite, there is some i such that $S_{i}$ attacks each partial argument in ${P A}_{n}$ . Therefore each full argument of height $> n$ in $A$ is attacked by $S_{i}$ .

Since the set ${F A}_{0} \cup \dots \cup {F A}_{n}$ is also finite, there is some j such that $S_{j}$ attacks each argument in this set. Therefore $S_{i} \cup S_{j}$ attacks each (full) argument in $A$ . Hence $S_{i} \cup S_{j}$ is a finite defense of B, contrary to the assumption that S is a infinite minimal defense of B.

We show now that there is an infinite sequence $T_{0} \subset T_{1} \subset . . .$ such that for each $i ⩾ 0$ : $T_{i} \in {P A N}_{i}$ .

It should be clear that each proof tree in ${P A N}_{i + 1}$ is obtained by expanding a proof tree in ${P A N}_{i}$ at all non-final leaf nodes of the later.

Let $T = (V, E)$ be a tree defined as follows: *
The set of vertices of $T$ is defined by: $V = {root} \cup ⋃_{i = 0}^{\infty} {P A N}_{i}$ where $root$ is the root of $T$ .23
*
The set of edges of $T$ is defined by: $(T, T^{'}) \in E$ iff *
$\exists i$ s.t. $T \in {P A N}_{i}$ and $T^{'} \in {P A N}_{i + 1}$ and $T \subseteq T^{'}$ ; or
*
$T = root$ and $T^{'} \in {P A N}_{0}$ .

Since ${P A N}_{i} \neq \emptyset$ for all i, $T$ is infinite and because $F$ is finitary, each child of $T$ has finitely many children. Thus there is an infinite path in $T$ . In other words, there is an infinite sequence $T_{0} \subset T_{1} \subset . . .$ such that for each $i ⩾ 0$ : $T_{i} \in {P A N}_{i}$ . Since each $T_{i}$ is a balanced tree of height i, the sequence $T_{0} \subset T_{1} \subset . . .$ is obviously fair.

Let $T = ⋃_{i = 0}^{\infty} T_{i}$ . T is therefore a full proof tree and hence an argument. T is hence an attack against B and not attacked by S. Contradiction.

Since the set of finite arguments in ${A F}_{F}$ contains the set of all non-self-attacking arguments, it follows immediately from Theorem 1 and the above Lemma 6: Theorem 2 ω-Groundedness of finitary ABA frameworks

Let $F$ be a finitary ABA framework. Then the following statements hold:

${A F}_{F}$ is finitary-defensible;

The characteristic function $F_{{A F}_{F}}$ is ad-continuous;

${A F}_{F}$ is ω-grounded.

4. .Grounded dispute derivations

In this section we will present a proof procedure for grounded semantics where proof trees together with their histories are fully and explicitly represented to shed light on the construction process of arguments and counter arguments during a derivation and hence providing key insights into the soundness and completeness of the procedure. Later, in Section 7, we present another procedure that is simply the result of flattening the one presented in this section. Consequently, the second procedure is both sound and complete but with much simpler data structure and hence much more amenable to possible implementation.

The purpose of the dispute derivations is to construct arguments. So it is kind of natural to refer to proof trees representing partly constructed arguments in a dispute derivation as partial arguments. It also makes it more intuitive to talk about attack between partial arguments.

Remark 6 Partial Arguments

Abusing the notation slightly for ease of reference, from now on until the end of the paper, we often refer to proof trees as partial arguments.

To avoid any possibility of misunderstanding, we often refer to arguments as full arguments.

We often say that a partial argument Tattacks a partial argument $T^{'}$ if there is an assumption $α \in A s s (T^{'})$ such that $C l (T) = \bar{α}$ .

We also often refer to a proof tree consisting only of the root and supporting a sentence δ by $[δ]$ , i.e. $[δ] = {(r o o t, δ)}$ .

In a dispute derivation, an argument could be constructed repeatedly many times at different stages in the computation. To distinguish between these distinct “copies” of the same argument, we consider them together with their histories.

Definition 11 Histories of Partial Arguments

A possible history of a partial argument T is represented by a sequence $(T_{0}, t_{0}), . . ., (T_{k}, t_{k})$ where $T_{0}, . . ., T_{k}$ are partial arguments such that

$T_{0} = [C l (T)]$ and $T = T_{k}$ ; and

$T_{i}$ , $0 < i ⩽ k$ , is an immediate expansion of $T_{i - 1}$ ; and

$t_{0} < t_{1} < \dots < t_{k}$ are natural numbers representing the stages in the dispute when such expansions happen.

Definition 12 Profiled Partial Arguments

A profiled partial argument (ppa) is a pair $π = (T, h)$ where T is a partial argument and $h = (T_{0}, t_{0}), . . ., (T_{k}, t_{k})$ is a history of T.

(1)
We also often refer to T and h by $T_{π}$ and $h_{π}$ respectively;
(2)
$t_{0}$ is often referred to as the starting time of π denoted by $st (π)$ while k is referred to as the length of the history of π denoted by $lh (π)$ ;
(3)
An assumption α is often referred to as the target of π denoted by $target (π)$ , if $C l (T) = \bar{α}$ ;

Example 4.
Considering again the argumentation framework $F_{2}$ in the introduction
$\begin{aligned} F_{2} : r : a \leftarrow n o t_α r^{″} : α \leftarrow n o t_β, f (0) r_{n} : f (n) \leftarrow f (n + 1), n ⩾ 0. \\ t : β \leftarrow \end{aligned}$

$π_{0} = (T_{0}, h_{0})$ is an example of a profiled partial argument where $T_{0} = [a]$ and $h_{0} = (T_{0}, 0)$ where $h_{0}$ says that $T_{0}$ is obtained at stage 0.

Suppose $T_{0}$ is expanded at stage 1 resulting in a new profiled partial argument $π_{1} = (T_{1}, h_{1})$ (see Fig. 7) where $h_{1} = (T_{0}, 0), (T_{1}, 1)$ . The history $h_{1}$ says that $T_{1}$ is obtained by expanding $T_{0}$ at stage 1 and $T_{0}$ is obtained a stage 0.

Fig. 7.
Proof trees of Example 4.

A dispute derivation is viewed as a game between a proponent and an opponent where the players take turn to develop their arguments. The goal of the proponent is to construct an argument to support some desired conclusion and other arguments to defend against the attacks from the opponent while the opponent’s goal is to construct arguments to attack proponent’s arguments. At each step, either player could choose to either expand their partly constructed arguments or start a new argument to attack the other’s argument.
Definition 13 Grounded Dispute Derivation

A grounded dispute derivation for a sentence σ is a (possibly infinite) sequence of the form

\begin{aligned} ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩ . . . \end{aligned}

where 24

(1)
for each $i ⩽ n$ , ${P P T}_{i}$ , ${O P T}_{i}$ are sets of profiled partial arguments; and
(2)
${P T A}_{i}$ is a set of assumptions appearing in the proponent partial arguments (up to stage i) that are to be attacked by the opponent; and
(3)
$P P T_{0}$ contains exactly one profiled partial argument consisting of only the root labeled by σ, i.e. ${P P T}_{0} = {(T_{0}, h_{0})}$ where $T_{0} = [σ]$ and $h_{0} = ([σ], 0)$ , and
(4)
${P T A}_{0} = \emptyset$ if σ is not an assumption, otherwise ${P T A}_{0} = {σ}$ , and
(5)
${O P T}_{0} = \emptyset$ .

at stage $i > 0$ , one of the dispute parties makes a move transforming the dispute from state $i - 1$ to state i as follows: (1)
Suppose the proponent makes a move at stage i. The proponent can choose one of the following two options: (a)
The proponent expands some profiled partial argument $π = (T, h) \in {P P T}_{i - 1}$ by: *
selecting a non-final leaf node N in T labeled by a non-assumption sentence δ and a rule r with $h d (r) = δ$ ; and
*
expanding $(T, h)$ at N by r.
The result will be: *
${P P T}_{i} = ({P P T}_{i - 1} ∖ {π}) \cup {π^{'}}$ where $π^{'} = (T^{'}, h^{'})$ and $T^{'} = \exp (T, N, r)$ and $h^{'} = h . (T^{'}, i)$ ;25
*
${P T A}_{i} = {P T A}_{i - 1} \cup A s s (r)$
*
${O P T}_{i} = {O P T}_{i - 1}$ .

(b)
The proponent attacks an opponent’s profiled partial argument $π = (T, h) \in {O P T}_{i - 1}$ at an assumption $α \in A s s (T)$ resulting in:

${P P T}_{i} = {P P T}_{i - 1} \cup {(T^{'}, h^{'})}$ where $T^{'} = [\bar{α}]$ and $h^{'} = ([\bar{α}], i)$ ; and

${P T A}_{i} = {P T A}_{i - 1}$

${O P T}_{i} = {O P T}_{i - 1} ∖ {π}$

(2)
Suppose the opponent makes a move at stage i. The opponent can choose one of the following two options: (a)
The opponent expands an opponent profiled partial argument $π = (T, h) \in {O P T}_{i - 1}$ at a non-final leaf node $N \in T$ labeled by a non-assumption sentence δ resulting in:

${P P T}_{i} = {P P T}_{i - 1}$

${P T A}_{i} = {P T A}_{i - 1}$

${O P T}_{i} = ({O P T}_{i - 1} ∖ {π}) \cup {π^{'} | π^{'} = (T^{'}, h^{'}), T^{'} \in C E (T, N), h^{'} = h . (T^{'}, i)}$ 26
(b)
The opponent attacks an assumption $α \in {P T A}_{i}$ resulting in:

${P P T}_{i} = {P P T}_{i - 1}$

${P T A}_{i} = {P T A}_{i - 1} ∖ {α}$

${O P T}_{i} = {O P T}_{i - 1} \cup {π}$ where $π = (T, h)$ and $T = [\bar{α}]$ and $h = ([\bar{α}], i)$

Remark 7.

When opponent carries out step (2.a), it is possible that $C E (T, N) = \emptyset$ . We often refer to this case as a failed expansion of opponent profiled partial argument π.

Note that if the assumption-based framework is not finitary, the set ${O P T}_{i}$ in step (2a) could be infinite, and hence not implementable.

A dispute derivation is successful (for the proponent) if i) the proponent manages to construct in full her arguments to support her stated conclusion and to defend against the attacks from the opponent and ii) the opponent runs out of attacks against the proponent.
Definition 14 Successful Grounded Dispute Derivation

A grounded dispute derivation

\begin{aligned} ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩ \end{aligned}

is successful (for the proponent) if

{P T A}_{n} = {O P T}_{n} = \emptyset

and for each

(T, h) \in {P P T}_{n}

, T is a full argument.

Table 1
A successful grounded dispute derivation of $F_{2}$ .

Stage Move $P P T$ $P T A$ $O P T$

0 $π_{0} = (T_{0}, h_{0})$ $h_{0} = (T_{0}, 0)$ $\emptyset$ $\emptyset$

1 $1 a$ $π_{1} = (T_{1}, h_{1})$ $h_{1} = (T_{0}, 0), (T_{1}, 1)$ $n o t_α$ $\emptyset$

2 $2 b$ $π_{1} = (T_{1}, h_{1})$ , $h_{1} = (T_{0}, 0), (T_{1}, 1)$ $\emptyset$ $π_{0}^{^{'}} = (T_{0}^{^{'}}, h_{0}^{^{'}})$ $h_{0}^{^{'}} = (T_{0}^{^{'}}, 2)$

3 $2 a$ $π_{1} = (T_{1}, h_{1})$ , $h_{1} = (T_{0}, 0), (T_{1}, 1)$ $\emptyset$ $π_{1}^{^{'}} = (T_{1}^{^{'}}, h_{1}^{^{'}})$ $h_{1}^{^{'}} = (T_{0}^{^{'}}, 2), (T_{1}^{^{'}}, 3)$

4 $1 b$ $π_{1} = (T_{1}, h_{1})$ , $h_{1} = (T_{0}, 0), (T_{1}, 1)$ $π_{0}^{^{″}} = (T_{0}^{^{″}}, h_{0}^{^{″}})$ , $h_{0}^{^{″}} = (T_{0}^{^{″}}, 4)$ $\emptyset$ $\emptyset$

5 $1 a$ $π_{1} = (T_{1}, h_{1})$ , $h_{1} = (T_{0}, 0), (T_{1}, 1)$ $π_{1}^{^{″}} = (T_{1}^{^{″}}, h_{1}^{^{″}})$ , $h_{1}^{^{″}} = (T_{0}^{^{″}}, 4), (T_{1}^{^{″}}, 5)$ $\emptyset$ $\emptyset$

Example 5.

A successful grounded dispute derivation

\begin{aligned} ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{5}, {P T A}_{5}, {O P T}_{5} ⟩ \end{aligned}

for sentence a (wrt the argumentation framework

F_{2}

in the introduction) is illustrated in Table 1 and explained in details below. For convenience we recall

F_{2}

below.

\begin{aligned} F_{2} : r : a \leftarrow n o t_α r^{″} : α \leftarrow n o t_β, f (0) r_{n} : f (n) \leftarrow f (n + 1), n ⩾ 0 \\ t : β \leftarrow \end{aligned}

At stage 0, we have ${P P T}_{0} = {π_{0}}$ , ${P T A}_{0} = {O P T}_{0} = \emptyset$ where $π_{0} = (T_{0}, h_{0})$ and $T_{0} = [a]$ and $h_{0} = (T_{0}, 0)$ .

At stage 1, the proponent makes a move to expand the ppa $π_{0}$ by applying step (1a) using rule r.

Hence ${P P T}_{1} = ({P P T}_{0} ∖ {π_{0}}) \cup {π_{1}} = {π_{1}}$ where $π_{1} = (T_{1}, h_{1})$ , $T_{1} = \exp (T_{0}, r o o t, r)$ and $h_{1} = (T_{0}, 0), (T_{1}, 1)$ ( $T_{1}$ is illustrated in Fig. 8).

Since rule r has the assumption $n o t_α$ (i.e. $A s s (r) = {n o t_α}$ ), we have ${P T A}_{1} = {P T A}_{0} \cup A s s (r) = {P T A}_{0} \cup {n o t_α} = {n o t_α}$ .

${O P T}_{1} = {O P T}_{0} = \emptyset$ .

Next, at stage 2, the opponent attacks the assumption $n o t_α \in {P T A}_{1}$ by applying step (2b). Hence ${O P T}_{2} = {O P T}_{1} \cup {π_{0}^{^{'}}} = {π_{0}^{^{'}}}$ where $π_{0}^{^{'}} = (T_{0}^{^{'}}, h_{0}^{^{'}})$ with $T_{0}^{^{'}} = [α]$ and $h_{0}^{^{'}} = (T_{0}^{^{'}}, 2)$ stating that $T_{0}^{^{'}}$ is created at stage 2 (See Fig. 8).

${P P T}_{2} = {P P T}_{1} = {π_{1}}$ .

${P T A}_{2} = {P T A}_{1} ∖ {n o t_α} = \emptyset$ .

At stage 3, the opponent applies step (2a) to expand $T_{0}^{^{'}}$ to $T_{1}^{^{'}}$ . Since rule $r^{″}$ is the only one with head α, it follows $C E (T_{0}^{^{'}}, r o o t) = {T_{1}^{^{'}}}$ with $T_{1}^{^{'}} = \exp (T_{0}^{^{'}}, r o o t, r^{″})$ (See Fig. 8). Therefore

${O P T}_{3} = ({O P T}_{2} ∖ {π_{0}^{^{'}}}) \cup {π_{1}^{^{'}}} = {π_{1}^{^{'}}}$ where $π_{1}^{^{'}} = (T_{1}^{^{'}}, h_{1}^{^{'}})$ and $h_{1}^{^{'}} = (T_{0}^{^{'}}, 2), (T_{1}^{^{'}}, 3)$ .

${P P T}_{3} = {P P T}_{2} = {π_{1}}$

${P T A}_{3} = {P T A}_{2} = \emptyset$

At stage 4, the proponent attacks opponent’s ppa $π_{1}^{^{'}}$ at assumption $n o t_β \in T_{1}^{^{'}}$ by applying step (1b).

Therefore ${P P T}_{4} = {P P T}_{3} \cup {π_{0}^{^{″}}} = {π_{1}, π_{0}^{^{″}}}$ where $π_{0}^{^{″}} = (T_{0}^{^{″}}, h_{0}^{^{″}})$ and $T_{0}^{^{″}} = [β]$ and $h_{0}^{^{″}} = (T_{0}^{^{″}}, 4)$ (See Fig. 8).

${P T A}_{4} = {P T A}_{3} = \emptyset$

${O P T}_{4} = {O P T}_{3} ∖ {π_{1}^{^{'}}} = \emptyset$ .

Finally at stage 5, the proponent applies step (1a), using rule t, to expand $T_{0}^{^{″}}$ to argument $T_{1}^{^{″}} = \exp (T_{0}^{^{″}}, r o o t, t)$ (See Fig. 8). Therefore

${P P T}_{5} = ({P P T}_{4} ∖ {π_{0}^{^{″}}}) \cup {π_{1}^{^{″}}} = {π_{1}, π_{1}^{^{″}}}$ where $π_{1}^{^{″}} = (T_{1}^{^{″}}, h_{1}^{^{″}})$ with $h_{1}^{^{″}} = (T_{0}^{^{″}}, 4), (T_{1}^{^{″}}, 5)$ .

${P T A}_{5} = {P T A}_{4} \cup A s s (t) = \emptyset$

${O P T}_{5} = {O P T}_{4} = \emptyset$

As there is no any other assumption in $P T A_{5}$ and $O P T_{5}$ is empty and all ppa in $P P T_{5}$ are full, the derivation is successful.

Fig. 8.

Proof trees for Example 5.

Example 6.

Consider the following argumentation framework

\begin{aligned} F_{3} : r : p \leftarrow n o t_a \end{aligned}

Table 2

A successful grounded dispute derivation of $F_{3}$ .

Stage	Move	$P P T$	$P T A$	$O P T$
0		$π_{0} = (T_{0}, h_{0})$ $h_{0} = (T_{0}, 0)$	$\emptyset$	$\emptyset$
1	$1 a$	$π_{1} = (T_{1}, h_{1})$ $h_{1} = (T_{0}, 0), (T_{1}, 1)$	$n o t_a$	$\emptyset$
2	$2 b$	$π_{1} = (T_{1}, h_{1})$ $h_{1} = (T_{0}, 0), (T_{1}, 1)$	$\emptyset$	$π_{0}^{^{'}} = (T_{0}^{^{'}}, h_{0}^{^{'}})$ $h_{0}^{^{'}} = (T_{0}^{^{'}}, 2)$
3	$2 a$	$π_{1} = (T_{1}, h_{1})$ $h_{1} = (T_{0}, 0), (T_{1}, 1)$	$\emptyset$	$\emptyset$

Fig. 9.

Proof trees of the dispute derivation for sentence “p”.

A successful dispute derivation for sentence “p”

\begin{aligned} ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{3}, {P T A}_{3}, {O P T}_{3} ⟩ \end{aligned}

is illustrated in Table 2 and is explained in details below.

At stage 0, we have ${P P T}_{0} = {π_{0}}$ , ${P T A}_{0} = {O P T}_{0} = \emptyset$ where $π_{0} = (T_{0}, h_{0})$ and $T_{0} = [p]$ and $h_{0} = (T_{0}, 0)$ (see Fig. 9).

At stage 1, the proponent makes a move to expand the ppa $π_{0}$ by applying step (1a) using rule r.

Hence ${P P T}_{1} = ({P P T}_{0} ∖ {π_{0}}) \cup {π_{1}} = {π_{1}}$ where $π_{1} = (T_{1}, h_{1})$ , $T_{1} = \exp (T_{0}, r o o t, r)$ (see Fig. 9) and $h_{1} = (T_{0}, 0), (T_{1}, 1)$ .

Since rule r has the assumption $n o t_a$ (i.e. $A s s (r) = {n o t_a}$ ), we have ${P T A}_{1} = {P T A}_{0} \cup A s s (r) = {P T A}_{0} \cup {n o t_a} = {n o t_a}$ .

${O P T}_{1} = {O P T}_{0} = \emptyset$ .

Next, at stage 2, the opponent attacks the assumption $n o t_a \in {P T A}_{1}$ by applying step (2b). Hence ${O P T}_{2} = {O P T}_{1} \cup {π_{0}^{^{'}}} = {π_{0}^{^{'}}}$ where $π_{0}^{^{'}} = (T_{0}^{^{'}}, h_{0}^{^{'}})$ with $T_{0}^{^{'}} = [a]$ and $h_{0}^{^{'}} = (T_{0}^{^{'}}, 2)$ stating that $T_{0}^{^{'}}$ is created at stage 2 (see Fig. 9).

${P P T}_{2} = {P P T}_{1} = {π_{1}}$ .

${P T A}_{2} = {P T A}_{1} ∖ {n o t_a} = \emptyset$ .

At stage 3, the opponent applies step (2a) to expand $T_{0}^{^{'}}$ . Since there is no rule with head a, it follows $C E (T_{0}^{^{'}}, r o o t) = \emptyset$ . Therefore

${O P T}_{3} = ({O P T}_{2} ∖ {π_{0}^{^{'}}}) \cup \emptyset = \emptyset$ .

${P P T}_{3} = {P P T}_{2} = {π_{1}}$

${P T A}_{3} = {P T A}_{2} = \emptyset$

As there is no any other assumption in $P T A_{3}$ and $O P T_{3}$ is empty and all ppa in $P P T_{3}$ are full, the derivation is successful.

5. .Soundness of grounded dispute derivation

We first introduce some new notations.

Notation 6.

We say a ppa $π^{'}$ is a continuation of another ppa π iff $h_{π}$ is a prefix of $h_{π^{'}}$ (and hence $T_{π} \subseteq T_{π^{'}}$ and $s t (π) = s t (π^{'})$ ).

$π^{'}$ is an immediate expansion of π if $h_{π} = (T_{0}, t_{0}), . . ., (T_{k}, t_{k})$ and $h_{π^{'}} = h_{π} . (T_{k + 1}, t_{k + 1})$ .27

A ppa π is said to be full iff $T_{π}$ is an argument.

We say two ppas π, $π^{'}$ are compatible if $s t (π) = s t (π^{'})$ and $T_{π}$ , $T_{π^{'}}$ are compatible.

We often refer to a ppa appearing in some ${P P T}_{i}$ (resp. ${O P T}_{i}$ ) in a grounded dispute derivation as a proponent ppa (resp opponent ppa).

The following lemma expresses the intuition that when the proponent has partially constructed an argument, she is expected to finish it. And she should not construct two distinct arguments for the same purpose at the same time, i.e. at any stage there should be no distinct continuations of the same proponent ppa at some previous stage.
Lemma 7.
Let $d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ be a grounded dispute derivation. (1)
Let π be some proponent ppa appearing in $d d$ . The following statements hold: (a)
For each $i : s t (π) ⩽ i ⩽ n$ , there is an unique continuation of π in ${P P T}_{i}$ .
(b)
Let $π_{i}$ , $π_{i + 1}$ ( $s t (π) ⩽ i < n$ ) be continuations of π in ${P P T}_{i}$ , ${P P T}_{i + 1}$ respectively. Then $π_{i + 1}$ is either an immediate expansion of $π_{i}$ or identical to $π_{i}$ .

(2)
Let π, $π^{'}$ be two proponent ppas in $d d$ such that $s t (π) = s t (π^{'})$ . Then one is a continuation of the other.

Consequently, if π, $π^{'}$ are full then they are identical.

Proof.
See proof of Lemma 7 in Appendix A.3.

The following lemma states intuitively that at any stage in a derivation, it is not possible for the opponent to construct the same argument in different ways.
Lemma 8.
Let $d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ be a grounded dispute derivation. It holds that for each $0 ⩽ i ⩽ n$ , for all $π, π^{'} \in {O P T}_{i}$ , if π, $π^{'}$ are compatible then π, $π^{'}$ are identical.
Proof.
See proof of Lemma 8 in Appendix A.3.
Remark 8.
An opponent ppa π in a dispute derivation $d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ is said to be discontinued at step i iff $π \in {O P T}_{i - 1}$ and there is no continuation of π afterwards, i.e. $\forall j ⩾ i$ there is no continuation of π in ${O P T}_{j}$ .

It is obvious that in a successful grounded dispute derivation, every opponent ppa is discontinued at some stage. The following lemma sheds light on the structure of the evolution of opponent ppas in a grounded dispute derivation.
Lemma 9.
Let $d d$ be a dispute derivation $d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ .

Further let A be an argument such that $C l (A) = \bar{α}$ for some assumption α and $π = ([\bar{α}], ([\bar{α}], i)) \in {O P T}_{i}$ for some $0 ⩽ i ⩽ n$ .

Then there is an unique sequence ${c o n t}_{d d} (π) = π_{0}, . . ., π_{k}$ ( $i ⩽ i + k ⩽ n$ ) such that (1)
$π_{0} = π$ ; and
(2)
for each $i < j ⩽ k$ , $π_{j} \in {O P T}_{i + j}$ and $π_{j}$ is a continuation of $π_{j - 1}$ and $T_{π_{j}} \subseteq A$ ; and
(3)
if $i + k < n$ then $π_{k}$ is discontinued at $i + k + 1$ and there is no ppa at any ${O P T}_{i + k + 1}, . . ., {O P T}_{n}$ that is compatible with $π_{k}$ .

Proof.
See proof of Lemma 9 in Appendix A.3.

The following lemma states that each argument attacking a proponent argument in a successful dispute derivation is counter-attacked by some proponent argument.
Lemma 10.
Let $d d$ be a successful grounded dispute derivation that terminates at $⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ and $π = (T, h) \in {P P T}_{n}$ and $T^{'}$ be an argument attacking argument T. Then there is a opponent ppa $π^{'}$ such that $s t (π) < s t (π^{'})$ and $T_{π^{'}} \subseteq T^{'}$ and $π^{'}$ is discontinued at some step between $s t (π^{'})$ and n.
Proof.
See proof of Lemma 10 in Appendix A.3.

The following theorem shows that in a successful dispute derivation, each proponent argument whose construction started at some stage i is defended by the proponent arguments constructed after stage i.
Theorem 3.
Let $d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ be a successful grounded dispute derivation and $π = (T, h) \in {P P T}_{n}$ . Further let $T_{π} = {T_{π^{'}} | π^{'} \in {P P T}_{n} a n d s t (π^{'}) > s t (π)}$ . It holds:
$\begin{aligned} T \in F_{{A F}_{F}} (T_{π}) \end{aligned}$

Proof.
Let $T^{'} \in {A r}_{F}$ such that $T^{'}$ attacks T. From Lemma 10 there is opponent ppa $π^{'}$ (discontinued at stage i) such that $s t (π) < s t (π^{'})$ and $T_{π^{'}} \subseteq T^{'}$ .

There are two cases: (1)
Case 1 The opponent makes a move at stage i. Because $π^{'}$ is discontinued at step i, the opponent expands $π^{'}$ at stage i. Because $T_{π^{'}} \subseteq T^{'}$ , it follows from Lemma 3 that $π^{'}$ has a continuation at stage i. Contradiction to the fact that $π^{'}$ is discontinued at stage i. Hence this case is not possible.
(2)
Case 2 The proponent makes a move at stage i. Since $π^{'}$ is discontinued at stage i, it follows that the proponent attacks $π^{'}$ at some assumption α at this stage. Since $T_{π^{'}} \subseteq T^{'}$ , it follows that α appears in $T^{'}$ .

Hence a new proponent ppa $π_{1} = (T_{1}, h_{1})$ is created in ${P P T}_{i}$ where $T_{1} = [\bar{α}]$ and $h_{1} = (T_{1}, i)$ .

Since $d d$ is successful, there is $π_{2} \in {P P T}_{n}$ that is a continuation of $π_{1}$ . Hence $T_{π_{2}}$ attacks $T^{'}$ .

Since $s t (π_{2}) = s t (π_{1}) = i > s t (π^{'}) > s t (π)$ , it follows that $T_{π_{2}} \in T_{π}$ . Thus $T_{π}$ defends T against $T^{'}$ .

Since $T^{'}$ is arbitrary selected, it follows that $T_{π}$ defends T against all attacks against T.

We have proved that $T \in F_{{A F}_{F}} (T_{π})$ .

An immediate consequence of Theorem 3 is the soundness of the grounded dispute procedure as stated in the following theorem. Theorem 4 Soundness Theorem

Let $d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ be a successful grounded dispute derivation. It holds

\begin{aligned} {T_{π} | π \in {P P T}_{n}} \subseteq {G E}_{{A F}_{F}} \end{aligned}

Proof.
Let $m = | {P P T}_{n} |$ . Let $π_{m}, . . ., π_{1}$ be an increasing (according to the starting times) listing of ppas in ${P P T}_{n}$ , i.e. for $m ⩾ i > 1$ , $s t (π_{m}) = 0$ and $s t (π_{i}) < s t (π_{i - 1})$ .

Let $T_{i} = T_{π_{i}}$ . We first prove by induction on i, $T_{i} \in F_{{A F}_{F}}^{i} (\emptyset)$ .

Basic Step $i = 1$ .

From Theorem 3, it follows immediately that $T_{1} \in F_{{A F}_{F}} (\emptyset)$ (because $T_{π_{1}} = \emptyset$ ).

Inductive Step Suppose for all j ( $i > j ⩾ 1$ ), $T_{j} \in F_{{A F}_{F}}^{j} (\emptyset)$ .

We prove that $T_{i} \in F_{{A F}_{F}}^{i} (\emptyset)$ .

From $F_{{A F}_{F}} (\emptyset) \subseteq F_{{A F}_{F}}^{2} (\emptyset) \subseteq \dots \subseteq F_{{A F}_{F}}^{i - 1} (\emptyset)$ and for each j ( $i > j ⩾ 1$ ), $T_{j} \in F_{{A F}_{F}}^{j} (\emptyset)$ , it follows that $T_{π_{i}} = {T_{i - 1}, . . ., T_{1}} \subseteq F_{{A F}_{F}} (\emptyset) \cup F_{{A F}_{F}}^{2} (\emptyset) \cup \dots \cup F_{{A F}_{F}}^{i - 1} (\emptyset) \subseteq F_{{A F}_{F}}^{i - 1} (\emptyset)$ .

Thus from Theorem 3, $T_{i} \in F_{A F} (T_{π_{i}}) \subseteq F_{A F} (F_{{A F}_{F}}^{i - 1} (\emptyset)) = F_{{A F}_{F}}^{i} (\emptyset)$ .

Therefore ${T_{π} | π \in {P P T}_{n}} = {T_{m}, . . ., T_{0}} \subseteq F_{{A F}_{F}}^{m} (\emptyset) \subseteq {G E}_{{A F}_{F}}$ .

6. .Completeness of grounded proof procedure

It should be clear that for each sentence $σ \in C l ({G E}_{{A F}_{F}})$ , there are always some arguments in ${G E}_{{A F}_{F}}$ supporting σ. The completeness of the grounded proof procedure means that at least one of such arguments could be derived in a successful grounded dispute derivation.

In other words, completeness of grounded procedure is not about verifying whether a sentence is supported by an argument in the grounded extension. It is rather about showing that for each sentence in the grounded extension, an argument supporting it could be derived by a grounded derivation.

The proof is constructive by first constructing (according to the definition of strongly grounded dd) for each sentence $σ \in C l ({G E}_{{A F}_{F}})$ , a special kind of grounded dispute derivation, and then show that each of such special grounded derivation is always successful.

For each argument $A \in {G E}_{{A F}_{F}}$ and sentence $δ \in C l ({G E}_{{A F}_{F}})$ , define

\begin{aligned} r a n k (A) = min {i | A \in F_{{A F}_{F}}^{i} (\emptyset)} and \\ r a n k (δ) = min {i | δ \in C l (F_{{A F}_{F}}^{i} (\emptyset))} \end{aligned}

Remark 9.
(1)
Since ${A F}_{F}$ is ω-grounded (because $F$ is finitary (see Convention 1)), both $r a n k (A)$ and $r a n k (δ)$ are natural numbers.
(2)
It is not difficult to see that for each $A \in {G E}_{{A F}_{F}}$ , $r a n k (C l (A)) ⩽ r a n k (A)$ .
(3)
For each $δ \in C l ({G E}_{{A F}_{F}})$ , an argument $A \in {G E}_{{A F}_{F}}$ with $C l (A) = δ$ and $r a n k (δ) = r a n k (A)$ , is often referred to as a ground support of δ.

It is obvious that each sentence $δ \in C l ({G E}_{{A F}_{F}})$ has a ground support.
(4)
A mapping λ assigning to each sentence in $δ \in C l ({G E}_{{A F}_{F}})$ a ground support $λ (δ) \in {G E}_{{A F}_{F}}$ of δ is often referred to as a ground map of $F$ .28

Lemma 11.
Let $A \in {G E}_{{A F}_{F}}$ and $α \in A s s (A)$ . Further let B be an argument attacking α. The following statements hold: (1)
$α \in C l ({G E}_{{A F}_{F}})$ and $r a n k (α) ⩽ r a n k (A)$ ; and
(2)
There is an assumption $β \in A s s (B)$ such that $\bar{β} \in C l ({G E}_{{A F}_{F}})$ and $r a n k (\bar{β}) < r a n k (α)$ .

Proof.
Since $A \in {G E}_{{A F}_{F}}$ , it follows from Theorem 2 that $A \in F_{{A F}_{F}}^{k} (\emptyset)$ where $k = r a n k (A)$ and k is a natural number. Hence, every attack against A is attacked by some argument in $F_{{A F}_{F}}^{k - 1} (\emptyset)$ . Thus every attack against α is attacked by some argument in $F_{{A F}_{F}}^{k - 1} (\emptyset)$ implying that $α \in C l (F_{{A F}_{F}}^{k} (\emptyset))$ . Hence $r a n k (α) ⩽ k = r a n k (A)$ .

Let $r a n k (α) = m$ . Hence $α \in C l (F_{{A F}_{F}}^{m} (\emptyset))$ . From Theorem 2, m is a natural number. Thus every attack against α is attacked by some argument in $F_{{A F}_{F}}^{m - 1} (\emptyset)$ . It follows that B is attacked by some argument $C \in F_{{A F}_{F}}^{m - 1} (\emptyset)$ at some assumption $β \in A s s (B)$ . Thus $C l (C) = \bar{β}$ and $r a n k (\bar{β}) ⩽ r a n k (C) ⩽ m - 1 < m = r a n k (α) ⩽ r a n k (A)$ .

We introduce the concept of strongly grounded dispute derivation below where the proponent arguments are grounded according to some ground map λ. This concept is inspired by the idea of the H-constrainted dispute derivations for admissibility semantics in [31].

The construction of strongly grounded dispute derivations mimics such derivations in abstract argumentation when arguments are assumed to be given and a key basic step is like: “pick some argument…”.

This step is elaborated in the strongly grounded dispute derivation by the proponents and opponents as follows:

Once the proponent has started to build up an argument, she will continue until getting the full argument constructed without being bothered to attack the other’s arguments. The opponent is not allowed to disrupt her even if he could attack her still partly constructed argument at some stage.

On the contrary, the opponent’s construction of his arguments will be disrupted by attacks from the proponent whenever she could launch such attacks. But the opponent is not allowed to interrupt the constructions of his own arguments to launch an attack against a proponent argument even if such attack is possible.
Definition 15 Strongly Grounded Dispute Derivation

A strongly grounded dispute derivation for a sentence δ wrt a ground map λ is a grounded dispute derivation for δ (as defined in Definition 13) such that the following extra constraints are satisfied:

The proponent executes step (1.a) (to expand proponent ppa $π = (T, h)$ ) with an extra condition that $\exp (T, N, r) \subseteq λ (C l (T))$ ;

The proponent executes step (1.b) (to attack an opponent ppa $π = (T, h) \in {O P T}_{i}$ at an assumption $α \in A s s (T)$ ) with two extra conditions:

*
$\bar{α} \in C l ({G E}_{{A F}_{F}})$ and $r a n k (\bar{α}) < r a n k (t a r g e t (π))$ ; and
*
step (1.a) is not possible;

The opponent executes step (2.a) (to expand an opponent ppa $π = (T, h) \in {O P T}_{i}$ ) with two extra conditions: *
$h (N, T) = h i (T)$ ;29
*
It is not possible for the proponent to perform any of steps (1.a) or (1.b).

The opponent executes step (2.b) (to attack a proponent assumption $α \in {P T A}_{i}$ ) with two extra conditions: *
It is not possible for the proponent to perform any of steps (1.a) or (1.b);
*
It is not possible for the opponent to perform step (2.a).

Remark 10.
We often simply refer to a strongly grounded dispute derivation without explicitly mentioning the associated ground map if there is no possibilities for misunderstanding.
Definition 16.
A strongly grounded dispute derivation $⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ is said to be terminated if neither the proponent nor the opponent could make a move at stage n.
Theorem 5 Completeness Theorem

Let $F$ be a finitary ABA framework and $σ \in C l ({G E}_{{A F}_{F}})$ . Then there is a successful strongly grounded dispute derivation for σ $⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ such that $σ \in C l (T_{π})$ for some $π \in {P P T}_{n}$ .

Proof.
See Section 6.1.

The proof of the completeness theorem follows directly from two insights: i)
each terminated strongly grounded dispute derivation for $σ \in C l ({G E}_{{A F}_{F}})$ is successful; and
ii)
there is no infinite strongly grounded dispute derivation.

We first show below that each terminated strongly grounded dispute derivation for $σ \in C l ({G E}_{{A F}_{F}})$ is successful.
Theorem 6.
Let $s d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ be a terminated strongly grounded dispute derivation for $δ \in C l ({G E}_{{A F}_{F}})$ wrt a ground map λ. Then $s d d$ is successful.
Proof.
Let $π \in {P P T}_{n}$ and $h_{π} = (T_{0}, i_{0}) . . . (T_{m}, i_{m})$ with $T_{0} = [δ]$ . From the design of the proof procedure in definitions 13, 15, it holds: $T_{0} \subset T_{1} \subset \dots \subset T_{m} \subseteq λ (δ)$ . Since $s d d$ is terminated, it is not possible to expand $T_{m}$ further into $λ (δ)$ . Hence $λ (δ) = T_{m} = T_{π}$ . Hence $T_{π}$ is a full argument.

Since the opponent can not carry out step (2.b) (attack proponent assumptions in ${P T A}_{n}$ ), even though all other steps are not possible, it follows that ${P T A}_{n} = \emptyset$ .

Since the opponent can not carry out step (2.a) (expand opponent partial arguments) even though none of steps (1.a, 1.b, 2.b) can be executed, it follows that for each $π \in {O P T}_{n}$ : $T_{π}$ is a full argument and there is $p \in {P P T}_{n}$ s.t. $T_{π}$ attacks $T_{p}$ . Since $T_{p} = λ (C l (T_{p}))$ , $T_{p} \in {G E}_{{A F}_{F}}$ .

From Lemma 11, it follows there is an assumption $α \in A s s (T_{π})$ such that $\bar{α} \in C l ({G E}_{{A F}_{F}})$ and $r a n k (\bar{α}) < r a n k (t a r g e t (π))$ . Thus it is possible for the proponent to execute step (1b) at stage n. Contradiction. Therefore π does not exist. Hence ${O P T}_{n} = \emptyset$ .

We have proved that $s d d$ is successful.

To show the completeness theorem, it remains for us to show that there is no infinite strongly grounded dispute derivation.
Lemma 12.
Let $s d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ be a strongly grounded dispute derivation wrt a ground map λ. The following statements hold: (1)
Each ${P P T}_{i}$ contains at most one not-full ppa;
(2)
Let $π \in {P P T}_{i}$ , $0 ⩽ i ⩽ n$ . Then it holds that π is not full iff there is an unique immediate expansion of π in ${P P T}_{i + 1}$ ;
(3)
Let $π = (T, h) \in {P P T}_{i}$ , $0 ⩽ i ⩽ n$ . Then h is of the form
$\begin{aligned} h = (T_{0}, i_{0}), (T_{1}, i_{0} + 1), . . ., (T_{k}, i_{0} + k) \end{aligned}$
such that

$i_{0} + k ⩽ i$ ; and

$T_{j} \subseteq λ (C l (T)))$ for $k ⩾ j ⩾ 1$ ; and

if π is not full then $i_{0} + k = i$ .
(4)
Let $π \in {P P T}_{i}$ ( $0 ⩽ i ⩽ n$ ) such that the proponent does not make a move to expand π at some stage k with $i ⩾ k > s t (π)$ . Then π is full.

Proof.
(1)
By induction on i. The statement holds obviously for $i = 0$ .

Suppose the statement holds for i. We show that it also holds for $i + 1$ . If the opponent makes a move at stage $i + 1$ then ${P P T}_{i + 1} = {P P T}_{i}$ . The statement holds obviously.

If the proponent executes step (1b) at stage $i + 1$ meaning that step (1a) is not possible at this stage. Hence all ppas in ${P P T}_{i}$ are full. The statement holds obviously.

Suppose the proponent executes step (1a) at stage $i + 1$ (to expand a ppa $π \in {P P T}_{i}$ into a new ppa $π^{'} \in {P P T}_{i + 1}$ ). Hence π is the only non-full ppa in ${P P T}_{i}$ . Therefore, if $π^{'}$ is full, there is no non-full ppa in ${P P T}_{i + 1}$ . If $π^{'}$ is not full, $π^{'}$ is the only non-full ppa in ${P P T}_{i + 1}$ . The statement holds.
(2)
Suppose π is not full. It follows immediately from the definition of sdd that the proponent will execute step (1a) at stage $i + 1$ to expand π into $π^{'} \in {P P T}_{i + 1}$ . The uniqueness of $π^{'}$ follows from Lemma 7.

Suppose $π^{'} \in {P P T}_{i + 1}$ is the unique immediate expansion of π. Hence π is no-full obviously.
(3)
By induction on i with $i ⩾ i_{0}$ . The statement holds obviously for $i = i_{0}$ . Suppose the statement holds for $i ⩾ i_{0}$ . We show that it also holds for $i + 1$ .

Let $π \in {P P T}_{i + 1}$ . There are two cases:

Case 1 $π \in {P P T}_{i}$ . From statements (1,2) and Lemma 7, it follows that π is full. The statement follows directly from the induction hypothesis.

Case 2 $π \notin {P P T}_{i}$ . Hence the proponent executes step (1a) at stage $i + 1$ to expand some $p \in {P P T}_{i}$ into π with $h_{p} = (T_{0}, i_{0}), (T_{1}, i_{0} + 1), . . ., (T_{k}, i_{0} + k)$ and $T_{p} = T_{k}$ . Hence p is not full. From the induction hypothesis, we have $i_{0} + k = i$ . Therefore $h_{π} = h_{p} . (T_{π}, i + 1)$ and $T_{π} \subseteq C l (T_{π})$ . Hence the statement holds.
(4)
Suppose π is not full. From statement (3), $h_{π} = (T_{0}, i_{0}), (T_{1}, i_{0} + 1), . . ., (T_{k}, i_{0} + k)$ with $i_{0} + k = i$ where $i_{0} = s t (π)$ . It follows that the proponent makes the move (1a) at every stage $j : i ⩾ j > 0$ . Contradiction. We have proved that π is full.

Lemma 13.
Let $s d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ be a strongly grounded dispute derivation for $δ \in C l ({G E}_{{A F}_{F}})$ wrt a ground map λ.

It holds that for all i: ${P T A}_{i} \subseteq C l ({G E}_{{A F}_{F}})$ .
Proof.
Let $α \in {P T A}_{i}$ , $0 ⩽ i ⩽ n$ . We show by induction on i that $α \in C l ({G E}_{{A F}_{F}})$ .

Base Step: “ $i = 0$ ”. If δ is not an assumption then ${P T A}_{0} = \emptyset$ . The lemma holds vacuously. Suppose δ is an assumption. The lemma holds since it is assumed that $δ \in C l ({G E}_{{A F}_{F}})$ .

Inductive Step: Suppose the lemma holds for $i - 1$ . We show that it also holds for i.

The lemma follows directly from the inductive hypothesis if at step i, the opponent makes a move or the proponent attacks an opponent ppa.

Suppose now that the proponent expands some ppa π at step i. If $α \in {P T A}_{i - 1}$ , the lemma follows from the inductive hypothesis.

Suppose now $α \in {P T A}_{i} ∖ {P T A}_{i - 1}$ . Therefore $α \in A s s (λ (C l (T_{π}))$ . Since $λ (C l (T_{π})) \in {G E}_{{A F}_{F}}$ , it follows $α \in C l ({G E}_{{A F}_{F}})$ .
Lemma 14.
Let $s d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ be a strongly grounded dispute derivation for $δ \in C l ({G E}_{{A F}_{F}})$ wrt a ground map λ.

For each $0 ⩽ i ⩽ n$ , for all $π, π^{'} \in {O P T}_{i}$ , it holds that $s t (π) = s t (π^{'})$ .
Proof.
Suppose there are π, $π^{'}$ s.t. $s t (π) \neq s t (π^{'})$ ; Without loss of generality, we assume that $s t (π) < s t (π^{'})$ . We first show that π is full.

Suppose π is not full. That means that at stage $s t (π^{'})$ , the opponent attacks a proponent assumption (step 2.b) even though the opponent could have perform step (2a) (expanding a prefix of π). Hence $s d d$ is not a strongly grounded dispute derivation. Contradiction.

We have proved that π is full.

Since step (2a) has higher priority than step (2b) in the definition of sdd, it follows that $s t (π) + l h (π) < s t (π^{'})$ .

Since π is full, $T_{π}$ is an argument. Let α be an assumption such that $C l (T_{π}) = \bar{α}$ . From Lemma 13, it follows $α \in C l ({G E}_{{A F}_{F}})$ . From Lemma 11, there is $β \in A s s (T_{π})$ such that $r a n k (\bar{β}) < r a n k (α)$ and $\bar{β} \in C l ({G E}_{{A F}_{F}})$ . It is thus possible for the proponent to execute step (1b) before $s t (π^{'})$ to attack β. Hence $π \notin {O P T}_{i}$ . Contradiction.

Therefore the assumption that $s t (π) \neq s t (π^{'})$ is wrong.
Definition 17.
Let π be an opponent ppa and $π^{'}$ , $π^{″}$ be proponent ppas in a strongly grounded dispute derivation $s d d$ . (1)
We say π hits $π^{'}$ at an assumption $α^{'} \in A s s (T_{π^{'}})$ if
$π^{'}$ is full and $\bar{α^{'}} = C l (T_{π})$ ; and

$s t (π^{'}) < s t (π)$ ; and

there is no opponent ppa p in $s d d$ such that $\bar{α^{'}} = C l (T_{p})$ and $s t (π^{'}) < s t (p) < s t (π)$ .
We say π hits $π^{'}$ if π hits $π^{'}$ at some assumption.
(2)
We say $π^{'}$ hits π (at an assumption $α \in A s s (T_{π})$ ) if the proponent attacks π at assumption α at stage $s t (π^{'})$ .
(3)
We say $π^{″}$ supports $π^{'}$ if there is an opponent ppa p such that p hits $π^{'}$ and $π^{″}$ hits p.

It is not difficult to see that the following lemma holds.
Lemma 15.
Let π be an opponent ppa and $π^{'}$ be proponent ppa in a strongly grounded dispute derivation $s d d$ . (1)
for each assumption $α \in T_{π}$ , there is at most one proponent ppa hitting π at α.
(2)
for each assumption $α^{'} \in T_{π^{'}}$ , there is at most one opponent ppa hitting $π^{'}$ at $α^{'}$ .
(3)
if $π^{'}$ hits π then π is discontinued at stage $s t (π^{'})$ ; 30

Lemma 16.
Let π, $π^{'}$ be two proponent ppas in a strongly grounded dispute derivation $s d d$ for $δ \in C l ({G E}_{{A F}_{F}})$ such that $π^{'}$ supports π. It holds $r a n k (C l (T_{π})) > r a n k (C l (T_{π}^{^{'}}))$ .
Proof.
Let p be an opponent ppa such that p hits π and $π^{'}$ hits p.

From Lemma 11, it follows $r a n k (C l (T_{π})) ⩾ r a n k (t a r g e t (p))$ . From the selection criteria for step (1b) in sdd, it follows $r a n k (t a r g e t (p)) > r a n k (C l (T_{π^{'}}))$ .

Hence $r a n k (C l (T_{π})) > r a n k (C l (T_{π^{'}}))$ .
Theorem 7.
Let $s d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩, . . .$ be an infinite strongly grounded dispute derivation for $δ \in C l ({G E}_{{A F}_{F}})$ wrt ground map λ.

Then for each k, the set ${O P T}^{k} = {π \in ⋃_{i = 0}^{\infty} {O P T}_{i} | s t (π) = k}$ is finite.
Proof.
Suppose the contrary that there is k, such that ${O P T}^{k}$ is infinite. From Definition 13 (of grounded dispute derivation), it follows that the opponent attacks a proponent assumption α at stage k. From Lemma 14, it follows ${O P T}_{k} = {π_{0}}$ where $π_{0} = (T_{0}, h_{0})$ with $T_{0} = [\bar{α}]$ and $h_{0} = ([\bar{α}], k)$ .

It follows that ${O P T}^{k}$ has the structure of a tree $T_{k}$ as follows:

The root of $T_{k}$ is $π_{0}$ . A ppa $π^{'} \in {O P T}^{k}$ is a child of $π \in {O P T}^{k}$ iff $π^{'}$ is an immediate expansion of π.

Because $F$ is finitary, each ppa has only finitely many immediate expansions. Hence each node in $T_{k}$ has finitely many children. Since $T_{k}$ is infinite (because ${O P T}^{k}$ is infinite), there is an infinite path labeled by $π_{0}, π_{1}, . . .$ , in $T_{k}$ such that $π_{i + 1}$ is an immediate expansion of $π_{i}$ .

We show that $T = ⋃_{i = 0}^{\infty} T_{π_{i}}$ is a full argument. Suppose T is not a full argument. Then there is a non-final leaf node N in T. Therefore there is m such that for each $j ⩾ m$ , N is a non-final leaf node in $T_{π_{j}}$ .

For each $j ⩾ m$ , let $N_{j}$ be the non-final leaf node in $T_{π_{j}}$ selected for expansion to $T_{π_{j + 1}}$ . It follows from the extra condition for step (2a) in Definition 15 of sdd, that $h (N_{j}, T) = h (N_{j}, T_{π_{j}}) ⩽ h (N, T_{π_{j}}) = h (N, T)$ . The set of $N_{j} s$ is therefore finite implying that the sequence $π_{0}, π_{1}, . . .$ is finite. Contradiction.

We have proved that T is a full argument.

It is clear that T attacks α. Since $α \in C l ({G E}_{{A F}_{F}})$ (Lemma 13), T is attacked by some $X \in {G E}_{{A F}_{F}}$ such that $r a n k (X) < r a n k (α)$ . It follows there is $β \in A s s (T)$ such that $\bar{β} = C l (X)$ . Hence $r a n k (\bar{β}) < r a n k (X) < r a n k (α)$ .

Let $j = min {i | β \in A s s (T_{π_{i}})}$ . From Definition 15 of sdd, it is possible for the proponent to execute step (1b) at stage j or some later stage $> j$ .31 As step (1b) has higher priority than step (2a), the infinite path $π_{0}, π_{1}, . . .$ , in $T_{k}$ does not exist. Contradiction

Hence tree $T_{k}$ is finite. Contradiction. Hence we have proved that ${O P T}^{k}$ is finite.
Lemma 17.
Let $s d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩, . . .$ be an infinite strongly grounded dispute derivation for $δ \in C l ({G E}_{{A F}_{F}})$ wrt ground map λ.

Let $π \in \cup {{P P T}_{i} | i ⩾ 0}$ and π be a full ppa. Then the set of proponent ppas in sdd supporting π is finite.
Proof.
It is obvious that for each assumption $α \in T_{π}$ there is at most one opponent ppa hitting π at α. Let P be the set of opponent ppas in sdd that hit π. Since $A s s (T_{π})$ is finite, it follows directly from Lemma 15 that P is finite. Hence it also follows directly from Lemma 15 that there are only finite number of proponent ppas hitting the ppas in P. Therefore the lemma holds.
Theorem 8.
Let $s d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩, . . .$ be an infinite strongly grounded dispute derivation wrt ground map λ.

The set of proponent profiled full arguments in $s d d$ is finite.
Proof.
We first prove two relevant properties.
Property 1.
(1)
Each opponent ppa in sdd hits some proponent ppa in sdd;
(2)
Each proponent ppa in sdd that does not start at stage 0 hits some opponent ppa in sdd.
(3)
Each full proponent ppa in sdd that does not start at stage 0 supports some other full proponent ppa in sdd.

Proof of Property 1. Proof of Property 1.

Statement 2 holds obviously. Statement 3 follows directly from statements 1,2. We prove statement 1. Let π be an opponent ppa in sdd and $i = s t (π)$ and $α \in {P T A}_{i - 1}$ such that $\bar{α} = C l (T_{π})$ .

Let $π^{'}$ be a proponent full ppa in sdd satisfying the following condition:

$α \in A s s (T_{π^{'}})$ ;

$s t (π^{'}) = max {s t (q) | α \in A s s (T_{q}) ~and~ q \in {P P T}_{i - 1}}$

We show that π hits $π^{'}$ . Suppose π does not hit $π^{'}$ . Hence there is opponent ppa p such that $s t (π^{'}) < s t (p) < s t (π)$ s.t. $\bar{α} = C l (T_{p})$ . Let $j = s t (p)$ . It follows $j < i$ and $α \notin {P T A}_{j}$ . Since $α \in {P T A}_{i - 1}$ , it follows that there is proponent full ppa q such that $s t (π^{'}) < j < s t (q) < i$ and $α \in T_{q}$ . Because $s t (q) < i$ , it follows $q \in {P P T}_{i - 1}$ . Contradiction to the construction of $π^{'}$ .

Let $π_{0}$ be the unique proponent profiled full argument such that $s t (π_{0}) = 0$ (the existence and uniqueness of $π_{0}$ follows from Lemma 12).

A support path in $s d d$ is a sequence of profiled full arguments $π_{0}, . . ., π_{n}$ ( $n ⩾ 0$ ) in $⋃_{i = 0}^{\infty} {P P T}_{i}$ such that $π_{i + 1}$ supports $π_{i}$ ( $0 ⩽ i < n$ ).

Property 2.
Each full proponent ppa π in sdd appears as the last element of a support path.

The proof is by induction on $s t (π)$ . The property holds obviously for $s t (π) = 0$ . Suppose that the property holds for all full proponent ppas that start before π. Therefore π supports some full proponent ppa $π^{'}$ (from above Property 1). Hence $s t (π^{'}) < s t (π)$ . From the induction hypothesis, it follows that $π^{'}$ is the last element of some support path $s q$ . Hence $s q . π$ is a support path.

The set of all support paths in $s d d$ forms a tree $T$ where the root is $π_{0}$ and the nodes in $T$ are support paths and a support path $π_{0}, . . ., π_{n}, π_{n + 1}$ is a child of $π_{0}, . . ., π_{n}$ .

Suppose the set of proponent profiled full argument in $s d d$ is infinite. Therefore $T$ is infinite.

From Lemma 17, each node in $T$ has only finitely many children. Hence there is an infinite support path in $T$ . Contrary to Lemma 16.

Hence the set of proponent profiled full arguments in $s d d$ is finite.
6.1. .Proof of completeness theorem

We only need to show that there exists no infinite $s d d$ for δ wrt λ.

Assume that there exists an infinite strongly grounded dispute derivation for $δ \in C l ({G E}_{{A F}_{F}})$ wrt ground map λ

\begin{aligned} s d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{i}, {P T A}_{i}, {O P T}_{i} ⟩, . . . \end{aligned}

From Theorem 8, it follows that there is n such that ${P P T}_{n}$ contains all proponent profiled full arguments in $s d d$ . Therefore the opponent makes a move at all stages $m > n$ in $s d d$ .

Let $K_{0}$ be the set of starting times before n of opponent ppas in $s d d$ while $K_{1}$ be the set of starting times of all opponent ppas in $s d d$ , i.e.

\begin{aligned} K_{0} & = {j | \exists π \in ⋃_{i = 0}^{\infty} O P T_{i} s . t . j = s t (π) < n}, and \\ K_{1} & = {j | \exists π \in ⋃_{i = 0}^{\infty} O P T_{i} s . t . j = s t (π)} . \end{aligned}

From the Definition 15 (of strongly grounded dispute derivation), it follows that $| K_{1} | ⩽ | K_{0} | + | {P T A}_{n} |$ .

From $⋃_{i = 0}^{\infty} {O P T}_{i} = ⋃_{k \in K_{1}} {O P T}^{k}$ , it follows immediately from Theorem 7 that $⋃_{i = 0}^{\infty} {O P T}_{i}$ is finite. Hence $s d d$ is finite. Contradiction.

We have proved that there is no infinite $s d d$ .

The completeness theorem follows directly from Theorem 6.

7. .Flatten dispute derivation

We have presented the grounded dispute derivations that are both sound and complete wrt finitary assumption-based frameworks where proof trees together with their histories are fully and explicitly represented to shed light on the construction process of arguments and counter arguments during a derivation and hence providing key structural insights into the soundness and completeness of the procedure.

In this section, we present another procedure that is simply the result of flattening the first where instead of the whole proof trees, only their supports are recorded. Consequently, the second procedure is both sound and complete but with much simpler date structure and hence much more amenable to possible implementation. The disadvantage of the flatten version (like Prolog for logic programming) is that it does not give the reasons how a returned answer is supported and defended.

In this section we propose the flatten grounded dispute derivations which focus on the supports of proof trees instead of the whole trees like other proposals including [17–19,24].

The representation of flatten grounded dispute derivations is based on multisets. To keep the paper self-contained, we recall in Appendix A.1 a brief but formal introduction of multisets from [31].32

Definition 18 Flatten Grounded Dispute Derivation

A flatten grounded dispute derivation for a sentence δ is a sequence of the form

\begin{aligned} ⟨ {P S}_{0}, {O S}_{0} ⟩, . . ., ⟨ {P S}_{n}, {O S}_{n} ⟩ \end{aligned}

where

for each i, ${P S}_{i}$ is a multiset of sentences while ${O S}_{i}$ is a multisets of multisets of sentences; and

${P S}_{0} = {δ}$ , and ${O S}_{0} = \emptyset$ , and

at stage i ( $i > 0$ ), one of the dispute parties makes a move satisfying the following properties:

(1)
Suppose the proponent makes a move at stage i. The proponent has two options: (a)
The proponent selects a non-assumption $σ \in {P S}_{i - 1}$ , a rule r with $h d (r) = σ$ and,

${P S}_{i} = ({P S}_{i - 1} ∖ {σ}) \oplus b d (r)$

${O S}_{i} = {O S}_{i - 1}$ .
(b)
The proponent selects $S \in {O S}_{i - 1}$ and an assumption $α \in S$ and,

${P S}_{i} = {P S}_{i - 1} \oplus {\bar{α}}$

${O S}_{i} = {O S}_{i - 1} ∖ {S}$

(2)
Suppose the opponent makes a move at stage i. The opponent has two options: (a)
The opponent selects $S \in {O S}_{i - 1}$ and a non-assumption $σ \in S$ and proceeds as follows:

${P S}_{i} = {P S}_{i - 1}$

${O S}_{i} = ({O S}_{i - 1} ∖ {S}) \oplus {(S ∖ {σ}) \oplus b d (r) | h d (r) = σ}$ .
(b)
The opponent selects an assumption $α \in {P S}_{i - 1}$ and,

${P S}_{i} = {P S}_{i - 1} - {α}$

${O S}_{i} = {O S}_{i - 1} \oplus {{\bar{α}}}$ .

Definition 19.
A flatten grounded dispute derivation $⟨ {P S}_{0}, {O S}_{0} ⟩, . . ., ⟨ {P S}_{n}, {O S}_{n} ⟩$ is successful if ${P S}_{n} = {O S}_{n} = \emptyset$ .

Table 3
A successful flatten grounded dispute derivation.

Stage Move $P S$ $O S$

0 ${a}$ $\emptyset$

1 $1 a$ ${n o t_α}$ $\emptyset$

2 $2 b$ $\emptyset$ ${{α}}$

3 $2 a$ $\emptyset$ ${{n o t_β, f (0)}}$

4 $1 b$ ${β}$ $\emptyset$

5 $1 a$ $\emptyset$ $\emptyset$

Example 7.
A successful flatten grounded dispute derivation $⟨ {P S}_{0}, {O S}_{0} ⟩, . . ., ⟨ {P S}_{5}, {O S}_{5} ⟩$ for sentence a (wrt the argumentation framework $F_{2}$ in the introduction) is illustrated in Table 3 and explained in details below. For convenience we recall $F_{2}$ below.
$\begin{aligned} F_{2} : r : a \leftarrow n o t_α r^{″} : α \leftarrow n o t_β, f (0) r_{n} : f (n) \leftarrow f (n + 1), n ⩾ 0 \\ t : β \leftarrow \end{aligned}$

At stage 0, we have ${P S}_{0} = {a}$ and ${O S}_{0} = \emptyset$ .
At stage 1, the proponent makes a move to expand the non-assumption a by applying step (1a) using rule r.

Hence ${P S}_{1} = ({P S}_{0} ∖ {a}) \oplus b d (r) = {n o t_α}$ where $b d (r) = {n o t_α}$ .

${O S}_{1} = {O S}_{0} = \emptyset$ .

Next, at stage 2, the opponent attacks the assumption $n o t_α \in {P S}_{1}$ by applying step (2b). Hence ${O S}_{2} = {O S}_{1} \oplus {{α}} = {{α}}$ .

${P S}_{2} = {P S}_{1} - {n o t_α} = \emptyset$ .

At stage 3, the opponent applies step (2a), selecting $S = {α}$ from $O S_{2}$ and expanding α. Since rule $r^{″}$ is the only one with head α, it follows

${O S}_{3} = ({O S}_{2} ∖ {S}) \oplus {(S ∖ {α}) \oplus b d (r^{″})} = {{n o t_β, f (0)}}$ .

${P S}_{3} = {P S}_{2} = \emptyset$

At stage 4, the proponent applies step (1b) by selecting $S = {n o t_β, f (0)} \in {O S}_{3}$ and assumption $n o t_β \in S$ for attack. Therefore

${P S}_{4} = {P S}_{3} \oplus {β} = {β}$ .

${O S}_{4} = {O S}_{3} ∖ {S} = \emptyset$ .

Finally at stage 5, the proponent applies step (1a), using rule t, to expand β. Therefore

${P S}_{5} = ({P S}_{4} ∖ {β}) \oplus b d (r) = \emptyset$ (since $b d (r) = \emptyset$ ).

${O S}_{5} = {O S}_{4} = \emptyset$

As both PS and OS are empty, the derivation is successful.
Definition 20.
(1)
Let $d d$ be a grounded dispute derivation of length n for a sentence δ (as defined in Definition 13).

Define a sequence of multisets of assumptions
$\begin{aligned} M (d d) = {M P T A}_{0}, . . ., {M P T A}_{n} \end{aligned}$
by:

${M P T A}_{0} = {P T A}_{0}$ .

Suppose ${M P T A}_{i - 1}$ is defined. Then *
${M P T A}_{i} = {M P T A}_{i - 1}$ if the move at stage i is (1b) or (2a);
*
${M P T A}_{i} = {M P T A}_{i - 1} \oplus A s s (r)$ if the move at stage i is (1a);
*
${M P T A}_{i} = {M P T A}_{i - 1} - {α}$ if the move at stage i is (2b);

(2)
For any proof tree T, $N S p m (T)$ and $S p m (T)$ denote respectively the multiset of the non-assumptions and the multiset of sentences labeling the leaf nodes of T and different to $t r u e$ .

$N S p m (T)$ and $S p m (T)$ are often referred to as the multiset non-assumption support or multiset support of T, respectively.

For a set S of ppas, define
$\begin{aligned} N S p m (S) = \oplus {N S p m (T_{π}) | π \in S}; \end{aligned}$

Lemma 18.
Let $d d$ be a grounded dispute derivation of length n for a sentence δ and $M (d d) = {M P T A}_{0}, . . ., {M P T A}_{n}$ . It holds that for all $0 ⩽ i ⩽ n$ , ${M P T A}_{i}$ and ${P T A}_{i}$ are set-equivalent.
Proof.
We prove by induction that for each i, ${M P T A}_{i}$ and ${P T A}_{i}$ are set-equivalent.

It is obvious that ${P T A}_{0} = {M P T A}_{0}$ .

Let $i > 0$ . Suppose for each $j < i$ , ${P T A}_{j}$ and ${M P T A}_{j}$ are set-equivalent. We show ${P T A}_{i}$ and ${M P T A}_{i}$ are set-equivalent. There are four cases according to four possible moves of the players at stage i.
The move at stage i is (1a). Hence ${P T A}_{i} = {P T A}_{i - 1} \cup A s s (r)$ and ${M P T A}_{i} = {M P T A}_{i - 1} \oplus A s s (r)$ . From the induction hypothesis, ${P T A}_{i - 1}$ and ${M P T A}_{i - 1}$ are set-equivalent, it follows obviously that ${P T A}_{i}$ and ${M P T A}_{i}$ are set-equivalent.

The move at stage i is (1b) or (2a). From the induction hypothesis, ${P T A}_{i - 1}$ and ${M P T A}_{i - 1}$ are set-equivalent and ${M P T A}_{i} = {M P T A}_{i - 1}$ and ${P T A}_{i} = {P T A}_{i - 1}$ , it follows obviously that ${P T A}_{i}$ and ${M P T A}_{i}$ are set-equivalent.

The move at stage i is (2b). Hence ${P T A}_{i} = {P T A}_{i - 1} ∖ {α}$ and ${M P T A}_{i} = {M P T A}_{i - 1} - {α}$ . From the induction hypothesis, ${P T A}_{i - 1}$ and ${M P T A}_{i - 1}$ are set-equivalent, it follows obviously that ${P T A}_{i}$ and ${M P T A}_{i}$ are set-equivalent.

The following lemmas show that each grounded dispute derivation could be translated into an equivalent flatten one and vice versa.
Lemma 19.
Let $d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ be a grounded dispute derivation for δ.

Further let $M (d d) = {M P T A}_{0}, . . ., {M P T A}_{n}$ .

Then the sequence $⟨ {P S}_{0}, {O S}_{0} ⟩, . . ., ⟨ {P S}_{n}, {O S}_{n} ⟩$ where for each $0 ⩽ i ⩽ n$ ,
${P S}_{i} = N S p m ({P P T}_{i}) \oplus {M P T A}_{i}$ ; and

${O S}_{i} = {S p m (T_{π}) | π \in {O P T}_{i}}$ ;
is a flatten grounded dispute derivation for δ.
Proof.
See Appendix A.4
Lemma 20.
Let $f d d = ⟨ {P S}_{0}, {O S}_{0} ⟩, . . ., ⟨ {P S}_{n}, {O S}_{n} ⟩$ be a flatten grounded dispute derivation for δ.

There is a grounded dispute derivation $d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ for δ such that for all $0 ⩽ i ⩽ n$ , the following properties hold:
${P S}_{i} = N S p m ({P P T}_{i}) \oplus {M P T A}_{i}$ ; and

${O S}_{i} = {S p m (T_{p}) | p \in {O P T}_{i}}$ ;
where $M (d d) = {M P T A}_{0}, . . ., {M P T A}_{n}$ .
Proof.
See Appendix A.5.
Theorem 9 Soundness Theorem for Flatten Grounded Dispute Derivation

Stage	Move	$P S$	$O S$
0		${a}$	$\emptyset$
1	$1 a$	${n o t_α}$	$\emptyset$
2	$2 b$	$\emptyset$	${{α}}$
3	$2 a$	$\emptyset$	${{n o t_β, f (0)}}$
4	$1 b$	${β}$	$\emptyset$
5	$1 a$	$\emptyset$	$\emptyset$

Let $d d = ⟨ {P S}_{0}, {O S}_{0} ⟩, . . ., ⟨ {P S}_{n}, {O S}_{n} ⟩$ be a successful flatten grounded dispute derivation for δ. Then $δ \in C l ({G E}_{{A F}_{F}})$ .

Proof.
From Lemma 20, there exists a grounded dispute derivation ${d d}^{'} = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ for δ such that ${P S}_{i} = N S p m ({P P T}_{i}) \oplus {M P T A}_{i}$ ; and ${O S}_{i} = {S p m (T_{p}) | p \in {O P T}_{i}}$ ;

Since ${P S}_{n} = \emptyset$ , the sets $N S p m ({P P T}_{n})$ are empty. Therefore all ppas in ${P P T}_{n}$ are full.

As ${O S}_{n} = {S p m (T_{p}) | p \in {O P T}_{n}}$ and ${O S}_{n} = \emptyset$ , it follows ${O P T}_{n} = \emptyset$ .

Because ${P S}_{n} = \emptyset$ and ${P S}_{n} = N S p m ({P P T}_{n}) \oplus {M P T A}_{n}$ , ${M P T A}_{n}$ is empty.

Since ${P T A}_{n}$ and ${M P T A}_{n}$ are set-equivalent (see Lemma 18) and ${M P T A}_{n}$ is empty, ${P T A}_{n}$ is empty.

Therefore ${d d}^{'}$ is a successful grounded dispute derivation. The theorem follows from Theorem 4.
Theorem 10 Completeness Theorem for Flatten Grounded Dispute Derivation

Let $F$ be a finitary ABA framework and $σ \in C l ({G E}_{F})$ . Then there is a successful flatten dispute derivation $⟨ {P S}_{0}, {O S}_{0} ⟩, . . ., ⟨ {P S}_{n}, {O S}_{n} ⟩$ for σ.

Proof.
From the completeness Theorem 5, there is a successful grounded dispute derivation $s d d = ⟨ {P P T}_{0}, {P T A}_{0}, {O P T}_{0} ⟩, . . ., ⟨ {P P T}_{n}, {P T A}_{n}, {O P T}_{n} ⟩$ for σ.

It holds that ${O P T}_{n} = \emptyset$ and all ppas in ${P P T}_{n}$ are full.

Let ${s d d}^{'} = ⟨ {P S}_{0}, {O S}_{0} ⟩, . . ., ⟨ {P S}_{n}, {O S}_{n} ⟩$ be the flatten dispute derivation for σ as defined in Lemma 19.

Since ${P T A}_{n} = \emptyset$ , ${M P T A}_{n} = \emptyset$ (see Lemma 18).

Since all ppas in ${P P T}_{n}$ are full, $N S p m ({P P T}_{n}) = \emptyset$ . It hence follows ${P S}_{n} = N S p m ({P P T}_{n}) \oplus {M P T A}_{n} = \emptyset$ .

Since ${O P T}_{n} = \emptyset$ , ${O S}_{n} = {S p m (T_{p}) | p \in {O P T}_{n}} = \emptyset$ , ${s d d}^{'}$ is successful.
8. .Discussion

We study the soundness and completeness of dialectical proof procedures for assumption-based argumentation with respect to the skeptical semantics. We have presented two proof procedures. In one, proof trees together with their histories are fully and explicitly represented. The other procedure is simply the result of flattening the first. We show the soundness and completeness of both proof procedures wrt grounded semantics of assumption-based argumentation frameworks where possibly non-terminating computation is represented by infinite arguments.

Assumption-based argumentation is an instance of abstract argumentation. Another well-known instance of abstract argumentation is the ASPIC+ system [27,28]. It would be interesting to see how to apply our proof procedures to ASPIC+.

In many applications, a sentence is (universally) accepted if it is accepted in every preferred extensions (or stable extensions) [2]. It would be interesting to see how our proof systems in this paper as well as in [31] could be extended for the universal acceptance.

Attacks may have different strength [16]. [7] proposed a dialectical proof procedure for abstract argumentation frameworks with attacks having different strength. It would be interesting to see how to integrate the ideas of [7]’s into our proof system for assumption-based argumentation with attacks of different strength.

Dialectical proof procedures are not the only approach to proof theory of logical argumentation. [1] proposes dynamic proof systems for logical argumentation. It would be intriguing to see the relationship between these rather distinct approaches.

Grounded semantics of an assumption-based argumentation could be viewed as a form of nonmonotonic inductive definition of the ABA framework [10]. In that sense, our proof system can be viewed as an example of a dialectical proof procedure for a nonmonotonic inductive definition. It may be worth exploring further whether dialectical proof systems could be developed for other nonmonotonic inductive definition systems as defined in [10].

There are recently several interesting works on the semantics of infinite argumentation frameworks [3,4]. It is worth noting that the inclusion of infinite arguments into the argumentation frameworks of assumption-based argumentation does not transform it into infinite argumentation frameworks as illustrated in the introduction. This leads to an interesting question of how to extend the results in [3,4] to frameworks with “two kinds of infinity”: infinite number of arguments and arguments of infinite size.

Dialectical procedures could be viewed as a form of dialogue games where for both players the sets of rules as well as assumptions are given and fixed at the beginning. A more general form of dialogue games is proposed in [23] where rules and assumptions are introduced during the dialogue. While the soundness of such games has been studied in [23], their completeness is not. The completeness results in this paper, especially the completeness of the flatten procedure could shed light on the completeness of such dialogue games.

Footnotes

Notes

References

Arieli

Straßer

, Logical argumentation by dynamic proof systems, Theoretical Computer Science 781 (2019), 63–91, https://www.sciencedirect.com/science/article/pii/S0304397519301252 . doi:10.1016/j.tcs.2019.02.019.

Arioua

Croitoru

, A dialectical proof theory for universal acceptance in coherent logic-based argumentation frameworks, in: Proceedings of the 22nd European Conference on Artificial Intelligence, ECAI 2016, 2016, pp. 55–63, http://liris.cnrs.fr/~aarioua/papers/ECAI2016.pdf .

Baumann

Spanring

, in: Infinite Argumentation Frameworks, 2015, pp. 281–295. ISBN 978-3-319-14725-3. doi:10.1007/978-3-319-14726-0_19.

Belardinelli

Grossi

Maudet

, Formal analysis of dialogues on infinite argumentation frameworks, in: Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI’15, AAAI Press, 2015, pp. 861–867. ISBN 9781577357384.

Blizard

W.D.

, Multiset theory, Notre Dame Journal of Formal Logic 30(1) (1988), 36–66. doi:10.1305/ndjfl/1093634995.

Bondarenko

Dung

P.M.

Kowalski

R.A.

Toni

, An abstract, argumentation-theoretic approach to default reasoning, Artif. Intell. 93 (1997), 63–101. doi:10.1016/S0004-3702(97)00015-5.

Cayrol

Devred

Lagasquie-Schiex

M.-C.

, Dialectical proofs accounting for strength of attacks in argumentation systems, in: 2010 22nd IEEE International Conference on Tools with Artificial Intelligence, Vol. 1, 2010, pp. 207–214, ISSN 2375-0197. doi:10.1109/ICTAI.2010.36.

Cayrol

Doutre

Mengin

, On decision problems related to the preferred semantics for argumentation frameworks, J. Log. Comput. 13(3) (2003), 377–403. doi:10.1093/logcom/13.3.377.

Davey

B.A.

Priestley

H.A.

, Introduction to Lattices and Order, 2nd edn, Cambridge University Press, 2002.

10.

Denecker

Ternovska

, A logic of nonmonotone inductive definitions, ACM Trans. Comput. Logic 9(2) (2008). doi:10.1145/1342991.1342998.

11.

Dershowitz

Manna

, Proving termination with multiset orderings, in: Automata, Languages and Programming, Springer, Berlin Heidelberg, 1979, pp. 188–202. doi:10.1007/3-540-09510-1_15.

12.

Dung

P.M.

, Negation by hypothesis, an abductive foundation of logic programming, in: 8th International Conference on Logic Programming, The MIT Press, Cambridge, and Massachusetts, 1991, pp. 3–17.

13.

Dung

P.M.

, Logic programming as dialogue games, Technical report, Division of Computer Science, Asian Institute of Technology, Thailand (submitted to LPNMR 1993), 1993.

14.

Dung

P.M.

, On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming, in: Proceedings of the 13th International Joint Conference in Artificial Intelligence (IJCAI), 1993, pp. 852–857.

15.

Dung

P.M.

, An argumentation theoretic foundation for logic programming, Journal of Logic Programming 22 (1995), 151–177. doi:10.1016/0743-1066(95)94697-X.

16.

Dung

P.M.

, On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games, Artif. Intell. 77(2) (1995), 321–358. doi:10.1016/0004-3702(94)00041-X.

17.

Dung

P.M.

Kowalski

R.A.

Toni

, Dialectic proof procedures for assumption-based, admissible argumentation, Artif. Intell. 170(2) (2006), 114–159. doi:10.1016/j.artint.2005.07.002.

18.

Dung

P.M.

Kowalski

R.A.

Toni

, Assumption-based argumentation, in: Argumentation in AI, Springer-Verlag, 2009.

19.

Dung

P.M.

Mancarella

Toni

, Computing ideal sceptical argumentation, Artif. Intell. 171(10–15) (2007), 642–674. doi:10.1016/j.artint.2007.05.003.

20.

Dung

P.M.

Thang

P.M.

, A modular framework for dialectical dispute in argumentation, in: Proc of IJCAI, 2009.

21.

Dunne

P.E.

Bench-Capon

T.J.M.

, Two party immediate response disputes: Properties and efficiency, Artif. Intell. 149(2) (2003), 221–250. doi:10.1016/S0004-3702(03)00076-6.

22.

Eshghi

Kowalski

R.A.

, Abduction compared with negation by failure, in: Logic Programming: Proceedings of the Sixth International Conference, The MIT Press, Cambridge, and Massachusetts, 1989, pp. 234–254.

23.

Fan

Toni

, A general framework for sound assumption-based argumentation dialogues, Artif. Intell. 216(1) (2014), 20–54. doi:10.1016/j.artint.2014.06.001.

24.

Gaertner

Toni

, Computing arguments and attacks in assumption-based argumentation, IEEE Intelligent Systems 22(6) (2007), 24–33. doi:10.1109/MIS.2007.105.

25.

Manna

Waldinger

, The Logical Basis for Computer Programming, Addison–Wesley Professional, 1985.

26.

Modgil

Caminada

, Proof theories and algorithms for abstract argumentation, in: Argumentation in AI, Springer Verlag, 2009.

27.

Modgil

Prakken

, A general account of argumentation with preferences, Artificial Intelligence 195 (2013), 361–397, https://www.sciencedirect.com/science/article/pii/S0004370212001361 . doi:10.1016/j.artint.2012.10.008.

28.

Prakken

, An abstract framework for argumentation with structured arguments, Argument & Computation 1 (2010), 93–124. doi:10.1080/19462160903564592.

29.

Spanring

, Set- and graph-theoretic investigations in abstract argumentation, PhD thesis, University of Liverpool, UK, 2017.

30.

Thang

P.M.

Dung

P.M.

, Tribute to Guillermo Simari: Infinite Arguments and Semantics of Assumption-Based Argumentation, College Publication, 2019.

31.

Thang

P.M.

Dung

P.M.

Pooksook

, Infinite arguments and semantics of dialectical proof procedure, J. Arguments and Computation 170(2) (2020), 114–159.

32.

Toni

, A generalised framework for dispute derivations in assumption-based argumentation, Artif. Intell. 195 (2013), 1–43. doi:10.1016/j.artint.2012.09.010.

33.

Toni

, A tutorial on assumption-based argumentation, Journal of Arguments and Computation (2013).

34.

Verheij

, A labeling approach to the computation of credulous acceptance in argumentation, in: JCAI 2007, Veloso

, ed., Morgan Kaufmann, 2007, pp. 623–628.

35.

Vreeswijk

Prakken

, Credulous and sceptical argument games for preferred semantics, in: JELIA 2000, Ojeda-Aciego

de Guzmán

I.P.

Brewka

Pereira

L.M.

, eds, Lecture Notes in Computer Science, Vol. 1919, Springer, 2000, pp. 239–253.

36.

Wielemaker

Schrijvers

Triska

Lager

, SWI-prolog, Theory and Practice of Logic Programming 12(1–2) (2012), 67–96. doi:10.1017/S1471068411000494.

ω -Groundedness of argumentation and completeness of grounded dialectical proof procedures

Abstract

Keywords

1. .Introduction

2.1. .Abstract argumentation

2.2. .Assumption-based argumentation

Remark 4. For convenience, we often refer to a partial proof tree without mentioning its conclusion if there is no possibility for misunderstanding. Notation 1 Nodes in Partial Proof Trees

3.1. .ω-Grounded argumentation frameworks

Definition 7 ω-Groundedness

Definition 8 Admissibility Continuity

Theorem 1 Finitary Defensibility implies ad-Continuity

Lemma 6 Finite Arguments are Finitary Defensible

4. .Grounded dispute derivations

Remark 6 Partial Arguments

Definition 11 Histories of Partial Arguments

Definition 12 Profiled Partial Arguments

7. .Flatten dispute derivation

Definition 18 Flatten Grounded Dispute Derivation

Footnotes

Notes

References

Remark 4.
For convenience, we often refer to a partial proof tree without mentioning its conclusion if there is no possibility for misunderstanding.
Notation 1 Nodes in Partial Proof Trees