We put forward and provide an empirical evaluation of strategies for fully automatic flexible dispute derivations for assumption-based argumentation (ABA). These being a novel dialectical means of judging claims in the context of ABA. Central among our findings is that our naive direct implementation of lfexible disputes outperforms the current state-of-the-art system for ABA disputes (acceptance of claims, admissible semantics) especially when allowing forward moves from premisses to claims in addition to backwards from conclusions to premisses.
opponent are completely omniscient in that they remember all arguments (and sub-arguments)
put forward during disputes; we have shown that this avoids redundancy. Flexible disputes, as a
consequence, generalise graph-based disputes [
In [
In this work we present, first of all, strategies and related algorithms for finding
successful disputes (for the admissible, complete, and stable semantics) which we implemented in a
revamped system which we appropriately redubbed to flexABle1. Secondly, we provide an
in-depth experimental study of such strategies. We also compare the performance of our system
to the main state-of-the-art system computing dispute derivations, abagraph, for determining
acceptance of claims w.r.t. the admissible semantics2. Despite ours being a comparably naive
direct implementation of flexible dispute derivations, while abagraph is based on SICStus
Prolog, we show that our system clearly outperforms abagraph especially when making use of
(conservative) forward moves. We finally, following the lead of [
For reasons of space we will only review the absolute minimal elements of ABA and flexible
dispute derivations required to follow our work. We refer to e.g. [
An ABA framework is a tuple ℱ = (ℒ , ℛ , , ) where (ℒ , ℛ ) is a deductive system, with a
language ℒ and a set of inference rules ℛ . Elements of the (non-empty) set ⊆ ℒ are referred
to as assumptions and is a total mapping from into ℒ , where a is the contrary of a. As in
all other work on reasoning methods for ABA we are aware of, we make a few further crucial
assumptions about ABA frameworks: 1) that ℒ is finite 3, 2) that ℒ consists of propositional
atoms, 3) that contraries do not appear in the heads of rules (i.e. we deal with flat ABA), 4) that all
elements in ℛ are given explicitly; given the previous assumptions, this means that they are Horn
rules of the form h ← b1, . . . , bn where h is an atom while b1, . . . , b2 can be atoms or contraries
1https://github.com/gorczyca/aba-dd-rule-based
2The only semantics which both systems caters for - abagraph also supports the grounded semantics.
3Definitions of dispute derivations, including flexible dispute derivations as defined in [
(B ∩ ℛ ) B− with B− = (B ∩ ) ∪ {s ∈ (B ∩ ℒ )↑↑ ⋃︀ ¬∃h ← B ∈
h = s} ∪ {h ← B ∈ B ∩ ℛ ⋃︀ B ∩ B− ≠ ∅} P∗ = (P ∩ ) ∪ {h ← B ∈ (P ∩ ℛ ) ⋃︀ B ⊆ P∗} ∪ {s ∈ (P ∩ (ℒ )) ⋃︀ ∃
h ← B ∈ P∗ with h = s} B∗ − = (B ∩ ( )) ∪ {h ← B ∈ (B B−) ∩ ℛ ⋃︀ B ⊆
B∗ − } ∪ {s ∈ (B B−) ∩ (ℒ ) ⋃︀ ∃h ← B ∈ B∗ − B!S − = ((B B−) ∩ S) ∪ {s ∈ (B B−) ∩ ℒ ⋃︀ ∃h ← B ∈ with h = s} B!S − ∩ ℛ
with s ∈ B} ∪ {h ← B ∈ (B B−) ∩ ℛ ⋃︀ h ∈ B!S −} ! = ∩ B! − = {u ∈ ℋ = {h ⋃︀
⋃︀ u ∉ B∗ − } h ← B ∈ P P∼, B ⊆ P∗}
statements in S ⊆ ℒ
only the second definition which is at the basis of our system flexABle. Needless to say, there is a clear correspondence between both definitions and at each dispute state it is straightforward to convert from one representation to another (something also possible in flexABle).
Rule-based flexible dispute derivations are sequences of dispute states of the form where B ⊆ (ℒ ∪ ℛ ) and P ⊆ B. B is the opponents claim and rule-set, and P the proponents. The initial dispute state is of the form (γ , γ ) with γ ⊆ ℒ (for which no atom and its contrary are in γ ) being the goals. To define moves in dispute derivations the auxiliary notation in Table 1 is (B, P),
OB-( ∪Y1)
OF-(( ∩ ) ∪Y2) needed.
Then, a proponent dispute state advancement from a dispute state (B, P) is a dispute state (B′, P′) with P′ = P ∪ T , B′ = B ∪ T , X1 ⊆ , X1 ⊆ , where T is defined as in Table 2.
PB- ( ! ∪ X1) PF-(( ! ∩ ) ∪ X2)
T = {h ← B} ∪ B for h ← B ∈ P P∼ with h ∈ (P ∩ ℒ )↓ T = {h} ∪ {h ← B} ∪ B for h ← B ∈ P P∼ with h ∈ ( ! ∪ X1) (P ∪ ) T = {h} ∪ {h ← B} for h ← B ∈ P P∼, B ⊆ P∗
T = {u} for u ∈ (( ! ∩ ) ∪ X2) (P ∪ {u} ∪ ∪ )
An opponent dispute state advancement from a dispute state (B, P) is a dispute state (B′, P) with B′ = B ∪ T , Y1 ⊆ , Y2 ⊆ , where T is defined as in Table 3.
The above definitions of moves allow several instantiations by varying the parameters
X1,X2,Y1,Y2. In this work we focus on dispute advancements as given in Table 4. The
termination criteria we consider in this work are in Table 54. Then, we have that dispute derivations
D + TA with D ∈ {DAB, DABF, DC, DS} are sound and complete for acceptance of claims w.r.t. the
admissible (thus also complete, preferred) semantics, while DC + TC and DS + TS are sound and
complete for determining respectively (full) complete and stable assumption sets congruous with
the goal claims [
DAB DABF DC DS PB-( !), PF-( ! ∩ )-2 PB-( !), PF-( ! ∩ ) PB-( !), PF-(( ! ∩ ) ∪ ) PB-( !), PF-( )
OB-( ), OF-( ∩ )-2
OB-( ), OF-( ∩ )-2
OB-( ∪ ), OF-(( ∪ ) ∩ )-2
OB-( ), OF-( ∩ )-2
4Note that here we introduced a slight addition to TC correcting [
Prop. winning γ ∪ ⊆ P∗, ∩B∗ − = ∅ γ ∪ ⊆ P∗, ∩ B∗ − = ∅ ⊆ , ℋ ⊆ P∗
, γ ∪ ⊆ P∗, ∩ B∗ − =
, ∅ ∪ =
OB-( ) ∪ OF-( ∩ )-2 or OF-( ) OB-( ) ∪ OF-( ∩ )-2 or OF-( ) OB-( ) ∪ OF-( ∩ )-2 or OF-( )
PB-( !) ∪ PF-( ! ∩ )-2 or PF-( ) PB-( !) ∪ PF-(( ! ∩ ) ∪ ) or PF-( ) PB-( !) ∪ PF-( )
For an example, consider the ABA framework with = {a, b, c, d}, where a = t, b = r, c = t, d = c. Also: ℛ = {p ← q; q ← a; r ← p; t ← b; t ← p, s; t ← q, u, d}. A DC + TA (as well as DS + TA, DC + TC, DS + TS) derivation for p has the initial state ({p}, {p}). The first two moves are backward of the proponent using move type PB15, first with p ← q and then q ← a (so now = {a}). Then, the opponent makes an OB2 move using t ← b. Here the proponent makes a “conservative” forward PF1 move (also a PB2 move in this case) using r ← p (so = {b}). Finally, the proponent makes a “non-conservative” forward move (before this step ℐ ∖ = ∖ ( ∪ ) = {c, d}) PF2 advancing c ( = {a, c}, = {b, d}). The dispute ends with the opponent not being able to advance further in OF-( ) manner. The assumption set = {a, c} is admissible, complete, and stable.
Strategies. We start by introducing a simple6 “preference-on-move-types-based” framework for strategies in which these consist of tuples (<M, H, R, A).
Each dispute derivation variant from Section 2 has associated a set of possible move types from M = {PB1, PB2, PF1, PF2, OB1, OB2, OF2}. So the first aspect of a strategy is a preference relation, a strict total order <M on move types. At each step in a dispute, from all possible moves, moves of type with lowest ranking w.r.t. <M are chosen.
There will often be several possible moves having lowest ranking w.r.t. <M. If the moves involve adding assumptions to the players sets (moves of type PF2, OF2) then the strategies in this work all return a random ordering of the assumptions. H, R, and A come into play when the moves involve adding rules to the players sets. Specifically, H is first of all a “rule-head selecting function”. Given a set of rules, it selects a subset by considering rule-heads. We consider two such functions, one mostRules which returns a (random) maximal set of rules from those rule 5Here and in the remainder of this work we often simplify the notation for moves by leaving the instantiations of parameters implicit. 6Note in particular we define strategies to be homogeneous among players. Non-homogeneous strategies can be defined in flexABle. sets that result when partitioning the rules according to their heads. The other, leastRules, selects a minimal such set.
So H gives a new set of rules to choose from, which strategies now order by using R and A. First R associates a natural number to rules. We define three such “rule comparison functions”: bodySize, newStatementsSize and lookaheadSize. The function bodySize simply returns the cardinality of the body of rules (⋃︀ B⋃︀ for r = h ← B). The function newStatementsSize computes how many new statements the rule introduces into the dispute. Concretely, at a dispute state (B, P), with the turn of p ∈ {proponent, opponent}, newStatementsSize(h ← B) = ⋃︀({ h} ∪ B) X︀⋃ with X = B if p = opponent and X = P if p = proponent. The function lookaheadSize is a measure of how close a move will get the proponent to winning7. Finally, to the last element of a strategy, A is one of or ⊺ with rules chosen by H being ordered ascendingly w.r.t. R if A = ⊺ and descendingly if A = (ties are resolved randomly).
Given a set of possible moves O = {(t1, p1), . . . , (tn, pn)} consisting of a move type ti and piece pi, either an assumption or a rule, we denote the application of a strategy Strat = (<M , H, R, A) on the possible moves as Strat(O) = (tx, P). Here 1 ≤ x ≤ n s.t. there is no ti with ti <M tx and P is a random ordering of P′ = {p ⋃︀ ( tx, p) ∈ O} if tx ∈ {PF2, OF2} or otherwise (tx ∈ {PB1, PB2, PF1, OB1, OB2})) an ordering of H(P′) w.r.t. R and A.
Algorithms. We turn to describing the search algorithm for flexible ABA disputes that underlies our system flexABle. We first extend dispute derivation states to be tuples S = (B, P, Ia, Ic) where Ia represents assumptions the proponent decides not to use (via PF2 moves), while Ic are assumptions the proponent decides not to attack (using moves PB2 or PF2). In the algorithms we denote sequences of elements where the order is important using delimiters ⎷⌄ rather than {}. Function GetNewStates from Algorithm 1 has a current (extended) dispute state, a strategy and a set of possible moves at the dispute state as input and returns the sequence of dispute states to be examined next. These are determined, first of all, by the strategy (line 2 in Algorithm 1) and then by the move type to which priority is given by the strategy (switch statement line 4). Here move types PB1,PB2, and PF2 introduce branching. In the case of PB1 (lines 5-6) this is because several possible rules for a claim can be considered, for PB2 (lines 7-11) in addition the proponent can decide not to consider some candidate for a culprit, while for PF2 move types (lines 15-24) the proponent can choose to use an assumption or not. Move type PF1 (lines 12-14) and all moves of the opponent (lines 25-30) do not introduce branching.
The main search procedure is then the recursive function GetSuccessfulDDs from
Algorithm 2. This takes as input a sequence of current dispute states, a set of found successful dispute
states, a strategy Strat, a termination criteria C and an advancement type A. In addition it has an
additional parameter St for defining the search to be depth-first or breadth-first. The procedure
is initialized with input (⎷( γ, γ, ∅, ∅)⌄ , ∅, Strat, C, A, St) (γ are the goals). If the sequence
of current dispute states is empty, the procedure returns the set of successful states (lines 2-3).
Otherwise, the first state in the sequence of current dispute states is taken for consideration and
removed from the current states (line 4), all possible moves at that dispute state are computed
(according to advancement A) (line 5), and moves which would make Ia ∩ ≠ ∅ or Ic ∩ ≠ ∅
7For lack of space we refer to Section 4.1 of [
input :S = (B, P, Ia, Ic), Strat = (<M , H, R, A), O = {(t1, p1), . . . , (tn, pn)} // current dispute state, strategy, and set of possible moves at the current state S w.r.t. the chosen advancement type output : newStates = ⎷( B1, P1, Ia1 , Ic1 ), . . . , (Bl , Pl , Ial , Icl )⌄ // chosen sequence of next states to be examined next; here 1 ≤ l ≤ n. 1 function GetNextStates(S, Strat, O) 2 (chosenMoveType, chosenMovesSequence) ←Ð Strat(O) // get chosen move type and moves sequence with
Strat 3 newStates ←Ð ⎷⌄ // initialize newStates 4 switch chosenMoveType do 5 case PB1 do // chosenMovesSequence is a sequence of rules 6 newStates ←Ð ⎷( B ∪ ({h} ∪ B1), P ∪ ({h} ∪ B1), Ia, Ic), . . . , (B ∪ ({h} ∪ Bl ), P ∪ ({h} ∪ Bl ), Ia, Ic)⌄ for h ← Bi ∈ chosenMovesSequence // create a sequence of new dispute states using rules in chosenMovesSequence, preserve the order case PF2 do // chosenMovesSequence is a sequence of assumptions b ←Ð chosenMovesSequence(︀ 0⌋︀ // take first assumption b takingState ←Ð (B ∪ {a}, P ∪ {a}, Ia, Ic) // get new state by adding b to B and P attackedAssumptions ←Ð {a ∈ ︀⋃ a = b} // get set of assumptions attacked by b ignoringState ←Ð Nil // initialize ignoringState if attackedAssumptions ≠ ∅ then // if b attacks some assumptions ignoringState ←Ð (B, P, Ia, Ic ∪ attackedAssumptions) // get new ignoringState by adding
attacked assumptions to ignored culprit candidates Ic else // otherwise, get new ignoringState by adding b to ignored assumptions Ia
ignoringState ←Ð (B, P, Ia ∪ {b}, Ic) newStates ←Ð ⎷ takingState, ignoringState⌄ // return both states case OB1 or OB2 or OF1 do // chosenMovesSequence is a sequence of rules h ← B ←Ð chosenMovesSequence(︀ 0︀⌋ // take first rule newStates ←Ð ⎷( B ∪ ({h} ∪ B), P, Ia, Ic)⌄ // get new state by adding rule to B case OF2 do // chosenMovesSequence is a sequence of assumptions a ←Ð chosenMovesSequence(︀ 0︀⌋ // take first assumption a newStates ←Ð ⎷( B ∪ {a}, P, Ia, Ic)⌄ // get new state by adding a to B return newStates hold are filtered-out (line 6). Then, the termination criteria C is applied at the taken state (line 9), if the proponent wins the state is appended to the successful states (lines 10-11), if the opponent wins the state is ignored (line 12), while if there is no winner yet (lines 13-18) function GetNextStates defined in Algorithm 1 is used to compute next possible states. The obtained sequence of the next possible states is then either appended at the beginning or the end of the sequence of current dispute states, depending on the search type (depth or breadth first). Then, the function is called again with the new sequence of current dispute states and set of successful dispute states (line 19).
Algorithm 2: Function GetSuccessfulDDs.
input :States = ⎷( B1, P1, Ia1 , Ic1 ), . . . , (Bn, Pn, Ian , Icn )⌄ // collection of dispute states
SuccStates = {(B1, P1, Ia1 , Ic1 ), . . . , (Bl , Pl , Ial , Icl )} // currently found succ. states Strat = (<M, H, R, A), C ∈ {TA, TC, TS}, A ∈ {DAB, DABF, DC, DS}, St ∈ {DFS, BFS} // strategy, termination criteria, advancement type, search type (depth-first-search or breadth-first search) output :succStates = {(B1, P1, Ia1 , Ic1 ), . . . , (Bk, Pk, Iak , Ick )} // successful states found 1 function GetSuccessfulDDs(States, SuccStates, Strat, C, A, St) 2 if States = ⎷⌄ then // if there are no more states to examine 3 return SuccStates // return found successful states currState ←Ð States.pop() // take first state from States possibleMoves ←Ð getPossibleMoves(currState, A) // get possible moves at the current state w.r.t. advancement type A possibleMoves ←Ð f ilter(possibleMoves, currState) // filter possible moves states′ ←Ð States // initialize states′ with remaining states succStates′ ←Ð SuccStates // initialize succStates′ with currently found successful states switch isOver(currState, possibleMoves,C) do // check if dispute over w.r.t. termination criteria C case ProponentWon do // C indicates that proponent has won
succStates′.append(currState) case OpponentWon do // C indicates that opponent has won
// do nothing... case NotOver do // C indicates that dispute has not terminated newStates ←Ð GetNextStates (currState, Strat, possibleMoves) if searchType = DFS then // if DFS prepend newStates to the beginning of the list
states′ ←Ð newStates. join(states′) else // else, if BFS append newStates at the end
states′ ←Ð states′. join(newStates)
GetSuccessfulDDs(states′, succStates′, Strat, C, A, St) // continue searching
Approximate Reasoning. We follow the lead of [
H leastRules mostRules leastRules leastRules mostRules leastRules random
R newStatementsSize newStatementsSize newStatementsSize newStatementsSize newStatementsSize newStatementsSize lookaheadSize
A ⊺ ⊺ ⊺ ⊺ ⊺
Experimental Setup. In our experiments we aimed to evaluate flexible dispute variants and
strategies in their exact and approximate versions, comparing also our system flexABle to the
current best system computing dispute derivations abagraph [
The strategies (following Section 3) we fixed are detailed in Table 6. We tried to keep strategies as diverse as possible, while varying in few parameters to ease comparison. The main distinction is between “patient strategies” S1 prioritizing opponents moves, and “eager strategies” S2 prioritizing the proponent. Within these, variants Sxa and Sx (x ∈ {1, 2}) differ in their use of H = leastRules vs. H = mostRules and A = ⊺ vs. A = . Variants Sxb serves to test the value of conservative forward moves, giving PF1 moves least priority. Strategy SAG simulates the default strategy of abagraph.
Using the same criteria as when selecting strategies of flexABle, we also settled on the
strategies for abagraph depicted in Table 79. Here parameter Turn indicates player priority.
Setting OppSet to smallest roughly means arguments of the opponent which have the fewest
yet unexpanded statements are expanded first. Sentence denotes which sentences are chosen to
expand by, with Patient meaning non-assumptions and Eager assumptions. Rule offers choices
for backward expansion from proponent sentences: Look-ahead 1-step and selecting a rule with
8http://robertcraven.org/proarg/abagraph.html; last accessed on 1.7.22.
9The parameters used to define strategies in abagraph are not directly comparable to the parameters from Section 3.
To the best of our knowledge there has also been no in-depth study of strategies of abagraph, hence the need to
define our own.
the smallest body. We refer to [
As to benchmark sets, we follow previous experiments for ABA [
As to the role of strategies, for setups with DAB, those making use of S2 outperform the others. For setups with DC and DS on the other hand, those making use of S2 perform worse. The latter further highlights that our experiments do not show random branching on PF2 moves to be an advantage (over the use of PF1) in terms of efficiency.
About the effects of strategies, furtheron, for all setups, Sxa (with H = mostRules and A = ) performs worse than Sx for x ∈ {1, 2}, but especially with DAB. Also for DAB setups, those using SAG are among the worst performing, while for setups with other advancement types those making use of SAG have performance comparable to the best.
DAB setups with BFS have slightly better performance than DFS setups, particularly with strategies S1a, S2a, and SAG. Our experiments suggest BFS to be avoided when non-conservative moves are often used (setups with DC and DS + strategies S2, S2a and S2b).
Comparison with abagraph. Table 9 shows our results for the admissible semantics with abagraph strategies. Figure 1 (x-axis indicates solving-time in seconds and y-axis number of instances solved) shows best and worst variants w.r.t. timeouts for: flexABle with DAB, flexABle with DABF, and abagraph. We also included the directly comparable strategies: SAG for flexABle and the default strategy for abagraph.
Clearly, flexABle with DABF significantly outperforms abagraph on any count. When
comparing flexABle with DAB and abagraph on the other hand several of the strategies of
abagraph have less time-outs, yet DAB setups with strategy S2 still clearly outperforms all
10http://robertcraven.org/proarg/experiments.html Last accessed on 1.7.22.
11We do not filter-out trivial instances, either derivable from empty assumptions or not derivable at all, as in other
work [
DABF
DC
DS
BFS abagraph strategies in terms of both timeouts and total solving time (115 and 26.08h in BFS variant). Also, as is most clearly seen in Figure 1, flexABle setups also with DAB solve instances faster on average than abagraph.
Approximate Reasoning. Table 10 shows surprisingly good results on accuracy, specificity, and sensitivity for approximate disputes for the combinations of pprop and popp values we considered. Figure 2 compares the rather representative run-time performance of static and dynamic bi-directional sampling for all considered values of p, as well as exact reasoning for the worstand best performing strategies for advancement types DAB and DABF and search type DFS. In general, we found little-to-no improvement in performance for DABF setups, yet some for DAB setups, especially using dynamic sampling.
Results for Complete and Stable Semantics. For DC + TC and DS + TS disputes we compared with an approach in which admissible assumptions congruous with the goal claim are searched for first and then extended to complete and stable sets. Results are in Table 11 and show that starting with DABF + TA provides better results. The patient strategy S1 performs better than S2 for the complete semantics, the opposite for stable.
Strategies have been defined for ABA disputes [
This research was partially funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 389792660 – TRR 248, and by the Bundesministerium für Bildung und Forschung (BMBF) Förderkennzeichen 01IS20056_NAVAS.