Wallner, J. (2014). Complexity results and algorithms for argumentation : Dung’s frameworks and beyond [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2014.24438
In den letzten Jahrzehnten hat sich die Argumentationstheorie als wichtiges Teilgebiet der Künstlichen Intelligenz (KI) etabliert. Die vielfältigen Wurzeln dieses jungen Gebietes liegen sowohl in der Philosophie, in den Rechtswissenschaften, als auch in der formalen Logik. Unterstützt durch die Computerwissenschaften ergaben sich aus dieser Theorie ebenso vielfältige Anwendungen, unter anderem für rechtliche Beweisführung, Medizin und E-Democracy. Als zentraler Aspekt, der in vielen Formalisierungen von Argumentation auftaucht, erweist sich eine gewisse Form von Abstraktion. Meist wird in einem solchen Abstraktionsprozess von konkreten Inhalten von Argumenten Abstand genommen und nur deren logische Relation betrachtet. Ein einflussreiches formales Model für die abstrakte Repräsentation von Diskursen sind die so genannten Argumentation Frameworks (AFs), entwickelt von Phan Minh Dung. In diesen AFs werden Argumente einfach als abstrakte Knoten in einem Graph dargestellt. Gerichtete Kanten repräsentieren wiederum die Relation zwischen Argumenten, welche in AFs als Angriff interpretiert wird. Beispielsweise kann ein attackierendes Argument als Gegenargument gesehen werden. In der Literatur wurden diverse Aspekte von AFs verallgemeinert, oder erweitert. Ein besonders genereller Vertreter dieser formalen Modelle sind die Abstract Dialectical Frameworks (ADFs). ADFs sind noch abstrakter als AFs, denn die Relation in ADFs beschränkt sich nicht auf Attacken, sondern kann mittels so genannter Akzeptanzbedingungen frei spezifiziert werden. Diese Bedingungen werden mittels boolescher Formeln modelliert. Die logischen Semantiken dieser Argumentationsstrukturen bestehen aus verschiedenen Kriterien zur Akzeptanz von Argumenten. Die automatische Berechnung von Mengen von Argumenten die gemeinsam akzeptiert werden können ist eine der wichtigsten Aufgaben auf AFs und ADFs. Allerdings haben praktisch alle solche Problemstellungen eine hohe Berechnungskomplexität. Manche Probleme auf AFs sind sogar hart für die zweite Stufe der polynomiellen Hierarchie. AFs sind Spezialfälle von ADFs, daher sind ADFs auch mindestens so komplex was die Berechnung der Semantiken angeht. Eine genaue Analyse der Komplexitätsschranken war jedoch offen für ADFs. Um diese Aufgaben dennoch zu bewältigen sind einige Algorithmen für AFs entwickelt worden. Man kann diese in zwei Richtungen klassifizieren. Die erste Richtung beschäftigt sich mit Reduktionen oder auch Übersetzungen. Dabei wird das Ursprungsproblem in ein anderes kodiert, für das performante Systeme existieren. Zu Beginn der Arbeiten an dieser Dissertation waren Reduktionen allerdings von rein monolithischer Natur. Das heißt, dass diese Reduktionen das Ursprungsproblem in eine einzelne Kodierung übersetzen. Zudem wurden in diesen Übersetzungen kaum Optimierungen berücksichtigt. Die zweite Richtung besteht aus direkten Methoden. Diese können leichter strukturelle oder semantische Eigenschaften von AFs nutzen um effizient Lösungen zu berechnen. Allerdings müssen hierfür Algorithmen von Grund auf neu implementiert werden. Das beinhaltet auch die zeitintensive Aufgabe geeignete Datenstrukturen und andere technische Details auszuarbeiten. Unser Beitrag zum wissenschaftlichen Stand der Technik in der Argumentationstheorie lässt sich in drei Bereiche gliedern. Erstens entwickeln wir hybride Ansätze, welche die Stärken von Reduktionen und direkten Methoden vereinen. Dabei reduzieren wir die Problemstellungen auf eine Folge von booleschen Erfüllbarkeitsproblemen (SAT). Bei Problemen die hart für die zweite Stufe der polynomiellen Hierarchie sind, lässt es sich, unter komplexitätstheoretischen Annahmen, nicht vermeiden, dass wir im schlimmsten Fall eine exponentielle Anzahl solcher Teilprobleme lösen müssen. Durch Verwendung von inhärenten Parametern von AFs können wir diese Anzahl jedoch beschränken. Zusätzlich zu dem klassischen SAT Problem, zeigen wir, dass sich Probleme in der Argumentation natürlicherweise auf Erweiterungen des SAT Problems reduzieren lassen. Konkret nutzen wir minimal correction sets (MCSes) und backbones von booleschen Formeln hierfür. Reduktionen zu diesen sind ebenfalls hybrid, allerdings näher zu strikt monolithischen Ansätzen und auch deklarativer als die anderen hybriden Methoden. Als zweites Ergebnis unserer Arbeit stellen wir Verallgemeinerungen unserer hybriden Ansätze für ADFs vor. Hierfür erweitern wir zuerst die theoretische Basis und zeigen wesentliche Komplexitätsresultate von ADFs. Es stellt sich heraus, dass Entscheidungsprobleme von ADFs im Allgemeinen eine um eine Stufe höhere Komplexität aufweisen als die jeweiligen Probleme auf AFs. Trotz der Tatsache, dass damit manche Probleme auf ADFs hart für die dritte Stufe der polynomiellen Hierarchie sind, können wir zeigen, dass eine wichtige Teilklasse von ADFs, die so genannten bipolaren ADFs (BADFs), nicht von der erhöhten Komplexität betroffen sind. Unser dritter Beitrag besteht aus Implementierungen unserer Methoden für AFs und deren experimentelle Evaluierung. Wir zeigen, dass unsere Implementierungen performanter als andere Systeme im Bereich der Argumentationstheorie sind. Diese Resultate deuten daraufhin, dass unsere hybriden Ansätze gut geeignet sind um die schwierigen Aufgaben, die in dieser Theorie vorkommen, zu bewältigen. Insbesondere können unsere prototypischen Softwareimplementierungen den Weg für Anwendungen, mit noch größeren Strukturen umzugehen, ebnen.
de
In the last couple of decades argumentation emerged as an important topic in Artificial Intelli gence (AI). Having its origin in philosophy, law and formal logic, argumentation in combination with computer science has developed into various formal models, which nowadays are found in diverse applications including legal reasoning, E-Democracy tools, medical applications and many more. An integral part of many formal argumentation theories within AI is a certain notion of abstraction. Hereby the actual contents of arguments are disregarded, but only the relation between them is used for reasoning purposes. One very influential formal model for representing discourses abstractly are Dung?s argumentation frameworks (AFs). AFs can simply be represented as directed graphs. The vertices correspond to abstract arguments and directed edges are interpreted as an attack relation for countering arguments. Many variants and generalizations of AFs have been devised, with abstract dialectical frameworks (ADFs) among the most general ones. ADFs are even more abstract than AFs: the relation between arguments is not fixed to the concept attack, but is specified via so-called acceptance conditions, describing the relationship via Boolean functions. The main computational challenge for AFs and ADFs is to compute jointly acceptable sets of arguments. Several criteria, termed semantics, have been proposed for accepting arguments. Applications of AFs or ADFs unfortunately face the harsh reality that almost all reasoning tasks defined for the frameworks are intractable. Decision problems for AFs can even be hard for the second level of the polynomial hierarchy. ADFs generalize AFs and thus are at least as computationally complex, but exact complexity bounds of many ADF problems are lacking in the literature. There have been some proposals how to implement reasoning tasks on AFs. Roughly these can be classified into reduction and direct approaches. The former approach solves the problem at hand by translation to another one, for which sophisticated solvers exist. However, at the start of this thesis, reduction approaches for argumentation were purely monolithic. Monolithic reduction approaches result into a single encoding and hardly incorporate domain-specific optimizations for more efficient computation. Direct approaches exploit structural or semantical properties of AFs for efficiency but must typically devise and implement an algorithm from scratch, including the highly consuming task of engineering solutions on a very deep algorithmic level e.g. the development of suitable data structures. In this thesis we provide three major contributions to the state of the art in abstract argumentation. First, we develop a novel hybrid approach that combines strengths of reduction and direct approaches. Our method reduces the problem at hand to iterative satisfiability (SAT) solving, i.e. a sequence of calls to a SAT-solver. Due to hardness for the second level of the polynomial hierarchy, we cannot avoid exponentially many SAT calls in the worst case. However, by exploiting inherent parameters of AFs, we provide a bound on the number of calls. Utilizing modern SAT technology to an even greater extent, we also employ more expressive variants of the SAT problem. It turns out that minimal correction sets (MCSes) and backbones of Boolean formulae are very well suited for our tasks. Like the iterative SAT algorithms, our algorithms based upon MCSes and backbones are hybrid approaches as well. Yet they are closer to monolithic reduction approaches and offer the benefit of requiring even less engineering effort and providing more declarativeness. Our second major contribution is to generalize our algorithms to ADFs. For doing so we first considerably extend ADF theory and provide a thorough complexity analysis for ADFs. Our results show that the reasoning tasks for ADFs are one step up in the polynomial hierarchy compared to their counterparts on AFs. Even though problems on ADFs suffer from hardness up to the third level of the polynomial hierarchy, our analysis shows that bipolar ADFs (BADFs) are not affected by this complexity jump. BADFs restrict the relations between arguments to be either of an attacking or supporting nature, but still offer a variety of interesting relations. Finally our third contribution is an empirical evaluation of implementations of our algorithms. Our novel algorithms outperform existing state-of-the-art systems for abstract argumentation. These results show that our hybrid approaches are indeed promising and that the provided proof-of-concept implementations can pave the way for applications for handling problems of increasing size and complexity.
en
Additional information:
Abweichender Titel laut Übersetzung der Verfasserin/des Verfassers Zsfassung in dt. Sprache