Computational Aspects of Formal Argumentation

Formal approaches to argumentation constitute a central research field within knowledge representation and reasoning, situated in the broader area of Artificial Intelligence (AI). Many approaches in argumentation are based on an argumentation workflow: starting from a knowledge base, often in a rule-based form, arguments are instantiated which are reasons in favour or against claims that can be constructed using information in the knowledge base. Conflicts among arguments then signal, e.g., diverging opinions or beliefs in the knowledge base. Argumentation semantics drive argumentative reasoning in presence of such conflicts to find acceptable sets of arguments from which conclusions can be drawn. Formal approaches for the whole workflow are called structured argumentation formalisms. Approaches that focus on the argumentative reasoning process using argumentation semantics and which operate on abstracted arguments are called abstract argumentation formalisms.

In this thesis we advance the state of the art of computational aspects of formal approaches in the argumentation workflow. We do so in three different directions. First, we study computational properties of argumentative reasoning tasks in the prominent formal approaches of abstract dialectical frameworks (ADFs) within abstract argumentation and assumption-based argumentation (ABA) and ASPIC+ for structured argumentation. We lay out novel complexity results and develop algorithms for these three formalisms and show that resulting prototype implementations show promising runtime performance.

For the inherent need of dynamics in argumentation, we investigate the so-called enforcement operation in abstract argumentation, defined on argumentation frameworks (AFs), that aims to find argumentative ways of arguing in favour of a desired outcome. Related to enforcement, we look at the problem of AF synthesis with which we study constructing (learning, synthesizing) AFs from given semantical information. For both enforcement and AF synthesis we show a thorough complexity map and provide an in-depth experimentation of prototypes based on Maximum Satisfiability solvers, which show promising scalability.

In a third direction, we study methods to support explaining argumentative outcomes of approaches using AFs as their reasoning engine. Based on recent notions of strong inconsistency, tailored to inconsistency in non-monotonic formalisms, we develop strongly accepting or rejecting subframeworks that give a potentially small subset of arguments sufficient for showing acceptance or rejection of arguments. We show formal properties of such subframeworks, including complexity results. Supporting explainability in a different direction, we apply the prominent approach of existential abstraction to AFs to arrive at a simplification methodology. We present a formalization of existential abstraction on AFs and associated formal properties.