Talks and Poster Presentations (with Proceedings-Entry):
J. Fichte, M. Hecher, T. Philipp:
"Inconsistency Proofs for ASP: The ASP-DRUPE Format";
Talk: Aspocp 2019 @ Lpnmr 2019,
2019-06-03; in: "Aspocp 2019 @ Lpnmr 2019",
ASP solvers are highly-tuned and complex procedures that
implicitly solve the consistency problem, i.e., deciding whether an ASP 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 ASP, including weights and optimization. ASP-DRUPE is based on the RUP format designed for Boolean satis ability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers.
Project Head Stefan Woltran:
Created from the Publication Database of the Vienna University of Technology.