anthem is a command line application for translating answer set programs in the mini-gringo dialect of clingo to first-order theories. Using an automated theorem prover, these theories can then be used to verify properties of the original programs, such as strong and external equivalence.

Check out the Manual to learn how to install and use anthem.

If you want to use anthem as a library to build your own application, you can do so. Check out the API documentation for the available functionalities.

Until recently, you would have found Patrick Lühne's version 1 of anthem here, which was discontinued and therefore moved to anthem-1. You are currently looking at version 2, which is the latest version and the only one that is actively developed. This version is a complete reimplementation of the original system with significantly extended capabilities. It was started by Zach Hansen and Tobias Stolzmann, but is now being developed by a growing group of people. We'd like to thank Patrick for the effort he put into his implementation and the kindness of resolving the naming conflict with us.

anthem is distributed under the terms of the MIT license. See LICENSE for details!

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in anthem by you shall be licensed as above, without any additional terms or conditions.