ANTHEM is a proof assistant designed for verifying several conditions that play an important role in answer set programming. In this note we show that ANTHEM can help us verify equivalence of logic programming solutions to the same problem that have been independently developed by different programmers.

PDF

To Appear In Proceedings of the European Conference on Logics in Artificial Intelligence, 2025.

@inproceedings{lif25a, title={An Experiment with Anthem: Semantic Equivalence of Tiling Programs}, author={Vladimir Lifschitz}, booktitle={Proceedings of the European Conference on Logics in Artificial Intelligence}, month={ }, url="http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=128127", year={2025} }