On Heuer's Procedure for Verifying Strong Equivalence

In answer set programming, two groups of rules are considered strongly equivalent if replacing one group by the other within any program does not affect the set of stable models. Jan Heuer has designed and implemented a system that verifies strong equivalence of programs in the ASP language mini-gringo. The design is based on the syntactic transformation tau * that converts mini-gringo programs into first-order formulas. Heuer's assertion about tau * that was supposed to justify this procedure turned out to be incorrect, and in this paper we propose an alternative justification for his algorithm. We show also that if tau * is replaced by the simpler and more natural translation nu then the algorithm will still produce correct results.