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)

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)



Webpage online

QADF webpage is online. You can download QADF version 0.1 below.


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) ( and pre-processing tool Bloqqer (version 031) ( Running QADF requires Scala (2.9.3) (


Command line options

First of all, let us take a look on a typical program call:

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 outputfile
Default 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


Here we provide some examples to test the program.

Input format for QADF

   required input
statement(x)  ...  for representing an argument/statement called 
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.


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.


Related Webpages


[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