ccT: A Correspondence-Checking Tool for Logic Programs Under the Answer-Set Semantics

Abstract In recent work, a general framework for specifying correspondences between logic programs under the answer-set semantics has been defined. The framework captures different notions of equivalence, including well-known ones like ordinary, strong, and uniform equivalence, as well as refined ones based on the projection of answer sets where not all parts of an answer set are of relevance. In this paper, we describe an implementation to verify program correspondences in this general framework. The system, called cc⊤, relies on linear-time constructible reductions to quantified propositional logic and uses extant solvers for the latter language as back-end inference engines.

Authors

• Johannes Oetsch
• Martina Seidl
• Hans Tompits
• Stefan Woltran

Keywords

No keywords are indexed for this paper.