A Lattice-Based Approach to Computing Warranted Beliefs in Skeptical Argumentation Frameworks

1 Introduction andMotivations

Abstract argumentation frameworks have played a major role as a way of understanding argument-based inference, resulting in different argument-based semantics. In order to compute such semantics, efficient argument-based proof procedures are required for determining when a given argument A is warranted. This involves the analysis of a potentially large search space of candidate arguments related to A by means of an attack relationship.

This paper presents a novel approach to model such search space for warrant computation in a skeptical abstract argumentation framework. We show that the above search space can be defined as a lattice, and illustrate how some constraints (called dialectical constraints) can play a role for guiding the efficient computation of warranted arguments. The rest of this paper is structured as follows. Section 2 presents the basic ideas of an abstract argumentation framework with dialectical constraints. Section 3 shows how so-called dialectical trees can be used to analyze the search space for computing warrants, representing it as a lattice. In Section 4 we analyze different criteria which can lead to compute warrant more efficiently on the basis of this lattice characterization. Finally, in Sections 5 and 6 we discuss some related work and present the main conclusions that have been obtained.

2 An Abstract Argumentation Framework with Dialectical Constraints

In this paper we are concerned with the study of warrant computation in argumentation systems, with focus on skeptical semantics for argumentation. As a basis for our analysis we will use an abstract argumentation framework (following Dung's seminal approach to abstract argumentation [Dung, 1995]) enriched with the notion of dialectical constraint.

∗This paper is based on a preliminary workshop paper from the same authors ("An Abstract Model For Computing Warrant in Skeptical Argumentation Frameworks", Proc. of the 11th NMR 2006 Workshop, Windermere, UK, June 2006).

Definition 1 [Dung, 1995] An argumentation framework Φ is a pair 〈Args, R〉, where Args is a finite set of arguments and R is a binary relation R ⊆ Args × Args. The notation (A, B) ∈ R (or equivalently ARB) means that A attacks B.

A dialectical constraint imposes a restriction characterizing when a given argument sequence λ is valid in a framework Φ. An argumentation theory is defined by combining an argumentation framework with a particular set of dialectical constraints. Formally:

Definition 2 Let Φ = 〈Args, R〉 be an argumentation framework. A dialectical constraint C in the context of Φ is any function C : LinesΦ → {True, False}, where LinesΦ denotes the set of all possible sequences of arguments [A0,A1,A2, . . . ,Ak] in Φ where for any pair of arguments Ai, Ai+1 it holds that Ai+1 R Ai.

Definition 3 An argumentation theory T (or just a theory T) is a pair (Φ, DC), where Φ is an argumentation framework, and DC = {C1,C2, . . . ,Ck} is a finite (possibly empty) set of dialectical constraints.

Given a theory T = (Φ, DC), the intended role of DC is to avoid fallacious reasoning [Hamblin, 1970; Rescher, 1977] by imposing appropriate constraints on argumentation lines to be considered rationally acceptable. It must be noted that a full formalization for dialectical constraints is outside the scope of this work. We do not claim to be able to identify every one of such constraints either, as they may vary from one particular argumentation framework to another; that is the reason why DC is included as a parameter in T .

Argument games provide a useful form to characterize proof procedures for skeptical semantics in argumentation. 1 Such games model defeasible reasoning as a dispute between two parties (Proponent and Opponent of a claim), who exchange arguments and counterarguments, generating dialogues. A proposition Q is provably justified on the basis of a set of arguments if its proponent has a winning strategy for an argument supporting Q, i.e., every counterargument (defeater) advanced by the Opponent can be ultimately defeated by the Proponent. Dialogues in such argument games have been given different names (dialogue lines, argumentation lines, dispute lines, etc.). The set of all possible dialogues can also be suitably defined as a tree structure (called dialectical tree or argument tree). 2 In the next subsection we extend such definitions in the context of an argumentation theory.

1 See an in-depth discussion in [Prakken, 2005].

2.1 Argumentation Line. Bundle set

Definition 4 Let T = (Φ, DC) be an argumentation theory. An argumentation line λ in T is any finite sequence of arguments [A0, A1, . . . , An] in LinesΦ. A subsequence λ′ = [A0,A1,A2, . . . ,Ak], k ≤ n, will be called an initial argumentation segment (or just initial segment) in λ of length k, denoted ⌊λ⌋k . When k < n we say that λ′ is a proper initial segment in λ.

We will say that λ is rooted in A0, writing | λ | = s to denote that λ has s arguments. We will also write LinesA to denote the set of all argumentation lines rooted in A in the theory T .

Example 1 Consider a theory T = (Φ, DC), with DC = ∅, where the set Args is {A0, A1, A2, A3, A4 }, and assume that the following relationships hold: A1 defeats A0, A2 defeats A0, A3 defeats A0, A4 defeats A1. Three different argumentation lines rooted in A0 can be obtained, namely λ1 = [A0,A1,A4], λ2 = [A0,A1,A2], and λ3 = [A0,A3]. In particular, ⌊λ1⌋2 = [A0,A1] is an initial argumentation segment in λ1.

Example 2 Consider a theory T ′ = (Φ, DC) where the set Args is {A0, A1 }, and assume that the following relationships hold: A0 defeats A1, and A1 defeats A0. An infinite number of argumentation lines rooted in A0 can be obtained (e.g., λ1 = [A0], λ2 = [A0,A1], λ3 = [A0,A1,A0], λ4 = [A0,A1,A0,A1], etc.).

Remark 1 Note that fromDef. 4, given an argumentation line [A0, A1, A2, . . . , An] every subsequence [Ai, Ai+1, . . . Ai+k] with 0 ≤ i, i+k ≤ n is also an argumentation line. In particular, every initial argumentation segment is also an argumentation line.

Intuitively, an argumentation line λ is acceptable iff it satisfies every dialectical constraint of the theory it belongs to. Formally:

Definition 5 An argumentation line λ is acceptable wrt T = (Φ, DC) iff Ci(λ) = True, for every Ci in DC.

In what follows, we will assume that the notion of acceptability imposed by dialectical constraints is such that if λ is acceptable wrt a theory T = (Φ, DC), then any subsequence of λ is also acceptable.

Example 3 Consider the theory T ′ in Ex. 2, and assume that DC={C1}, with C1 = {repetition of arguments is not allowed }. 3 Then λ1 and λ2 are acceptable argumentation lines in T ′ , but λ3 and λ4 are not.

Definition 6 Let T be an argumentation theory, and let λ and λ′ be two acceptable argumentation lines in T . We will say that λ′ extends λ in T iff λ = ⌊λ′ ⌋k , for some k < | λ′ | (i.e., λ′ extends λ iff λ is a proper initial argumentation segment of λ′ ).

2 For in-depth discussion see [Prakken and Vreeswijk, 2002].

3 Note that this corresponds to a function C1(λ) = True iff there is no Ai, Aj in λ such that Ai =Aj , and False otherwise.

We will say that λ is exhaustive if there is no acceptable argumentation line λ′ in T such that | λ | < | λ′ |, and for some k, λ = ⌊λ′ ⌋k (i.e., there is no λ′ that extends λ in T). Non-exhaustive argumentation lines will be referred to as partial argumentation lines.

Example 4 Consider the theory T presented in Ex. 1. Then λ1, λ2 and λ3 are exhaustive argumentation lines whereas ⌊λ1⌋2 is a partial argumentation line. In the case of the theory T ′ in Ex. 2, the argumentation line λ2 extends λ1. Argumentation line λ2 is exhaustive, as it cannot be further extended on the basis of T ′ with the dialectical constraint introduced in Ex. 3.

We will distinguish the set S = {λ1, λ2, . . . , λk} of all argumentation lines rooted in the same initial argument and with the property of not containing lines that are initial subsequences of other lines in the set.

Definition 7 Given a theory T, a set S = {λ1, λ2, . . . , λn} of argumentation lines rooted in a given argument A, denoted SA, is a bundle set wrt T iff there is no λi, λj ∈ SA such that λi extends λj .

Example 5 Consider the theory T = (Φ, DC) from Ex. 1, and the argumentation lines λ1, λ2, and λ3. Then SA0 = {λ1, λ2, λ3} is a bundle set of argumentation lines wrt T .

2.2 Dialectical Trees

A bundle set SA is a set of argumentation lines rooted in a given argument A. Such set can be thought of as a tree structure, where every line corresponds to a branch in the tree. Formally:

Definition 8 Let T be a theory, and let A be an argument in T, and let SA = {λ1, λ2, . . . , λn} be a bundle set of argumentation lines rooted in A. Then, the dialectical tree rooted in A based on SA, denoted TA, is a tree structure defined as follows:

1) The root node of TA is A;

2) Let F={tail(λ), for every λ ∈ SA}, and H={head(λ), for every λ ∈ F}. 4 If H = ∅ then TA has no subtrees. Otherwise, if H = {B1, . . . , Bk}, then for every Bi ∈ H, we define getBundle(Bi) = {λ ∈ F | head(λ) = Bi}. We put TBi as an immediate subtree of A, where TBi is a dialectical tree based on getBundle(Bi). We will write TreeA to denote the family of all possible dialectical trees based on A. We will represent as TreeT the family of all possible dialectical trees in the theory T.

Example 6 Consider the theory T = (Φ, DC) fromEx. 1. In that theory it holds that SA0 = {λ1, λ2, λ3} is a bundle set. Fig. 1(a) shows an associated dialectical tree TA0 .

Clearly, Definition 8 induces an equivalence relation on the set of all TreeA . Formally:

Definition 9 Let T be a theory, and let TreeA be the set of all possible dialectical trees rooted in an argument A in T. We will say that TA is equivalent to T ′A, denoted TA ≡τ T ′A iff they are obtained from the same bundle set SA.

4 The functions head(·) and tail(·) have the usual meaning in list processing, returning the first element in a list and the list formed by all elements except the first, respectively.

Given an argument A, there is a one-to-one correspondence between a bundle set SA of argumentation lines rooted in A and the corresponding equivalence class of dialectical trees that share the same bundle set as their origin (as specified in Def. 8). Each member of an equivalence class represents a different way in which a tree could be built. Each particular computational method used to generate the dialectical tree from the bundle set will produce a particular member of the equivalence class.

Definition 10 Let T be an argumentative theory, and let SA be a bundle set of argumentation lines rooted in an argument A of T . We define the mapping T : ℘(LinesA) \ {∅} → TreeA as T(SA) =def TA, where TreeA is the quotient set of TreeA by ≡τ , and TA denotes the equivalence class of TA.

Proposition 1 For any argument A in an argumentative theory T , the mapping T is a bijection. 5

As the mapping T is a bijection, we can also define the inverse mapping S =def T-1 . In what follows, we will use indistinctly a set notation (a bundle set of argumentation lines rooted in an argument A) or a tree notation (a dialectical tree rooted in A), as the former mappings S and T allow us to go from any of these notations to the other.

Proposition 2 Let T be a theory, and TA a dialectical tree in T. Then it holds that any subtree T ′A of TA, rooted in A, is also a dialectical tree wrt T .

2.3 Acceptable dialectical trees

Definition 11 Let T be a theory. A dialectical tree TA in T is acceptable iff every argumentation line in the associated bundle set S(TA) is acceptable. We will distinguish the subset ATreeA (resp. ATreeT ) of all acceptable dialectical trees in TreeA (resp. TreeT ).

As acceptable dialectical trees are a subclass of dialectical trees, all the properties previously shown apply also to them. In the sequel, we will just write "dialectical trees" to refer to acceptable dialectical trees, unless stated otherwise.

5 Proofs not included for space reasons.

Definition 12 A dialectical tree TA will be called exhaustive iff it is constructed from the set SA of all possible exhaustive argumentation lines rooted in A, otherwise TA will be called partial.

The exhaustive dialectical tree for any argument A can be proven to be unique.

Proposition 3 Let T be a theory, and let A be an argument in T . Then there exists a unique exhaustive dialectical tree TA in T (up to an equivalence wrt ≡τ as given in Def. 9)

Acceptable dialectical trees allow to determine whether the root node of the tree is to be accepted (ultimately undefeated) or rejected (ultimately defeated). A marking function provides a definition of such acceptance criterion. Formally:

Definition 13 Let T be a theory. A marking criterion for T is a function Mark : TreeT → {D, U}. We will write Mark(Ti) = U (resp. Mark(Ti) = D) to denote that the root node of Ti is marked as U-node (resp. D-node).

Several marking criteria can be defined for capturing skeptical semantics for argumentation. A particular criterion (which we will later use in our analysis for strategies for computing warrant) is the and-or marking of a dialectical tree, which corresponds to Dung's grounded semantics [Dung, 1995].

Definition 14 Let T be a theory, and let TA be a dialectical tree. The and-or marking of TA is defined as follows: 1) If TA has no subtrees, then Mark(TA) = U. 2) If TA has subtrees T1, . . . , Tk then a) Mark(TA) = U iff Mark(Ti) = D, for all i = 1 . . . k. b) Mark(TA) = D iff ∃ Ti such that Mark(Ti) = U, for some i = 1 . . . k.

Proposition 4 Let T be a theory, and let TA be a dialectical tree. The and-or marking defined in Def. 14 assigns the same mark to all the members of TA.

Definition 15 Let T be an argumentative theory and Mark a marking criterion for T. An argument A is a warranted argument (or just a warrant) in T iff the exhaustive dialectical tree TA is such that Mark(TA) = U.

Example 7 Consider the exhaustive dialectical tree TA0 in Ex. 6 shown in Fig. 1(a). Fig. 1(b) shows the corresponding marking by applying Def. 14, showing that A0 -the root of TA0 - is an ultimately defeated argument, i.e., Mark(TA0 ) = D. Hence A0 is not a warranted argument. Fig. 1(c)-(d) shows two marked dialectical trees belonging to the same equivalence class TA0 .

3 Warrant Computation via Dialectical Trees

Our main concern is to model warrant computation in skeptical argumentation frameworks, and in such a case tree structures lend themselves naturally to implementation. In fact, some implementations of skeptical argumentation systems (e.g., DeLP [Garc´ıa and Simari, 2004]) rely on tree structures (such as dialectical trees) which can be computed by performing backward chaining at two levels. On the one hand, arguments are computed by backward chaining from a query (goal) using a logic programming approach (e.g., SLD resolution). On the other hand, dialectical trees can be computed by recursively analyzing defeaters for a given argument, defeaters for those defeaters, and so on. In particular, in more complex and general settings (such as admissibility semantics) dialectical proof procedures have been developed [Dung et al., 2006] using a similar strategy to compute warranted belief.

In our abstract model the process of building an arbitrary dialectical tree TA0 can be thought of as a computation starting from an initial tree (consisting of a single node) and evolving into more complex trees by adding new arguments (nodes) stepwise. Elementary steps in this computation can be related via a precedence relationship "⊑" among trees:

Definition 16 Let T be a theory, and let TA, T ′A be acceptable dialectical trees rooted in an argument A. We define a relationship ⊑ ⊆ TreeA × TreeA . We will write TA ⊏ T ′A whenever T ′A can be obtained from TA by extending some argumentation line λ in TA by exactly one argument. As usual, we write TA⊑T ′A iff TA = T ′A or TA⊏T ′A. We will also write TA⊑∗T ′A iff there exists a (possibly empty) sequence T1, T2, . . . , Tk s.t. TA = T1⊑. . .⊑Tk = T ′A.

Every dialectical tree Ti can be seen as a 'snapshot' of the status of a disputation between two parties (proponent and opponent), and the relationship "⊑" allows to capture all possible evolutions of a given disputation. 6 In particular, note that for any argumentative theory T, given an argument A the ordered set (TreeA ,⊑∗) is a poset, where the least element is A and the greatest element is the exhaustive dialectical tree TA. From Def. 16 the notion of exhaustive dialectical tree can be recast as follows: A dialectical tree Ti is exhaustive iff there is no Tj ̸= Ti such that Ti ⊏ Tj.

We are now concerned with the following question: can we enumerate all possible ways of computing the exhaustive dialectical tree TA rooted in a given initial argument A? The answer is yes. In fact, as we will see in the next definitions, we can provide a lattice characterization for the space of all possible dialectical trees rooted in a given argument A on the basis of join of dialectical trees (∨) (resulting in a new tree corresponding to the 'union" of T1 and T2) and meet of dialectical trees (∧) (resulting in a new tree corresponding to the "intersection" of T1 and T2). Formally:

Definition 17 Let T be an argumentative theory, and let T1 and T2 be dialectical trees rooted in A. We define the meet and join of T1 and T2, (written T1 ∧ T2 and T1 ∨ T2) as follows:

• λ is an argumentation line in T1 ∧ T2 iff λ = ⌊λ1⌋k = ⌊λ2⌋k , for some k > 0 such that λ1 ∈ T1 and λ2 ∈ T2 and there is no λ′ that extends λ satisfying this situation.
• λ is an argumentation line in T1 ∨ T2 iff 1) λ ∈ T1 and there is no λ′ ∈ T2 such that λ′ extends λ, or 2) λ ∈ T2 and there is no λ′ ∈ T1 such that λ′ extends λ.

For any argumentation theory T the set of all possible acceptable dialectical trees rooted in an argument A ∈ T can be conceptualized as a lattice. Formally:

Lemma 1 Let A be an argument in a theory T, and let (ATreeA,⊑∗) be the associated poset. Then (ATreeA, ∨, ∧) is a lattice.

Given the lattice (ATreeA, ∨, ∧), we will write T ⊥ A to denote the bottom element of the lattice (i.e., the dialectical tree involving only A as root node) and T ⊤ A to denote the top element of the lattice (i.e., the exhaustive dialectical tree).

6 Note however that Ti ⊑ Tj does not imply that one party has advanced some argument in Ti and the other party has replied in Tj . Thus our framework provides a setup to define unique- and multimove protocols as defined by Prakken [Prakken, 2005].

Example 8 Consider the theory T from Ex. 1, and the exhaustive dialectical tree rooted in A0 shown in Ex. 6. The complete lattice associated with A0 is shown in Fig. 2.

4 ComputingWarrant Efficiently

We have shown that given an argumentative theory T , for any argument A in T there is a lattice (ATreeA, ∨, ∧) whose bottom element is a dialectical tree with a single node (the argument A itself) and whose top element is the exhaustive dialectical tree TA. In that lattice, whenever Tk = Ti∨Tj it is the case that Ti⊑Tk and Tj⊑Tk.

In Fig. 2(top) corresponding to Example 8 we can see that for dialectical trees T2 and T3, it holds that Mark(T2) = Mark(T3) = D (assuming that Mark is defined as in Def. 14). Clearly, it is the case that any tree Ti where T2⊑Ti or T3⊑Ti satisfies that Mark(Ti) = D. In other words, whichever is the way the tree T2 (or T3) evolves into a new tree in (ATreeA0 , ∨, ∧) it turns out that the associated marking remains unchanged. We formalize that situation as follows:

Definition 18 Let T be an argumentation theory, and let TA be a dialectical tree, such that for every T ′A evolving from TA (i.e., TA⊑∗T ′A) it holds that Mark(TA) = Mark(T ′A). Then TA is a settled dialectical tree in T .

Now we have a natural, alternative way of characterizing warrant.

Proposition 5 Let T be a theory, and let A be an argument in T . Then A is a warrant wrt T iff Mark(TA) = U, where TA is a settled dialectical tree.

Clearly, computing settled dialectical trees is less expensive than computing exhaustive dialectical trees, as fewer nodes (arguments) are involved in the former case. Following Hunter's approach [Hunter, 2004], in what follows we will formalize the cost of computing a dialectical tree as a function cost : TreeT → ℜ. As explained in [Hunter, 2004], several issues can be considered when computing such cost. For simplicity, in our formalization we will assume that cost is linearly related to the number of nodes in a dialectical tree, such that cost(T) = C ∗ Nodes(T), where C > 0 is a constant and Nodes(·) stands for the number of nodes in a tree.

The next definition refines the class of settled dialectical trees by distinguishing those trees involving as few arguments as possible in order to determine whether the root of the tree is ultimately a warranted argument according to the marking procedure. From the many possible minimally settled dialectical trees rooted in a given argument A, a dialectical tree T is optimally settled if ̸ ∃ T ′ that is less expensive than T.

Definition 19 A dialectical tree T is a minimally settled dialectical tree iff there is no T ′⊏T such that T ′ is a settled dialectical tree. A dialectical tree T is an optimally settled dialectical tree iff T is minimally settled, and for any other settled tree T ′ , cost(T) ≤ cost(T ′ ).

Example 9 Consider the theory T from Ex. 1, and the complete lattice (ATreeA0 , ∨, ∧) shown in Fig. 2 (top). Then T2 and T3 are minimally settled dialectical trees.

Let SettledA, MinimalA and OptimalA be the sets of all settled, minimally settled and optimally settled dialectical trees for an argument A, resp. Clearly, it holds that OptimalA ⊆ MinimalA ⊆ SettledA ⊆ ATreeA. The sets SettledA, MinimalA and OptimalA can be identified in any lattice (ATreeA, ∨, ∧), as shown in Fig. 2 (bottom). The borderline on top of the lattice denotes all possible minimally settled dialectical trees T1, . . . , Tk rooted in A. Some of such trees in that set may be optimal. Any dialectical tree that evolves from settled dialectical trees T1, . . . , Tk will be also a settled dialectical tree. In particular, the exhaustive dialectical tree is also settled.

4.1 Dialectical Constraints (Revisited)

As we have analyzed previously, the lattice associated with any argument A accounts for the whole search space for detecting if A is warranted. To do so it is not necessary to compute the exhaustive dialectical tree rooted in A; rather, it suffices to focus search on settled dialectical trees, as they involve less nodes and are consequently more efficient. When determining whether a conclusion is warranted, argumentbased inference engines are supposed to compute a sequence of dialectical trees T1, T2, . . . , Tk such that Tk is a settled dialectical tree. For skeptical argumentation semantics, inference engines like DeLP [Garc´ıa and Simari, 2004] use depthfirst search to generate dialectical trees for queries and determine if a given literal is warranted. Such search can be improved by applying α - β pruning, so that not every node (argument) is computed. In other words, depth-first search naturally favors the computation of settled dialectical trees.

Example 10 Consider the marked dialectical trees in Fig. 1(right) belonging to the same equivalence class TA0 (Ex. 7). Then depthfirst computation using α - β pruning will perform better on the tree in Fig. 1(d) than on the tree in Fig. 1(c), as in the first case, only two nodes need to be explored to obtain the final marking of the tree (A0 and A3), whereas in the second case four nodes (A0, A1, A3 and A4) need to be traversed.

The natural question that arises next is how to compute minimally settled trees. Given a theory T = (Φ, DC), it turns out that the set of dialectical constraints DC can help to provide a way of approximating such minimally settled trees, based on the fact that in depth-first search the order in which branches are generated is important: should shorter branches be computed before longer ones, then the resulting search space can be proven to be smaller on an average search tree [Ches˜nevar et al., 2005]. Usually heuristics are required to anticipate which branches are likely to be shorter than the average. Constraints in DC can help provide such kind of heuristics. In this setting, heuristics for efficient computation of dialectical trees can be understood as functions which improve the associated dialectical proof procedure by tending to approximate optimally settled trees.

Example 11 In DeLP the set DC includes as a constraint that arguments advanced by the proponent (resp. opponent) should not be contradictory in any argumentation line. The following heuristics [Ches˜nevar et al., 2005] can be shown to favor the computation of shorter argumentation lines when applying depth-first search in the context of DeLP: if the current argument A0 is a leaf node in a dialectical tree T, and has different candidate defeaters A1, A2, . . . , Ak, then the Ai which shares as many literals as possible with A0 should be chosen when performing the depth-first computation of TA0 . Thus, while depth-first computation of dialectical trees favors naturally the construction of minimally settled dialectical trees, by applying this heuristics an approximation to optimally settled dialectical trees is obtained.

4.2 Relevance in Dialectical Trees

In [Prakken, 2001] the notion of relevance was introduced in the context of argument games and the characterization of protocols for liberal disputes. According to [Prakken, 2001], a move is relevant in a dispute D iff it changes the disputational status of D's initial move. 7 In our context, dialectical trees correspond to such disputes. In the setting presented in [Prakken, 2001], moves are performed by both parties involved in a dispute (Proponent and Opponent).

Interestingly, there is a clear relation between minimally settled dialectical trees and this notion of relevance, as the notion of extending an argumentation line by one argument (as introduced in Def. 16) can be recast as performing a move.

7 The notion of relevance as well as some interesting properties were further studied and refined [Prakken, 2005].

Definition 20 Let T = (Φ, DC) be an argumentation theory, and let TA1 , T ′A1 be acceptable dialectical trees. We will say that there is a move M from TA to T ′A, denoted as Move(TA, T ′A), iff TA ⊏T ′A. It must be remarked that a proper conceptualization of move in argumentation demands more parameters, such as identifying the argumentation line in which a argument is introduced, who is the player (Proponent or Opponent) making the move, etc. Such an approach has been formalized by [Prakken, 2001; 2005]. Our approach in this case is intentionally oversimplified, as it just aims to relate the notion of relevance and the notion of minimally settled dialectical trees. In fact, note that Def. 20 allows us to formalize the computation of an acceptable dialectical tree Tk rooted in A0 as a sequence of moves Move(T0, T1), Move(T1, T2), . . . , Move(Tk-1, Tk), where T0 is a dialectical tree with a single node T ⊥ A0 . In fact, Prakken's notion of relevant move can be stated in our setting as follows: a move M = Move(TA, T ′A) is relevant iff Mark(TA) ̸= Mark(T ′A).

The following proposition shows that minimally settled trees are only those obtained by performing a sequence of relevant moves ending in a settled dialectical tree.

Proposition 6 Let T be an argumentation theory, and let TA be a dialectical tree. Then TA is minimally settled iff there is a sequence of moves M1, M2, . . . , Mk such that every move Mi is relevant, and Mk results in a settled dialectical tree.

5 RelatedWork

Dialectical constraints have motivated research in argumentation theory in different directions. In our proposal dialectical constraints are left as a particular parameter to be included in the argumentation theory. Different argument-based proof procedures have included particular dialectical constraints as part of their specification. In [Besnard and Hunter, 2001] the authors present a logic of argumentation which disallows repetition of arguments in argument trees [Besnard and Hunter, 2001, p.215] Other approaches for computing wellfounded semantics via trees (e.g., [Kakas and Toni, 1999]) defense nodes (which account for Proponent's argument in an argumentation line) cannot attack any other defense node in the tree. Similarly, in [Dung et al., 2006], for computing assumption-based admissible semantics there is a further requirement in the proof procedure that "the proponent does not attack itself". Such kind of restrictions can be seen as particular dialectical constraints in the context of our proposal.

Recently there have been other research oriented towards formalizing dialectical proof procedures for argumentation. To the best of our knowledge, none of such works formalizes the dialectical search space through a lattice as presented in this paper. Our work complements previous research concerning the dynamics of argumentation, notably [Prakken, 2001] and [Brewka, 2001]. Although Prakken develops a very comprehensive general framework, some important computational issues (e.g., search space considerations) are not taken into account.

6 Conclusions. FutureWork

In this paper we have presented a novel approach to model the search space associated with warrant computation in an abstract argumentation framework. We have shown how the notion of dialectical tree can be used constructively to model different stages in the process of computing warranted arguments. We have also shown how the process of computing warrant can be recast into computing dialectical trees within a lattice, illustrating how dialectical constraints can play a role for guiding an efficient computation of warranted literals. Part of our future work is related to studying theoretical properties of the proposed framework, analyzing their incidence for developing efficient argument-based inference engines. Research in this direction is currently being pursued.

Acknowledgements

We thank anonymous reviewers for comments which helped to improve the final version of this paper. This research was partially supported by the Dept. of Computer Science and Eng., SeCyT, U.N.Sur, CONICET, and ANPCyT (PICT 13096, 15043, PAV076), Argentina. Partial research support was also obtained from Project TIN200407933-C03-01/03 and Ram´on y Cajal Program (MCyT, Spain).