A system for reasoning about acceptance in structured argumentation via abstract argumentation

The aba2af system is developed by the Constraint Optimization and Reasoning Group at Department of Computer Science, University of Helsinki. The system is implemented by Tuomo Lehtonen.


Abstract argumentation frameworks (AFs) are a simple and powerful argumentation formalism. An AF consist of arguments and attacks between arguments. AFs are represented as directed graphs where arguments are vertices and attacks are edges. Assumption-based argumentation (ABA) is a form of structured argumentation, where the arguments are not just given, but their structure is explicit. In ABA, arguments are built from assumptions using rules. Attacks between arguments are determined by contraries, of which each assumption has one. ABA is in many senses an extension of abstract argumentation and queries about the acceptabilty of sentences in ABA under many semantics can be answered by translating the ABA framework to an AF and solving a corresponding reasoning task in the AF. This system does that translation, producing the necessary files which can be inputted to an ASP solver in order to answer the query.

More details on the approach implemented in aba2af can be found in [1]. Please use [1] as the main reference for aba2af.


aba2af supports

  • answering credulous and skeptical queries about acceptability of sentences in ABA under admissible, preferred and stable semantics via a translation from ABA to AF

The underlying ASP solver clingo is available here. Newest version checked to work with our format is 4.5.4.


USAGE: aba2af -f (arg) -r (arg) -s (arg) [-e] [-h]

 -f,--file (arg)             Input file defining the ABA framework
 -r,--reasoning-task (arg)   Reasoning task (cred | skept)
 -s,--semantic (arg)         Semantic (adm | prf | stb)

 -e,--enumeration-mode       If set, the program prints the AF instance
                             file and full query files for all queried
                             sentences, even if they could be trivially
 -h,--help                   Display help message and exit
 -a,--arguments-file         If set, a file showing the contents of each
                             AF argument is produced

Input format

In the input file defining an ABA framework, the following lines are recognized:

myAsm(X).              :  X is an assumption
contrary(X, Y).        :  Y is the contrary of (assumption) X
query(X).              :  We wish to query the acceptability status of X

Below are the contents of a well-formatted input file, named example.txt:


contrary(a, x).
contrary(b, y).
contrary(c, z).

myRule(x, []).
myRule(y, [b]).
myRule(z, [a,c]).



aba2af will produce the following files.

  • AF input file of the form afinput_(filename).dl, where filename is the name of the ABA input file with extension(s) ignored. Defines the AF framework with arguments: "arg(N)." and non-attacks: "natt(N,M).". Not produced if all the queried sentences are trivially decided and flag -e is unset.
  • Query file(s) of the form query_(filename)_(sentence).dl where filename is as above and sentence the queried sentence. One of these is created for each queried sentences.
  • If flag -a is set, a file mapping the arguments (represented by numbers in the AF files) to the sentences containing them.

Answering queries

For credulous queries, the answer to the query is true iff the ASP query -- defined by the semantic encoding, an AF input file and a query file -- is satisfiable. For skeptical reasoning under admissible semantics the program will simply output the answer, as this task is polynomial time solvable. For other skeptical queries, the opposite to credulous holds, i.e. the query is true iff the ASP query is unsatisfiable. This is because for skeptical queries, we are looking for counterexamples. There are special cases which are noted as comments in the query files. All of the special cases can be decided as outlined above, but taking them into account can make solving faster if the goal is to simply answer a true/false query instead of enumerating all extensions. For these special cases, please refer to [1].


For the above-mentioned file example.txt, calling

aba2af -s adm -r cred -f example.txt

will produce four files:

afinput_example.lp      :  Defines the arguments and attacks
query_example_x.lp      :  Defines the query for x
query_example_y.lp      :  Defines the query for y
query_example_c.lp      :  Defines the query for c

Now running for each query

clingo adm-dual.lp afinput_example.lp query_example_(sentence).lp

we find out that the query for x is satisfiable, i.e. x is credulously accepted under admissible semantics, as is c, but not y.

Here "adm-dual.lp" is the encoding file defining admissible semantics in terms of non-attacks. You can find it below.

To enumerate all extensions, put 0 at the end of the clingo call.

Flag -e

The difference the flag -e makes can now be illustrated. If it is unset, query_example_x.lp contains the following line:

% Queried sentence is derivable from empty body and therefore accepted

However, when set, the file will contain two lines:

% Queried sentence is derivable from empty body and therefore accepted
:- not in(0).

(0 being the only argument containing x and the second line asserting that not in(0) must be false, i.e. 0 must be in the extension)

In addition, if x were the only queried sentence (and flag -e not set), the file afinput_example.lp would not be produced at all.


Version 2017-07-21 of aba2af is available here. See README for instructions.

ASP encodings for admissible, preferred and stable semantics defined with non-attacks instead of attacks.


[1] From Structured to Abstract Argumentation: Assumption-Based Acceptance via AF Reasoning.
Tuomo Lehtonen, Johannes P. Wallner, and Matti Järvisalo.
in ???,editors, Proceedings ofthe 14th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2017), volume ????? of Lecture Notes in Computer Science, pages ???-???. Springer, 2017.
[doi:???] [pdf] [abstract/bibtex]