Realising argumentation using answer set programming and quantified boolean formulas

Abstract

Argumentation is one of the key manners in which humans individually and collectively make sense of complex scenarios about which the information that is available is incomplete or even inconsistent. Computational or artificial argumentation is thus also an increasingly important sub-field of AI aiming at supporting or even automating human argumentation as well as enhancing computational systems with means of generating and evaluating arguments. This work is concerned with the implementation of general formal models underlying computational argumentation systems. What most of such models have in common is their high computational complexity; in the case of the reasoning problems we study, these range from being complete for the first levels of the polynomial hierarchy to being undecidable in general. A standard way of addressing computational problems with such high complexity is by providing translations to other formalisms for which efficient systems exist. Given the complexity of the tasks we address, in this work we consider quantified boolean formulas (QBFs) and answer set programming (ASP) as target formalisms. The first being a generalisation of propositional logic having sub-classes of formulas whose complexity is complete for each level of the polynomial hierarchy. Answer set programming, on the other hand, is a paradigm for declarative problem solving having sprung out of logic programming and being undecidable in general, yet having important decidable fragments. Concretely, we develop means of implementing some of the main reasoning problems for abstract dialectical frameworks and defeasible theories. Abstract dialectical frameworks (ADFs) are one of the most comprehensive graphical formalisms for evaluating argumentation scenarios, with nodes representing statements or assertions and acceptance conditions associated to the nodes specifying complex relations, such as attack and support, between the statements. Different semantics provide conflict resolution mechanisms on the basis of such an abstract representation. Defeasible theories, on the other hand, allow for expressing collections of strict and defeasible first order rules. Potential conflicts between the defeasible rules are resolved via the direct stable semantics, which also provides means of generating arguments for particular claims on the basis of the information expressed in a defeasible theory. In this work we, first of all, develop complexity sensitive QBF encodings for the stable semantics for ADFs as well as link information sensitive QBF encodings for all the majorsemantics for ADFs. The latter make use of information about the link (relationships between the nodes) types of ADFs whenever available; the motivation being that solvers for QBFs are able to make use of this information to the same degree as which availability of the information can make the complexity of the reasoning tasks we study easier. We secondly develop novel dynamic ASP encodings for the main semantics for ADFs. We make use of the fact that the combined complexity of reasoning on ASP programs with predicates of bounded arity size exactly matches the complexity of the reasoning tasks we investigate for ADFs. Finally, we study the implementation of the whole pipeline of evaluating collections of strict and defeasible rules expressed in a prominent controlled natural language (CNL), ACE, to the translation of such rules into defeasible theories and their evaluation via the direct stable semantics. This involves studying the translation of the rules expressed in the CNL into defeasible theories, the encoding of general rules involving existential quantification into normal (i.e. not having existential quantification) rules, as well as the evaluation of defeasible theories via the direct stable semantics using ASP encodings. We have produced prototype systems for all of the implementation strategies we devise in this work and also report on preliminary empirical evaluations.