QADF -
QBF based system for ADFs to compute acceptable sets of arguments
Welcome to the QADF system page, for computing acceptable sets of arguments (models and interpretations) for Abstract Dialectical Frameworks (ADFs)
It is developed within the project "Abstract Dialectical Frameworks: Advanced Tools for Formal Argumentation"
(funded by Deutsche Forschungsgemeinschaft (DFG) and the Austrian Science Fund (FWF) under grants BR-1817/7-1 and I1102 (DFG/
FWF)
Contents
News
Webpage online
29.3.2014QADF webpage is online. You can download QADF version 0.1 below.
About
QADF is a system for solving reasoning problems on Abstract Dialectical Frameworks (ADFs) using systems for quantified Boolean Formulas (QBFs). Given an ADF and reasoning problem as input, the tool QADF returns the encoding of the reasoning problem as a QBF for that ADF. A subsequent QBF solver then solves the reasoning task. At the moment the system has been tested using the QSAT solver DepQBF (version 2.0) (lonsing.github.io) and pre-processing tool Bloqqer (version 031) (fmv.jku.at). Running QADF requires Scala (2.9.3) (scala-lang.org).
Usage
Command line options
First of all, let us take a look on a typical program call:
- Credulous acceptance of argument "a" with admissible semantics:
scala qadf_2.9.3-1.0.jar -adm -C a filename | \ ./path/to/bloqqer | ./path/to/depqbf
We provide the complete usage (which is subject to change in future versions):
usage: qadf [options] inputfile with options: -h display this help -3m three valued models -2m two valued models -adm admissible -comp complete -pref preferred -ground ground -E existence -N non trivial existence -C statement credulous acceptance -S statement skeptical acceptance -O outputfile print output to outputfileDefault mode is print encoding of enumeration problem of selected semantics to standard output
NOTE: A statement is credulously accepted for adm/comp/pref if and only if encoding is UNSAT. A statement is skeptically accepted for 2mod/3mod/pref if and only if encoding is UNSAT
Examples
Here we provide some examples to test the program.
Input format for QADF
required input
statement(x) ... for representing an argument/statement called
"x"
ac(x,f) ... for the acceptance condition f of x which is
encoded in propositional logic using the
following syntax:
c(v), c(f) for true, false
and(p,q), or(p,q) and neg(p) for the usual
boolean connectives and subformulae p and q,
nested as needed.
-
For examples see:
- example archive.
Download
QADF version 0.1 can be downloaded here: QADF version 0.1
For the execution of the programs one needs a QBF solver like DepQBF.
Team
- Martin Diller
- Johannes Peter Wallner
- Stefan Woltran
Related Webpages
References
| [2] |
Reasoning in Abstract Dialectical Frameworks Using Quantified Boolean Formulas Martin Diller, Johannes P. Wallner and Stefan Woltran. In Proceedings of the 5th International Conference on Computational Models of Argument, COMMA 2014 |
| [1] |
Solving Reasoning Problems on Abstract Dialectical Frameworks via Quantified Boolean Formulas Martin Diller Master's Thesis, Technische Universität Wien, Stefan Woltran and Johannes P. Wallner advisors, 2014. |
Top