Solving reasoning problems on abstract dialectical frameworks via quantified boolean formulas

Abstract

"Abstrakte Argumentation", als Teilgebiet des interdisziplinären Forschungsfeld der "Argumentationstheorie", hat während der letzten beiden Dekaden innerhalb der Computerwissenschaften und der Künstlichen Intelligenz immer mehr an Bedeutung gewonnen. Ausgehend vom Konzept der "Argumentation Frameworks" (AFs), entwickelt von P. M. Dung im Jahre 1995, wurden viele verschiedene Formalismen für abstrakte Argumentation entworfen. In all diesen Formalismen gilt es zu entscheiden unter welchen Umständen ein Argument in einer Debatte "akzeptabel" ist bzw. wann eine Menge von Argumenten in sich "akzeptabel" ist. Alle Forma- lismen für abstrakte Argumentation beinhalten Konzepte für die Repräsentation von Argumenten, deren Relation untereinander (zusammengenommen also das "Framework"), verschiedene Methoden um anhand der Struktur des Frameworks festzustellen, welche Argumente zu akzeptieren sind (die "Semantiken"), sowie verschiedene Möglichkeiten von Schlüsse, welche mittels der Frameworks und deren Semantiken gezogen werden können. Einer der allgemeinsten Formalismen in diesem Kontext sind die kürzlich entwickelten "Abstract Dialectical Frameworks" (ADFs), welche eine direkte Repräsentation von komplexen Relationen zwischen den Argumenten mittels boolescher Formeln ("acceptance conditions") ermöglichen. Diese - im Vergleich zu AFs - erhöhte Ausdruckstärke bedingt, dass verschiedene Schlussweisen auf ADFs nun eine höhere Komplexität aufweisen, als jene Schlussweisen auf AFs, welche sie verallgemeinern. Manche Schlussweisen sind sogar vollständig für die dritte Stufe der polynomiellen Hierarchie. Quantifizierte boolesche Logik auf der anderen Seite ist ein etablierter Formalismus in den Computerwissenschaften, welche eine direkte Verbindung mit der polynomiellen Hierarchie der Komplexitätsklassen hat. Durch den Fortschritt der Software Systeme für diese Logik hat sich die quantifizierte boolesche Logik als vielversprechender Formalismus, um Probleme innerhalb der polynomiellen Hierarchie zu lösen, herauskristallisiert. In dieser Arbeit präsentieren wir Reduktionen, oder Kodierungen, von einigen der Schlussweisen in ADFs für die wichtigsten Semantiken auf das Problem der Erfüllbarkeit von quantifizierten booleschen Formeln (QSAT), welche die Komplexität der ursprünglichen Probleme berücksichtigen. Auf diese Art stellen wir eine uniforme Axiomatisierung für diese Schlussweisen in quantifizierter boolescher Logik bereit. Weiters bahnen wir den Weg für Implementierungen dieser Schlussweisen, da sie die fortschrittlichen Techniken, welche für QSAT entwickelt wurden, nutzen können. Schlussendlich beschreiben wir einen von uns implementierten Prototypen eines solchen Systems und diskutieren Ergebnisse erster Experimente.

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