  Answer Set Programming (ASP) solvers are highly-tuned and complex procedures
that implicitly solve the consistency problem, i.e., deciding whether a logic
program admits an answer set. Verifying whether a claimed answer set is
formally a correct answer set of the program can be decided in polynomial time
for (normal) programs. However, it is far from immediate to verify whether a
program that is claimed to be inconsistent, indeed does not admit any answer
sets. In this paper, we address this problem and develop the new proof format
ASP-DRUPE for propositional, disjunctive logic programs, including weight and
choice rules. ASP-DRUPE is based on the Reverse Unit Propagation (RUP) format
designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and
discuss how to integrate it into modern ASP solvers. Later, we provide an
implementation of ASP-DRUPE into the wasp solver for normal logic programs.
This work is under consideration for acceptance in TPLP.
