Inconsistency Proofs for ASP: The ASP - DRUPE Format. Issue 5 (September 2019)

• Record Type: Journal Article
• Authors: ALVIANO, MARIO; DODARO, CARMINE; FICHTE, JOHANNES K.; HECHER, MARKUS; PHILIPP, TOBIAS; RATH, JAKOB
• Is Part Of: Theory and practice of logic programming. Volume 19:Issue 5/6(2019)
• Page Start: 891
• Page End: 907
• Publication Date: 2019-09
• Subjects: Answer Set Programming, -- Reverse Unit Propagation proofs, -- inconsistency proofs; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068419000255
• Languages: English
• ISSNs: 1471-0684

Abstract

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 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.