# Inconsistency Proofs for ASP: The ASP-DRUPE Format

arXiv: https://arxiv.org/abs/1907.10389 · HTML: https://mlsanity.com/paper/1907.10389/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Jul 2019.

## Built on by (most cited first, 2 of 2)

- [An XAI View on Explainable ASP: Methods, Systems, and Perspectives](https://mlsanity.com/paper/2601.14764/) (2026)
- [Towards a Certifying Grounder](https://mlsanity.com/paper/2607.21199/) (2026)

## Abstract (arXiv)

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.