Argumentation games, which model reasoning as adversarial dialogue, ofer intuitive and explainable mechanisms for decision-making in AI. However, their implementation has lagged behind inference-focused approaches, particularly in structured argumentation frameworks like assumption-based argumentation (ABA). This work presents, to our knowledge, the first application of multi-shot answer set programming (ASP) for implementing argument games, focusing on ABA dispute derivations. Leveraging a recent rule-based representation of ABA disputes, our method combines a declarative program with lightweight script-based control of multi-shot aspects, yielding a modular and adaptable system. We extend this core approach to support alternative games and show how it can also be used to implement argument games for Dung's abstract argumentation formalism. Empirical results show that our implementation outperforms existing ABA dispute systems. We also introduce an approximate variant that further improves eficiency - reaching the level of the best current inference-focused ABA system - while maintaining perfect specificity (i.e. true negative rate), demonstrating the practical value of multi-shot ASP, particularly in interactive settings where explainability is key.
Argumentation plays a crucial role in human decision-making, especially in complex situations without clear-cut answers. Formal models of argumentation, rooted in research in non-monotonic reasoning, ofer argumentation approaches to knowledge representation and reasoning in AI. These models underpin a wide range of applications including in law, medicine, and e-governance.
Models of argumentation range from highly abstract to more detailed, structured approaches. Abstract models focus on the relationships between arguments – most notably, attacks – without considering their internal content. In contrast, structured models represent the internal composition of arguments, including premises and inference steps. Structured models are often viewed as concrete instantiations of their abstract counterparts.
On the reasoning side, a key distinction is between approaches that treat argumentation as inference –
focusing on selecting acceptable arguments under various semantics – and those that also consider the
argumentation process itself. Among the latter, argument-game approaches are prominent, modeling
reasoning as an adversarial dialogue between a proponent, who defends a claim, and an opponent,
who challenges it [
Research on eficient implementation methods in argumentation has largely focused on abstract
models, though structured models – despite their greater complexity – are gaining increasing attention.
In contrast, argumentation-game approaches have received relatively little attention in this regard. A
likely reason is that the reduction techniques successful in implementing argumentation-as-inference
(as evidenced by top-performing systems in the recent main argumentation competition-ICCMA’23 [
© 2025 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). are less readily applicable to game-based approaches, due to their iterative and potentially interactive nature.
Among reduction-based methods, those targeting answer set programming (ASP) are particularly popular. ASP is a declarative programming paradigm for knowledge representation and reasoning, ofering a concise, expressive rule-based language and eficient solvers. Its strengths in modularity and succinctness make it a powerful tool for modeling complex problems, with growing use in academia and industry.
In the standard approach to problem solving with ASP, valid solutions are specified through logic rules such that the answer sets of a program correspond to the solutions of the problem. A major computational bottleneck is the grounding phase, where variables are instantiated with constants to produce variable-free programs. This becomes especially costly in iterative scenarios, where similar but slightly modified programs must be re-grounded from scratch at each step.
Multi-shot ASP is a recent advancement that enables modifying and re-solving logic programs across
iterations, significantly reducing grounding and solving overhead [
This paper presents, to our knowledge, the first study of multi-shot ASP for argumentation, in
particular, for implementing argument games. Specifically, we focus on dispute derivations in
assumptionbased argumentation (ABA) [
We begin by very briefly introducing Dung’s AFs, ABA, and ASP programs, focusing on the syntax. We explain the aspects most relevant to our work in more detail (and provide examples) when turning to presenting the core ideas behind our approach in Section 3.
An abstract argumentation framework (AF) is a tuple ℱ = (, ), where is a set of (abstract)
arguments and ⊆ × denotes the attack relation. We say that 1 attacks 2 if (1, 2) ∈ . A
set of arguments ⊆ is said to be conflict-free if for no pair of arguments 1, 2 ∈ , 1 attacks 2.
An argument 1 ∈ is said to be defended from 2 ∈ by ⊆ , if 2 attacks 1 and there is an
argument 3 ∈ that, in turn, attacks 2. Finally, a set ⊆ is admissible if is conflict-free and
defends every argument ∈ from any argument attacking . All classical semantics introduced
in [
ABA frameworks add further structure to AFs. Concretely, an ABA framework ℱ consists of a tuple (ℒ, , , ℛ). Here, ℒ is the language underlying the framework. As in most work on implementations for ABA we restrict our attention to what is arguably also the most common instance of ABA: those frameworks for which ℒ is a finite set of propositional atoms. ⊆ ℒ are the set of assumptions. is the contrary relation associating to each ∈ its set of contraries ( ) ⊆ ℒ . ℛ is a set of rules of the form ℎ ← , where ⊆ ℒ and ℎ ∈ ℒ. is the body, while ℎ is the head of the rule. Again, following most work on implementations for ABA, we also restrict our attention to flat ABA, i.e. frameworks for which assumptions cannot appear in the heads of rules. This is also the instance of ABA which has been featured at the ICCMA competition since 2023.
Arguments in ABA are built by deriving claims from facts via the rules. I.e. the head ℎ of any rule ℎ ← ∅ with empty body is an argument with conclusion ℎ (such ℎ can be considered facts). Moreover, if 1, . . . , are arguments with conclusions ℎ1, . . . , ℎ and = ℎ ← { ℎ1, . . . , ℎ} ∈ ℛ, then the composition of 1, . . . , with is an argument with conclusion ℎ. Arguments are, thus, commonly represented as proof trees with nodes labelled by atoms, and the parent-child relation in the tree indicating that the atom labelling the parent node is in the body of a rule used to derive the child node. One argument attacks another if the first argument has as conclusion an atom which is a contrary of an assumption that is used in the second argument.
As explained in the introduction, disputes are a procedural means of deciding acceptance of an atom
(the goal claim) modelled after argumentation: the proponent must find an argument deriving the
goal claim and defend itself from the opponent by finding jointly consistent arguments attacking the
counter-arguments constructed by the opponent. The opponents role, on the other hand, is precisely to
ifnd counter-arguments to any argument constructed by the proponent. Whoever has the last word in
the dispute wins: i.e. if the opponent builds a counter-argument which the proponent cannot defend
against then the opponent wins, while the proponent wins if it finds defending arguments against
all counter-arguments of the opponent and the opponent cannot find any further counter-arguments.
The goal claim is deemed acceptable whenever there is a dispute for it which the proponent wins;
otherwise the goal claim is unacceptable. As we also indicated in the introduction, diferent versions
of disputes exist difering in the way arguments are represented and the semantics that they cover.
In this work we make use of the rule-based representation of disputes defined in [
For ASP we make use of the syntax of clingo [
Rules without variables are called ground. Rules with variables are shorthand for the set of ground rules obtained by uniformly replacing the variables in the (non-ground) rule with all constants occurring in the ASP program. If the rule is ground then it can informally be interpreted to mean that 0 must be derived, i.e. be part of a solution of the program, if 1, . . . , are derived and +1, . . . , + are not derived. Rules with empty bodies (of the form 0 :- .) are facts, while those with empty heads (of the form :- 1, . . . , , not +1, . . . , not +.) are integrity constraints. While the first indicate that 0 must be a part of all solutions, the second indicates that solutions that satisfy the body of the rule are not allowed. Formally, solutions to ASP programs, so called answer-sets, are distinguished sets of (ground) atoms given by the stable-model semantics.
To ease ASP programming, several extensions of the basic syntax have been defined. For instance, arithmetic expressions can be used in bodies of rules. Also, numbers and strings (enclosed in quotation marks) can be used as constants, while "_" represents an anonymous variable: an unnamed fresh variable whose scope is that of the rule where it is used. More significantly, conditional literals are extensions of literals and are written as :1, . . . , where and the s are positive or negated atoms. These express that should be included (e.g. in the body of a rule) whenever 1, . . . , are derived. They are particularly useful when combined with variables: for instance, ():() denotes all instances of () for which () is derived. Another construct we make use of are cardinality constraints of the form {1; . . . ; } = expressing that exactly of the conditional literals must be derived. For instance, {() : ()} = 1 means that from all of the instances of () for which () is derived, exactly one must be selected.
In multi-shot ASP [
In this section, we present our proposal for using multi-shot ASP to implement disputes. For ease of understanding and also show the flexibility of our approach, we first consider the simpler case of Dung’s AFs in Section 3.1, and then apply the same methodology to implement ABA disputes in Section 3.2. In Section 3.3 we present extensions for the stable semantics and visualisation purposes.
For Dung AFs we make use of the fact that these can also be captured in ABA and, thus, tackle a specialization of ABA disputes for AFs. Our multi-shot implementation comprises two components shown in Figure 1: the ASP encoding, and the Python script controlling multi-shot solving via the clingo API. The latter forms the backbone of our approach and will also be reused in the ABA implementation described in Section 3.2.
The implementation assumes an input AF instance and a designated argument whose acceptance is to be evaluated, both encoded as ASP facts. Given an argumentation framework ℱ = (, ), its ASP encoding is:
en(ℱ ) := {arg() | ∈ } ∪ {att(, ) | (, ) ∈ } The designated argument ∈ , referred to as the goal argument, is encoded as g().
The ASP encoding in Figure 1 is divided into three subprograms via lines 1, 5 and 17: 1) base: for initialization, 2) updateState(t): to update the internal state at each step, and 3) step(t): to select the next move. The updateState(t) and step(t) subprograms take the current dispute step number as a parameter.
1 #program base. 2 % initialize 3 m(0,p,G) :- g(G), not att(G,G), arg(G). 4 5 #program updateState(t). 6 defeat(t,C) :- m(_,p,P), att(P,C). % defeated 7 pm(t,p,P) :- m(_,o,O), att(P,O), not defeat(_,P), 8 not m(_,p,P), not att(P,P), 9 not att(P,D1) : m(_,p,D1). % possible p. move 10 pm(t,o,O) :- m(_,p,P), att(O,P), not defeat(_,O), 11 not m(_,o,O). % possible o. move 12 end(t,p) :- g(G), m(_,p,G), not pm(t,o,_), 13 defeat(_,O1) : m(_,o,O1). % p. won 14 end(t,o) :- not pm(t,p,_), m(_,o,O), 15 not defeat(_, O). % opp. won 16 17 #program step(t). 18 m(t,o,A) :- pm(t-1,o,A). 19 { m(t,p,A) : pm(t-1,p,A) } = 1 :- not pm(t-1,o,_). 20 21 #show m/3.
1 from clingo import Control , Number as N 2 Function as F 3 def main ( instance , base_code , encoding ): 4 ctl = Control () 5 ctl . load ( instance ) 6 ctl . load ( encoding ) 7 ctl . add (" base ", [] , base_code ) 8 ctl . ground ([( " base ", ())]) 9 t = 0 10 while True : 11 ctl . ground ([( " updateState " ,[N(t )])]) 12 p_win = (F(" end " ,[N(t),F("p")]) , True ) 13 res = ctl . solve ( assumptions =[ p_win ], 14 on_model = print ) 15 if res . satisfiable : 16 return True 17 o_win = (F(" end " ,[N(t),F("o")]) , False ) 18 res = ctl . solve ( assumptions =[ o_win ]) 19 if res . unsatisfiable : 20 return False 21 t += 1 22 ctl . ground ([( " step " ,[N(t )])])
At an abstract level, a dispute is a sequence of moves. For AFs, each move consists of a player – proponent or opponent, represented by constants p and o (the colors are for ease of reading) – choosing an argument to play. The key predicate is m/3, representing a move with parameters: step number, player, and chosen argument. The predicate pm/3, on the other hand, indicates available moves at a given step.
The base subprogram is grounded at the start, initiating the dispute with the proponent playing the goal argument at step 0, provided it is consistent (i.e., it does not attack itself).
The updateState(t) subprogram updates the internal state at each step t using auxiliary predicates. The predicate defeat/2 collects all arguments attacked by the proponent so far (the "defeated" arguments). In Line 7, possible proponent moves are determined. A valid proponent move must (i) counter an opponent’s argument, (ii) not be defeated, (iii) not have been used before by the proponent, (iv) be consistent, and (v) not attack other proponent arguments. In Line 10, opponent moves are derived. These must (i) attack a proponent’s argument, (ii) not be defeated, and (iii) not have been used already by the opponent.
The rules in Line 12 and Line 14 define the end/2 predicate, indicating whether the game has been won. The proponent wins if (i) the goal is among their arguments, (ii) the opponent has no more available moves, and (iii) all opponent arguments have been defeated. It is easy to see that if the proponent wins, their argument set corresponds to an admissible extension as per Section 2. The opponent wins if (i) the proponent has no available moves and (ii) at least one undefeated opponent argument remains.
The step(t) subprogram selects the next move. Disputes branch only at proponent moves, as admissibility requires the opponent to play all possible counter-attacks to a proponent’s argument. Conversely, for each opponent move, the proponent must select one counter-argument. For eficiency (though this is easy to adapt), the encoding prioritizes opponent moves, performing all available opponent moves at each step (Line 18). A proponent move is selected only when no opponent moves are possible (Line 19).
The #show directive at the end of Figure 1 simply indicates which atoms are shown when printing the answer-sets. Concretely, the atoms indicating the moves made at each step are shown.
We now turn to the Python control script presented in Figure 1 (right). The main function (Line 3) takes three arguments: the ASP encoding of the input AF, a base program for initialization, and the main encoding for the argumentation formalism (e.g., the ASP code in Figure 1, left). The base program ofers additional flexibility and control. For Dung’s AFs, for instance, it is used to specify the goal 2 e 1 c 0 d 0 a argument of the dispute in a short ASP program, such as that containing the fact g() for a given goal argument .
Once the encodings are loaded, the base subprogram is grounded – this includes grounding the input framework as well as the goal directive. The step counter t is then initialized to 0.
The main loop begins in Line 10, where the subprogram updateState(t) is grounded for the current step t. In Line 12, an assumption is constructed – this is a pair consisting of a literal and a truth value. For a given step t = , the assumption (end(,p), True) is created, asserting that the proponent has won at step . This assumption is passed to the solver to constrain answer sets accordingly. If the solve is successful, this indicates that a dispute of length exists in which the proponent wins.
If the solve fails, the script proceeds to Line 17, where the assumption (end(, o), False) is created. This assumption asserts that the opponent has not won at step (i.e., there is at least one answer set which does not contain end(, o), meaning also that the proponent has not yet lost and the dispute may continue). If this second solve also fails, it implies that - regardless of the move the proponent makes at step - they will loose to the opponent and, hence, the procedure can terminate.
If neither condition holds, the search proceeds: t is incremented, a new move is selected via the step(t) subprogram (Line 22), and the next iteration begins. Figure 2 provides the visualisation of a dispute for an exemplary AF generated by our system MS-DIS1 (using the listings from Figure 1).
To implement ABA disputes our approach is the same as that presented in Section 3.1. In particular, Figure 1 (right) continues to serve as the Python script controlling the multi-shot execution. The only diference lies in the inputs provided to this script.
Given an ABA instance ℱ = (ℒ, , , ℛ), its encoding as a set of ASP facts is defined as follows: ∪ en(ℱ ) := {assumption() | ∈ } ∪ {contrary(, ) | (, ) ∈ } ⋃︁
{head(, ℎ)} ∪ {body(, ) | ∈ }
The goal of the dispute is a statement ∈ ℒ that is to be justified dialectically. This is encoded as g(). For ABA, further inputs (which we will explain shortly) are facts encoding the termination condition and the advancement type. For the dispute for the admissible semantics these are "tt(ta)." and "at(dabf)." respectively.
The multi-shot ASP encoding for ABA disputes is shown in Figure 3. As with the encoding for AF disputes, the program is divided into three sub-programs: base, updateState(t), and step(t), each fulfilling the same roles as in the AF encoding.
At the most abstract level, ABA disputes also consist of a sequence of moves. The main diference compared to disputes for AFs is that each move now involves one of the players – the proponent or 1https://github.com/gorczyca/MS-DIS
=ℎ← ∈ℛ the opponent (represented by the constants p and o as in the AF encoding) – putting forward either an assumption or a rule from the ABA framework. Thus, what is explicitly constructed is a rule set for each player, consisting of the assumptions and rules they have played. When a rule is played by a player, each statement in the rule’s body and head is also considered as played by that player. For the proponent, this amounts to committing to the rule and its associated statements; for the opponent, it reflects an exploration of a possible line of attack against the proponent’s commitments. To avoid redundancy, the proponent’s rule set is considered a subset of the opponent’s rule set.
The rule sets determine, in an implicit manner, the arguments available to each player: these are exactly the arguments that can be constructed from the rules and claims contained in their rule set. Hence, the proponent’s arguments are those derivable from the proponent’s rule set, while the opponent’s arguments include all arguments derivable from their own rule set, which subsumes that of the proponent.
The fact that players in ABA disputes put forward both rules and assumptions allows us to distinguish between diferent types of moves. In the encoding given in Figure 3, we distinguish between eight move types, represented by the constants pb1, pb2, pf1, pf2, ob1, ob2, of1 and of2. Proponent move types begin with p, and opponent move types begin with o. The letters b and f stand for "backward" and "forward", respectively.
The backward moves pb1 and ob1 are used to justify a claim already in the player’s rule set by introducing a rule ℎ ← such that ℎ = . Conversely, the forward moves pf1 and of1 add a rule ℎ ← when its body is in the player’s current claim set.
The backward moves pb2 and ob2 are used to attack an assumption of the opposing player by introducing a rule ℎ ← such that ℎ ∈ (). Finally, the forward moves pf2 and of2 introduce an assumption 1 ∈ (2), provided that 2 is an assumption in the opposing players claim set.
We refer to all move types that involve rules (i.e., all except pf2 and of2) as rule move types, and they are declared using the predicate rMT/1. Among the proponent’s moves, all except pf1 are considered branching, and are denoted using the branchMT/1 predicate. As in the case of AF disputes, only the proponent can introduce branching in the search for a winning dispute. The reason why pf1 is not branching is that it simply derives consequences from claims the proponent has already committed to. Therefore, pf1 does not introduce a choice point, but rather derives consequences that follow from previous choices.
Moves in ABA disputes are encoded via the predicate m/4, which now takes four arguments to represent (i) the dispute step, (ii) the player, (iii) the move type, and (iv) the rule or assumption involved in the move. Specifically, m(t,P,T,X) encodes a move made at turn t, by player P, of type T. If T is a rule move type (i.e., rMT(T) holds), then X refers to the rule’s identifier; otherwise, it refers to the assumption introduced.
As in the AF encoding, possible moves are defined via the predicate pm/4, which also now has arity 4. To track the evolving rule sets of each player, we use the auxiliary predicates stS/3 and stR/4. The predicate stS(t,S,P) denotes that statement S has been used by player P at step t. Similarly, stR(t,P,h,r) records that a rule = ℎ ← has been used by player P at step t.
Turning now from the predicates used to the encoding itself, as in the encoding for AFs, the base and updateState(t) subprograms define various auxiliary predicates that are used to constrain the possible moves available to the proponent and opponent at each step. The actual move to perform is selected by the step(t) subprogram.
The base subprogram, which is grounded at the start, defines in lines 2 to 4 the rule move types and branching move types, as well as the players (via the plr/1 predicate). In lines 5 and 6, all statements appearing in rules are collected using the rS/2 predicate. In Line 7, the dispute is initialised by adding the goal statement to both the proponent and opponent rule sets, provided the goal is not an inconsistent assumption. In Line 8, the remBloR/4 predicate – encoding rules that are initially blocked for the proponent – is populated with those rules that are inconsistent.
The updateState(t) subprogram, as in the AF case, updates the internal state of the dispute. Lines 11 and 12 define the so-called defences and culprits: defences are assumptions to which the proponent is committed, while culprits are assumptions contrary to some claim in the proponent’s rule set (i.e. these 1 #program base. 2 rMT(pb1;pb2;pf1;ob1;ob2;of1). % rule move types 3 branchMT(pb1;pb2;pf2). % branching (br.) move types 4 plr(p;o). % players; proponent (p.) and opponent (o.) 5 rS(R,S) :- head(R,S). % rule’s statements from rule heads 6 rS(R,S) :- body(R,S). % rule’s statements from rule bodies 7 stS(0,S,P) :- g(S), not contrary(S,S), plr(P). % goal - initial statement 8 remBloR(0,R,H,p) :- head(R,H), rS(R,S1), rS(R,S2), contrary(S1,S2). % blocked, inconsistent rules 9 10 #program updateState(t). 11 def(t,D) :- stS(_,D,p), assumption(D). % defence 12 cul(t,C) :- stS(_,S,p), contrary(C,S). % culprit 13 defCtr(t,DC) :- def(_,D), contrary(D,DC). % defence contrary 14 culCtr(t,CC) :- cul(_,C), contrary(C,CC). % culprit contrary 15 16 remR(t,R,H,P) :- not stR(_,R,H,P), head(R,H), plr(P). % remaining player’s rule 17 remBloR(t,R,H,P) :- remR(t,R,H,P), body(R,B), cul(_,B), plr(P). % blocked remaining player P.’s rule 18 remBloR(t,R,H,p) :- remR(t,R,H,p), rS(R,S), defCtr(_,S). % blocked remaining p.’s rule 19 20 unexpS(t,H,p) :- stS(_,H,p), not stR(_,_,H,p). % unexpanded statement 21 stExpS(t,H,o) :- stS(_,H,o), remBloR(_,R,H,o) : remR(t,R,H,o). % fully expanded statement 22 stBloS(t,S,o) :- stS(_,S,o), cul(_,S). % state blocked statement 23 stBloS(t,S,o) :- stExpS(t,S,o), not assumption(S), stBloR(t,R,S,o) : stR(_,R,S,o). 24 stBloR(t,R,H,o) :- stR(_,R,H,o), body(R,B), stBloS(t,B,o). % state blocked rule 25 26 comS(t,S,p) :- def(_,D). % complete statement 27 comS(t,H,p) :- stR(_,R,H,p), comS(t,S,p) : body(R, S). 28 unbloComS(t,S,o) :- stS(_,S,o), assumption(S), not cul(_,S). % unblocked complete (unb. com.) statement 29 unbloComS(t,H,o) :- stS(_,H,o), not stBloS(t,H,o), unbloComR(t,_,H,o). 30 unbloComR(t,R,H,o) :- stR(_,R,H,o), not stBloR(t,R,H,o), unbloComS(t,B,o) : body(R, B).% unb. com. rule 31 unbloSupSS(t,S,o) :- stS(_,S,o), contrary(D,S), def(t,D), not stBloS(t,S,o).% unb. statements support. S 32 unbloSupSS(t,S,o) :- stS(_,S,o), not stBloS(t,S,o), unbloSupSR(t,R,_,o), body(R, S). 33 unbloSupSR(t,R,H,o) :- stR(_,R,H,o), not stBloR(t,R,H,o), unbloSupSS(t,H,o).% unb. rules supporting S 34 culCan(t,C) :- assumption(C), unbloSupSS(t,C,o). % culprit candidate 35 36 pm(t,p,pb1,R) :- remR(t,R,H,p), not remBloR(_,R,H,p), unexpS(t,H,p). % possible move (pm) "PB1" 37 pm(t,p,pb2,R) :- remR(t,R,H,p), not remBloR(_,R,H,p), culCan(t,C), contrary(C, H), not stS(_,H,p), 38 not contrary(D, H) : def(_,D). % pm "PB2" 39 pm(t,p,pf1,R) :- remR(t,R,H,p), not remBloR(_,R,H,p), comS(t,B,p) : body(R, B). % pm "PF1" 40 pm(t,p,pf2,A) :- culCan(t,C), contrary(C,A), assumption(A), not stS(_,A,p), not contrary(A,A), 41 not cul(_,A), not contrary(D,A) : def(_,D). % pm "PF2" 42 pm(t,o,ob1,R) :- remR(t,R,H,o), not remBloR(_,R,H,o), unbloSupSS(t,H,o). % pm "OB1" 43 pm(t,o,ob2,R) :- remR(t,R,H,o), not remBloR(_,R,H,o), contrary(D, H), def(_,D). % pm "OB2" 44 pm(t,o,of1,R) :- remR(t,R,H,o), not remBloR(_,R,H,o), unbloComS(t,B,o) : body(R, B). % pm "OF1" 45 pm(t,o,of2,A) :- contrary(D,A), def(_,D), assumption(A), not stS(_,A,o). % pm "OF2" 46 47 stS(t,S,P) :- m(_,p,T,R), rMT(T), rS(R,S), plr(P). % new state statement 48 stS(t,A,P) :- m(_,p,T,A), not rMT(T), plr(P). 49 stS(t,S,o) :- m(_,o,T,R), rMT(T), rS(R,S). 50 stS(t,A,o) :- m(_,o,T,A), not rMT(T). 51 stR(t,R,H,P) :- m(_,p,T,R), head(R,H), rMT(T), plr(P). % new state rule 52 stR(t,R,H,o) :- m(_,o,T,R), head(R,H), rMT(T). 53 54 term(t) :- tt(ta), g(G), comS(_,G,p), comS(_,CC,p) : culCtr(_,CC); 55 not unbloComS(t,DC,o) : defCtr(_,DC). 56 end(t,p) :- term(t), not pm(t,o,_,_). % p. won; termination condition satisfied and o. cannot move 57 end(t,o) :- not term(t), not pm(t,p,_,_). % o won; term. cond. not satisfied and p. cannot move 58 59 #program step(t). 60 m(t,P,T,X) :- pm(t-1,P,T,X), not branchMT(T), t > 0. % proceed with non-br. move type 61 { m(t,P,T,X) : pm(t-1,P,T,X) } = 1 :- t > 0, branchMT(T) : pm(t-1,_,T,_). % choose one br. move 62 63 #show m/4. are attacked by the proponent). Lines 13 and 14 then define the contraries of defences and culprits.
In Line 16, the predicate remR/4 gathers the remaining rules for each player, i.e., rules not yet used. The subsequent lines define the subset of these that are blocked. For both players (Line 17), rules are blocked if they contain a culprit in the body – i.e., assumptions that are attacked by the proponent. Additionally, for the proponent, rules that contain the contrary of a defence in their body are also blocked, as they would render the proponent’s rule set inconsistent.
In Line 20, the predicate unexpS/3 identifies unexpanded statements within the proponent’s rule set: statements for which no rule has yet been introduced that justifies them. Conversely, in Line 21, the predicate stExpS/3 identifies fully expanded statements in the opponent’s rule set – those for which all matching-head rules are blocked. The next lines then define the opponent’s blocked statements: either culprits (Line 22), or non-assumption statements for which all rules with a matching head are blocked (Line 23). A blocked rule (stBloS/4), defined in Line 24, is any rule that contains a blocked statement in its body.
Lines 26 and 27 define the complete statements of the proponent: every defence is a complete statement, as is any statement derivable via rules whose body is composed entirely of other complete statements. These capture the statements for which the proponent has complete arguments. The opponent’s analogous notions – unblocked complete statements (unbloComS/3) and unblocked complete rules (unbloComR/4) – are defined in Line 28-30. These represent statements and rules that are part of 4 t xd 4 t xd 2 xa complete arguments of the opponent and that are not attacked by the proponent.
Lines 31-33 identify unblocked supporting statements and rules of the opponent (unbloSupSS/3, unbloSupSR/4), i.e. those that contribute to justifying a contrary of a defence. These support the identification of culprit candidates in Line 34 – assumptions that appear in such justifications. Since these assumptions are part of a potential attack on the proponent, they become potential targets for counter-attack.
Lines 36-45 define the possible moves to choose from at step t. These are: • pb1 – the proponent introduces a rule ℎ ← with head ℎ = to justify a currently unexpanded statement in their rule set, provided ℎ ← is non-blocked and unused. • pb2 – the proponent introduces a rule ℎ ← whose head is contrary to a culprit candidate, such that ℎ ← is consistent, non-blocked, unused, and does not attack any defences. • pf1 – the proponent introduces an unblocked rule ℎ ← whose body consists of complete statements, thus allowing the derivation of the new claim ℎ. • pf2 – the proponent introduces an assumption ¯ that is the contrary of a culprit candidate and ¯ is consistent, unused, not itself a culprit, and does not attack any defences. • ob1 – the opponent introduces a rule ℎ ← with head ℎ = , where is a statement contributing to an argument attacking a defence, and ℎ ← is non-blocked and unused. • ob2 – the opponent introduces a rule ℎ ← whose head is contrary to a defence, provided ℎ ← is non-blocked and unused. • of1 – the opponent introduces a rule ℎ ← whose body is composed solely of unblocked complete statements, thereby reinforcing or extending attacks on the proponent. • of2 – the opponent introduces an assumption ¯, provided it is the contrary of a defence and has not yet been used.
Lines 47-52 then extract the statements and rules used in the selected move and add them to the respective player’s rule set, ensuring that the opponent also has access to any rule or statement used by the proponent.
Finally, Line 54 defines the termination condition for admissible semantics ( ta): the dispute terminates successfully if (i) the goal is a complete statement of the proponent (i.e. the proponent has a complete argument for the goal), (ii) all culprits are complete statements (the proponent has complete arguments for all statements used to attack the opponent), and (iii) no contrary of a defence is an unblocked complete statement (all arguments of the opponent attacking the proponent are blocked, i.e. in turn attacked by the proponent). If this condition holds and no further opponent moves are possible, the proponent wins (Line 56); if the condition fails and the proponent has no remaining moves, the opponent wins (Line 57).
As in the encoding for AFs, the step(t) subprogram selects the next move, giving precedence to non-branching moves. Only if no such move is applicable will a single branching move among the available branching types be selected. Finally, the #show directive indicates that when printing the answer sets only the atoms encoding selected moves at each step are shown.
1 #program updateState(t). 2 % add another option to perform "PF2" move 3 pm(t,p,pf2,A) :- at(ds), assumption(A), 4 not cul(_,A), not stS(_,A,p), 5 not contrary(A,A), 6 not contrary(D,A) : def(_,D). 7 8 % define: remaining assumptions 9 % - neither defences, nor culprits 10 remA(t,A) :- tt(ts), assumption(A), 11 not def(_,A), not cul(_,A). 12 13 % modify termination criteria: 14 term(t) :- tt(ts), g(G), comS(_,G,p), 15 comS(_,CC,p) : culCtr(_,CC); 16 not unbloComS(t,DC,o) : defCtr(_,DC); 17 not remA(t,A) : assumption(A). 18 % require no assumption be remaining 1 graph(m). 2 graph((A,l),m) :- arg(A). 3 node(A,(A,l)) :- arg(A). 4 edge((A,B),m) :- att(A,B). 5 6 attr(node,A,fillcolor,"green") :- m(_,p,A). 7 attr(node,A,fillcolor,"yellow") :- m(_,o,A). 8 attr(graph,(A,l),label,T) :- m(T,_,A). 9 10 ldefeat(Tm,A) :- defeat(Tm,A), not m(_,_,A), 11 Tm = #min { T : defeat(T,A) }. 12 attr(graph,(A,l),label,Tm) :- ldefeat(Tm,A). 13 attr(node,A,fillcolor,"red") :- ldefeat(_,A). 14 15 lpm(Tm,P,A) :- pm(Tm,P,A), not m(_,_,A), not defeat(_,A), 16 Tm = #max { T : pm(T,_,A) }. 17 attr(graph,(A,l),label,T) :- lpm(T,_,A).
18 attr(node,A,fillcolor,"lightblue") :- lpm(_,_,A).
Two steps of a dispute as generated by our system MS-DIS for an exemplary ABA framework is shown in Figure 4. This shows the rule-based representation which consists in the graph of dependencies and attacks among rules, together with labels (via colors) indicating the status of statements and rules at the dispute state. The corresponding argument-based representation is shown in Figure 5.
One of the main advantages of the ASP-based approach is its modularity: adding new functionalities
often requires only small, local modifications. This section illustrates this extensibility with two
examples: first, we show how to adapt the ABA dispute encoding to support stable semantics, and
second: we demonstrate how to obtain a graphical representation of AF disputes, utilizing clingraph.
Stable semantics. Figure 6 (left) shows a code fragment extending Figure 3 for the stable semantics.
For a goal statement , the proponent wins the dispute if a stable extension exists containing an argument
for . The proponent’s defence set in such a case corresponds to a set of stable assumptions [
Graphical representation. Figure 6 (right) shows how a graphical representation of disputes – here
for AFs – can be generated with just a few lines of ASP code using clingraph [
The code listings in Section 3 are part of our system MS-DIS, which implements dispute derivations
for both AFs and ABA. The system supports both automatic and interactive modes and includes a
visualization component. In automatic mode, given a claim and an ABA framework (or an argument
and an AF), the system attempts to construct a winning dispute for the proponent. In interactive mode,
the user is guided through the dispute process, with the system presenting available moves at each step
and updating the dispute state based on the selected move. The visualization component is implemented
using clingraph [
In our experiments, we focus on the implementation of MS-DIS (version 1.0) for ABA and, specifically, on the eficiency of its automatic mode. Since the automatic and interactive modes can also be interleaved, the results are relevant beyond the purely automatic setting.
We consider four aspects: (1) the performance benefit of the multi-shot approach; (2) comparison with previous implementations of ABA disputes; (3) comparison with the most eficient inference-oriented (i.e. also not dispute-based) system for ABA; and (4) the use of approximation within MS-DIS.
As to (1), we compare the multi-shot variant of MS-DIS – our main approach – with a naïve oneshot iterative version that restarts grounding and solving from scratch at each step. For a given step number , the first solver call checks whether the proponent can win within steps, and the second whether the search should continue. These correspond to lines 13 and 18 in Figure 1 (right).
As to (2), we compare MS-DIS with flexABle (version 1.0), which implements rule-based dispute
derivations for ABA as proposed in [
As to (3), we compare MS-DIS to aspforaba [
As to (4), we evaluate a step-bounded approximation mode of MS-DIS, where a winning dispute
is returned only if found within a fixed step limit; otherwise, the instance is deemed unsatisfiable.
We test bounds of 5, 10, and 25 steps. This ensures 100% specificity (true negative rate), allowing a
fair comparison with an approximate mode of flexABle ofering similar guarantees. In flexABle,
approximation is achieved by restricting the opponent to a randomly selected subframework [
For our experiments, we use the ICCMA’23 ABA benchmarks [
aspforaba flexABle
MS-DIS a=5 aspforaba # t-out. time [h] # t-out. # inc. time [h] % acc. % acc. t 350 250 200 150
In our experiments both MS-DIS and aspforaba make use of the ASP solver clingo [
The results of our experiments are summarized in Figure 7. MS-DIS, in the exact (i.e. non-approximate), multi-shot variant solved 36 more instances than flexABle and took 5 hours less of total solving time. Interestingly, even the naïve iterative MS-DIS variant performs slightly better than flexABle.
Regarding approximate methods, we find MS-DIS to outperform flexABle across nearly all metrics. For instance, an approximation with an upper bound of 10 steps in MS-DIS results in significantly fewer timeouts compared to flexABle with 25% sampling (81 timeouts for MS-DIS versus 146 for flexABle in the instances in the bottom half of the table). Additionally, MS-DIS achieves greater accuracy (90% compared to 71%, excluding timeouts; 71% compared to 44%, including timeouts) and a shorter total solving time (19 hours versus 25 hours). Notably, setting the upper bound to 25 steps guarantees 100% accuracy (excluding timeouts), suggesting that successful disputes rarely require more than 25 steps, regardless of the framework size.
By sacrificing accuracy, MS-DIS approaches the performance of aspforaba, and with a 5-step bound, it can even surpass aspforaba – albeit with an approximate accuracy of 60%. This highlights a potential niche for dispute-based systems, even when the primary goal is merely to determine the acceptance of claims. In particularly hard instances, executing a bounded dispute (especially with human-in-the-loop guidance) may yield more insight than receiving a time-out from systems such as aspforaba.
To the best of our knowledge, this is the first study of multi-shot solving for argument games, focusing on disputes in ABA and AFs. Our prototype, MS-DIS, outperforms existing dispute ABA systems, and its approximate variant matches the eficiency of the leading inference-focused ABA system – showing the benefits of the approach, especially when interaction and explanation are needed. More generally, our modular encodings and modern ASP systems suggest that multi-shot solving can serve as a common basis for implementing and comparing argument games. As shown for AFs and ABA, the control components (Figure 1-right) are reusable across two-player games, while the ASP modules for initialization (base), state updates (updateState(t)), and move selection (step(t)) must be adapted. We envision developing a library of encodings for argument games in diverse formalisms.
This work was supported by funding from BMFTR within projects SEMECO (grant no. 03ZU1210B), KIMEDS (grant no. GW0552B), and MEDGE (grant no. 16ME0529).
The authors used ChatGPT in order to: paraphrase and reword. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.