Master Thesis Defense by Mr Martin Diller
Mr Martin Diller defended his master thesis on 'Reasoning on Abstract Dialectical Frameworks via Quantified Boolean Formulas'
Mr Martin Diller defended his master thesis on 'Reasoning on Abstract Dialectical Frameworks via Quantified Boolean Formulas' on 11 April 2014 at TUW.
Abstract: Abstract argumentation" is a subfield of the interdisciplinary area of study "argumentation theory" that has developed into an increasingly important area of computer science and artificial intelligence in the last two decades. Starting with the "argumentation frameworks" (AFs) proposed by P. M. Dung in 1995, several different formalisms for abstract argumentation have been devised to date with just as many desiderata in mind, the overarching focus of study of this field though still being to determine when an argument (or set of arguments) can be considered to remain undefeated or even come out victorious in the context of a dispute. All formalisms for abstract argumentation include a means of representing arguments and their relationships ("a framework"), several methods to determine which arguments can be accepted together based on the structure of the frameworks (the "semantics"), as well as "reasoning tasks" that are defined in terms of these frameworks and semantics. One of the most general formalisms is that of "abstract dialectical frameworks" (ADFs), which is of a relatively recent date and allows for the direct representation of complex relations of support and attack between arguments through boolean formulas ("acceptance conditions") associated to the arguments. This increase in expressive power with respect to AFs has the consequence that many of the reasoning tasks that can be defined for ADFs suffer from an even "higher complexity" than the tasks they generalise in the context of AFs, being complete for up to third level of the polynomial hierarchy. Quantified boolean logic on the other hand is a relatively well established formalism in computer science, being of special relevance because of its connection with the polynomial hierarchy of complexity classes. Given the advances in the performance of software systems for this logic in recent years, it is also increasingly recognized to be a promising formalism in which to translate computational problems located within the polynomial hierarchy. In this work we present complexity-sensitive reductions or encodings of some of the main reasoning tasks defined for ADFs with respect to some of the major semantics into the satisfiability problem of quantified boolean logic (QSAT). In this manner we provide a uniform axiomatization of these reasoning tasks into quantified boolean logic. Moreover, we pave the way for implementations of these reasoning tasks via the already mentioned advances in technologies for QSAT. Finally, we also describe a prototype of such a system we have implemented and report on preliminary experiments that serve as a first benchmark for implementations of these tasks via QSAT.