Infinite arguments and semantics of dialectical proof procedures

Thang, Phan Minh; Dung, Phan Minh; Pooksook, Jiraporn

doi:10.3233/AAC-200546

Infinite arguments and semantics of dialectical proof procedures

Article type: Research Article

Authors: Thang, Phan Minh^{a; *} | Dung, Phan Minh^b | Pooksook, Jiraporn^c

Affiliations: [a] International College of Burapha University, Burapha University, Thailand | [b] Department of ICT, Asian Institute of Technology, Thailand | [c] Department of Electrical and Computer Engineering, Naresuan University, Thailand

Correspondence: [*] Corresponding author. E-mail: [email protected].

Keywords: Dialectical proof procedure, infinite arguments, admissibility semantic, soundness and completeness

DOI: 10.3233/AAC-200546

Journal: Argument & Computation, vol. 13, no. 2, pp. 121-157, 2022

Published: 1 June 2022

Get PDF

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.

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.

F1:r:p←not_δr′:δ←f(0)rn:f(n)←f(n+1),n⩾0t:β←F2:r:p←not_δr″:δ←not_β,f(0)rn:f(n)←f(n+1),n⩾0t:β←

The semantics of F1 and F2 are determined by the arguments illustrated in Fig. 1.

Fig. 1.

Arguments of F1 and F2.

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 F1 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 F2 despite the presence of the same loop D.

The distinct behavior of the dialectical proof procedures wrt the two frameworks F1, F2 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 F1, there is an infinite argument for δ represented by the infinite proof tree C1. This argument can not be attacked as it is not based on any assumption.

For framework F2, there is an infinite argument for δ represented by the infinite proof tree C2. 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 F1 while it is still admissible wrt F2.

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 C1 can not be attacked by any other argument wrt F1, should it be accepted and δ concluded?

As infinite loops represent a kind of unfinished, inconclusive business, C1 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 1
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 2

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)∈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,‾) where R is a set of inference rules of the form l0←l1,…ln (n⩾0 and l1,…,ln∈L), and A⊆L is a set of assumptions, and ‾ is a (total) one-one mapping from A into L∖A, where 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 3

An ABA framework F=(R,A,‾) is finitary if for each sentence σ∈L, the set of rules of the form σ←l1,…ln (n⩾0 and l1,…,ln∈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 l0←l1,…ln, l0 and the set {l1,…,ln} 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,‾).

Definition 1

Definition 1(Partial proof).

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

(root,σ0).(r1,σ1).…(rn,σn)

where ri∈R, i⩾1 such that σi−1=hd(ri) and σi∈bd(ri). If bd(ri)=∅ then σi=true.

Example 2.

Consider the argumentation framework F2 in Example 1.

Some partial proofs supporting p and δ are given below and illustrated in Fig. 2.

ψ=(root,p)ψ′=(root,p).(r,not_δ)π0=(root,δ)π1′=(root,δ).(r″,not_β)π1=(root,δ).(r″,f(0))π2=(root,δ).(r″,f(0)).(r0,f(1))…πn+1=(root,δ).(r″,f(0)).(r0,f(1))…(rn−1,f(n))

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

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

π≡(root,σ0).(r1,σ1).…(rn,σn),n>0

from T, the following properties hold:

the partial proof π′≡(root,σ0).(r1,σ1).…(rn−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 π′.(rn,σ′) with σ′∈bd(rn), 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.

A0={ψ}A={ψ,ψ′}C0={π0}C20={π0,π1,π1′}C21={π0,π1′,π1,π2}C2={π0,π1′,π1,π2,π3,…,πn,…}

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

Notation 1(Nodes in partial proof trees).

Abusing the notation for convenience, we often refer to a partial proof (root,σ0).(r1,σ1).…(rn,σ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 C20 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 C20, C21, C2 are {not_β,f(0)}, {not_β,f(1)} and {not_β} respectively.

Definition 3

Definition 3(Arguments).

A full proof tree is a partial proof tree whose support consists only of assumptions.4 4
An argument for α is a full proof tree for α.
The set of all arguments wrt the ABA framework F is denoted by ARF while the set of all finite arguments is denoted by ARfin,F.

Example 4.

Continue from Example 3. A, B, C2 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 C1 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

Definition 4(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 ARF is denoted by attF while the attack relations between finite arguments is denoted by attfin,F. Define
AFF=(ARF,attF)andAFfin,F=(ARfin,F,attfin,F)

Example 5.

Consider again Example 1, we have AFF1=(ARF1,attF1) where ARF1⊇{A,B,C1} and attF1⊇{(C1,A),(C1,C1)}.

Further AFF2=(ARF2,attF2) where ARF2⊇{A,B,C2} and attF2⊇{(C2,A),(B,C2),(C2,C2)}.

If we consider only finite arguments, ARfin,F1=ARfin,F2 and attfin,F1=attfin,F2. Hence AFfin,F1=AFfin,F2.

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⊆ARF be admissible wrt AFF=(ARF,attF). Then S contains only finite arguments.

Definition 5

Definition 5(Admissibility and strict admissibility).

Abusing the notation slightly for simplicity, we say that a set of arguments S⊆ARF is

strictly admissible iff it is admissible wrt the argumentation framework AFF=(ARF,attF), and
admissible iff it is admissible wrt the argumentation framework AFfin,F=(ARfin,F,attfin,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 AFF2 but not wrt AFF1 as B attacks C2 but not C1.

We define accordingly the notions of admissible and strictly admissible sets of assumptions.

Definition 6

Definition 6(Admissible and strictly admissible sets of assumptions).

Let H be a set of assumptions and ARH be the set of all finite arguments whose supports are subsets of H.

(1) We say H is admissible (resp strictly admissible) iff there is subset S⊆ARH such that Ass(S)=H and S is admissible (resp. strictly admissible).
(2) 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∈ARH such that Cl(A)=σ.
(3) We write H|∼σ to denote that σ is strictly credulously derived from H.

Example 6.

Consider again Example 5 and let H={not_δ}. Hence, ARH⊃{A,B} (wrt both F1, F2).

Since C1 attacks A wrt F1 but there is no attack against C1 wrt F1, H is not strictly admissible wrt F1.

In contrast, H is strictly admissible wrt F2 as B attacks C2. Hence p is strictly credulously derived from H wrt F2 but not wrt F1.

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 5

T′ is an immediate expansion of T at N if there is a rule r of the form σ←b1,…,bm such that T′ is obtained from T by adding m children N.(r,b1),…,N.(r,bm) to N (for m=0, a child node N.(r,true) is added to N), i.e. T′=T∪{N.(r,b1),…,N.(r,bm)}.
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
CE(T,N)={exp(T,N,r′)∣r′ is a rule s.t. hd(r′)=σ}andCE(T,N,S)={exp(T,N,r′)∣r′ is a rule s.t. hd(r′)=σ,bd(r)∩S=∅}
where S is a set of assumptions.

It is easy to see that CE(T,N)=CE(T,N,∅).

Example 7.

Consider the partial proof tree C20={π0,π1,π1′} in Fig. 3.

Let N=π1. Then

exp(C20,N,r0)=C20∪{π1.(r0,f(1))}={π0,π1′,π1,π2}=C21.

Notation 4.

Let T0, T1 be partial proof trees for σ0.

We say T0 is a prefix of T1 iff T0⊆T1.

We say T0 is a proper prefix of T1 if T0 is a prefix of T1 and T0≠T1.

Lemma 2.

Let T0, T1 be partial proof trees. The following statements hold:

(1) If T1 is an immediate expansion of T0 then T0 is a prefix of T1.
(2) Suppose T0 is a prefix of T1. It holds that
- (a) the roots of T0, T1 coincide; and
- (b) if N is a node in T0 then the parent and children of N in T0 (if exist) are respectively also the parent and children of N in T1.

Proof.

Obvious. □

Lemma 3.

Let T be an argument, T0 be a partial proof tree such that T0 is a proper prefix of T. Furthermore, let N be a leaf node in T0 and S be a set of assumptions. The following statements hold:

(1) Suppose CE(T0,N)≠∅. Then there is T1∈CE(T0,N) such that T1 is a prefix of T.
(2) Suppose Ass(T)∩S=∅ and CE(T0,N,S)≠∅. Then there is T1∈CE(T0,N,S) such that T1 is a prefix of T

Proof.

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

Since CE(T0,N,S)≠∅, 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 γ∈bd(r). From the definition of proof trees (Definition 2), it follows T1=exp(T0,N,r)⊆T. Since Ass(T)∩S=∅, it follows that bd(r)∩S=∅. Hence T1∈CE(T0,N,S). The second statement holds. □

An increasing sequence of partial proof trees T0⊆T1⊆…Ti⊆… is said to be fair if for each Ti, for each non-final leaf node N∈Ti there is a node M∈Tj, j>i, such that N is a proper prefix of M.

Lemma 4.

Let sq≡T0⊆T1⊆…Ti⊆… be an increasing sequence of partial proof trees. The following statements hold:

(1) T0∪T1∪…Ti∪… is a partial proof tree.
(2) If the sequence sq is fair then T0∪T1∪…Ti∪… is an argument.

Proof.

The first statement is obvious. We prove the second. Suppose T≡T0∪T1∪…Ti∪… is not an argument. Hence T has a non-final leaf node N labeled by δ. Thus N∈Ti for some i. Since sq is fair, N is a proper prefix of some node M∈Tj, j>i. Hence N is not a leaf of T. Contradiction. □

Notation 5.

Let T be a partial proof tree and N≡(root,σ0).(r1,σ1).…(ri,σ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 6

The maximum of the heights of the non-final leaf nodes in T is denoted by ha(T), i.e.

ha(T)=max{h(N,T)∣N is a non-final leaf node in T}

Notation 6.

Two partial proof trees T, T′ are compatible iff T∪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∈Π such that ha(T)>n, there is T′∈Π such that T′⊆T and ha(T′)=n; and
for each n⩾0, the set {T∈Π∣ha(T)⩽n} is finite; and
for all T,T′∈Π such that T, T′ are compatible, it holds that T⊆T′ or T′⊆T.

Then there is an infinite strictly increasing sequence of proof trees

T0⊂T1⊂⋯⊂Tn⊂…

such that for each i⩾0, Ti∈Π.

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 ⟨PT0,PA0,OT0,OA0⟩,…,⟨PTi,PAi,OTi,OAi⟩ where at each stage i,

PTi is the set of partial proof trees the proponent has constructed until stage i;
OTi is the set of partial proof trees the opponent has constructed and not yet attacked by the proponent until stage i;
PAi (resp OAi) 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

Definition 7(Proof tree-based dispute derivation).

A proof-tree-based dispute derivation for a sentence σ is a (possibly infinite) sequence of the form

⟨PT0,PA0,OT0,OA0⟩,…,⟨PTi,PAi,OTi,OAi⟩

where

for each i, PAi, OAi are sets of assumptions and PTi, OTi are sets of partial proof trees, and
PT0 contains exactly one partial proof tree consisting of only the root labeled by σ (i.e. PT0={{(root,σ)}}), and
PA0=OT0=OA0=∅, and
at stage i, 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 expands one of her partial arguments by selecting a partial proof tree T∈PTi, a non-final leaf node N in T labeled by δ, a rule r with head δ such that bd(r)∩OAi=∅ and expanding T resulting in:
    PTi+1=(PTi∖{T})∪{exp(T,N,r)}.PAi+1=PAiOTi+1=OTiOAi+1=OAi
  - (b) The proponent attacks partial proof trees in OTi at an assumption α∈Ass(OTi)∖Ass(PTi).7 7 Then
    PTi+1=PTi∪{{(root,α‾)}}PAi+1=PAiOTi+1=OTi∖{T′∈OTi∣α∈Ass(T′)}OAi+1=OAi∪{α}.
- (2) Suppose the opponent makes a move at stage i. The opponent has two options:
  - (a) The opponent attacks a proponent partial proof tree T∈PTi at a leaf node labeled by an assumption α∈Ass(T)∖PAi:
    PTi+1=PTiPAi+1=PAi∪{α}OTi+1=OTi∪{{(root,α‾)}}OAi+1=OAi.
  - (b) The opponent expands an opponent partial proof tree T∈OTi at a non-final leaf node N filtered by the assumptions in OAi, i.e.,
    PTi+1=PTiPAi+1=PAiOTi+1=(OTi∖{T})∪CE(T,N,OAi)OAi+1=OAi.

Definition 8.

A proof-tree-based dispute derivation ⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩ is successful if OTn=∅, and PTn consists only of full proof trees and PAn=Ass(PTn).

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 F2 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	A0	∅	∅	∅	1a
1	A	∅	∅	∅	2a
2	A	not_δ	C0	∅	2b
3	A	not_δ	C20	∅	2b
4	A	not_δ	C21	∅	1b
5	A, B0	not_δ	∅	not_β	1a
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=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩ be a dispute derivation. The following statements hold:

(1) Ass(OTn)∩OAn=∅.
(2) For each α∈OAn, there is a partial proof tree T∈PTn such that Cl(T)=α‾.
(3) For each β∈PAn there is a unique stage i, i<n, such that {β}=PAi+1∖PAi and {(root,β‾)}∈OTi+1∖OTi.
For each a partial proof tree T∈OTi, i⩽n, there is a unique β∈PAn such that Cl(T)=β‾.
(4) Let T,T′∈OTi, 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

Definition 9(Scope).

Let T be a proof tree and dd=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩ be a dispute derivation for σ.

A scope of length k of T in dd is a pair (sq,i) where sq≡T0,T1,…,Tk−1, i⩾0 and k⩾1, such that the following conditions hold:

(1) T0={(root,Cl(T))} and T0∈OTi∖OTi−1.
(2) For each 0⩽j⩽k−1: Tj∈OTi+j and Tj⊆T;
(3) For each 0⩽j<k−1: either Tj+1=Tj or Tj+1 is an immediate expansion of Tj.

A scope (seq,i) of T in dd is a full scope if there is no prefix of T in OTi+k.

Lemma 7.

Let T be a proof tree and dd=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩ be a dispute derivation. The following statements hold:

(1) Let (sq,i), (sq′,j) be two scopes of T in dd of equal length. Then i=j and sq, sq′ are identical;
(2) If T∈OTn then there is a scope (sq,i), sq=T0,…,Tk−1, of T in dd such that i+k−1=n and T=Tk−1;
(3) If dd is a successful dispute derivation that terminates at ⟨PTn,PAn,OTn,OAn⟩ and T is an argument attacking some argument in PTn then there is a unique full scope of T in dd.

Proof.

See Appendix A.4. □

Lemma 8.

Let dd=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩ be a successful dispute derivation and let T be an argument attacking some argument in PTn. Then Ass(T)∩OAn≠∅.

Proof.

Let (sq,i) with sq=T0,…,Tk−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 OTi+k. Hence there are two cases:

Tk−1 is attacked by the proponent at stage i+k−1 in dd using (1.b). It follows that Tk−1 (and hence T) contains an assumptions in OAi+k−1⊆OAn.
Tk−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 Tk−1 is selected such that
OTi+k=(OTi+k−1∖{Tk−1})∪CE(Tk−1,N,OAi+k−1)

Suppose Ass(T)∩OAn=∅. Hence Ass(T)∩OAi+k−1=∅. From Lemma 3, it follows that there is T′∈CE(Tk−1,N,OAi+k−1) such that T′ is a prefix of T. Contradiction since there is no proof tree in OTi+k that is a prefix of T.

Therefore Ass(T)∩OAn≠∅. □

Lemma 9.

Let dd=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩ be a successful dispute derivation for σ. Then PAn∩OAn=∅.

Proof.

Suppose there exists α∈PAn∩OAn. Let i be the stage in dd where α is attacked by the proponent (step (1.b) in Definition 7) and inserted into OAi. Therefore α does not appear in PTi. The only ways for α to show up in PTn later is by applying step (1.a).

It is also clear that for each i<j⩽n, α∈OAj. At any stage j>i in dd, if the proponent expands a partial proof tree T∈PTj then only rules r with bd(r)∩OAj=∅ are selected (the filtering condition in step (1.a) of Definition 7). Therefore α can never show up in PTj. Hence α∉PAn. Contradiction. □

Theorem 2

Theorem 2(Soundness theorem).

Let dd=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩ be a successful dispute derivation for σ. The following statements hold:

(1) PTn is strictly admissible and σ∈Cl(PTn).
(2) PAn|∼σ.

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 PTn.

Suppose an argument T attacks PTn. From the Lemmas 8, 6, it follows immediately that T is attacked by PTn.

We show now that PTn is conflict-free. Suppose the contrary that PTn is not conflict-free. Then there are arguments T,T′∈PTn such that T attacks T′. From Lemma 8, T contains an assumption from OAn. From Ass(T)⊆Ass(PTn)=PAn, it follows PAn∩OAn≠∅. Contradiction to Lemma 9. □

5.Completeness of proof-tree-based dispute derivation

Theorem 3

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|∼σ. Then there is a successful proof-tree-based dispute derivation ⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩ for σ such that PAn⊆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|∼σ, the task is to construct a successful dispute derivation

⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩

for σ such that PAn⊆H and PTn⊆ARH.8 8

The key idea is rather simple: Associate each partial proof tree T∈PTi to some argument A∈ARH 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.

r1:σ←not_δr2:δ←not_βr3:β←not_γr4:β←d

Let H={not_δ,not_γ}. Hence ARH⊇{T1,T3} (see Fig. 5).

Consider the dispute derivations for σ represented in Tables 2, 3. At stage 4, either r3 or r4 could be selected for an expansion of T2. Selecting r4 leads to a failed derivation (Table 2). If we associate T2 with T3 at stage 4 when it is created, we would select r3 to expand T2 towards T3 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	T0	∅	∅	∅	1a
1	T1	∅	∅	∅	2a
2	T1	not_δ	A0	∅	2b
3	T1	not_δ	A1	∅	1b
4	T1, T2	not_δ	∅	not_β	1a
5	T1, T3′	not_δ	∅	not_β	fail

Table 3

A successful tree-based dispute derivation

Stage	PT	PA	OT	OA	Step
0	T0	∅	∅	∅	1a
1	T1	∅	∅	∅	2a
2	T1	not_δ	A0	∅	2b
3	T1	not_δ	A1	∅	1b
4	T1, T2	not_δ	∅	not_β	1a
5	T1, T3	not_δ	∅	not_β	success

More formally, at each stage ⟨PTi,PAi,OTi,OAi⟩ in a dispute derivation, we add a new component λi representing a function that associates each proof tree T∈PTi to an argument λi(T)∈ARH 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∈X,y∈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

hi(T)=min{h(N,T)∣N is a non-final leaf node in T}9

For9 a set S of proof trees, define

hi(S)=min{hi(T)∣T∈S}

A partial proof tree T is said to be almost balanced iff ha(T)⩽hi(T)+1.

Definition 10.

Let H be a set of assumptions. A H-constrained dispute derivation for σ is a (possibly infinite) sequence

⟨PT0,PA0,OT0,OA0,λ0⟩,…,⟨PTi,PAi,OTi,OAi,λi⟩

where

for each i, PAi, OAi are sets of assumptions, PTi, OTi are sets of partial proof trees, and
λi:PTi→ARH; and
PT0, PA0, OT0, OA0 are defined as in Definition 7; and
{(root,σ)}⊆λ0({(root,σ)});
at stage i, 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 proceeds as in step (1.a) in Definition 7 with an extra condition that exp(T,N,r)⊆λi(T), and computes λi+1 as follows:
    λi+1=(λi∖{(T,λi(T))})∪{(exp(T,N,r),λi(T))}
  - (b) The proponent selects an assumption α∈Ass(OTi)∖Ass(PTi) and an argument A∈ARH such that Cl(A)=α‾ and then proceeds to compute PTi+1, PAi+1, OTi+1, OAi+1 as in step (1.b) in Definition 7, and computes λi+1 as follows:
    λi+1=λi∪{(T0,A)}with T0={(root,α‾)}.
- (2) Suppose the opponent makes a move at stage i. The opponent has two options:
  - (a) The opponent proceeds as in step (2.a) in Definition 7 where λi+1 is computed by λi+1=λi.
  - (b) The opponent proceeds as in step (2.b) in Definition 7 with two extra conditions:
    ∗ h(N,T)=hi(OTi); and
    ∗ it is not possible for the proponent to execute step 1.b.10 10
    PTi+1, PAi+1, OTi+1, OAi+1 are computed as in step (2.b) in Definition 7, and λi+1=λi

Definition 11.

A H-constrained dispute derivation

⟨PT0,PA0,OT0,OA0,λ0⟩,…,⟨PTn,PAn,OTn,OAn,λn⟩is successful iff the dispute derivation⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩is successful.

Example 10.

Consider again Example 9 (the partial proof trees of this example can be seen in Fig. 5) where H={not_δ,not_γ} and ARH⊇{T1,T3}.

A H-constrained dispute derivation for σ is given in Table 4. Note that at stage 4, guided by λ4(T2)=T3, rule r3 must be selected to expand T2 into T3. In other words, rule r4 can not be selected and hence no failed derivation can be constructed.

Table 4

A successful tree-based dispute derivation

Stage	PT	PA	OT	OA	λ	Step
0	T0	∅	∅	∅	(T0,T1)	1a
1	T1	∅	∅	∅	(T1,T1)	2a
2	T1	not_δ	A0	∅	(T1,T1)	2b
3	T1	not_δ	A1	∅	(T1,T1)	1b
4	T1, T2	not_δ	∅	not_β	(T1,T1), (T2,T3)	1a
5	T1, T3	not_δ	∅	not_β	(T1,T1), (T3,T3)	success

Lemma 10.

Let ⟨PT0,PA0,OT0,OA0,λ0⟩,…,⟨PTi,PAi,OTi,OAi,λi⟩ be a H-constrained dispute derivation for σ. The following conditions hold:

(1) ⟨PT0,PA0,OT0,OA0⟩,…,⟨PTi,PAi,OTi,OAi⟩ is a dispute derivation for σ (as defined in Definition 7).
(2) λi:PTi→ARH, i⩾0, such that for each T∈PTi: T⊆λi(T);

Proof.

Statement 1 follows directly from Definition 7 and 10.

We prove the second statement by induction on n.

Basic step: n=0. The statement follows directly from the definition of ⟨PT0,PA0,OT0,OA0,λ0⟩ in Definition 10.

Inductive step. We show the statement holds for n+1 assuming it holds for n.

If the step applied at stage n is (2.a) or (2.b), then the statement holds obviously since PTn=PTn+1, λn=λn+1.

Suppose step (1.a) is applied at stage n. Let T∈PTn be the selected proof tree. Therefore for any T′∈PTn and T′≠T, λn+1(T′)=λn(T′)⊇T′.

Let exp(T,N,r) be the expansion of T at stage n. Hence

λn+1(exp(T,N,r))=λn(T)⊇exp(T,N,r).

The statement holds.

Suppose step (1.b) is applied at stage n. The statement follows immediately from the fact that

PTn+1=PTn∪{{(root,α‾)}}andλi+1=λi∪{(T0,A)}with T0={(root,α‾)} and A∈ARH such that Cl(A)=α‾.

□

Lemma 11.

Let H be a strictly admissible set of assumptions and

cdd≡⟨PT0,PA0,OT0,OA0,λ0⟩,…,⟨PTn,PAn,OTn,OAn,λn⟩

be a terminated H-constrained dispute derivation for σ (i.e. neither of the players could make a move at stage n).

Then cdd is successful.

Proof.

Since step (1.a) can not be executed at stage n, each proof tree in PTn is full. Therefore PTn⊆ARH.

Since the opponent can not make a move with step (2.a) at stage n, it follows that

PAn=Ass(PTn)⊆H.

Since the proponent can not make a move with step (1.b) at n, it follows that

Ass(OTn)⊆Ass(PTn)=PAn⊆H.

Since the opponent can not make a move with step(2.b) at stage n, it follows that all partial proof trees in OTn are full. Hence each argument in OTn attacks H.

From Ass(OTn)⊆Ass(PTn)=PAn⊆H, it follows OTn⊆ARH. Since H is strictly admissible, OTn is empty.

From Definition 8, 11, cdd is successful. □

Lemma 12.

Let cdd=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTi,PAi,OTi,OAi⟩ be a H-constrained dispute derivation for σ. For all i⩾0, OTi is finite and every proof tree in OTi is almost balanced.

Proof.

See Appendix A.5. □

Lemma 13.

Let H be a strictly admissible finite set of assumptions. Then there is no infinite H-constrained dispute derivation for σ wrt F.11 11

Proof.

See Appendix A.6. □

5.2.Proof of completeness theorem (Theorem 3)

Construct a H-constrained dispute derivation for σ. The construction will terminate since no infinite H-constrained dispute derivation exists (Lemma 13). From Lemma 11, it follows that any terminated constrained dispute derivation is successful.

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 ⟨PTi+1,PAi+1,OTi+1,OAi+1⟩ from ⟨PTi,PAi,OTi,OAi⟩, we need only the sentences in the supports of arguments in PTi∪OTi. Hence a “simplification” of the proof tree based dispute derivation could be obtained by replacing each tree in PTi∪OTi 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

Definition 12(Flatten dispute derivation).

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

⟨PS0,PA0,OS0,OA0⟩,…,⟨PSn,PAn,OSn,OAn⟩

where

for each i, PAi, OAi are sets of assumptions and PSi is a multiset of sentences and OSi is a multiset of multisets of sentences, and
PS0={σ}, and PA0=OS0=OA0=∅, and
at step i, one of the dispute parties makes a move satisfying the following properties:
- (1) Suppose the proponent makes a move at step i. The proponent has two options:
  - (a) The proponent selects a non-assumption δ∈PSi, a rule r with head δ such that bd(r)∩OAi=∅ and proceeds as follows:
    PSi+1=(PSi∖{δ})⊕(bd(r)∖PAi).PAi+1=PAiOSi+1=OSiOAi+1=OAi
  - (b) The proponent selects an assumption α appearing in OSi but not in PSi∪PAi and proceeds as follows:
    PSi+1=PSi⊕{α‾}PAi+1=PAiOSi+1=OSi∖{S∈OSi∣α∈S}12OAi+1=OAi∪{α}.
- (2) Suppose12 the opponent makes a move at step i. The opponent has two options:
  - (a) The opponent selects an assumption α∈PSi and proceeds as follows:
    PSi+1=PSi−{α}PAi+1=PAi∪{α}OSi+1=OSi⊕{{α‾}}OAi+1=OAi.
  - (b) The opponent selects S∈OSi and a non-assumption δ∈S and proceeds as follows:
    PSi+1=PSiPAi+1=PAiOSi+1=(OSi∖{S})⊕{(S∖{δ})⊕bd(r)∣hd(r)=δ,bd(r)∩OAi=∅}OAi+1=OAi.

Definition 13.

A dispute derivation ⟨PS0,PA0,OS0,OA0⟩,…,⟨PSn,PAn,OSn,OAn⟩ is successful if PSn=OSn=∅.

Example 11.

Consider again the argumentation framework F2 in Example 1.

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

Table 5

A successful flatten dispute derivation for p wrt F2 in Example 1

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

Lemma 14.

Let ⟨PS0,PA0,OS0,OA0⟩,…,⟨PSn,PAn,OSn,OAn⟩ be a (possibly infinite) flatten dispute derivation. Then for any n⩾0, the following properties hold:

(1) PSn∩PAn=∅;
(2) OAn∩⨁OSn=∅.

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 13 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 14

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=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩ be a proof-tree-based dispute derivation for σ.

Then the sequence ⟨PS0,PA0,OS0,OA0⟩,…,⟨PSn,PAn,OSn,OAn⟩ where for each 0⩽i⩽n, PSi=Spm(PTi)−PAi and OSi={Spm(T)∣T∈OTi}, is a flatten dispute derivation for σ.

Proof.

See Appendix A.8. □

Lemma 16.

Let ⟨PS0,PA0,OS0,OA0⟩,…,⟨PSn,PAn,OSn,OAn⟩ be a flatten dispute derivation for σ.

There is a proof-tree-based dispute derivation

⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩

for σ such that for all 0⩽i⩽n, the following properties hold:

(1) PAi⊆Ass(PTi) and PSi=Spm(PTi)−PAi;
(2) OSi={Spm(T)∣T∈OTi}.

Proof.

See Appendix A.9. □

Theorem 4

Theorem 4(Soundness theorem for flatten dispute derivation).

Let

dd=⟨PS0,PA0,OS0,OA0⟩,…,⟨PSn,PAn,OSn,OAn⟩

be a successful flatten dispute derivation for σ. Then PAn|∼σ.

Proof.

From Lemma 16, there exists a proof-tree-based dispute derivation

dd′=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩

for σ such that PSi=Spm(PTi)−PAi and OSi={Spm(T)∣T∈OTi}.

Since PSn=∅, the set Spm(PTn) contains only assumptions belonging to PAn. Therefore all proof trees in PTn are full. From PAn⊆Ass(PTn), it follows that Ass(PTn)=PAn.

Since OSn={Spm(T)∣T∈OTn} and OSn=∅, it follows OTn=∅.

Therefore dd′ is a successful proof-tree-based dispute derivation. From Theorem 2, it follows PAn|∼σ. □

Theorem 5

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|∼σ. Then there is a successful flatten dispute derivation

⟨PS0,PA0,OS0,OA0⟩,…,⟨PSn,PAn,OSn,OAn⟩

for σ such that PAn⊆H.

Proof.

From the completeness Theorem 3, there is a successful tree-based dispute derivation

dd=⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩

such that PAn|∼σ.

It holds that OTn=∅ and all proof trees PTn are full and Ass(PTn)=PAn.

Let dd′=⟨PS0,PA0,OS0,OA0⟩,…,⟨PSn,PAn,OSn,OAn⟩ be the flatten dispute derivation for σ as defined in Lemma 15.

Since all proof trees PTn are full and Ass(PTn)=PAn, it follows PSn=Spm(PTn)−PAn=∅.

Since OTn=∅, OSn=∅. Hence dd′ is successful and PAn|∼σ. □

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 OSi is removed while in our case, all elements of OSi containing the selected assumption are removed, 2) the second and more or less technical point is that while in our case PAi is the set of all proponent assumptions that have been attacked by the opponent, in [15,17] PAi 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].

Notes

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.

2 An extended abstract of this paper has been published in [34].

3 In non-standard ABA frameworks [22], the contrary α‾ 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 δ∈α‾, add a new rule: α′←δ 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.

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

5 See Notations 2 and 1.

6 Hence the height of the root is 0.

7 See Notation 2.

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

9 See also Notation 5.

10 I.e. step (2.b) is selected by the opponent only if it is not possible for the proponent to execute step (1.b) meaning that an opponent proof tree is expanded only if no assumptions appearing in it could be attacked by the proponent.

11 Note that F is finitary.

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

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

14 I.e. Spm(S)=⨁{Spm(T)∣T∈S}.

15 {(2,3),(5,1)} represents the function assigning 3 to 2 and 1 to 5.

16 As H-constrained dispute derivations could be viewed as special form of dispute derivations, the notion of scope in Definition 9 could be applied directly on H-constrained derivations.

Appendices

Appendix

A.1.Multisets

We introduce the basic operations of multisets. More about multisets can be found in [4,11,27].

Intuitively, a multiset is like a set but allowing each element to have many instances.

Formally, a multiset is a pair A=(B,μ) where B is a set referred to as the base set of A, and μ is a function from B into the set of positive integers. The function μ is referred to as the multiplicity function of the multiset A and often denoted by μA.

For simplicity, we often represent a multiset like a set where some element may occur multiple times like the multiset representing the prime factorization of 40 is represented by {2,2,2,5} instead of ({2,5},μ) where μ={(2,3),(5,1)}.15 15

Definition 14.

The union and intersection of two multisets A=(B,μ), A′=(B′,μ′) are defined by:

(1) A⊕A′=(B∪B′,μ+μ′) where for x∈B∪B′, (μ+μ′)(x)=μ(x)+μ′(x).
(2) A∩A′=(B∩B′,μ″) where μ″(x)=min{μ(x),μ′(x)}.

We also introduce two notions of difference and strong difference between multisets and sets in the definition below.

Definition 15.

Let A=(B,μ), A′=(B′,μ′) be multisets and S be a set.

(1) The difference between A, A′ is defined by:
A∖A′=(B″,μ″)
where the following conditions are satisfied:
- (a) B″=(B∖B′)∪{x∈B∩B′∣μ(x)>μ′(x)}.
- (b)
  μ″(x)=μ(x)if x∈B∖B′μ(x)−μ′(x)if x∈B∩B′
- (c) The strong difference between A and S is defined by
  A−S=(B∖S,μ′)
  where for each x∈B∖S, μ′(x)=μ(x).

A.2.Proof of Lemma 5

For T∈Π, define ΠT={T′∈Π∣T⊆T′,ha(T′)⩾ha(T)+1}.

We construct inductively an increasing sequence of proof trees

T0⊂T1⊂⋯⊂Tn⊂⋯

such that for each n⩾0, Tn∈Π and ha(Tn)=n and ΠTn is infinite.

(1) Base Step: We construct T0 and ΠT0.
Let Π0={T∈Π∣ha(T)=0}. It follows ⋃{ΠT∣T∈Π0}=Π∖Π0.
Since the set Π0 is finite and non-empty by the assumptions, it follows that there is T0∈Π0 such that ΠT0 is infinite.
(2) Suppose we have constructed an increasing sequence
T0⊂T1⊂⋯⊂Tn
such that for each 0⩽i⩽n, Ti∈Π and ha(Ti)=i and ΠTi is infinite.
Define X={T∈ΠTn∣ha(T)=n+1}. From the lemma assumptions, X is finite.
- We show that X is non-empty and ⋃{ΠT∣T∈X}⊇ΠTn∖X.
  Since ΠTn is infinite and X is finite, ΠTn∖X≠∅.
  Let T′∈ΠTn∖X. Hence ha(T′)⩾n+2. From the lemma assumptions, there is T∈Π such that ha(T)=n+1 and T⊂T′. Since Tn⊂T′, it follows from T⊂T′ that T, Tn are compatible. From the lemma assumptions, either T⊆Tn or Tn⊆T. Since ha(T)=n+1>n=ha(Tn), it follows Tn⊂T.Thus T∈ΠTn. From ha(T)=n+1, it follows T∈X. Hence X is not empty.
  From T⊂T′, it follows that T′∈ΠT⊆⋃{ΠT∣T∈X}. Thus ΠTn∖X⊆⋃{ΠT∣T∈X}.
- It holds obviously that ⋃{ΠT∣T∈X}⊆ΠTn∖X.
We have proved that ⋃{ΠT∣T∈X}=ΠTn∖X. Thus ⋃{ΠT∣T∈X} is infinite. Since X is finite, there is Tn+1∈X such that ΠTn+1 is infinite and Tn⊂Tn+1.

A.3.Proof of Lemma 6

(1) We prove by induction on n. The statement holds obviously for n=0.
We prove Ass(OTn+1)∩OAn+1=∅ assuming Ass(OTn)∩OAn=∅.
- If the procedure step applied at stage n is (1.a) or (2.a), then Ass(OTn+1)=Ass(OTn) and OAn+1=OAn. The statement holds.
- Suppose the procedure step applied at stage n is (1.b). Then Ass(OTn+1)⊆Ass(OTn)∖{α} and OAn+1=OAn∪{α}. It holds obviously Ass(OTn+1)∩OAn+1⊆Ass(OTn)∩OAn=∅.
- Suppose the procedure step applied at stage n is (2.b). It holds OAn+1=OAn. Let S={exp(T,N,r)∣bd(r)∩OAi=∅}.
  There are two cases:
  - ∗ S=∅. Hence Ass(OTn+1)⊆Ass(OTn). It holds obviously
    Ass(OTn+1)∩OAn+1=∅.
  - ∗ S≠∅. Let T′=exp(T,N,r′)∈S. It follows that Ass(T′)=Ass(T)∪Ass(bd(r′)). Therefore Ass(OTn+1)=Ass(OTn)∪X where
    X=⋃{Ass(bd(r))∣hd(r)=δ,bd(r)∩OAn=∅}.
    
    Thus X∩OAn=∅.
    Hence
    Ass(OTn+1)∩OAn+1=(Ass(OTn)∪X)∩OAn=(Ass(OTn)∩OAn)∪(X∩OAn)=∅.
(2) Let α∈OAn and i be the stage where α is inserted into OAi, i.e. {α}=OAi+1∖OAi. Therefore T0={(root,α‾)}∈PTi+1. Therefore there is a partial proof tree T∈PTn such that T0⊆T. Hence Cl(T)=α‾.
(3) β∈PAn and i be the stage where β is inserted into PAi, i.e. {α}=PAi+1∖PAi. Therefore {(root,β‾})∈OTi+1∖OTi. As β can not be inserted into PAn twice, i is unique.
Let T∈⋃{OTi∣i⩽n} and T0={(root,Cl(T)}. Hence T0⊆T and there is an i such that {T0}=OTi+1∖OTi. Therefore there is an assumption α∈PAi+1∖PAi such that α‾=Cl(T). Since PAi+1⊆PAn, it holds that α∈PAn. The uniqueness of α comes from the one-one property of the contrary mapping.
(4) We prove by induction on i.
It is clear that the statement holds for i=0. Suppose the statement holds for i. We show that it also holds for i+1.
Assume the contrary that there are T,T′∈OTi+1 such that T, T′ are compatible and T≠T′. From the induction hypothesis, it follows that the procedure step applied at stage i in dd can not be (1.a) or (1.b).
- Suppose the procedure step applied at stage i in dd is (2.a). From the induction hypothesis, one of T, T′, say T, is the newly introduced proof tree of the form {(root,α‾)} with {α}=PAi+1∖PAi. Since T′≠T, T′∈OTi. Since T, T′ are compatible, it follows T⊆T′. Hence from two previous statements in this lemma, there is a unique j<i such that {α}=PAj+1∖PAj. Since j<i, j+1⩽i. Thus {α}∈PAi. Contradiction. Hence this case does not happen.
- Suppose the procedure step applied at stage i in dd is (2.b). From the induction hypothesis, one of T, T′, say T, is of the form exp(T1,N,r), T1∈OTi. Therefore T′∈OTi and T′≠T1. Therefore T′, T1 is not compatible. Since T1⊆T, it follows T′∪T is also not compatible. Contradiction. Hence this case can not happen.
Therefore the assumption that T, T′ are compatible and T≠T′ leads to a contradiction, and hence impossible.

A.4.Proof of Lemma 7

(1) We first prove that i=j. Let σ=Cl(T). It follows immediately from Definition 9 that {(root,σ)}∈OTi∖OTi−1 and {(root,σ)}∈OTj∖OTj−1.
From Lemma 6, it follows that there is an assumption α∈PAn such that α‾=σ and α∈PAi+1∖PAi (i.e. α is attacked by the opponent at stage i); and α∈PAj+1∖PAj (i.e. α is attacked by the opponent at stage j).
Since PA0⊆PA1⊆⋯⊆PAn, it follows from the uniqueness of i, j (Lemma 6), that i=j.
We prove by induction that sq=sq′.
Basic Step: The length of sq, sq′ is 1. It is obvious that sq=sq′={(root,σ)}.
Inductive Step: Let sq=T0,…,Tk,Tk+1 and sq′=T0,…,Tk,Tk+1′. Since both Tk+1, Tk+1′ are prefixes of T, they are compatible. Because both Tk+1, Tk+1′ belong to OTi+k, it follows from Lemma 6 (last statement) that they are identical.
(2) We prove by induction on n.
Base Step: n=0. The statement holds obviously.
Inductive Step: Suppose the statement holds for n. We prove that it also holds for n+1. There are two cases:
- T∈OTn. From the induction hypothesis, there is a scope (sq′,i), sq′=T0,…,Tj of T in dd such that with Tj=T and i+j=n. It follows that (sq′.T,i) is also a scope of T in dd
- T∉OTn. Therefore the procedure step applied at stage n is either (2.a) or (2.b).
  - ∗ The procedure step applied at stage n is (2.a).
    Therefore T={(root,α‾)} for α∈PAn+1∖PAn. Then (T,n+1) is a desired scope (of length 1).
  - ∗ The procedure step applied at stage n is (2.b). T is hence an immediate expansion of T′∈OTn. From the induction hypothesis, there is a scope (sq′,i), sq′=T0,…,Tj of T′ in dd such that i+j=n and T′=Tj.
    It is obvious that (sq′.T,i) is a scope of T in dd of length j+1 such that i+j+1=n+1 and T is the last element in sq′.T.
(3) Since T attacks PTn, there is an assumption α∈Ass(PTn) such that Cl(T)=α‾. Since dd is successful, Ass(PTn)=PAn. Lemma 6 implies that there is a unique stage i such that {(root,Cl(T))}∈OTi∖OTi−1. Statement 1 of this lemma implies that there exists a unique maximal scope (sq,i) of T of length k in dd.
We show that (sq,i) is a full scope of T. Let sq=T0,…,Tk−1. Suppose the contrary that (sq,i) is not a full scope of T. Hence there is T′∈OTi+k such that T′ is a prefix of T. From the previous statement of this lemma, there is a scope (sq′,i) of length k+1 of T′ in dd such that T′ is its last element. From the statement 4 in Lemma 6, sq is a prefix of sq′. Hence sq′=sq.T′. Contradiction the assumption that (sq,i) is maximal scope of T in dd.

A.5.Proof of Lemma 12

By induction on i. It is obvious that the lemma holds for i=0. Suppose the lemma holds for i. We prove that it also holds for i+1.

If the stage i in cdd is not step (2.b), the lemma holds obviously.

Suppose stage i in cdd is step (2.b). Let T be the partial proof tree selected at stage i and N be the selected non-final leaf node.

Let S={exp(T,N,r)∣bd(r)∩OAi=∅}

Since F is finitary, S is finite. Since OTi is finite (inductive hypothesis), OTi+1=(OTi∖{T})∪S is finite.

Let T′∈OTi+1. If T′∈OTi then T′ is almost balanced (inductive hypothesis). Let T′∈OTi+1∖OTi. Therefore T′∈S, i.e. T′=exp(T,N,r) for some rule r. Let N′ be a child of N in T′. Therefore h(N′,T′)=h(N,T)+1. It holds: ha(T′)=max{ha(T),h(N′,T′)}=max{ha(T),h(N,T)+1}. From ha(T)⩽hi(T)+1⩽h(N,T)+1, it follows ha(T′)=h(N,T)+1.

There are two cases:

N is the only non-final leaf node of height hi(T) in T. Therefore all non-final leaf nodes of T′ are of the same height. Thus T′ is almost balanced.
N is not the only non-final leaf node of height hi(T) in T. Hence hi(T)=hi(T′). From hi(T)=h(N,T) and ha(T′)=h(N,T)+1, it follows that ha(T′)=hi(T′)+1. T′ is thus most balanced.

A.6.Proof of Lemma 13

Suppose the contrary that there exists an infinite H-constrained dispute derivation

cdd=⟨PT0,PA0,OT0,OA0,λ0⟩,…,⟨PTn,PAn,OTn,OAn,λn⟩for σ.

(1) We show that the set Π=⋃{OTi∣i⩾0} is infinite (i.e. step (2.b) is applied infinitely many times).
Suppose the contrary that the set Π=⋃{OTi∣i⩾0} is finite. Hence there are only finitely many applications of steps (1.b), (2.a) and (2.b) in cdd. Let PIT={{(root,α‾)}∣∃i:α∈OAi}⊆⋃{PTi∣i⩾0}. Thus PIT is finite.
Hence the set {A∈ARH∣∃i,∃T∈PIT:λi(T)=A} is finite. It follows that the number of applications of steps (1.a) is also finite. Thus cdd is finite. Contradiction.
Therefore Π is infinite.
(2) We show that the following conditions are satisfied.
- (a) For all n⩾0, for each T∈Π such that ha(T)>n, there is T′∈Π such that T′⊆T and ha(T′)=n.
  Let T∈OTm. Lemma 7 (second statement) implies that there a scope (sq,i), sq≡T0,T1,…,Tk−1, of T in cdd such that i+k−1=m and Tk−1=T.16 16
  From the definition of scope (Definition 9), it follows immediately that ha(T0)=0 and for each 0⩽i<k−1, ha(Ti+1)⩽ha(Ti)+1. Therefore there is Tj such that ha(Tj)=n.
- (b) For all T,T′∈Π such that T, T′ are compatible, it holds that T⊆T′ or T′⊆T.
  Let n,m⩾0 such that T∈OTn and T′∈OTm.
  If m=n, it follows immediately from Lemma 6 (fourth statement) that T=T′.
  Without loss of generality, let m>n. From Lemma 7 (second statement), there are scopes (sq,i), (sq′,j), sq=T0,…,Tk−1, sq′=T0′,…,Th−1′, of T, T′ respectively such that i+k−1=n and j+h−1=m and Tk−1=T and Th−1′=T′.
  Since Cl(T)=Cl(T′), if follows T0=T0′ and i=j. Further since T, T′ are compatible, Tk−1, Tk−1′ are also compatible. Since Tk−1,Tk−1′∈OTn, Lemma 6 (fourth statement) implies that T=Tk−1=Tk−1′⊆T′.
- (c) For each n⩾0, the set {T∈Π∣ha(T)⩽n} is finite.
  Let Γn={T∈Π∣ha(T)⩽n} and Γn′={T∈Π∣ha(T)=n}
  We prove by induction on n that Γn is finite.
  Base Step: n=0.
  From Γ0⊆{Tα∣α∈H} where Tα={(root,α‾)}, it is clear that Γ0 is finite.
  Inductive Step: We show that Γn+1 is finite assuming that Γn is finite.
  Let Δ be the set of sentences labeling the non-final leaf nodes in proof trees in Γn′ and
  k=max{nδ∣δ∈Δ, and nδ is the number of rules with head δ}m=max{mT∣T∈Γn′ and mT is the number of non-final leaf nodes in T labeled by some sentence from Δ}.
  
  Since the ABA framework F is finitary, k is finite.
  Since for each T∈Γn+1′ there is T′∈Γn′ such that T′⊂T, it holds that |Γn+1′|⩽(k+1)m.|Γn′|.
  From Γn+1=Γn∪Γn+1′, the finiteness of Γn+1 follows from the finiteness of Γn and Γn+1′.
From Lemma 5, there exists increasing sequence T0⊂T1⊂⋯⊂Tk⊂… of almost balanced partial proof trees in Π.
(3) Let T=⋃{Ti∣i⩾0}. From Lemma 4, T is a partial proof tree.
We show that the sequence sq≡T0⊂T1⊂⋯⊂Tk⊂… is fair.
Suppose the contrary that sq is not fair. Hence there is Ti and a non-final leaf node M in Ti such that M is also a non-final leaf node in all Tj, j⩾i.
Let h(M,Ti)=n.
Since sq is strictly increasing, there is Tj, j>i such that ha(Tj)=n+3. Since all trees in sq are almost balanced (Lemma 12), it follows that ha(Tj)<hi(Tj)+1. Since M is a non-final leaf node in Tj, it holds that h(M,Tj)⩾hi(Tj).
Therefore n+3=ha(Tj)<hi(Tj)+1<h(M,Tj)+1=n+1. Contradiction.
We have proved that sq is fair. Therefore T is an argument.
The sequence sq can only be constructed by infinitely many applications of procedure step (2.b). Since step (2.b) is selected only if step (1.b) is not possible, it follows that no assumption appearing in T could be attacked by any argument in ARH. Hence T is an infinite argument attacking H but no argument in ARH attacks T. Contradiction since H is strictly admissible.
Therefore cdd does not exist. The lemma holds.

A.7.Proof of Lemma 14

The proof is by induction on n.

Base Step: n=0. Obvious

Inductive Step. We show that the lemma holds for n+1 assuming that it holds for n.

There are four cases:

(1) The proponent makes a move at stage n according to step (1.a) in Definition 12.
PSn+1∩PAn+1=((PSn∖{δ})⊕(bd(r)∖PAn))∩PAn=((PSn∖{δ})∩PAn)∪((bd(r)∖PAn)∩PAn).

From ((bd(r)∖PAn))∩PAn=∅, and (PSn∖{δ})∩PAn⊆PSn∩PAn=∅, it follows
PSn+1∩PAn+1=∅.

Since OSn+1=OSn and OAn+1=OAn, and OAn∩⨁OSn=∅, it follows
OAn+1∩⨁OSn+1=∅.
(2) The proponent makes a move at stage n according to step (1.b) in Definition 12.
PSn+1∩PAn+1=(PSn⊕{α‾})∩PAn=(PSn∩PAn)∪({α‾}∩PAn)=∅.(⨁OSn+1)∩OAn+1=⨁(OSi∖{S∈OSi∣α∈S})∩(OAi∪{α})=⋃{S∩(OAi∪{α})∣S∈OSi,α∉S}=⋃{S∩OAi∣S∈OSi,α∉S}⊆⋃{S∩OAi∣S∈OSi}=∅.
(3) The opponent makes a move at stage n according to step (2.a) in Definition 12.
From α∈PSn and the induction hypothesis that PSn∩PAn=∅, it follows α∉PAn.
As PSn+1 is obtained from PSn by removing all instances of α, and α∉PAn, it follows
PSn+1∩PAn+1=PSn+1∩(PAn∪{α})=PSn+1∩PAn⊆PSn∩PAn=∅.OAn+1∩⨁OSn+1=OAn∩(⨁(OSn⊕{{α‾}})=(OAn∩⨁OSn)∪({α‾}∩OAn)=∅.
(4) The opponent makes a move at stage n according to step (2.b) in Definition 12.
It is obvious that
PSn+1∩PAn+1=PSn∩PAn=∅.OAn+1∩⨁OSn+1=OAn∩⨁((OSn∖{S})⊕{(S∖{δ})⊕bd(r)∣hd(r)=δ,bd(r)∩OAn=∅})⊆(OAn∩⨁OSn)∪⋃{OAn∩((S∖{δ})⊕bd(r))∣hd(r)=δ,bd(r)∩OAn=∅}=⋃{OAn∩(S⊕bd(r))∣hd(r)=δ,bd(r)∩OAn=∅}=OAn∩S⊆OAn∩⨁OSn=∅.

A.8.Proof of Lemma 15

We prove the lemma by induction on n.

Base Step: n=0. Obvious.

Inductive Step: We prove that the lemma holds for n+1 assuming it holds for n.

There are four cases to consider:

(1) At stage n in dd, step (1.a) is applied. Hence
PTn+1=(PTn∖{T})∪{exp(T,N,r)}
for some proof tree T∈PTn and a non-final leaf node N in T labeled by the head δ of r such that bd(r)∩OAi=∅.
Hence
Spm(PTn+1)=(Spm(PTn∖{T})⊕Spm(exp(T,N,r))=(Spm(PTn)∖Spm(T))⊕Spm(exp(T,N,r)).

From Spm(exp(T,N,r))=(Spm(T)∖{δ})⊕bd(r), it follows
Spm(PTn+1)=(Spm(PTn)∖{δ})⊕bd(r).
Hence
Spm(PTn+1)−PAn+1=(Spm(PTn)∖{δ})⊕bd(r))−PAn+1.

Since PAn+1=PAn, we have
PSn+1=Spm(PTn+1)−PAn+1=(Spm(PTn)∖{δ})⊕bd(r))−PAn=((Spm(PTn)∖{δ})−PAn)⊕(bd(r)−PAn)

Because δ∉PAn, it holds (Spm(PTn)∖{δ})−PAn=(Spm(PTn)−PAn)∖{δ}=PSn∖{δ}.
Since both bd(r) and PAn are sets, it holds bd(r)−PAn=bd(r)∖PAn
Thus
PSn+1=(PSn∖{δ})⊕(bd(r)∖PAn).

Because OTn+1=OTn and PAn+1=PAn, it follows obviously from inductive hypothesis that OSn+1=Spm(OTn+1).
We have proved that ⟨PSn+1,PAn+1,OSn+1,OAn+1⟩ can be obtained from ⟨PSn,PAn,OSn,OAn⟩ by application of step (1.a) of the flatten dispute derivation procedure.
(2) At stage n in dd, step (1.b) is applied. Hence
PTn+1=PTn∪{{(root,α‾)}}andOTn+1=OTn∖{T′∈OTn∣α∈Ass(T′)}.

It follows that
PSn+1=Spm(PTn+1)−PAn+1=(Spm(PTn)⊕Spm({(root,α‾)}))−PAn=PSn∪{α‾}.OSn+1={Spm(T)∣T∈OTn+1}={Spm(T)∣T∈OTn,α∉Ass(T)}={Spm(T)∣T∈OTn}∖{Spm(T′)∣T′∈OTn,α∈Ass(T′)}=OSn∖{S∣S∈OSn,α∈S}.

We have proved that ⟨PSn+1,PAn+1,OSn+1,OAn+1⟩ can be obtained from ⟨PSn,PAn,OSn,OAn⟩ by application of step (1.b) of the flatten dispute derivation procedure.
(3) At stage n in dd, step (2.a) is applied. Hence
PTn+1=PTnandOTn+1=OTn∪{{(root,α‾)}}.

From PAn+1=PAn∪{α}, it follows that
PSn+1=Spm(PTn+1)−PAn+1=(Spm(PTn)−PAn)−{α}=PSn−{α}.

It follows that
OSn+1={Spm(T)∣T∈OTn+1}={Spm(T)∣T∈OTn}⊕{Spm({(root,α‾)})}=OSn⊕{{α‾}}.

We have proved that ⟨PSn+1,PAn+1,OSn+1,OAn+1⟩ can be obtained from ⟨PSn,PAn,OSn,OAn⟩ by application of step (2.a) of the flatten dispute derivation procedure.
(4) At stage n in dd, step (2.b) is applied. Hence
PTn+1=PTn,PAn+1=PAnandOTn+1=(OTn∖{T})∪{exp(T,N,r)∣bd(r)∩OAn=∅}

Therefore it is obvious that PSn+1=PSn.
{Spm(T′)∣T′∈OTi+1}={Spm(T′)∣T′∈OTi,T′≠T})⊕{Spm(exp(T,N,r))∣bd(r)∩OAn=∅}.

Let S=Spm(T) and δ be the sentence labeling N in T. Hence
Spm(exp(T,N,r))=(S∖{δ})⊕bd(r)OSn+1={Spm(T′)∣T′∈OTn+1}={Spm(T′)∣T′∈OTn,T′≠T})⊕{Spm(exp(T,N,r))∣bd(r)∩OAn=∅}=(OSn∖{S})⊕{(S∖{δ})⊕bd(r)∣bd(r)∩OAn=∅}

We have proved that ⟨PSn+1,PAn+1,OSn+1,OAn+1⟩ can be obtained from ⟨PSn,PAn,OSn,OAn⟩ by application of step (2.b) of the flatten dispute derivation procedure.

A.9.Proof of Lemma 16

We prove the lemma by induction on n.

Base Step: n=0. Obvious.

Inductive Step: We prove that the lemma holds for n+1 assuming it holds for n.

There are four cases to consider:

(1) At stage n in dd, step (1.a) is applied.
Let PTn+1=(PTn∖{T})∪{exp(T,N,r)} and OTn+1=OTn.
From the induction hypothesis, it is obvious that
⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩,⟨PTn+1,PAn+1,OTn+1,OAn+1⟩
is a tree-based dispute derivation.
- (a) Let δ∈PSn be the selected non-assumption sentence. From the inductive hypothesis, there is a tree T∈PTn such that δ∈Spm(T).
  It holds:
  Spm(PTn+1)=(Spm(PTn)∖Spm(T))⊕Spm(exp(T,N,r))
  
  From Spm(exp(T,N,r))=Spm(T)∖{δ}⊕bd(r), it follows
  Spm(PTn+1)=(Spm(PTn)∖Spm(T))⊕Spm(exp(T,N,r))=((Spm(PTn)∖Spm(T))⊕(Spm(T)∖{δ})⊕bd(r))=(Spm(PTn)∖{δ})⊕bd(r).
  
  Since PAn+1=PAn, we have
  Spm(PTn+1)−PAn+1=((Spm(PTn)∖{δ})⊕bd(r))−PAn=(Spm(PTn)∖{δ})−PAn)⊕(bd(r)−PAn)=(PSn∖{δ})⊕(bd(r)−PAn)=(PSn∖{δ})⊕(bd(r)∖PAn)=PSn+1
  
  We have proved PSn+1=Spm(PTn+1)−PAn+1.
  Since δ is not an assumption, from PTn+1=(PTn∖{T})∪{exp(T,N,r)}, it follows Ass(PTn+1)=Ass(PTn)∪Ass(bd(r)). From PAn⊆Ass(PTn) (induction hypothesis) and PAn+1=PAn, it holds: PAn+1⊆Ass(PTn+1).
- (b) Because OSn+1=OSn, OTn+1=OTn and OSn={Spm(T)∣T∈OTn} (induction hypothesis), it follows OSn+1={Spm(T)∣T∈OTn+1}.
(2) At stage n in dd, step (1.b) is applied. Let α∈S, S∈OSn, be the selected assumption to be attacked.
From the inductive hypothesis, PSn=Spm(PTn)−PAn.
Let PTn+1=PTn∪{{(root,α‾)}}, and OTn+1=OTn∖{T′∈OTn∣α∈Ass(T′)}. Therefore
⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩,⟨PTn+1,PAn+1,OTn+1,OAn+1⟩
is a tree-based dispute derivation.
- (a) From PAn+1=PAn, it holds:
  Spm(PTn+1)−PAn+1=(Spm(PTn)⊕Spm({(root,α‾)})−PAn=(Spm(PTn)⊕{α‾})−PAn=(Spm(PTn)−PAn)⊕{α‾}=PSn⊕{α‾}=PSn+1.
  
  We have proved that PSn+1=Spm(PTn+1)−PAn+1.
  Since PAn+1=PAn and PTn⊂PTn+1, it holds obviously PAn+1⊆Spm(PTn+1).
- (b) Since OSn={Spm(T)∣T∈OTn} (inductive hypothesis), there is a tree T′∈OTn such that S=Spm(T′).
  It holds:
  {Spm(T)∣T∈OTn+1}={Spm(T)∣T∈OTn}∖{Spm(T′)∣T′∈OTn,α∈Ass(T′)}=OSn∖{S∣S∈OSn,α∈S}=OSn+1.
  
  We have proved that OSn+1={Spm(T)∣T∈OTn+1}.
(3) At stage n in dd, step (2.a) is applied.
Let PTn+1=PTn, and OTn+1=OTn∪{{(root,α‾)}}. Therefore from the induction hypothesis,
⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩,⟨PTn+1,PAn+1,OTn+1,OAn+1⟩
is a tree-based dispute derivation.
- (a) It holds:
  Spm(PTn+1)−PAn+1=Spm(PTn)−(PAn∪{α})=(Spm(PTn)−PAn)−{α}=PSn−{α}=PSn+1.
  
  We have proved that PSn+1=Spm(PTn+1)−PAn+1.
  From α∈PSn⊆Spm(PTn), it follows α∈Ass(PTn).
  From PAn⊆Ass(PTn)=Ass(PTn+1) and PAn+1=PAn∪{α} and α∈Ass(PTn), it follows PAn+1=PAn∪{α}⊆Ass(PTn+1).
- (b) It holds that
  {Spm(T)∣T∈OTn+1}={Spm(T)∣T∈OTn}⊕{Spm({(root,α‾)})}=OSn⊕{{α‾}}=OSn+1.
  
  We have proved that OSn+1={Spm(T)∣T∈OTn+1}.
(4) At stage n in dd, step (2.b) is applied.
Let δ∈S, S∈OSn, be the selected non-assumption sentence. From the inductive hypothesis, there is a tree T∈OTn such that S=Spm(T).
Let PTn+1=PTn and OTn+1=(OTn∖{T})∪{exp(T,N,r)∣bd(r)∩OAn=∅}.
Therefore ⟨PT0,PA0,OT0,OA0⟩,…,⟨PTn,PAn,OTn,OAn⟩, ⟨PTn+1,PAn+1,OTn+1,OAn+1⟩ is a tree-based dispute derivation.
- (a) Because PAn+1=PAn, PSn+1=PSn and PSn=Spm(PTn)−PAn (induction hypothesis), it follows immediately that PSn+1=Spm(PTn+1)−PAn+1.
  Since PTn+1=PTn and PAn+1=PAn and PAn⊆Ass(PTn), it holds PAn+1⊆Ass(PTn+1).
- (b) Because Spm(T)=S, it follows that Spm(exp(T,N,r))=(S∖{δ})⊕bd(r) where δ labels N and hd(r)=δ
  It holds
  {Spm(T′)∣T′∈OTn+1}=({Spm(T′)∣T′∈OTn}∖{Spm(T)})⊕{Spm(exp(T,N,r))∣bd(r)∩OAn=∅}=(OSn∖{S})⊕{S∖{δ}⊕bd(r)∣bd(r)∩OAn=∅}=OSn+1
  
  We have proved that OSn+1={Spm(T′)∣T′∈OTn+1}.

References

[1]	O. Arieli and C. 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.
[2]	P. Baroni, F. Cerutti, M. Giacomin and G. Simari (eds), Proceedings of Conference on Computational Models of Arguments, IOS Press, (2010) .
[3]	P. Besnard, S. Doutre and A. Hunter (eds), Proceedings of Conference on Computational Models of Arguments Computational Models of Arguments, IOS Press, (2008) .
[4]	W.D. Blizard, Multiset theory, Notre Dame Journal of Formal Logic 30: (1) ((1988) ), 36–66. doi:10.1305/ndjfl/1093634995.
[5]	A. Bondarenko, P.M. Dung, R.A. Kowalski and F. Toni, An abstract, argumentation-theoretic approach to default reasoning, Artif. Intell. 93: ((1997) ), 63–101. doi:10.1016/S0004-3702(97)00015-5.
[6]	M. Caminada and L. Amgoud, On the evaluation of argumentation formalisms, Artificial Intelligence 171: ((2007) ), 286–310. doi:10.1016/j.artint.2007.02.003.
[7]	C. Cayrol, S. Doutre and J. 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.
[8]	R. Craven and F. Toni, Argument graphs and assumption-based argumentation, Artificial Intelligence 233: ((2016) ), 1–59. doi:10.1016/j.artint.2015.12.004.
[9]	B.A. Davey and H.A. Priestley, Introduction to Lattices and Order, Cambridge University Press, (2002) .
[10]	M. Denecker and E. Ternovska, A logic of nonmonotone inductive definitions, ACM Trans. Comput. Logic 9: (2) ((2008) ). doi:10.1145/1342991.1342998.
[11]	N. Dershowitz and Z. 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 F. 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 F. Toni, Assumption-based argumentation, in: Argumentation in AI, Springer-Verlag, (2009) .
[17]	P.M. Dung, P. Mancarella and F. 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 T. 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]	K. 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]	D. Gaertner and F. 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]	G. Governatori, M.J. Maher, G. Antoniou and D. 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]	Z. Manna and R. Waldinger, The Logical Basis for Computer Programming, Addison-Wesley Professional, (1985) .
[28]	S. Modgil and M. Caminada, Proof theories and algorithms for abstract argumentation frameworks, in: Argumentation in AI, Springer Verlag, (2009) .
[29]	S. Modgil and H. 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]	D. 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]	I. Rahwan and G. Simari (eds), Handbook of Argumentation in AI, Springer Verlag, (2009) .
[33]	C. 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]	F. 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]	F. Toni, A tutorial on assumption-based argumentation, Journal of Arguments and Computation ((2013) ).
[37]	B. Verheij, A labeling approach to the computation of credulous acceptance in argumentation, in: JCAI 2007, M. Veloso, ed., Morgan Kaufmann, (2007) , pp. 623–628.
[38]	B. Verheij, S. Szeider and S. Woltran (eds), Proceedings of Conference on Computational Models of Arguments, IOS Press, (2012) .
[39]	G. Vreeswijk and H. Prakken, Credulous and sceptical argument games for preferred semantics, in: JELIA 2000, M. Ojeda-Aciego, I.P. de Guzmán, G. Brewka and L.M. Pereira, eds, Lecture Notes in Computer Science, Vol. 1919: , Springer, (2000) , pp. 239–253.