An Experiment with Anthem: Semantic Equivalence of Tiling Programs (2025)
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.
View:
PDF
Vladimir Lifschitz Faculty vl [at] cs utexas edu