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.

PDF

In Proceedings of European Conference on Logics in Artificial Intelligence, 2023.

@inproceedings{heuer, title={On Heuer’s Procedure for Verifying Strong Equivalence}, author={Jorge Fandinno and Vladimir Lifschitz}, booktitle={Proceedings of European Conference on Logics in Artificial Intelligence}, month={ }, url="http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=128026", year={2023} }