Introduction

Welcome to the latest system developed as part of the “ASP + Theorem Proving“ (anthem) project! This system consolidates the findings and functionalities of previous prototypes into a more stable tool for verifying ASP programs. The theory behind anthem has been given a thorough treatment in the ASP literature – if you are interested, the system description is a good starting point. Additionally, the papers on verifying strong equivalence, checking programs against specs, and program to program verification provide more details on the theoretical background of anthem.

As the name suggests, anthem is a tool for automated verification of ASP programs. For a broad class of clingo and ASP-Core-2 programs, anthem can translate a program into a set of formulas written in the syntax of first-order logic. Given a specification (written in first-order logic or as another ASP program), anthem can automatically check certain types of equivalence hold between a program of interest and the specification by invoking the automated theorem prover vampire.

If you wish to experiment with anthem through a web interface, we provide one here.