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

1.Introduction

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

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

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

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

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

The behaviors of F1 and F2 could be explained by the proof trees (viewed arguments) in Fig. 1.

Fig. 1.

Arguments of F1 and F2.

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

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

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

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

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

SWI-prolog delivers respectively the answers “True”, “False”, “True” to the queries ←a?, “←α?” and “←β?” wrt program F2.33 The answer to “←α?” is false because the only argument supporting it is C2 that is based on assumption not_β that is attacked by argument B. We could hence say that infinite arguments are attacked the same way finite arguments are attacked.

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

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

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

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

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

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

Fig. 2.

Illustration of Example 1.

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

The grounded extension of an argumentation framework AF=(Ar,att) coincides with the least fixed point of the characteristic function FAF. It hence follows that the grounded extension of AF contains the set FAFω(∅)=∪{FAFi(∅)|i is a natural number}.44

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

Example 2.

Let AF=(Ar,att) with Ar={B,A0,A1,…,Ai,Ai+1,…} and att={(A2k+1,B)|k⩾0}∪{(Ak,Ak+1)|k⩾0}. (A graphical illustration of this argumentation framework is in Fig. 3).

It is easy to see that for each natural number ⩾1: FAFi(∅)={A0,A2,…,A2(i−1)}. Hence Fω(∅)=∪{FAFi(∅)|i is a natural number}={A0,A2,…,A2i,…}.

The grounded extension of AF is: FAF(FAFω(∅))=FAFω(∅)∪{B}.

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

Fig. 3.

An argumentation framework that is not ω-grounded.

To address this issue, we introduce the class of ω-grounded argumentation frameworks where the grounded extension is “computed” after at most ω steps, i.e. the grounded extension of AF coincides with FAFω(∅)=∪{FAFi(∅)|i is a natural number}. We then present several key results:

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

2.Preliminaries: Argumentation with infinite arguments

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

2.2.Assumption-based argumentation

Given a logical language L, a standard assumption-based argumentation (ABA) framework ([6]) is a triple F=(R,A,‾) where R is a set of inference rules of the form l0←l1,…ln (n⩾0 and l0,…,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.

Remark 1.

In non-standard ABA frameworks ([24]), 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.

Remark 2.

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

Remark 3.

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

Further the set of assumptions (resp non-assumptions) appearing in the body of r is denoted by Ass(r) (resp. NAss(r)).

Definition 1

Definition 1(Finitary ABA).

An ABA framework F=(R,A,‾) is finitary if for each sentence δ∈L, the set of rules with head δ is finite.1010

Convention 1.

From now on until the end of the paper,

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

• if not otherwise mentioned, we assume an arbitrary but fixed finitary standard assumption-based argumentation framework F=(R,A,‾).

Definition 2

Definition 2(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 3.

Let’s consider an argumentation framework F2 in the introduction.

F2:r:a←not_αr″:α←not_β,f(0)rn:f(n)←f(n+1),n⩾0t:β←

Some partial proofs supporting a and α are described below and illustrated in Fig. 4.

ψ=(root,a)ψ′=(root,a).(r,not_α)p0=(root,α)p1′=(root,α).(r″,not_β)p1=(root,α).(r″,f(0))p2=(root,α).(r″,f(0)).(r0,f(1))…pn+1=(root,α).(r″,f(0)).(r0,f(1))…(rn−1,f(n))

Fig. 4.

A graphical representation of partial proofs of Example 3.

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

Definition 3

Definition 3(Partial Proof Trees).

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

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

from T, the following properties hold:

• The partial proof p′≡(root,σ0).(r1,σ1).…(rn−1,σn−1) also belongs to T and is referred to as the unique parent of p whereas p is referred to as a child of p′;

• Every partial proof of the form p′.(rn,σ′) with σ′∈bd(rn), also belongs to T and is a child of p′;

• p′ has no other children.

σ0 is often referred to as the conclusion of T, denoted by Cl(T) while the partial proof (root,σ0) is referred to as the root of T.

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

Remark 4.

For convenience, we often refer to a partial proof tree without mentioning its conclusion if there is no possibility for misunderstanding.

Notation 1

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 partial proof tree T as a node labeled by σn in T.

Fig. 5.

Some proof trees of F2.

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 from true.

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

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

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

Considering Fig. 5, the partial proof (root,α).(r″,f(0)) is a leaf node of Tr0 while, (root,α).(r″,f(0))…(rn−1,f(n)) is a leaf node of Trn.

Further, the support of Tr0, i.e. Sp(Tr0), is {not_β,f(0)} and Ass(Tr0) is {not_β}.

Definition 4

Definition 4(Arguments).

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

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

• The set of all arguments wrt the ABA framework F is denoted by ArF.

Convention 2.

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

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

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

Definition 5

Definition 5(Attacks).

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

  • (1) The conclusion of A is the contrary of some assumption in the support of B.

  • (2) A and B are identical and infinite.

• The attack relation between arguments in ArF is denoted by attF. Define

  AFF=(ArF,attF)

Due to the fact that the infinite arguments always attack themselves, the following lemma holds obviously.

Lemma 1.

Let S⊆ArF be admissible wrt AFF=(ArF,attF). Then S contains only finite arguments.

Notation 3.

Let T, T′ be proof trees and N be a non-final leaf node in T labeled by a non-assumption σ.1111

• T′ is an immediate expansion of T at N if there is a rule r of the form σ←b1,…,bm such that T′=T∪{N.(r,b1),…,N.(r,bm)}.

  Note that if m=0, T′=T∪{N.(r,true)}.1212

• 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′)=σ}.

Considering Fig. 5, Tr1=exp(Tr0,N,r0) where N is (root,α).(r″,f(0)).

Further the set of all immediate expansion of Tr0 at node N, i.e. CE(Tr0,N), is {Tr1}.

Notation 4.

Let T0, T1 be proof trees for σ0.

• We say T, T′ are compatible iff T∪T′ is also a proof tree.

• We say T0 is a prefix of T1 iff T0⊆T1.1313 1414

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

Considering Fig. 5, Tr0 is a prefix of Tr1.

Remark 5.

It is worthwhile to note that two proof trees could be compatible without being in a prefix-relationship as illustrated below (see Fig. 6).

Consider an assumption-based framework with three rules:

r1:a←b,c;r2:b←;r3:c←.

Consider two proof trees:

T0={p0,p1,p2,p3},T1={p0,p1,p2,p4}wherep0=(root,a),p1=(root,a).(r1,b),p2=(root,a).(r1,c)andp3=(root,a).(r1,b).(r2,true),p4=(root,a).(r1,c).(r3,true).T0,T1are compatible but neither is a prefix of the other.

Fig. 6.

Two compatible proof trees.

Lemma 2.

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

• (1) If T1 is an immediate expansion of T0 then T0 is a proper 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 (if exist) of N in T0 are respectively also the parent and children of N in T1.

Proof.

Obvious. □

Lemma 3.

Let T be an argument, T0 be a proof tree such that T0 is a proper prefix of T. Furthermore, let N be a leaf node in T0 such that CE(T0,N)≠∅. Then there is an unique T1∈CE(T0,N) such that T1 is a prefix of T.

T1 is often simply denoted by exp(T0,N,T).

We also define exp(T0,T)={exp(T0,N,T)|N is a non-final leaf node of T0}.1515

Proof.

Lemma 3 in [31] proves the existence of T1. The uniqueness of T1 should be obvious. □

Definition 6.

An increasing sequence of 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 proof trees. The following statements hold:

• (1) T0∪T1∪…Ti∪… is a proof tree.

• (2) If the sequence sq is fair then T0∪T1∪…Ti∪… is an argument.

Proof.

This is Lemma 4 in [31]. □

Notation 5.

Let T be a 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.1616

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

3.ω-Groundedness of argumentation frameworks

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

4.Grounded dispute derivations

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

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

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

Fig. 7.

Proof trees of Example 4.

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

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