Witnesses for Answer Sets of Basic Logic Programs

Explanation plays an important role in the decisions of both symbolic and neural network-based AI systems. Logic programs under answer set semantics (ASP) have been a typical declarative reasoning and problem-solving paradigm that has extensive applications in various AI domains. In this paper, we consider the issue of explanation for logic programs with abstract constraint atoms (c-atoms) under SPT-answer set semantics. Such c-atoms are general enough to capture complex constructors of logic programs, including aggregates, and the SPT-answer sets exclude circular justifications that other semantics have. We propose a minimal reduct for logic programs with c-atoms that yields a new semantic characterization of SPT-answer sets, and then introduce an extension of resolution for clauses with c-atoms. As we show, every atom in an SPT-answer set enjoys an extended resolution proof from the minimal reduct of its logic program. Finally, we present minimal sufficient subsets of logic programs (witnesses) to structure such an extended resolution proof for an atom in an SPT-answer set. Our results contribute to the justification of answer sets and provide a basis for explainability of ASP-based applications.