Skip to Content

TU Wien Fakultät für Informatik DBAI Database and Artificial Intelligence Group
Top-level Navigation: Current-level Navigation:

Path: DBAI > research > projects > adf project > software > QADF

Tools: Print page

     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).



QADF 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.

QADF webpage with version 0.1 is online.


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) ( and pre-processing tool Bloqqer (version 37) ( QADF (version 0.4.0) is implemented in (Scala) and can be run as a (Java) executable.


A typical call of QADF (using a UNIX command line) looks as follows:

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


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:
  • Examples
  • 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.


    Related Webpages


    [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.


    Home / Kontakt / Webmaster / Offenlegung gemäß § 25 Mediengesetz: Inhaber der Website ist das Institut für Logic and Computation an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. Disclaimer / Datenschutzerklärung