Abstract ANTHEM 2.0 is a tool to aid in the verification of logic programs written in an expressive fragment of CLINGO ’s input language named MINI-GRINGO, which includes arithmetic operations and simple choice rules but not aggregates. It can translate logic programs into formula representations in the logic of here-and-there and analyze properties of logic programs such as tightness. Most importantly, ANTHEM 2.0 can support program verification by invoking first-order theorem provers to confirm that a program adheres to a first-order specification or to establish strong and external equivalence of programs. This paper serves as an overview of the system’s capabilities. We demonstrate how to use ANTHEM 2.0 effectively and interpret its results.

Abstract We show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs P and Q and vocabulary V (set of predicates) the existence of a program R in V such that $$P \cup R$$ P ∪ R and $$P \cup Q$$ P ∪ Q are strongly equivalent can be expressed as a first-order entailment. Moreover, our result is effective: A program R can be constructed from a Craig interpolant for this entailment, using a known first-order encoding for testing strong equivalence, which we apply in reverse to extract programs from formulas. As a further perspective, this allows transforming logic programs via transforming their first-order encodings. In a prototypical implementation, the Craig interpolation is performed by first-order provers based on clausal tableaux or resolution calculi. Our work shows how definability and interpolation, which underlie modern logic-based approaches to advanced tasks in knowledge representation, transfer to answer set programming.