Answer-set programming (ASP) has emerged as a declarative programming paradigm where problems are encoded as logic programs, such that the so-called answer sets of theses programs represent the solutions of the encoded problem. The efficiency of the latest ASP solvers reached a state that makes them applicable for problems of practical importance. Consequently, problems from many different areas, including diagnosis, data integration, and graph theory, have been successfully tackled via ASP. In this work, we present such ASP-encodings for problems associated (...) to abstract argumentation frameworks (AFs) and generalisations thereof. Our encodings are formulated as fixed queries, such that the input is the only part depending on the actual AF to process. We illustrate the functioning of this approach, which is underlying a new argumentation system called ASPARTIX in detail and show its adequacy in terms of computational complexity. (shrink)

dialectical frameworks constitute a recent and powerful generalisation of Dung's argumentation frameworks, where the relationship between the arguments can be specified via Boolean formulas. Recent results have shown that this enhancement comes with the price of higher complexity compared to AFs. In fact, acceptance problems in the world of ADFs can be hard even for the third level of the polynomial hierarchy. In order to implement reasoning problems on ADFs, systems for quantified Boolean formulas thus are suitable engines to be (...) employed. In this paper we give complexity sensitive QBF encodings of ADF problems generalising recent work on QBFs for AF labellings. Our encodings provide a uniform and modular way of translating reasoning in ADFs to QBFs, that can be used as the basis for novel systems for ADF reasoning. (shrink)

As is well known, answer-set programs do not satisfy the replacement property in general, i.e., programs and that are equivalent may cease to be so when they are put in the context of some other program, i.e., and may have different answer sets. Lifschitz, Pearce, and Valverde thus introduced strong equivalence for context-independent equivalence, and proved that such equivalence holds between given programs and iff and are equivalent theories in the monotonic logic of here-and-there. In this article, we consider a (...) related question: given a program, does there exist some program from a certain class of programs such that and are equivalent under a given notion of equivalence? Furthermore, if the answer to this question is positive, how can we recast as an equivalent program from? In particular, we consider classes of programs that emerge by allowing disjunction and/or negation, and as equivalence notions we consider strong, uniform, and ordinary equivalence. Based on general model-theoretic properties and a novel form of canonical programs, we develop semantic characterisations for the existence of such a program, determine the computational complexity of checking existence, and provide rewriting rules for recasting. (shrink)

Many proposals for logic-based formalisations of argumentation consider an argument as a pair (Φ,α), where the support Φ is understood as a minimal consistent subset of a given knowledge base which has to entail the claim α. In case the arguments are given in the full language of classical propositional logic reasoning in such frameworks becomes a computationally costly task. For instance, the problem of deciding whether there exists a support for a given claim has been shown to be -complete. (...) In order to better understand the sources of complexity (and to identify tractable fragments), we focus on arguments given over formulæ in which the allowed connectives are taken from certain sets of Boolean functions. We provide a complexity classification for four different decision problems (existence of a support, checking the validity of an argument, relevance and dispensability) with respect to all possible sets of Boolean functions. Moreover, we make use of a general schema to enumerate all arguments to show that certain restricted fragments permit polynomial delay. Finally, we give a classification also in terms of counting complexity. (shrink)