Mario Alviano, Carmine Dodaro, Johannes K. Fichte, Markus Hecher, Tobias Philipp...
TL;DR本研究提出了基于Reverse Unit Propagation格式的ASP-DRUPE证明格式，可用于判断标准程序是否有答案集，它可以与现代ASP求解器集成，并在wasp求解器中实现。
Abstract
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