[Back]

P. Bellositz:
"Advancements in Equivalence Checking for Abstract Argumentation Frameworks";
Supervisor: W. Dvorak, S. Woltran; Instute of Logic and Computation, E192-02, 2018; final examination: 2018-10-03.

Formal Argumentation is an actively studied field within Artificial Intelligence. Abstract Argumentation Frameworks (AFs), introduced by Dung in 1995, are an approach to reason over inconsistent knowledge. This knowledge is represented by arguments which may attack one another. Sets of non-conflicting arguments may then be grouped into extensions according to some argumentation semantics of which many different ones have been introduced over the years. When working with AFs, changes in arguments and attacks may occur and therefore change the information contained within the framework. Hence abstract argumentation can be described as dynamic reasoning. To study the effects of such changes to AFs and whether they affect changes in extensions, different notions of equivalency have been proposed. These include standard, expansion, strong and C-relativised equivalence. C-relativised equivalence is defined for the stable, admissible, preferred, complete and grounded semantics originally introduced by Dung. These semantics are modified (i.e. C-restricted) to only consider the relations of a set of core arguments. By not reasoning over all arguments, this concept enables local replacements of sub-AFs. This thesis examines how to automate C-relativised equivalence checking to replace large numbers of locally equivalent frameworks with simpler alternatives and therefore reduce computational strain on AF solver programs. This goal is achieved by formally defining C-relativised equivalency patterns that guarantee equivalence of an AF before and after replacement of a sub-AF therein with respect to some semantics and under some constraints for attack relations. To find C-relativised equivalence patterns, this work presents a system of encodings of C-restricted semantics as well as C-relativised equivalence characterisations. This system accepts arbitrary numbers of AFs and determines whether they are pairwise equivalent. For this work, the results of large numbers of equivalency computations are systematically analysed to find C-relativised equivalency patterns. Found patterns are then formally proven and the effects of applying them to generated frameworks are discussed, based on experiments that are conducted.

Abstract Argumentation, Answer Set Programming, Equivalence Notions , Nonmonotonic Reasoning