aba2afA system for reasoning about acceptance in structured argumentation via abstract argumentationThe 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. AboutAbstract 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. Featuresaba2af supports
The underlying ASP solver clingo is available here. Newest version checked to work with our format is 4.5.4. UsageUSAGE: aba2af -f (arg) -r (arg) -s (arg) [-e] [-h] COMMAND LINE ARGUMENTS (all required): -f,--file (arg) Input file defining the ABA framework -r,--reasoning-task (arg) Reasoning task (cred | skept) -s,--semantic (arg) Semantic (adm | prf | stb) COMMAND LINE OPTIONS: -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 decided -h,--help Display help message and exit -a,--arguments-file If set, a file showing the contents of each AF argument is produced Input formatIn 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: myAsm(a). myAsm(b). myAsm(c). contrary(a, x). contrary(b, y). contrary(c, z). myRule(x, []). myRule(y, [b]). myRule(z, [a,c]). query(x). query(y). query(c). Outputaba2af will produce the following files.
Answering queriesFor 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]. ExampleFor 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 -eThe 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. DownloadsVersion 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. References
[1] From Structured to Abstract Argumentation: Assumption-Based Acceptance via AF Reasoning. |