Inconsistency proofs for ASP: the ASP-DRUPE format
From MaRDI portal
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. This work is under consideration for acceptance in TPLP.
Recommendations
- Explaining inconsistency in answer set programs and extensions
- Tableau calculi for logic programs under answer set semantics
- Extended ASP Tableaux and rule redundancy in normal logic programs
- Conflict-driven answer set solving: from theory to practice
- Answer set programming based on propositional satisfiability
Cites work
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- A Constructive semantic characterization of aggregates in answer set programming
- A unified proof system for QBF preprocessing
- Advances in WASP
- Answer set based design of knowledge systems
- Answer set programming modulo acyclicity
- Conflict-driven answer set solving: from theory to practice
- Detecting inconsistencies in large biological networks with answer set programming
- DRAT proofs for XOR reasoning
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Efficient certified RAT verification
- Expressing symmetry breaking in DRAT proofs
- Extended resolution simulates \({\mathsf{DRAT}}\)
- GRASP: a search algorithm for propositional satisfiability
- Logic Programming and Nonmonotonic Reasoning
- Logic programs with abstract constraint atoms: the role of computations
- Logic programs with propositional connectives and aggregates
- Multi-criteria optimization in answer set programming
- Semantics and complexity of recursive aggregates in answer set programming
- Shared aggregate sets in answer set programming
- Some (in)translatability results for normal logic programs and propositional theories
- Stable inference as intuitionistic validity
- Team-building with answer set programming in the Gioia-Tauro seaport
- Theory and Applications of Satisfiability Testing
- Trichotomy and dichotomy results on the complexity of reasoning with disjunctive logic programs
- Verifying Refutations with Extended Resolution
- Vicious circle principle and logic programs with aggregates
- Well-founded and stable semantics of logic programs with aggregates
Cited in
(2)
This page was built for publication: Inconsistency proofs for ASP: the ASP-DRUPE format
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5108508)
