Algorithms and efficient encodings for argumentation frameworks and arithmetic problems

Resumen

In this thesis we focus on the design and implementation of a particular framework of Possibilistic Defeasible Logic Programming (RP-DeLP). This framework is based on a general notion of collective (non-binary) conflict among arguments allowing to ensure direct and indirect consistency properties with respect to the strict knowledge. An output of an RP-DeLP program is a pair of sets of warranted and blocked conclusions (literals), all of them recursively based on warranted conclusions but, while warranted conclusions do not generate any conflict, blocked conclusions do. An RP-DeLP program may have multiple outputs in case of circular definitions of conflicts among arguments. We introduce two semantics, the first one where all possible outputs are computed and the second one which is a characterization of an unique output property. The computation of the outputs for both semantics relies on two main problems: the problem of finding a collective conflict among a set of arguments and the problem of finding almost valid arguments for a conclusion. Both problems are combinatorial problems, so we propose two resolution approaches: a first one based on SAT techniques and a second one based on Answer Set Programming techniques. We propose an implementation and we empirically test our algorithms. We provide an analysis on the performance of the implementation of the algorithms, and we explain the results on the resolution of some randomly generated problems. In this thesis we also focus on the resolution of some combinatorial problems. We analyze, design and implement some resolution tools for arithmetic problems, modular constraints and networking problems. We studied empirically how our approaches perform and we compared them to other solving techniques known as best proposals in the literature.