Equipping Abstract Argumentation Solvers for Verifying Negative Results

Abstract

Abstract argumentation frameworks (AFs) are a popular formalism for modeling argumentation processes. Thus, various solvers have been developed that can be used to answer decision problems on such frameworks and that regularly compete within the context of competitions. For positive results, these solvers typically provide some sort of model or extension, making it easy to verify their results. However, negative results cannot be easily verified in such a way, creating a need for some sort of certificate to be able to check these results as well. While, for instance, SAT solvers commonly support inconsistency proofs, this is not the case for abstract argumentation solvers yet. In this work, we provide a formal definition of such a certificate for SETAFs, a generalization of Dung AFs, and provide a prototype implementation of a genuine CDCL-based solver for SETAFs that can produce such inconsistency proofs as well as a tool for verifying these proofs.