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)
Its development started 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). Its development continues within the project "A Semantical Framework for Graph-Based Argument Processing" (funded by DFG under grant BR 1817/7-2 and FWF under grant I2854).
Contents
News
18.2.2019QADF version 0.4.0 is online. It produces intermediate representations as well as link information sensitive encodings for the admissible, preferred, and stable semantics. You can download QADF version 0.4.0 below. QADF version 0.1.0 (which has support for the three valued models, two valued models, admissible, complete, preferred, and grounded semantics) can still be downloaded at below.
29.3.2014
QADF webpage with version 0.1 is online.
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 mainly using the QSAT solver DepQBF (version 6.03) (lonsing.github.io) and pre-processing tool Bloqqer (version 37) (fmv.jku.at). QADF (version 0.4.0) is implemented in (Scala) and can be run as a (Java) executable.
Usage
A typical call of QADF (using a UNIX command line) looks as follows:
- Credulous acceptance of argument "a" with dual version of the link information sensitive encoding for the admissible semantics:
java -jar qadf_0.4.0.jar -adm -cred a -L -D 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 (also works with --h, \
-help, --help)
-version print version
-adm admissible
-prf preferred
-stb stable
-stb2 stable (using Dung's 2018 characterisation)
-cred s check credulous acceptance of statement s
-scep s check skeptical acceptance of statement s
-O outputfile print output to outputfile
-D use dual encoding
-L use link information sensitive encoding
-noTransform do not apply any transformation to encoding
-Tseitin only apply tseitin transformation to encoding
-Circuit Output circuit representation
-QCIR Output circuit representation in QCIR 14 format
Default mode is print encoding of existence problem of \
selected semantics to standard output (in qdimacs format)
Note that only adm, prf, stb in QDIMACS format have been tested more extensively
Examples
Input format for QADF:
required input
s(x). ... for representing an argument/statement called
"x" (also "statement(x)" as in version 0.1.0
can be used)
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.
att(x,y). ... for an attacking link (x,y)
sup(x,y). ... for a supporting link (x,y)
dep(x,y). ... for a dependent link (x,y)
For examples see:
Download version 0.4.0
QADF version 0.4.0 can be downloaded here: QADF version 0.4.0
Download version 0.1.0
QADF version 0.1.0 (run with "scala qadf_2.9.3-1.0.jar -h" for options) can be downloaded here: QADF version 0.1
For solving the encoded problems a QBF solver like DepQBF is needed.
Team
Related Webpages
References
| [3] |
Reasoning in Abstract Dialectical Frameworks Using Quantified Boolean Formulas Martin Diller, Johannes P. Wallner and Stefan Woltran. In Argument & Computation, 2015 |
| [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