A Unified Framework for Representation and Development of Dialectical Proof Procedures in Argumentation

1 Introduction

Argumentation is a form of reasoning, that could be viewed as a dispute resolution, in which the participants present their arguments to establish, defend or attack certain propositions.

The probably most abstract among the well-known formalisms for argumentation is the abstract argumentation framework [Dung, 1995b] (or abstract argumentation for short) consisting simply of a set of "atomic" arguments together with a binary relation representing attack relation between them. There is extensive research on dialectical proof procedures for abstract argumentation [Cayrol,Doutre,Mengin, 2003; Dunne,Bench-Capon, 2003; Modgil,Caminada, 2009; Vreeswijk,Prakken, 2000; Jakobovits,Vermeir, 1999; Vreeswijk, 2006; Verheij, 2007]. Though clearly related, their formal and precise relationship remains unexplored. We address this problem by providing an unified framework for representing dialectical proof procedures based on the notions of legal enviroments and dispute derivation trees. A key insight of this paper is that the opponent moves determine the soundness of a dispute while the completeness depends on the proponent moves.

2 Abstract Argumentation: Preliminaries

An abstract argumentation framework [Dung, 1995b] is a pair AF = (A, att ), where A is a set of arguments, and att is a binary relation over A representing the attack relation between the arguments (att ⊆ A × A) with (A, B) ∈ att meaning A attacks B. For simplicity, we restrict ourself on frameworks with finite sets of arguments. A set S of arguments attacks an argument A if some argument in S attacks A; S attacks another set S ′ if S attacks some argument in S ′ .

A set S of arguments is conflict-free iff it does not attack itself. Argument A is acceptable with respect to S iff S attacks each argument attacking A. S is admissible iff S is conflictfree and each argument in S is acceptable with respect to S. S is a preferred extension iff S is maximally (wrt set inclusion) admissible.

The semantics of argumentation could also be characterized by a fixpoint theory of the characteristic function F(S) = {A ∈ A | A is acceptable wrt S}. It is easy to see that S is admissible iff S is conflict free and S ⊆ F(S). As F is monotonic , it follows that S is a preferred extension iff S is a maximal fixpoint of F. The least fixed point of F is defined as the grounded extension.

An argument A is said to be credulously accepted iff it is contained in at least one preferred extension and groundedly accepted iff it is contained in the grounded extension.

Given an argument B ∈ A, AttackB and AttackedB denote the set of arguments attacking B, i.e. AttackB = {A | (A,B) ∈ att}, and attacked by B, i.e. AttackedB = {A | (B, A) ∈ att}.

3 Dispute derivations

In a dispute, the proponent starts by putting forward an initial argument and then the proponent and opponent alternate in attacking each other's previous arguments. The proponent wins if the opponent runs out of arguments to make a move. A dispute is represented by a dispute derivation in which dispute derivation trees are successively constructed by expanding the previous one by adding children to some frontier (or leaf) nodes following some legal move functions for the dispute parties. The initial partial derivation tree consists of only the root.

Definition 3.1 A dispute derivation tree (or simply derivation tree for short) T for an argument A is defined as follows:

1. Every node of T is labeled by an argument and is assigned the status of proponent node or opponent node, but not both. The status of a child node is different from that of its parent. Arguments labeling children nodes attack arguments labeling their parent node.
2. The root is a proponent node labeled by A.

For example, various derivation trees are given in figure 1. Abusing the notation, for a node N labeled by A, we often refer to AttackA by AttackN .

In the following, we introduce the notion of legal environments generalizing the well-known notions of legal move functions in the literature.

Definition 3.2 · A partial function F is called a proponent (resp opponent) legal move function if F assigns to pairs (N, T) of a frontier opponent (resp. proponent) node N in a derivation tree T an argument in (resp. a subset of) AttackN. If F(N, T) is not defined, we write F (N, T ) = ⊥.

• A pair of proponent and opponent legal move functions Φ = (ΦP , ΦO) is called a legal environment.

Examples of legal move functions are given in figure 1. For simplicity, if it is clear from context, we often write Φ(N, T ) for ΦP (N, T) if N is a opponent node, and for ΦO(N, T) if N is an proponent node. We often refer to the leaf nodes in a derivation tree as frontier nodes to indicate that they are the ones to be expanded later.

Definition 3.3 Given a legal environment Φ = (ΦP ,ΦO) and derivation trees T, T ′ . We say that T ′ is obtained from T by expansion of a frontier (leaf) node N in T wrt Φ if Φ(N, T ) is defined and following condition holds:

• If N is an opponent node then a child node labeled by an argument selected in ΦP (N, T ) is added to N
• If N is proponent node then a set of child nodes labeled by arguments in ΦO(N, T ) are added to N. There is oneone correspondence between the children nodes of N and the arguments in ΦO(N, T )

In our model of dispute, when the opponent moves against a proponent argument, he delivers all attacks that are legal at once. This assumption simplifies the formal framework without affecting its generality. We discuss alternative strategies later.

Definition 3.4 · A dispute derivation wrt legal environment Φ = (ΦP , ΦO) is a sequence T0, ..., Ti, ..., Tn of derivation trees where T0 consists of a single node and Ti+1 is obtained from Ti by expansion of a frontier node N in Ti.

• A dispute derivation T0, . . . , Tn terminates if for each frontier node N of the final tree Tn, Φ(N, Tn) = ∅
• A terminating dispute derivation is said to be successful if all the frontier nodes of the final tree are proponent nodes.

The sequence T0, T1, T2 in figure 1 is an example of a successful dispute derivation.

For a derivation tree T, PRO(T), OPP(T) denote respectively the sets of arguments labeling the proponent or opponent nodes in T. Arguments in PRO(T) or OPP(T) are often called respectively proponent or opponent arguments.

Definition 3.5 1. A derivation tree T is consistent if there is no argument labeling both a proponent node and an opponent node.

1. A derivation tree is successful wrt legal environment Φ if it is the final tree of a successful dispute derivation wrt Φ.

Consider a frontier proponent node N in a derivation tree T such that AttackN ∩ PRO(T) ̸= ∅. This implies immediately that the set of proponent arguments is not conflictfree as one of them attacks the argument labeling N. We certainly do not want to expand T at this node, i.e. ΦO(N, T) should not be defined. Further in general, we want to consider only those legal environments guaranteeing that an expansion of consistent derivation trees leads to consistent ones. This requirement imposes that for frontier opponent node N, ΦP (N, T ) ∩ OP P (T ) = ∅.

Definition 3.6 · A legal environment Φ is eligible iff following conditions are satisfied:

1. For each derivation tree T, and each frontier proponent node N of T, ΦO(N, T ) = ⊥ if AttackN ∩ PRO(T) ̸= ∅.
2. If N is an opponent node then ΦP (N, T) ⊆ AttackN \ OP P (T )
3. An eligible legal environment is said to be fully defined if the "if" in the condition (1) above is replaced by "iff".

Examples of eligible legal environments are given in figure 2.

It is not difficult to show that the eligibility of legal environment guarantees that only consistent derivation trees are generated in a dispute derivation.

Lemma 3.1 Let Φ = (ΦP , ΦO) be an eligible legal environment and T0, . . . , Tn be a dispute derivation wrt Φ. Then for each i, Ti is consistent.

Proof By induction and left to the readers. □

Definition 3.7 Let Φ be a legal environment.

1. Φ is said to be credulously (resp. groundedly) sound if the sets of proponent arguments of the successful derivation trees wrt Φ are admissible (resp. admissible subsets of the grounded extension).
2. Φ is said to be credulously (resp. groundedly) complete if for each credulously (resp. groundedly ) accepted argument there is a successful derivation tree wrt Φ whose initial argument is A.
3. Φ is said to be terminating if there exists no infinite dispute derivation wrt Φ.

4 Legal Environments for Credulous Semantics

To ensure admissibility of proponent arguments, the legal environment should guarantee that all possible attacks against proponent arguments are accounted for. This is the case if for each proponent node N, ΦO(N, T ) = AttackN . But if some arguments in AttackN have been defeated by the proponent arguments then deploying them will not help the opponent winning the case. The opponent also does not need to deploy arguments already deployed by itself in previous steps. This insight is formalized in the following theorem in which a general class of credulously sound legal environments is introduced.

Theorem 4.1 Let Φ = (ΦP ,ΦO) be an eligible legal environment such that for each derivation tree T, each proponent node N in T

whenever ΦO(N, T ) is defined.

Then Φ is credulously sound .

Proof Let T0, . . . , Tn be a successful derivation wrt Φ. First we want to show that PRO(Tn) counterattacks every attack against it. Let A be an argument attacking an argument B ∈ PRO(Tn). Let N be a proponent node labelled by B. There are two cases:

1. N is a leaf node in Tn. Hence ΦO(N, Tn) = ∅. From AttackN \ (AttackedPRO(T) ∪ OPP(Tn)) ⊆ ΦO(N, Tn), it follows AttackN \ (AttackedPRO(Tn)∪ OPP(T)) = ∅, i.e. AttackN ⊆ (AttackedPRO(Tn) ∪ OPP(Tn)) . Hence A ∈ (AttackedPRO(Tn) ∪ OPP(Tn)) . As all leaf nodes in Tn are proponent nodes, it follows that OPP(Tn) ⊆ AttackedPRO(Tn). A is hence attacked by PRO(Tn).
2. N is an internal node N in Tn. Let Ti be the tree at which the opponent attacks N and expands Ti into Ti+1. If A ∈ ΦO(N, Ti) then A labels one of the opponent child of N. As Tn is a successful tree, A has a proponent child in Tn. Hence A is attacked by PRO(Tn). If A ̸∈ ΦO(N, Ti), then A ∈ (AttackedPRO(Tn) ∪ OPP(Tn)). As each opponent node in Tn has a proponent child, it follows that A is attacked by PRO(Tn).

It remains to show that PRO(Tn) is conflict-free. Suppose PRO(Tn) is not conflict-free. An argument A ∈ PRO(Tn) is said to be controversial if A attacks or is attacked by some argument in PRO(Tn). Hence the set of controversial arguments in PRO(Tn) is not empty.

We first show that no such argument labels a leaf node in Tn. Suppose the contrary that a controversial argument A labels a leaf node N in Tn. As PRO(Tn) counterattacks every attack against it, it follows that there is some proponent argument in Tn attacking A. Hence AttackN ∩ PRO(Tn) ̸= ∅. Therefore ΦO(N, Tn) = ⊥ contradiction to the successfulness of Tn.

Therefore every controversial argument labels an internal node in Tn. Let m be the maximum number such that Tm is expanded at a proponent node N (by the opponent) labelled by controversial argument A. Further let B ∈ PRO(Tn) such that B attacks A. From the definition of m, it follows that B labels a proponent node in Tm. Hence AttackN∩PRO(Tm) ̸= ∅. Therefore ΦO(N, Tn) = ⊥ contradiction to the successfulness of Tn.

Therefore the set of controversial arguments is empty. Contradiction. Hence PRO(Tn) is conflict-free.

□

Theorem 4.1 states formally that the soundness of a legal environment will not be affected if filtering mechanisms are deployed to filter out some or all arguments in AttackedPRO(T) ∪ OPP(T). An important insight gained from this theorem is that the soundness of a legal environment depends only on the legal moves of the opponent. The following theorem shows that the legal moves of the proponent determine the completeness.

Theorem 4.2 Let Φ = (ΦP , ΦO) be an eligible, credulously sound and terminating legal environment. Further suppose that Φ is fully defined and for each derivation tree T, each opponent node N in T

where Conf(T) consists of all self-attacking arguments and all arguments attacking or being attacked by arguments in P RO(T ).

Then Φ is credulously complete.

Proof Let A be a credulously accepted argument and S be an admissible set of arguments and A ∈ S. We construct by induction on i a successful derivation T0, . . . , Ti, . . . , Tn such that A labels the root of the trees and PRO(Ti) ⊆ S.

If Ti is successful then we are done, the theorem is proved. Suppose now that Ti is not successful. Select a frontier node N of Ti.

Suppose N is a opponent node. Then from the admissibility of S and PRO(Ti) ⊆ S, it follows that AttackN ∩ S ̸= ∅. Because S is conflict-free and PRO(Ti) ⊆ S, it follows that S ∩Conf(Ti) = ∅. Therefore (AttackN \Conf(Ti))∩S ̸= ∅. Hence there is an argument B ∈ S ∩ ΦP (N, Ti). Select B and expand Ti by adding a child to N labelled by B.

Suppose N is a proponent node. As the argument labelling N belongs to S and S is admisisble and PRO(Ti) ⊆ S, it follows that AttackN ∩ PRO(Ti) = ∅. Sinc Φ is fully defined, it follows that ΦO(N, Ti) ̸= ⊥. If ΦO(N, Ti) ̸= ∅ then expand Ti at N.

As Φ is terminating, the process must stop sometimes. It follows that all the frontier nodes are proponent nodes. The theorem is proved.□

The following theorem shows that one can guarantee the termination of dispute by not allowing the opponent to repeat his moves.

Theorem 4.3 Let Φ = (ΦP ,ΦO) be an eligible legal environment such that

where AOPP(N, T) contains all arguments labeling opponent nodes on the path from the root to N.

Then Φ is terminating.

Proof Suppose Φ is not terminating and ΦO(N, T) ⊆ AttackN \ AOPP(N, T). Let T0, . . . , Ti, . . . be a nonterminating derivation. Let T be the limit of this sequence of trees. T is hence infinite. There is then an infinite path in T. There are hence infinite opponent nodes on this path. Since the set of arguments is finite, there are many opponent nodes labelled by the same argument. Contradition.□

As we have discussed, a key insight of theorems 4.1, 4.2 is that the credulous soundness of a legal environment is determined by opponent legal moves while its completeness depends on the legal moves of the proponent. This insight is best illustrated by the special case where ΦO(N, T) = AttackN whenever it is defined. It turns out that in this case, the legal environment is even groundedly sound.

Lemma 4.1 Let Φ be an eligible legal environment such that ΦO(N, T ) = AttackN whenever ΦO(N, T ) is defined. Then Φ is groundedly sound.

Proof Let Φ′ be a legal environment such that Φ′O (N, T) = AttackN whenever it is defined and Φ′P (N, T ) = AttackN \ OPP(T). It is easy to see that each successful derivationwrt Φ is a successful derivation wrt Φ′ . Let T be a successful derivation tree wrt Φ′ . It is easy to show by induction on the hight of T that PRO(T) is a subset of the grounded extension. □

5 Legal Environments for Grounded Semantics

We are now turning our attention to legal environments for grounded semantics. Lemma 4.1 points out that the opponent could do nothing wrong if he/she keeps bringing up all possible counter-evidences to whatever the proponent says. The legal environment is groundedly sound independent of whatever the proponent does. The best the proponent could do in such cases is to make sure that it can win if the initial argument is groundedly accepted, i.e. to ensure that its legal move function guarantees completeness. This is the case if ΦP(N.T) = AttackN \ OPP(T). But this environment is not terminating. It turns out that to ensure both termination and completeness, the proponent should not repeat arguments put forward by itself previously. Though the legal environment just described is groundedly sound, complete and terminating, it could be quite inefficient as the opponent could repeat many arguments that have been defeated before as the following example illustrates.

Consider the derivation tree T in figure 3. It would be wasteful if argument D at node N should be defeated again. We hence expect from an efficient legal environment that ΦO(N, T) = ∅. But in contrast to the credulous case, not all previous opponent arguments could be filtered out as illustrated by derivation tree T' in figure 3. If the opponent argument B is filtered out at N i.e. ΦO(N, T) = ∅ then T ′ would be a successful derivation tree though A is not groundedly accepted.

The examples suggest that we should allow the opponent to filter out previous opponent arguments except those lying on the path from the root to the considered node, i.e. AttackN \ (OPP(T) \ AOPP(N, T) ) ⊆ ΦO(N, T). Unfortunately, this constraint is not strong enough to guarantee the grounded soundness of the legal environment as the following example shows:

Note that when an argument labels exactly one node in a derivation tree, we identify the argument and the node for simplicity.

In figure 4, AOPP(E, T) = {B},AttackE = {C},OPP(T) = {B,C}. Hence AttackE \ (OPP(T) \ AOPP(E, T)) = ∅. AOPP(D, T) = {C},AttackD = {B}. Hence AttackD \ (OPP(T) \ AOPP(D, T)) = ∅. Hence ΦO(E, T ) = ΦO(D, T ) = ∅ satisfies the constraint. T would be a successful derivation tree though A is not groundedly accepted. The reason is that B,E,C,D,B is a cycle in the argumentation framework and this cycle makes the filtering of B,C groundedly unsound. It turns out filtering is groundedly sound if it avoids filtering out previous opponent arguments lying in cycles like B, E, C, D, B. This motivates the following definition.

Definition 5.1 Let T be a derivation tree.

1. Let N be a proponent node and M be an opponent node and A be the argument of M. M is an adopted child of N in T if A attacks the argument of N and N has no child labelled by A 1 .
2. A generalized path in T is a sequence of nodes N0, . . . ,Nk, k ≥ 1 such that Ni+1 is either a child or an adopted child of Ni.

A generalized path is a cycle if the first and last nodes coincide.

In figure 3, E is an adopted child of N in T and the sequence B,N,E is a generalized path. B,A,B is a cycle in T ′ while T contains no cycle. In figure 4, the sequence B,E,C,D,B is a cycle in T.

Definition 5.2 Let N be a frontier proponent node in T, and A be an argument attacking N. A is said to be a taboo for filtering out by opponent at N if there is an cycle N0, . . . , Nn in T such that N = Ni and A labels Ni+1 for some i.

The set of taboos for filtering out at N by opponent in T is denoted by TABOO(N,T).

In figure 3, TABOO(N, T) = ∅. Hence it is possible to filter out the argument E attacking D at node N. In contrast, TABOO(N, T ′ ) = {B}. Hence it is not possible to filter out B at N. T ′ is hence not a successful derivation tree while T is. Similarly, in figure 4, TABOO(E, T) = {C}, T ABOO(D, T ) = {B}.

Theorem 5.1 Let Φ = (ΦP ,ΦO) be an eligible legal environment such that for each derivation tree T, each frontier proponent node N labeled by A,

whenever ΦO(N, T ) is defined.

Then Φ is groundedly sound.

Proof Let T0, . . . , Tn be a successful dispute derivation wrt Φ. A cycle is said to be internal if it does not contain any frontier node. We prove by induction that for each i,there is no internal cycle in Ti.

Suppose that there is no internal cycle in Ti but some internal cycles in Ti+1. Let Cyc = N0, . . . ,Nn be an internal cycle in Ti+1 labelled by A0, . . . , An. As there is no internal cycle in Ti, Cyc must contain a frontier node in Ti. Since Cyc is an internal cycle in Ti+1, Cyc contains exactly one frontier node in Ti that is the frontier node N at which Ti is expanded. Let N = Nk. If N is an opponent node in Ti then Nk+1 is a child of N. Hence Nk+1 is a frontier node of Ti+1. Contradiction to the assumption that Cyc is an internal cycle in Ti+1.

Hence N must be a proponent node in Ti. As Cyc is an internal cycle, Nk+1 is not a frontier node in Ti+1. Hence Nk+1 is an adopted child of N in Ti and Ti+1. From definition 5.2, it follows that Ak+1 ∈ TABOO(N, Ti).

1 Note that we do not define adopted children for opponent nodes

As Nk+1 is an adopted child of N also in Ti+1, there is no child of N in Ti+1 labelled by Ai+1. It follows Ai+1 ̸∈ ΦO(N, Ti). From the properties of Φ, it follows that Ai+1 ̸∈ AttackN \ (OPP(Ti) \ TABOO(N, Ti) ). Therefore Ai+1 ∈ (OPP(T) \ TABOO(N, Ti) ). Hence Ai+1 ̸∈ TABOO(N, Ti). Contradiction.

We prove now that there is no cycle in Tn. Suppose that there is a cycle Cyc in Tn. As Tn has no internal cycle, Cyc must contains a frontier node, say N. Therefore TABOO(N, Tn) ̸= ∅. Hence ΦO(N, Tn) ̸= ∅. Contradiction.

We prove now that for all nodes M in Tn, if M is a proponent (resp opponent) node then the argument labelling M is groundedly accepted (resp rejected, i.e. attacked by a groundedly accepted argument). The proof is by induction on the rank of the nodes in Tn defined as follows..

The rank of nodes without any kind of children is 0. The rank of a node M is equal 1 plus the maximum of the ranks of the children or adopted children of M.

We show by induction that the nodes of even (resp odd) ranks are proponent (resp. opponent) nodes. Obviously that nodes of rank 0 are proponent nodes. Suppose now that the property holds for all nodes of rank ≤ i. Let M be a node of rank i + 1. As one of the children or adopted children of M is of rank i, M is a proponent (resp opponent) node if i is odd (resp even) from the induction hypothesis.

We could easily prove by induction now that nodes of even (resp odd) ranks are groundedly accepted (resp rejected) based on the following property:

Let N be proponent node in Tn. Then AttackN = {A | A labels a child or an adopted child of N}.

Let Ti be the tree at which N is selected for expansion. Suppose A is an argument attacking N and A does not label a child of N. Hence A ̸∈ ΦO(N, Ti). Therefore A ∈ (OPP(Ti) \ TABOO(N, Ti)). Hence there is an opponent node M in Ti labeled by A. As A does not label a child of N, M is an adopted child of N. □

Theorem 5.2 Let Φ = (ΦP , ΦO) be an eligible and groundedly sound legal environment such that for each derivation tree T, each frontier opponent node N in T

where APRO(N, T ) contains all proponent arguments lying on the path from the root to N.

Then Φ is groundedly complete and terminating

Proof For groundedly accepted (resp rejected) argument A, define rank(A) to be the smallest number i such that A ∈ F i (∅) (resp. A is attacked by F i (∅)). We prove the theorem by induction on rank(A).

Let A be a groundedly accepted argument. A successful derivation T0, . . . , Tn of A is constructed by induction as follows:

If Tk is obtained from Tk-1 by expanding an opponent node then select an argument belonging to F j (∅) where j is the rank of the argument labelling the node that is expanded.

It is not difficult to see that constructing Ti's that way will produce a successful derivation wrt Φ. □

6 Discussion and Conclusion

In [Cayrol,Doutre,Mengin, 2003], two proof procedures called φ1, φ2 are given for credulous semantics. φ1 corresponds to a sequentialization of a legal environment with Φ1,O(N, T) = AttackN \ (AttackedPRO(T) ∪ OPP(T)) and Φ1,P(N, T) = AttackN \ Conf(T). φ2 corresponds to Φ2,O(N, T) = AttackN \ AttackedAPRO(N,T) and Φ2,P(N, T) = AttackN \ Conf(N, T)2 . [Modgil,Caminada, 2009] gives also several proof procedures for credulous semantics. They are somewhat similar to the φ2 procedure above. For example, one of them corresponds to the legal environment: Φ3,O(N, T) = AttackN \ AOP P (N, T ) and Φ3,P (N, T ) = AttackN \ Conf (N, T ). While φ1 is sound, complete and terminating, φ2, Φ3 may not be eligible and hence are sound only if their successful derivation trees are consistent. But no condition is given under what conditions is the consistency of the successful derivation trees is guaranteed. [Modgil,Caminada, 2009] gives also proof procedures for grounded semantics. The basic one corresponds to the sound and complete and terminating legal environment: ΦO(N, T) = AttackN and ΦP(N, T) = AttackN \ APRO(N, T ).

In general, the opponent does not need to unleash all of his attacks at once. By dropping the "one-one-correspodence" condition in the second bullet of the definition 3.3 and requires an extra condition in theorem 4.1 and 5.1 that ΦO(N, T ) does not contain any arguments labelling children of N and allowing the opponent to attack at all proponent nodes as long as there is an option for him there, we obtain new dispute procedures with the same characteristics.

A possible application of the insight that the soundness of a dispute is determined by the opponent moves while its completeness by the proponent ones, is a modular methodology for designing dispute procedures. The design consists of four tasks: ensuring the eligibility of the legal environment, ensuring the soundness by looking at opponent moves and guaranteeing completeness by looking at proponent moves and enforcing terminating by forbidding one of the participant not to repeat his moves.

A possible interesting application of this paper lies in the design of proof procedures for logic-based argumentation systems [Dung,Kowalski,Toni, 2006; Dung,Mancarella,Toni , 2007; Eshghi,Kowalski, 1989; Kakas,Toni, 1999; Dung, 1995a] by translating automotacically proof procedures in abstract argumentation into ones for the latter systems.

7 Acknowledgements

We thank the referees for constructive comments and criticisms. This work was partially funded by the Sixth Framework IST program of the European Commission under the 035200 ARGUGRID project.

2 Conf(N,T) consists of all arguments that selfattack or attacked or being attacked by proponent arguments on the path from the root to N