Welcome to EqArgSolver

Thank you for your visit

EqArgSolver is a program used in the computation of solutions to decision and enumeration problems under several argumentation semantics.

EqArgSolver is implemented by Odinaldo Rodrigues in C++ and uses a number of recent advances in the computation of argumentation semantics including the discrete version of the Gabbay-Rodrigues Iteration Schema and a new algorithm for computation of extensions (to be published).

Given an argumentation network <S,R>, GRIS can be used to compute one or all of the extensions of the network under the grounded, complete, preferred and stable semantics as well as to decide whether an argument X of S is accepted in one or all of the extensions under one of these four semantics.

Argumentation problems must be submitted to EqArgSolver using probo's syntax (whose basic usage can be found here). The input argumentation framework must be supplied as a file in the trivial graph format (TGF), which is basically a text file containing a sequence of node designators one per line, followed by the separator “#” in its own line, and then followed by a list of pairs of nodes, a pair per line, where the first element of each pair is the source of an edge in the graph (the attacker) and the second element is its target (the node being attacked).

Basic usage

EqArgSolver must be invoked from the command line. In Windows, run a terminal window by right-clicking “Start” then typing “cmd” and then invoking EqArgSolver as detailed below. For linux, simply type eqargsolver in any terminal window.

Running EqArgSolver

<command> -f <inputfile> -p <problem> -fo tgf [-a <argumenttocheck>]

where command is one of eqargsolver (linux 64-bit); eqargsolver32.exe (Windows 32-bit); or eqargsolver64.exe (Windows 64-bit); inputfile is an input file in the TGF file format; and problem is one of
  • SE-σ: compute one extension under semantics σ
  • EE-σ: compute all extensions under semantics σ
  • DC-σ: decide whether argumenttocheck is accepted in some extension under semantics σ (decide credulously)
  • DS-σ: decide whether argumenttocheck is accepted in all extensions under semantics σ (decide skeptically)
Valid values for σ are: GR (grounded), CO (complete), PR (preferred) and ST (stable). For single extension semantics, such as the grounded semantics, only SE-GR and DC-GR are available.

For example, consider the argumentation framework of Figure 6.2 (taken from “Efficient Computation of Argumentation Semantics”, by Beishui Liao, page 72):

Its TGF representation is as follows (click here to download this file):

a1
a2
a3
a4
a5
a6
a7
a8
a9
a10
#
a1 a2
a2 a1
a2 a5
a2 a3
a3 a4
a4 a5
a5 a6
a6 a5
a7 a6
a7 a7
a8 a7
a9 a8
a10 a9


To calculate all preferred extensions of this network, invoke eqargsolver as follows (linux version assumed):

./eqargsolver -f f6.2.tgf -fo tgf -p EE-PR

EqArgSolver will return
[[a10,a2,a4,a6,a8],[a1,a10,a3,a6,a8],[a1,a10,a3,a5,a8]]
indicating that the sets with arguments [a10,a2,a4,a6,a8]; and [a1,a10,a3,a6,a8]; and [a1,a10,a3,a5,a8] correspond to all the preferred extensions of this network.

Similarly, notice that a10 is accepted in all preferred extensions; a2 is accepted in one of the preferred extensions but not all; and a9 is not accepted in any preferred extenstions. Therefore, the following invokations of EqArgSolver would produce the corresponding results below.

-a -p DC-PR -p DS-PR
a10 Yes Yes
a2 Yes No
a9 No No

Limitations

EqArgSolver is not currently able to handle very large problems in the preferred semantics. By large we mean a network with a large number of nodes in a single SCC, or a network with a large number of non-trivial SCCs, or a combination of these, especially if these SCCs appear close to a source node in the network induced by the SCCs. EqArgSolver has successfully run is less complex networks with up to 2,500,000 arguments.

The two papers below describe EqArgSolver in some detail, although improvements are regularly made to the solver.

Downloading EqArgSolver

EqArgSolver has been submitted to the 2nd International Competition on Computational Models of Argumentation, but it is not yet avalable for general distribution. Public distribution will be available late in 2018. In the meantime, you can request a copy directly to odinaldo.rodrigues@kcl.ac.uk.

System description

EqArgSolver works as described in the picture below.

Overall execution behaviour

Development path

EqArgSolver is used as a laboratory for experimentation with algorithms for argumentation reasoning and as such is continually being updated.

The latest version uses an improved version of the algorithm described here, fixes some bugs found after the ICCMA 2017 competition, and includes some general improvements in performance.

In the Summer 2018, we will be implementing a framework to make EqArgSolver available through the Internet as a web page and a web service.