Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
M. Alviano, C. Dodaro, J. Fichte, M. Hecher, T. Philipp, J. Rath:
"Inconsistency Proofs for ASP: The ASP - DRUPE Format";
Vortrag: ICLP 2019 - 35th International Conference on Logic Programming,
Las Cruces, New Mexico, USA;
20.09.2019
- 25.09.2019; in: "Theory and Practice of Logic Programming",
TPLP,
19
(2019),
S. 891
- 907.
Kurzfassung englisch:
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.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1017/S1471068419000255
Zugeordnete Projekte:
Projektleitung Stefan Woltran:
START
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.