Infinite arguments and semantics of dialectical proof procedures

Abstract

We study the semantics of dialectical proof procedures. As dialectical proof procedures are in general sound but not complete wrt admissibility semantics, a natural question here is whether we could give a more precise semantical characterization of what they compute. Based on a new notion of infinite arguments representing (possibly infinite) loops, we introduce a stricter notion of admissibility, referred to as strict admissibility, and show that dialectical proof procedures are in general sound and complete wrt strict admissibility.

Keywords

Dialectical proof procedure infinite arguments admissibility semantic soundness and completeness

1. Introduction

Argumentation is a reasoning model in which reasons for conclusions that are drawn for resolving conflicts are given explicitly. While abstract argumentation studies the acceptance of arguments, structured argument systems like assumption-based argumentation or defeasible logic programming provide frameworks for structuring arguments based on assumptions and rules [5,6,13,23,24,29,31]. Argument-based systems are becoming increasingly popular due to their intuitive appeal to the ways humans perform their practical and daily reasoning [2,3,19,32,38].

Dialectical proof procedures for argumentation have been developed both for abstract argumentation [7,18,20,28,37,39] and for rule-based instances of it like logic programming [12,14,21] or assumption-based argumentation [15–17,22,35,36]. A proof procedure for assumption-based argumentation could be viewed as an integration of the dialectical procedures of abstract argumentation with the process of argument constructions where the later could get into a non-terminating loop leading to the incompleteness wrt the admissibility semantics.

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

The following example illustrates this point (as logic programming is an instance of assumption-based argumentation where the contrary of a negation-as-failure assumption $not_δ$ is δ, we will represent our examples in logic programming for convenience).

Example 1.
Consider two logic programs below. $\begin{array}{l} \begin{matrix} F_{1} : & r : p \leftarrow not_δ r^{'} : δ \leftarrow f (0) r_{n} : f (n) \leftarrow f (n + 1), n ⩾ 0 \\ t : β \leftarrow \end{matrix} \\ \begin{matrix} F_{2} : & r : p \leftarrow not_δ r^{″} : δ \leftarrow not_β, f (0) r_{n} : f (n) \leftarrow f (n + 1), n ⩾ 0 \\ t : β \leftarrow \end{matrix} \end{array}$

The semantics of $F_{1}$ and $F_{2}$ are determined by the arguments illustrated in Fig. 1.

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

The unique argument supporting p in both frameworks is A supported by assumption $not_δ$ . It is obvious that δ is not supported as there is no (finite) argument supporting it. Hence there are no attacks (by finite arguments) against both A and B in both frameworks. ${A, B}$ is consequently admissible wrt both frameworks. But dialectical reasoning engines like the proof procedures for logic programming or assumption-based argumentation in [14–17,21,22,26,35,36] fail to deliver A wrt the first framework $F_{1}$ as they could not overcome the non-termination of the process to construct an argument supporting δ due to the “infinite-loop” represented by D, though all of them deliver A wrt the second framework $F_{2}$ despite the presence of the same loop D.

The distinct behavior of the dialectical proof procedures wrt the two frameworks $F_{1}$ , $F_{2}$ suggests that to fully understand their semantics, we need to consider the effects of “infinite loops” on their behavior. In this paper, we accomplish this by introducing a new notion of infinite arguments to represent such “infinite loops”.

For framework $F_{1}$ , there is an infinite argument for δ represented by the infinite proof tree $C_{1}$ . This argument can not be attacked as it is not based on any assumption.

For framework $F_{2}$ , there is an infinite argument for δ represented by the infinite proof tree $C_{2}$ . This argument is based on assumption $not_β$ and hence is attacked by the argument B.

Therefore, if infinite arguments are taken into account, the set ${A, B}$ is not admissible wrt $F_{1}$ while it is still admissible wrt $F_{2}$ .

The example suggests that a stronger notion of admissibility taking into account also the effects of infinite arguments, is needed to characterize the semantics of dialectical proof procedures.

As argument $C_{1}$ can not be attacked by any other argument wrt $F_{1}$ , should it be accepted and δ concluded?

As infinite loops represent a kind of unfinished, inconclusive business, $C_{1}$ can not be viewed as a support of δ.

In general, a finite argument has two roles: As a direct support for its conclusion and as an attacker against certain arguments. In contrast, infinite arguments have only one role as attacker against some other arguments. They can not support their conclusion.

To capture this peculiar character of infinite arguments, we model infinite arguments as self-attacking arguments. This very simple idea presents a declarative view of the “spoiling role” of infinite loops: A presence of infinite loops in a computation prevents it to come to a conclusion.

We make three key contributions in this paper:

The introduction of infinite arguments and a new stricter notion of admissibility;

We show the soundness and completeness of dialectical proof procedures wrt the new notion of strict admissibility for general assumption based frameworks. To accomplish this goal, we introduce a new dialectical proof procedure that are based explicitly on proof trees (i.e. arguments and partial arguments).1
¹
The new procedure could be viewed as a full embracement of the idea of explainable AI in dialectical procedures in which we not only state which assumptions provide support and defence for a conclusion, but also explicitly state which arguments are employed to accomplish such tasks.

Last but not least, we introduce a new view of proof trees (and arguments) as sets of the partial proofs represented by paths from the root to their nodes. This view of “trees as sets” of partial proofs allows simple characterizations of dispute derivation and simplifies in no small amount the technical machinery needed in the proofs of soundness and completeness of dialectical procedures.

The paper also offers an interesting conceptual insight about the “spoiling” role of arguments that are unacceptable (like the infinite arguments in our case or more abstractly the self-attacking arguments in abstract argumentation). As the problem of non-termination is not decidable, such arguments can not be dismissed and practical rule-based argumentation systems need to take care of them. In the context of assumption-based argumentation, these “spoiler (infinite) arguments” lead to strict admissibility as the semantics of dialectical procedures.

The paper is organized in 8 sections including the Introduction. In the following section, we recall the basic notions of abstract and assumption-based argumentation as well as introduce the infinite arguments together with a new notion of strict admissibility. We then present a proof-tree based dialectical proof procedure in Section 3. We show the soundness of the proof-tree based procedure in Section 4 and its completeness in Section 5. We introduce a flattened version of the proof-tree based procedure together with its soundness and completeness in Section 6. We then conclude the paper with a short discussion in Section 7. The last section is the Appendix.2
²
An extended abstract of this paper has been published in [34].

2. Assumption-based argumentation with infinite arguments

2.1. Abstract argumentation

An argumentation framework [13] is a pair $AF = (AR, att)$ , where $AR$ is a set of arguments, and att is a binary relation over $AR$ representing the attack relation between the arguments where $(A, B) \in att$ means that A attacks B. A set S of arguments attacks an argument A if some argument in S attacks A.

A set S of arguments is conflict-free iff it does not attack itself. S is self-defensible iff S attacks each argument attacking S. S is admissible iff S is conflict-free and self-defensible. S is a preferred extension iff S is maximally (wrt set inclusion) admissible.

An argument A is said to be credulously accepted iff it is contained in at least one preferred extension. It follows that an argument is credulously accepted iff it belongs to an admissible set of arguments.

2.2. Assumption-based argumentation

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

³
In non-standard ABA frameworks [22], the contrary $\overline{α}$ 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 \overline{α}$ , add a new rule: $α^{'} \leftarrow δ$ to $R$ .

It is not difficult to see that the new framework is equivalent to the old one. Hence focusing on standard ABA does not cause any loss of generality while simplifying the technical machinery in no small amount.

An ABA framework $F = (R, A, \overline{})$ is finitary if for each sentence $σ \in L$ , the set of rules of the form $σ \leftarrow l_{1}, \dots l_{n}$ ( $n ⩾ 0$ and $l_{1}, \dots, l_{n} \in L$ ), is finite.

Logic programming is a well-known instance of standard ABA where the contrary of a negation-as-failure assumption $not_p$ is p.

Remark 1.

For each rule r of the form $l_{0} \leftarrow l_{1}, \dots l_{n}$ , $l_{0}$ and the set ${l_{1}, \dots, l_{n}}$ are referred respectively as the head and the body of r and denoted by $hd (r)$ , $bd (r)$ .

Convention 1.

From now on until the end of the paper,

we restrict our consideration to standard ABA. Hence whenever we refer to an ABA framework, we mean a standard one, and

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

Definition 1 (Partial proof).

Given an ABA $F$ , a partial proof supporting $σ_{0}$ (wrt $F$ ) is a finite sequence of the form $\begin{matrix} (root, σ_{0}) . (r_{1}, σ_{1}) . \dots (r_{n}, σ_{n}) \end{matrix}$ where $r_{i} \in R$ , $i ⩾ 1$ such that $σ_{i - 1} = hd (r_{i})$ and $σ_{i} \in bd (r_{i})$ . If $bd (r_{i}) = \emptyset$ then $σ_{i} = true$ .

Example 2.
Consider the argumentation framework $F_{2}$ in Example 1.

Some partial proofs supporting p and δ are given below and illustrated in Fig. 2. $\begin{array}{l} ψ = (root, p) \\ ψ^{'} = (root, p) . (r, not_δ) \\ π_{0} = (root, δ) \\ π_{1}^{'} = (root, δ) . (r^{″}, not_β) \\ π_{1} = (root, δ) . (r^{″}, f (0)) \\ π_{2} = (root, δ) . (r^{″}, f (0)) . (r_{0}, f (1)) \\ \dots \\ π_{n + 1} = (root, δ) . (r^{″}, f (0)) . (r_{0}, f (1)) \dots (r_{n - 1}, f (n)) \end{array}$

Fig. 2.
A graphical representation of partial proofs of Example 2.

We next define partial proof trees where we identify the nodes in a proof tree with the partial proofs representing the unique paths from the root to them. This allows us to treat proof trees as sets simplifying the technical machinery for presenting and understanding dialectical procedures significantly.
Definition 2 (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{matrix} π \equiv (root, σ_{0}) . (r_{1}, σ_{1}) . \dots (r_{n}, σ_{n}), n > 0 \end{matrix}$ from T, the following properties hold:

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

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

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

σ_{0}

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

Cl (T)

while the partial proof

(root, σ_{0})

is referred to as the root of T.

Example 3.
Continue from Example 2. Some partial proof trees for p and δ are given below and illustrated in Fig. 3. $\begin{array}{l} A_{0} = {ψ} \\ A = {ψ, ψ^{'}} \\ C_{0} = {π_{0}} \\ C_{20} = {π_{0}, π_{1}, π_{1}^{'}} \\ C_{21} = {π_{0}, π_{1}^{'}, π_{1}, π_{2}} \\ C_{2} = {π_{0}, π_{1}^{'}, π_{1}, π_{2}, π_{3}, \dots, π_{n}, \dots} \end{array}$

Note that ${π_{0}, π_{1}}$ and ${π_{0}, π_{1}^{'}}$ are not partial proof trees.

Fig. 3.
Some partial proof trees from Example 3.
Remark 2.
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 $(root, σ_{0}) . (r_{1}, σ_{1}) . \dots (r_{n}, σ_{n})$ in a 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 $true$ or by an assumption. N is non-final if it is not final.

The support of T, denoted by $Sp (T)$ , is the set of all sentences labeling the leaves of T and different to $true$ .

The union of supports of proof trees in S is denoted by $Sp (S)$ .

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

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

The set of conclusions of proof trees in S is denoted by $Cl (S)$ .

Consider the partial proof tree $C_{20}$ in Fig. 3, the partial proof $π_{0} = (root, δ)$ is the parent of the node $π_{1} = (root, δ) . (r^{″}, f (0))$ and the node $π_{1}^{'} = (root, δ) . (r^{″}, not_β)$ . Also, $π_{1}$ and $π_{1}^{'}$ are the children of $π_{0}$ .

The support of A is ${not_δ}$ while the supports of $C_{20}$ , $C_{21}$ , $C_{2}$ are ${not_β, f (0)}$ , ${not_β, f (1)}$ and ${not_β}$ respectively.
Definition 3 (Arguments).

A full proof tree is a partial proof tree whose support consists only of assumptions.4

⁴
I.e. all leaves of any full proof tree T are final and $Ass (T) = Sp (T)$ .

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

The set of all arguments wrt the ABA framework $F$ is denoted by ${AR}_{F}$ while the set of all finite arguments is denoted by ${AR}_{fin, F}$ .

Example 4.

Continue from Example 3. A, B, $C_{2}$ are full proof trees and their supports are assumptions which are ${not_δ}$ , ∅, and ${not_β}$ respectively. Hence they all are arguments.

If the opponent in a dialectical computation is constructing an infinite argument to attack some proponent argument (like argument $C_{1}$ in Fig. 1), the computation may not terminate and the admissibility of the proponent arguments can not be established. Declaratively, we model this situation as an attack of the infinite argument against some proponent arguments.

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 4 (Attacks).

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

The conclusion of A is the contrary of some assumption in the support of B.

A and B are identical and infinite.

The attack relation between arguments in ${AR}_{F}$ is denoted by ${att}_{F}$ while the attack relations between finite arguments is denoted by ${att}_{fin, F}$ . Define $\begin{matrix} {AF}_{F} = ({AR}_{F}, {att}_{F}) and {AF}_{fin, F} = ({AR}_{fin, F}, {att}_{fin, F}) \end{matrix}$

Example 5.
Consider again Example 1, we have ${AF}_{F_{1}} = ({AR}_{F_{1}}, {att}_{F_{1}})$ where ${AR}_{F_{1}} \supseteq {A, B, C_{1}}$ and ${att}_{F_{1}} \supseteq {(C_{1}, A), (C_{1}, C_{1})}$ .

Further ${AF}_{F_{2}} = ({AR}_{F_{2}}, {att}_{F_{2}})$ where ${AR}_{F_{2}} \supseteq {A, B, C_{2}}$ and ${att}_{F_{2}} \supseteq {(C_{2}, A), (B, C_{2}), (C_{2}, C_{2})}$ .

If we consider only finite arguments, ${AR}_{fin, F_{1}} = {AR}_{fin, F_{2}}$ and ${att}_{fin, F_{1}} = {att}_{fin, F_{2}}$ . Hence ${AF}_{fin, F_{1}} = {AF}_{fin, F_{2}}$ .

The graphical representation of attacks among arguments can be seen in Fig. 4.

Fig. 4.
A graphical representation of attacks among arguments.

Due to the fact that the infinite arguments always attack themself, the following lemma holds obviously.
Lemma 1.
Let $S \subseteq {AR}_{F}$ be admissible wrt ${AF}_{F} = ({AR}_{F}, {att}_{F})$ . Then S contains only finite arguments.
Definition 5 (Admissibility and strict admissibility).

Abusing the notation slightly for simplicity, we say that a set of arguments $S \subseteq {AR}_{F}$ is

strictly admissible iff it is admissible wrt the argumentation framework ${AF}_{F} = ({AR}_{F}, {att}_{F})$ , and

admissible iff it is admissible wrt the argumentation framework ${AF}_{fin, F} = ({AR}_{fin, F}, {att}_{fin, F})$ .

It holds obviously.

Theorem 1.
If S is strictly admissible then S is also admissible.

In Fig. 1, the set of arguments ${A, B}$ is strictly admissible wrt ${AF}_{F_{2}}$ but not wrt ${AF}_{F_{1}}$ as B attacks $C_{2}$ but not $C_{1}$ .

We define accordingly the notions of admissible and strictly admissible sets of assumptions.
Definition 6 (Admissible and strictly admissible sets of assumptions).

Let H be a set of assumptions and ${AR}_{H}$ be the set of all finite arguments whose supports are subsets of H.

We say H is admissible (resp strictly admissible) iff there is subset $S \subseteq {AR}_{H}$ such that $Ass (S) = H$ and S is admissible (resp. strictly admissible).

A sentence σ is said to be credulously derived (resp. strictly credulously derived) from H if H is admissible (resp. strictly admissible) and there is $A \in {AR}_{H}$ such that $Cl (A) = σ$ .

We write $H | \sim σ$ to denote that σ is strictly credulously derived from H.

Example 6.
Consider again Example 5 and let $H = {not_δ}$ . Hence, ${AR}_{H} \supset {A, B}$ (wrt both $F_{1}$ , $F_{2}$ ).

Since $C_{1}$ attacks A wrt $F_{1}$ but there is no attack against $C_{1}$ wrt $F_{1}$ , H is not strictly admissible wrt $F_{1}$ .

In contrast, H is strictly admissible wrt $F_{2}$ as B attacks $C_{2}$ . Hence p is strictly credulously derived from H wrt $F_{2}$ but not wrt $F_{1}$ .
3. Introducing proof-trees-based dialectical proof procedures

Dialectical proof procedures could be viewed as games between a proponent who is trying to construct an argument for some conclusion and defend it from the attacking arguments constructed by an opponent. Both players construct their arguments by expanding partial proof trees stepwise to the full proof trees. In [15–17,35,36], the constructed proof trees are implicit, acting more or less as intuitive guidances. The procedures only present a flattened view of the proof trees represented by multisets of their supports. [22] introduces more structure by representing proof trees as a pair of support and conclusion.

We will present two procedures. In one, proof trees are fully and explicitly represented. The explicit representation of proof trees (or partial arguments) allows deeper structural insights into process of argument construction by incorporating the concept of expansion of partial arguments into the procedures and hence making the task of tracing the construction of proof trees simpler and more natural. It simplifies the associated technical machinery in no small amount. The second procedure is a result of flattening the first.

We first present some key insights into the structure of proof trees that are needed to understand the procedures.

3.1. Sequence of partial proof trees

Notation 3.
Let T, $T^{'}$ be partial proof trees and N be a non-final leaf node in T labeled by a non-assumption σ.5
⁵
See Notations 2 and 1.

$T^{'}$ is an immediate expansion of T at N if there is a rule r of the form $σ \leftarrow b_{1}, \dots, b_{m}$ such that $T^{'}$ is obtained from T by adding m children $N . (r, b_{1}), \dots, N . (r, b_{m})$ to N (for $m = 0$ , a child node $N . (r, true)$ is added to N), i.e. $T^{'} = T \cup {N . (r, b_{1}), \dots, N . (r, b_{m})}$ .

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{array}{l} CE (T, N) = {exp (T, N, r^{'}) ∣ r^{'} is a rule s.t. hd (r^{'}) = σ} and \\ CE (T, N, S) = {exp (T, N, r^{'}) ∣ r^{'} is a rule s.t. hd (r^{'}) = σ, bd (r) \cap S = \emptyset} \end{array}$ where S is a set of assumptions.

It is easy to see that $CE (T, N) = CE (T, N, \emptyset)$ .
Example 7.
Consider the partial proof tree $C_{20} = {π_{0}, π_{1}, π_{1}^{'}}$ in Fig. 3.

Let $N = π_{1}$ . Then $\begin{matrix} exp (C_{20}, N, r_{0}) = C_{20} \cup {π_{1} . (r_{0}, f (1))} = {π_{0}, π_{1}^{'}, π_{1}, π_{2}} = C_{21} . \end{matrix}$
Notation 4.
Let $T_{0}$ , $T_{1}$ be partial proof trees for $σ_{0}$ .

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

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}$ .
Lemma 2.
Let $T_{0}$ , $T_{1}$ be partial proof trees. The following statements hold:
If $T_{1}$ is an immediate expansion of $T_{0}$ then $T_{0}$ is a prefix of $T_{1}$ .

Suppose $T_{0}$ is a prefix of $T_{1}$ . It holds that

the roots of $T_{0}$ , $T_{1}$ coincide; and

if N is a node in $T_{0}$ then the parent and children of N in $T_{0}$ (if exist) 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 partial proof tree such that $T_{0}$ is a proper prefix of T. Furthermore, let N be a leaf node in $T_{0}$ and S be a set of assumptions. The following statements hold:
Suppose $CE (T_{0}, N) \neq \emptyset$ . Then there is $T_{1} \in CE (T_{0}, N)$ such that $T_{1}$ is a prefix of T.

Suppose $Ass (T) \cap S = \emptyset$ and $CE (T_{0}, N, S) \neq \emptyset$ . Then there is $T_{1} \in CE (T_{0}, N, S)$ such that $T_{1}$ is a prefix of T

Proof.
The first statement follows directly from the second one. We prove the second one.

Since $CE (T_{0}, N, S) \neq \emptyset$ , N is labeled by a non-assumption sentence δ different to $true$ . Since T is an argument, N is not a leaf node in T. Thus N has a child of the form $N . (r, γ)$ in T where $hd (r) = δ$ and $γ \in bd (r)$ . From the definition of proof trees (Definition 2), it follows $T_{1} = exp (T_{0}, N, r) \subseteq T$ . Since $Ass (T) \cap S = \emptyset$ , it follows that $bd (r) \cap S = \emptyset$ . Hence $T_{1} \in CE (T_{0}, N, S)$ . The second statement holds. □

An increasing sequence of partial proof trees $T_{0} \subseteq T_{1} \subseteq \dots T_{i} \subseteq \dots$ 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 $sq \equiv T_{0} \subseteq T_{1} \subseteq \dots T_{i} \subseteq \dots$ be an increasing sequence of partial proof trees. The following statements hold:
$T_{0} \cup T_{1} \cup \dots T_{i} \cup \dots$ is a partial proof tree.

If the sequence $sq$ is fair then $T_{0} \cup T_{1} \cup \dots T_{i} \cup \dots$ is an argument.

Proof.
The first statement is obvious. We prove the second. Suppose $T \equiv T_{0} \cup T_{1} \cup \dots T_{i} \cup \dots$ is not an argument. Hence T has a non-final leaf node N labeled by δ. Thus $N \in T_{i}$ for some i. Since $sq$ is fair, N is a proper prefix of some node $M \in T_{j}$ , $j > i$ . Hence N is not a leaf of T. Contradiction. □
Notation 5.
Let T be a partial proof tree and $N \equiv (root, σ_{0}) . (r_{1}, σ_{1}) . \dots (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$ .6
⁶
Hence the height of the root is 0.

The maximum of the heights of the non-final leaf nodes in T is denoted by $ha (T)$ , i.e. $\begin{matrix} ha (T) = max {h (N, T) ∣ N is a non-final leaf node in T} \end{matrix}$
Notation 6.
Two partial proof trees T, $T^{'}$ are compatible iff $T \cup T^{'}$ is also a partial proof tree.
Lemma 5.
Let Π be a infinite set of partial proof trees wrt a finitary ABA $F$ such that
for all $n ⩾ 0$ , for each $T \in Π$ such that $ha (T) > n$ , there is $T^{'} \in Π$ such that $T^{'} \subseteq T$ and $ha (T^{'}) = n$ ; and

for each $n ⩾ 0$ , the set ${T \in Π ∣ ha (T) ⩽ n}$ is finite; and

for all $T, T^{'} \in Π$ such that T, $T^{'}$ are compatible, it holds that $T \subseteq T^{'}$ or $T^{'} \subseteq T$ .

Then there is an infinite strictly increasing sequence of proof trees $\begin{matrix} T_{0} \subset T_{1} \subset \dots \subset T_{n} \subset \dots \end{matrix}$ such that for each $i ⩾ 0$ , $T_{i} \in Π$ .
Proof.
See Appendix A.2. □

3.2. Dialectical proof procedure

We give below a dialectical proof procedure for constructing an admissible set of arguments supporting some sentence σ. The procedure could be viewed as a stage-wise construction of the dispute derivation of the form $⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{i}, {PA}_{i}, {OT}_{i}, {OA}_{i} ⟩$ where at each stage i,

${PT}_{i}$ is the set of partial proof trees the proponent has constructed until stage i;

${OT}_{i}$ is the set of partial proof trees the opponent has constructed and not yet attacked by the proponent until stage i;

${PA}_{i}$ (resp ${OA}_{i}$ ) is the set of assumptions that 1) appear in the partial proof trees constructed by the proponent (resp opponent) until stage i and 2) have been attacked by the other party until stage i.

Definition 7 (Proof tree-based dispute derivation).

A proof-tree-based dispute derivation for a sentence σ is a (possibly infinite) sequence of the form $\begin{matrix} ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{i}, {PA}_{i}, {OT}_{i}, {OA}_{i} ⟩ \end{matrix}$ where

for each i, ${PA}_{i}$ , ${OA}_{i}$ are sets of assumptions and ${PT}_{i}$ , ${OT}_{i}$ are sets of partial proof trees, and

${PT}_{0}$ contains exactly one partial proof tree consisting of only the root labeled by σ (i.e. ${PT}_{0} = {{(root, σ)}}$ ), and

${PA}_{0} = {OT}_{0} = {OA}_{0} = \emptyset$ , and

at stage i, one of the dispute parties makes a move satisfying the following properties:

Suppose the proponent makes a move at stage i. The proponent has two options:

The proponent expands one of her partial arguments by selecting a partial proof tree $T \in {PT}_{i}$ , a non-final leaf node N in T labeled by δ, a rule r with head δ such that $bd (r) \cap {OA}_{i} = \emptyset$ and expanding T resulting in: $\begin{array}{l} {PT}_{i + 1} = ({PT}_{i} ∖ {T}) \cup {exp (T, N, r)} . \\ {PA}_{i + 1} = {PA}_{i} \\ {OT}_{i + 1} = {OT}_{i} \\ {OA}_{i + 1} = {OA}_{i} \end{array}$

The proponent attacks partial proof trees in ${OT}_{i}$ at an assumption $α \in Ass ({OT}_{i}) ∖ Ass ({PT}_{i})$ .7

⁷
See Notation 2.

Then

\begin{array}{l} {PT}_{i + 1} = {PT}_{i} \cup {{(root, \overline{α})}} \\ {PA}_{i + 1} = {PA}_{i} \\ {OT}_{i + 1} = {OT}_{i} ∖ {T^{'} \in {OT}_{i} ∣ α \in Ass (T^{'})} \\ {OA}_{i + 1} = {OA}_{i} \cup {α} . \end{array}

Suppose the opponent makes a move at stage i. The opponent has two options:

The opponent attacks a proponent partial proof tree $T \in {PT}_{i}$ at a leaf node labeled by an assumption $α \in Ass (T) ∖ {PA}_{i}$ : $\begin{array}{l} {PT}_{i + 1} = {PT}_{i} \\ {PA}_{i + 1} = {PA}_{i} \cup {α} \\ {OT}_{i + 1} = {OT}_{i} \cup {{(root, \overline{α})}} \\ {OA}_{i + 1} = {OA}_{i} . \end{array}$

The opponent expands an opponent partial proof tree $T \in {OT}_{i}$ at a non-final leaf node N filtered by the assumptions in ${OA}_{i}$ , i.e., $\begin{array}{l} {PT}_{i + 1} = {PT}_{i} \\ {PA}_{i + 1} = {PA}_{i} \\ {OT}_{i + 1} = ({OT}_{i} ∖ {T}) \cup CE (T, N, {OA}_{i}) \\ {OA}_{i + 1} = {OA}_{i} . \end{array}$

Definition 8.

A proof-tree-based dispute derivation $⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ is successful if ${OT}_{n} = \emptyset$ , and ${PT}_{n}$ consists only of full proof trees and ${PA}_{n} = Ass ({PT}_{n})$ .

Remark 3.

For simplicity, in the next two Sections 4, 5, we refer to proof tree-based dispute derivation just as dispute derivation if there is no possibility for misunderstanding.

Example 8.

Consider again the argumentation framework $F_{2}$ in Example 1 with the partial arguments in Fig. 3.

A proof-tree based-dispute derivation for p is given in Table 1.

Table 1

A successful tree-based dispute derivation

$Stage$	$PT$	$PA$	$OT$	$OA$	$Step$
0	$A_{0}$	∅	∅	∅	$1 a$
1	A	∅	∅	∅	$2 a$
2	A	$not_δ$	$C_{0}$	∅	$2 b$
3	A	$not_δ$	$C_{20}$	∅	$2 b$
4	A	$not_δ$	$C_{21}$	∅	$1 b$
5	A, $B_{0}$	$not_δ$	∅	$not_β$	$1 a$
6	A, B	$not_δ$	∅	$not_β$	success

4. Soundness of dispute derivation

Before giving the soundness theorem, we present a number of lemmas to illuminate the structure of dispute derivations.

Lemma 6.
Let $dd = ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ be a dispute derivation. The following statements hold:
$Ass ({OT}_{n}) \cap {OA}_{n} = \emptyset$ .

For each $α \in {OA}_{n}$ , there is a partial proof tree $T \in {PT}_{n}$ such that $Cl (T) = \overline{α}$ .

For each $β \in {PA}_{n}$ there is a unique stage i, $i < n$ , such that ${β} = {PA}_{i + 1} ∖ {PA}_{i}$ and ${(root, \overline{β})} \in {OT}_{i + 1} ∖ {OT}_{i}$ .

For each a partial proof tree $T \in {OT}_{i}$ , $i ⩽ n$ , there is a unique $β \in {PA}_{n}$ such that $Cl (T) = \overline{β}$ .

Let $T, T^{'} \in {OT}_{i}$ , $i ⩾ 0$ . If T, $T^{'}$ are compatible then T, $T^{'}$ are identical.

Proof.
See Appendix A.3. □

We next introduce a new relevant notion of scope of a proof tree in dispute derivation to describe the expansion process of opponent proof trees in dispute derivations. Definition 9 (Scope).

Let T be a proof tree and $dd = ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ be a dispute derivation for σ.

A scope of length k of T in $dd$ is a pair $(sq, i)$ where $sq \equiv T_{0}, T_{1}, \dots, T_{k - 1}$ , $i ⩾ 0$ and $k ⩾ 1$ , such that the following conditions hold:

$T_{0} = {(root, Cl (T))}$ and $T_{0} \in {OT}_{i} ∖ {OT}_{i - 1}$ .

For each $0 ⩽ j ⩽ k - 1$ : $T_{j} \in {OT}_{i + j}$ and $T_{j} \subseteq T$ ;

For each $0 ⩽ j < k - 1$ : either $T_{j + 1} = T_{j}$ or $T_{j + 1}$ is an immediate expansion of $T_{j}$ .

A scope $(seq, i)$ of T in $dd$ is a full scope if there is no prefix of T in ${OT}_{i + k}$ .

Lemma 7.
Let T be a proof tree and $dd = ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ be a dispute derivation. The following statements hold:
Let $(sq, i)$ , $({sq}^{'}, j)$ be two scopes of T in $dd$ of equal length. Then $i = j$ and $sq$ , ${sq}^{'}$ are identical;

If $T \in {OT}_{n}$ then there is a scope $(sq, i)$ , $sq = T_{0}, \dots, T_{k - 1}$ , of T in $dd$ such that $i + k - 1 = n$ and $T = T_{k - 1}$ ;

If $dd$ is a successful dispute derivation that terminates at $⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ and T is an argument attacking some argument in ${PT}_{n}$ then there is a unique full scope of T in $dd$ .

Proof.
See Appendix A.4. □
Lemma 8.
Let $dd = ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ be a successful dispute derivation and let T be an argument attacking some argument in ${PT}_{n}$ . Then $Ass (T) \cap {OA}_{n} \neq \emptyset$ .
Proof.
Let $(sq, i)$ with $sq = T_{0}, \dots, T_{k - 1}$ , $1 ⩽ k$ , be the unique full scope of T in $dd$ (the existence of $(sq, i)$ follows from Lemma 7). As $(sq, i)$ is a full scope of T, there is no prefix of T in ${OT}_{i + k}$ . Hence there are two cases:
$T_{k - 1}$ is attacked by the proponent at stage $i + k - 1$ in $dd$ using (1.b). It follows that $T_{k - 1}$ (and hence T) contains an assumptions in ${OA}_{i + k - 1} \subseteq {OA}_{n}$ .

$T_{k - 1}$ is filtered out by the opponent at stage $i + k - 1$ in $dd$ using (2.b). It follows that a non-final leaf node N of $T_{k - 1}$ is selected such that $\begin{matrix} {OT}_{i + k} = ({OT}_{i + k - 1} ∖ {T_{k - 1}}) \cup CE (T_{k - 1}, N, {OA}_{i + k - 1}) \end{matrix}$

Suppose $Ass (T) \cap {OA}_{n} = \emptyset$ . Hence $Ass (T) \cap {OA}_{i + k - 1} = \emptyset$ . From Lemma 3, it follows that there is $T^{'} \in CE (T_{k - 1}, N, {OA}_{i + k - 1})$ such that $T^{'}$ is a prefix of T. Contradiction since there is no proof tree in ${OT}_{i + k}$ that is a prefix of T.

Therefore $Ass (T) \cap {OA}_{n} \neq \emptyset$ . □
Lemma 9.
Let $dd = ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ be a successful dispute derivation for σ. Then ${PA}_{n} \cap {OA}_{n} = \emptyset$ .
Proof.
Suppose there exists $α \in {PA}_{n} \cap {OA}_{n}$ . Let i be the stage in $dd$ where α is attacked by the proponent (step (1.b) in Definition 7) and inserted into ${OA}_{i}$ . Therefore α does not appear in ${PT}_{i}$ . The only ways for α to show up in ${PT}_{n}$ later is by applying step (1.a).

It is also clear that for each $i < j ⩽ n$ , $α \in {OA}_{j}$ . At any stage $j > i$ in $dd$ , if the proponent expands a partial proof tree $T \in {PT}_{j}$ then only rules r with $bd (r) \cap {OA}_{j} = \emptyset$ are selected (the filtering condition in step (1.a) of Definition 7). Therefore α can never show up in ${PT}_{j}$ . Hence $α \notin {PA}_{n}$ . Contradiction. □
Theorem 2 (Soundness theorem).

Let $dd = ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ be a successful dispute derivation for σ. The following statements hold:

${PT}_{n}$ is strictly admissible and $σ \in Cl ({PT}_{n})$ .

${PA}_{n} | \sim σ$ .

Proof.
The second statement follows directly from the first. We proceed to prove the first statement below.

It is obvious that σ labels the root of some full proof tree in ${PT}_{n}$ .

Suppose an argument T attacks ${PT}_{n}$ . From the Lemmas 8, 6, it follows immediately that T is attacked by ${PT}_{n}$ .

We show now that ${PT}_{n}$ is conflict-free. Suppose the contrary that ${PT}_{n}$ is not conflict-free. Then there are arguments $T, T^{'} \in {PT}_{n}$ such that T attacks $T^{'}$ . From Lemma 8, T contains an assumption from ${OA}_{n}$ . From $Ass (T) \subseteq Ass ({PT}_{n}) = {PA}_{n}$ , it follows ${PA}_{n} \cap {OA}_{n} \neq \emptyset$ . Contradiction to Lemma 9. □

5. Completeness of proof-tree-based dispute derivation

Theorem 3 (Completeness theorem).

Let $F$ be a finitary ABA framework, H be a strictly admissible finite set of assumptions and σ be a sentence such that $H | \sim σ$ . Then there is a successful proof-tree-based dispute derivation $⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ for σ such that ${PA}_{n} \subseteq H$ .

To prove the theorem, we construct a successful dispute derivation for σ by imposing certain extra conditions on the steps of proponent and opponent in the dispute derivation procedure (Definition 7). The formal proof is given in Section 5.2 below.

5.1. H-Constrained dispute derivation

Given $H | \sim σ$ , the task is to construct a successful dispute derivation $\begin{matrix} ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩ \end{matrix}$ for σ such that ${PA}_{n} \subseteq H$ and ${PT}_{n} \subseteq {AR}_{H}$ .8

⁸
${AR}_{H}$ is the set of all finite arguments whose assumptions belong to H.

The key idea is rather simple: Associate each partial proof tree $T \in {PT}_{i}$ to some argument $A \in {AR}_{H}$ such that 1) T is a prefix of A and 2) at step (1.a) when T is selected, expand T towards A so that at the end of the derivation, A is fully constructed.

We illustrate this idea in Example 9 below.

Example 9.

$\begin{array}{l} r_{1} : σ \leftarrow not_δ r_{2} : δ \leftarrow not_β \\ r_{3} : β \leftarrow not_γ r_{4} : β \leftarrow d \end{array}$

Let $H = {not_δ, not_γ}$ . Hence ${AR}_{H} \supseteq {T_{1}, T_{3}}$ (see Fig. 5).

Consider the dispute derivations for σ represented in Tables 2, 3. At stage 4, either $r_{3}$ or $r_{4}$ could be selected for an expansion of $T_{2}$ . Selecting $r_{4}$ leads to a failed derivation (Table 2). If we associate $T_{2}$ with $T_{3}$ at stage 4 when it is created, we would select $r_{3}$ to expand $T_{2}$ towards $T_{3}$ leading to a successful dispute derivation (Table 3).

Fig. 5.

Partial proof trees of Example 9.

Table 2

A failed tree-based dispute derivation

$Stage$	$PT$	$PA$	$OT$	$OA$	$Step$
0	$T_{0}$	∅	∅	∅	$1 a$
1	$T_{1}$	∅	∅	∅	$2 a$
2	$T_{1}$	$not_δ$	$A_{0}$	∅	$2 b$
3	$T_{1}$	$not_δ$	$A_{1}$	∅	$1 b$
4	$T_{1}$ , $T_{2}$	$not_δ$	∅	$not_β$	$1 a$
5	$T_{1}$ , $T_{3}^{'}$	$not_δ$	∅	$not_β$	fail

Table 3

A successful tree-based dispute derivation

$Stage$	$PT$	$PA$	$OT$	$OA$	$Step$
0	$T_{0}$	∅	∅	∅	$1 a$
1	$T_{1}$	∅	∅	∅	$2 a$
2	$T_{1}$	$not_δ$	$A_{0}$	∅	$2 b$
3	$T_{1}$	$not_δ$	$A_{1}$	∅	$1 b$
4	$T_{1}$ , $T_{2}$	$not_δ$	∅	$not_β$	$1 a$
5	$T_{1}$ , $T_{3}$	$not_δ$	∅	$not_β$	success

More formally, at each stage $⟨ {PT}_{i}, {PA}_{i}, {OT}_{i}, {OA}_{i} ⟩$ in a dispute derivation, we add a new component $λ_{i}$ representing a function that associates each proof tree $T \in {PT}_{i}$ to an argument $λ_{i} (T) \in {AR}_{H}$ such that T is a prefix of $λ_{i} (T)$ . $λ (T)$ will guide the expansions of T so that at the end of the derivation, $λ (T)$ is fully constructed. Hence if procedure step (1.a) is applied at stage i, and T is selected and expanded into $T^{'}$ then $T^{'}$ is also a prefix of $λ_{i} (T)$ and $λ_{i + 1} (T^{'}) = λ_{i} (T)$ .

Convention 2.

For ease of representation, we often represent a function f from X to Y as a binary relation $f = {(x, y) ∣ x \in X, y \in Y : y = f (x)}$ .

We introduce two new notions.

Notation 7.

The minimum of the heights of the non-final leaf nodes in a proof tree T is denoted by $\begin{matrix} hi (T) = min {h (N, T) ∣ N is a non-final leaf node in T}^{9} \end{matrix}$

For

⁹

$Stage$	$PT$	$PA$	$OT$	$OA$	λ	$Step$
0	$T_{0}$	∅	∅	∅	$(T_{0}, T_{1})$	$1 a$
1	$T_{1}$	∅	∅	∅	$(T_{1}, T_{1})$	$2 a$
2	$T_{1}$	$not_δ$	$A_{0}$	∅	$(T_{1}, T_{1})$	$2 b$
3	$T_{1}$	$not_δ$	$A_{1}$	∅	$(T_{1}, T_{1})$	$1 b$
4	$T_{1}$ , $T_{2}$	$not_δ$	∅	$not_β$	$(T_{1}, T_{1})$ , $(T_{2}, T_{3})$	$1 a$
5	$T_{1}$ , $T_{3}$	$not_δ$	∅	$not_β$	$(T_{1}, T_{1})$ , $(T_{3}, T_{3})$	success

6. Flatten dispute derivation

In many proof procedures for assumption-based argumentation [15–17,22], only the supports of proof trees are of interest, not the arguments themselves. In such cases, there is often no need to carry along entire proponent or opponent trees.

A closer observation of the definition of proof tree-based dispute derivation reveals that to compute $⟨ {PT}_{i + 1}, {PA}_{i + 1}, {OT}_{i + 1}, {OA}_{i + 1} ⟩$ from $⟨ {PT}_{i}, {PA}_{i}, {OT}_{i}, {OA}_{i} ⟩$ , we need only the sentences in the supports of arguments in ${PT}_{i} \cup {OT}_{i}$ . Hence a “simplification” of the proof tree based dispute derivation could be obtained by replacing each tree in ${PT}_{i} \cup {OT}_{i}$ by its support.

The definition of flatten dispute derivations uses the notion of multisets. A very short introduction to multisets is given in Appendix A.1.

Definition 12 (Flatten dispute derivation).

A flatten dispute derivation for a sentence σ is a sequence of the form $\begin{matrix} ⟨ {PS}_{0}, {PA}_{0}, {OS}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PS}_{n}, {PA}_{n}, {OS}_{n}, {OA}_{n} ⟩ \end{matrix}$ where

for each i, ${PA}_{i}$ , ${OA}_{i}$ are sets of assumptions and ${PS}_{i}$ is a multiset of sentences and ${OS}_{i}$ is a multiset of multisets of sentences, and

${PS}_{0} = {σ}$ , and ${PA}_{0} = {OS}_{0} = {OA}_{0} = \emptyset$ , and

at step i, one of the dispute parties makes a move satisfying the following properties:

Suppose the proponent makes a move at step i. The proponent has two options:

The proponent selects a non-assumption $δ \in {PS}_{i}$ , a rule r with head δ such that $bd (r) \cap {OA}_{i} = \emptyset$ and proceeds as follows: $\begin{array}{l} {PS}_{i + 1} = ({PS}_{i} ∖ {δ}) \oplus (bd (r) ∖ {PA}_{i}) . \\ {PA}_{i + 1} = {PA}_{i} \\ {OS}_{i + 1} = {OS}_{i} \\ {OA}_{i + 1} = {OA}_{i} \end{array}$

The proponent selects an assumption α appearing in ${OS}_{i}$ but not in ${PS}_{i} \cup {PA}_{i}$ and proceeds as follows: $\begin{array}{l} {PS}_{i + 1} = {PS}_{i} \oplus {\overline{α}} \\ {PA}_{i + 1} = {PA}_{i} \\ {OS}_{i + 1} = {OS}_{i} ∖ {S \in {OS}_{i} ∣ α \in S}^{12} \\ {OA}_{i + 1} = {OA}_{i} \cup {α} . \end{array}$

Suppose

¹²
For clarity, consider a multiset $X = {2, 2, 5}$ . Then $Y = {x \in X ∣ x is even} = {2, 2}$ .

the opponent makes a move at step i. The opponent has two options:

The opponent selects an assumption $α \in {PS}_{i}$ and proceeds as follows: $\begin{array}{l} {PS}_{i + 1} = {PS}_{i} - {α} \\ {PA}_{i + 1} = {PA}_{i} \cup {α} \\ {OS}_{i + 1} = {OS}_{i} \oplus {{\overline{α}}} \\ {OA}_{i + 1} = {OA}_{i} . \end{array}$

The opponent selects $S \in {OS}_{i}$ and a non-assumption $δ \in S$ and proceeds as follows: $\begin{array}{l} {PS}_{i + 1} = {PS}_{i} \\ {PA}_{i + 1} = {PA}_{i} \\ {OS}_{i + 1} = ({OS}_{i} ∖ {S}) \oplus {(S ∖ {δ}) \oplus bd (r) ∣ hd (r) = δ, bd (r) \cap {OA}_{i} = \emptyset} \\ {OA}_{i + 1} = {OA}_{i} . \end{array}$

Definition 13.

A dispute derivation $⟨ {PS}_{0}, {PA}_{0}, {OS}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PS}_{n}, {PA}_{n}, {OS}_{n}, {OA}_{n} ⟩$ is successful if ${PS}_{n} = {OS}_{n} = \emptyset$ .

Example 11.

Consider again the argumentation framework $F_{2}$ in Example 1.

An flatten dispute derivation for p is given in Table 5.

Table 5

A successful flatten dispute derivation for p wrt $F_{2}$ in Example 1

$Stage$	$PS$	$PA$	$OS$	$OA$	$Step$
0	p	∅	∅	∅	$1 a$
1	$not_δ$	∅	∅	∅	$2 a$
2	∅	$not_δ$	${δ}$	∅	$2 b$
3	∅	$not_δ$	${not_β, f (0)}$	∅	$2 b$
4	∅	$not_δ$	${not_β, f (1)}$	∅	$1 b$
5	β	$not_δ$	∅	$not_β$	$1 a$
6	∅	$not_δ$	∅	$not_β$	success

Lemma 14.

Let $⟨ {PS}_{0}, {PA}_{0}, {OS}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PS}_{n}, {PA}_{n}, {OS}_{n}, {OA}_{n} ⟩$ be a (possibly infinite) flatten dispute derivation. Then for any $n ⩾ 0$ , the following properties hold:

${PS}_{n} \cap {PA}_{n} = \emptyset$ ;

${OA}_{n} \cap ⨁ {OS}_{n} = \emptyset$ .

Proof.

See Appendix A.7. □

Notation 8.

For any proof tree T, $Spm (T)$ denotes the multiset of the sentences labeling the leaf nodes of T and different to $true$ .13

¹³

That means that if a sentence δ labels three leaf nodes of T, then $μ_{Spm (T)} = 3$ .

Spm (T)

is referred to as the multiset support of T.

For a set of proof trees S, $Spm (S)$ is the union of the multiset supports of trees belonging to S.14

¹⁴

I.e. $Spm (S) = ⨁ {Spm (T) ∣ T \in S}$ .

The following lemmas show that each proof-tree-based dispute derivation could be translated into an equivalent flatten one and for each flatten dispute derivation there is an equivalent proof-tree-based one. Lemma 15.

Let $dd = ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩$ be a proof-tree-based dispute derivation for σ.

Then the sequence $⟨ {PS}_{0}, {PA}_{0}, {OS}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PS}_{n}, {PA}_{n}, {OS}_{n}, {OA}_{n} ⟩$ where for each $0 ⩽ i ⩽ n$ , ${PS}_{i} = Spm ({PT}_{i}) - {PA}_{i}$ and ${OS}_{i} = {Spm (T) ∣ T \in {OT}_{i}}$ , is a flatten dispute derivation for σ.

Proof.

See Appendix A.8. □

Lemma 16.

Let $⟨ {PS}_{0}, {PA}_{0}, {OS}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PS}_{n}, {PA}_{n}, {OS}_{n}, {OA}_{n} ⟩$ be a flatten dispute derivation for σ.

There is a proof-tree-based dispute derivation $\begin{matrix} ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩ \end{matrix}$ for σ such that for all $0 ⩽ i ⩽ n$ , the following properties hold:

${PA}_{i} \subseteq Ass ({PT}_{i})$ and ${PS}_{i} = Spm ({PT}_{i}) - {PA}_{i}$ ;

${OS}_{i} = {Spm (T) ∣ T \in {OT}_{i}}$ .

Proof.

See Appendix A.9. □

Theorem 4 (Soundness theorem for flatten dispute derivation).

Let $\begin{matrix} dd = ⟨ {PS}_{0}, {PA}_{0}, {OS}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PS}_{n}, {PA}_{n}, {OS}_{n}, {OA}_{n} ⟩ \end{matrix}$ be a successful flatten dispute derivation for σ. Then ${PA}_{n} | \sim σ$ .

Proof.
From Lemma 16, there exists a proof-tree-based dispute derivation $\begin{matrix} {dd}^{'} = ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩ \end{matrix}$ for σ such that ${PS}_{i} = Spm ({PT}_{i}) - {PA}_{i}$ and ${OS}_{i} = {Spm (T) ∣ T \in {OT}_{i}}$ .

Since ${PS}_{n} = \emptyset$ , the set $Spm ({PT}_{n})$ contains only assumptions belonging to ${PA}_{n}$ . Therefore all proof trees in ${PT}_{n}$ are full. From ${PA}_{n} \subseteq Ass ({PT}_{n})$ , it follows that $Ass ({PT}_{n}) = {PA}_{n}$ .

Since ${OS}_{n} = {Spm (T) ∣ T \in {OT}_{n}}$ and ${OS}_{n} = \emptyset$ , it follows ${OT}_{n} = \emptyset$ .

Therefore ${dd}^{'}$ is a successful proof-tree-based dispute derivation. From Theorem 2, it follows ${PA}_{n} | \sim σ$ . □
Theorem 5 (Completeness theorem for flatten dispute derivation).

Let $F$ be a finitary ABA framework, H be a strictly admissible finite set of assumptions and σ be a sentence such that $H | \sim σ$ . Then there is a successful flatten dispute derivation $\begin{matrix} ⟨ {PS}_{0}, {PA}_{0}, {OS}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PS}_{n}, {PA}_{n}, {OS}_{n}, {OA}_{n} ⟩ \end{matrix}$ for σ such that ${PA}_{n} \subseteq H$ .

Proof.
From the completeness Theorem 3, there is a successful tree-based dispute derivation $\begin{matrix} dd = ⟨ {PT}_{0}, {PA}_{0}, {OT}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PT}_{n}, {PA}_{n}, {OT}_{n}, {OA}_{n} ⟩ \end{matrix}$ such that ${PA}_{n} | \sim σ$ .

It holds that ${OT}_{n} = \emptyset$ and all proof trees ${PT}_{n}$ are full and $Ass ({PT}_{n}) = {PA}_{n}$ .

Let ${dd}^{'} = ⟨ {PS}_{0}, {PA}_{0}, {OS}_{0}, {OA}_{0} ⟩, \dots, ⟨ {PS}_{n}, {PA}_{n}, {OS}_{n}, {OA}_{n} ⟩$ be the flatten dispute derivation for σ as defined in Lemma 15.

Since all proof trees ${PT}_{n}$ are full and $Ass ({PT}_{n}) = {PA}_{n}$ , it follows ${PS}_{n} = Spm ({PT}_{n}) - {PA}_{n} = \emptyset$ .

Since ${OT}_{n} = \emptyset$ , ${OS}_{n} = \emptyset$ . Hence ${dd}^{'}$ is successful and ${PA}_{n} | \sim σ$ . □

7. Discussion

Dialectical proof procedures for assumption-based argumentation are in general sound but not complete wrt the admissibility semantics. The reason is that these procedures may get stuck in infinite loops. To give a precise characterization of their semantics, we represent these loops as infinite arguments. Infinite arguments are characterized by two distinctive features: i) they attack other arguments in the same way as finite arguments do (and hence showing up in the execution of the dialectical procedures as the finite arguments do), and ii) they attack themselves (and hence can not be accepted as support of their conclusions).

The inclusion of infinite arguments in assumption-based argumentation leads to a new semantics referred to as strict admissibility that is stricter than admissibility, i.e. if a set of arguments is strictly admissible, it is also admissible but not vice versa.

To show that dialectical proof procedures are sound and complete wrt strict admissibility, we proceed in two stages: We first develop a new dialectical proof procedure based explicitly on the notion of arguments and partial arguments (also referred to as full proof trees and partial proof trees) and show the soundness and completeness of this procedure wrt strict admissibility semantics. We then flatten this procedure to get more “traditional” ones that are based on sets and multisets similar to procedures in [15,16].

Our version of flatten dispute derivation differs from the ones in [15,17] in two interesting aspects: 1) the first and more relevant point is that a stronger filtering mechanism for filtering opponent supports in step (1.b) is employed. In [15,17], only one element of ${OS}_{i}$ is removed while in our case, all elements of ${OS}_{i}$ containing the selected assumption are removed, 2) the second and more or less technical point is that while in our case ${PA}_{i}$ is the set of all proponent assumptions that have been attacked by the opponent, in [15,17] ${PA}_{i}$ is the set of all assumptions appearing in the supports of proponent proof trees.

As strict admissibility implies admissibility, Theorem 4 could be viewed as generalizing the soundness theorem wrt admissibility of the dialectical proof procedures in [15,17].

[15,17] show the completeness of dialectical proof procedure wrt admissibility semantics for ABA frameworks without infinite arguments. As strict admissibility and admissibility coincide for this restricted class of ABA frameworks, the completeness result in [15,17] could be viewed as a special case of Theorem 5.

[22] proposes structured dispute derivation where instead of proof trees only their supports and conclusions are represented. Gaertner and Toni’s procedure could also be viewed as a flattened version of our proof-tree based procedure. [8] has introduced argument graph to deal with a loop in frameworks with a finite set of rules. For frameworks with infinite set of rules as in our Example 1, argument graphs can not capture strict admissiblity.

A novel contribution of this paper is to view partial proof trees as sets of partial proofs allowing us to define infinite arguments simply as the union of an increasing sequence of finite partial arguments. This simplifies the technical machinery needed for understanding properties of the dialectical procedures in no small amount.

Infinite arguments have also been introduced in [25] to capture ambiguity blocking and ambiguity propagating proof theories in defeasible logic as discussed in [30]. As the frameworks of assumption-based argumentation and defeasible logics are based on distinct concepts, it would be interesting to look at the relationship between our approach and the approach in [25].

In an abstract argumentation framework by assuming the existence of preferred extensions we actually implicitly assume the maximality axiom or the axiom of choice. More on this point can be seen in [9,33].

Footnotes

Appendix

References

Arieli and

Straßer, Logical argumentation by dynamic proof systems, Theoretical Computer Science 781 (2019), 63–91, https://www-sciencedirect-com-443.web.bisu.edu.cn/science/article/pii/S0304397519301252 . doi:10.1016/j.tcs.2019.02.019.

Baroni,

Cerutti,

Giacomin and

Simari (eds), Proceedings of Conference on Computational Models of Arguments, IOS Press, 2010.

Besnard,

Doutre and

Hunter (eds), Proceedings of Conference on Computational Models of Arguments Computational Models of Arguments, IOS Press, 2008.

W.D.

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

Bondarenko,

P.M.

Dung,

R.A.

Kowalski and

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

Caminada and

Amgoud, On the evaluation of argumentation formalisms, Artificial Intelligence 171 (2007), 286–310. doi:10.1016/j.artint.2007.02.003.

Cayrol,

Doutre and

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.

Craven and

Toni, Argument graphs and assumption-based argumentation, Artificial Intelligence 233 (2016), 1–59. doi:10.1016/j.artint.2015.12.004.

B.A.

Davey and

H.A.

Priestley, Introduction to Lattices and Order, Cambridge University Press, 2002.

10.

Denecker and

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

11.

Dershowitz and

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.

P.M.

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

13.

P.M.

Dung, 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.

14.

P.M.

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

15.

P.M.

Dung,

R.A.

Kowalski and

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

16.

P.M.

Dung,

R.A.

Kowalski and

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

17.

P.M.

Dung,

Mancarella and

Toni, Computing ideal skeptical argumentation, Artificial Intelligence 171 (2007).

18.

P.M.

Dung and

P.M.

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

19.

P.E.

Dunne and

Bench-Capon (eds), Proceedings of Conference on Computational Models of Arguments Computational Models of Arguments, IOS Press, 2006.

20.

P.E.

Dunne and

T.J.M.

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

21.

Eshghi and

R.A.

Kowalski, 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.

22.

Gaertner and

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

23.

A.J.

Garcia and

G.R.

Simari, Defeasible logic programming: An argumentative approach, TPLP 4(1–2) (2004), 95–138.

24.

A.J.

Garcia and

G.R.

Simari, Defeasible logic programming: DeLP servers, contextual queries and explanation for answers, J. Arguments and Computation (2014).

25.

Governatori,

M.J.

Maher,

Antoniou and

Billington, Argumentation semantics for defeasible logic, J. Log. Comput. 14(5) (2004), 675–702. doi:10.1093/logcom/14.5.675.

26.

J.W.

Lloyd, Foundations of Logic Programming, Springer Verlag, 1987.

27.

Manna and

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

28.

Modgil and

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

29.

Modgil and

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

30.

Nute, Defeasible logic programming: DeLP servers, contextual queries and explanation for answers, in: Proc. 20th Hawaii International Conference on System Science, IEEE Press, 1987.

31.

J.L.

Pollock, Defeasible reasoning, Cognitive Science 11(4) (1987), 481–518. doi:10.1207/s15516709cog1104_4.

32.

Rahwan and

Simari (eds), Handbook of Argumentation in AI, Springer Verlag, 2009.

33.

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

34.

P.M.

Thang and

P.M.

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

35.

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.

36.

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

37.

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

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

38.

Verheij,

Szeider and

Woltran (eds), Proceedings of Conference on Computational Models of Arguments, IOS Press, 2012.

39.

Vreeswijk and

Prakken, Credulous and sceptical argument games for preferred semantics, in: JELIA 2000,

Ojeda-Aciego,

I.P.

de Guzmán,

Brewka and

L.M.

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

Infinite arguments and semantics of dialectical proof procedures

Abstract

Keywords

1. Introduction

2.1. Abstract argumentation

2.2. Assumption-based argumentation

4 I.e. all leaves of any full proof tree T are final and Ass ( T ) = Sp ( T ) .

3.1. Sequence of partial proof trees

Definition 7 (Proof tree-based dispute derivation).

7 See Notation 2.

Theorem 3 (Completeness theorem).

5.1. H-Constrained dispute derivation

8 AR H is the set of all finite arguments whose assumptions belong to H.

6. Flatten dispute derivation

Definition 12 (Flatten dispute derivation).

12 For clarity, consider a multiset X = { 2 , 2 , 5 } . Then Y = { x ∈ X ∣ x is even } = { 2 , 2 } .

Footnotes

Appendix

References

⁴
I.e. all leaves of any full proof tree T are final and $Ass (T) = Sp (T)$ .

⁷
See Notation 2.

⁸
${AR}_{H}$ is the set of all finite arguments whose assumptions belong to H.

¹²
For clarity, consider a multiset $X = {2, 2, 5}$ . Then $Y = {x \in X ∣ x is even} = {2, 2}$ .