Inconsistency Proofs for ASP: The ASP-DRUPE Format
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
On Inconsistency Indices and Inconsistency Axioms in Pairwise Comparisons
Pairwise comparisons are an important tool of modern (multiple criteria) decision making. Since human judgments are often inconsistent, many studies focused on the ways how to express and measure this inconsistency, and …
Decision MakingLoss as the Inconsistency of a Probabilistic Dependency Graph: Choose Your Model, Not Your Loss Function
In a world blessed with a great diversity of loss functions, we argue that that choice between them is not a matter of taste or pragmatics, but of model. Probabilistic depencency graphs (PDGs) are probabilistic models th…
DiversityVariational InferenceA Stronger Foundation for Computer Science and P=NP
This article describes a Turing machine which can solve for $\beta^{'}$ which is RE-complete. RE-complete problems are proven to be undecidable by Turing's accepted proof on the Entscheidungsproblem. Thus, constructing a…
The Possibilistic Horn Non-Clausal Knowledge Bases
Posibilistic logic is the most extended approach to handle uncertain and partially inconsistent information. Regarding normal forms, advances in possibilistic reasoning are mostly focused on clausal form. Yet, the encodi…
Safe Distributed Learning-Enhanced Predictive Control for Multiple Quadrupedal Robots
Quadrupedal robots exhibit remarkable adaptability in unstructured environments, making them well-suited for formation control in real-world applications. However, keeping stable formations while ensuring collision-free …
Collision AvoidanceModel Predictive Control