Verification of Locally Tight Programs

ANTHEM is a proof assistant that can be used for verifying the correctness of tight programs in the input language of the answer set grounder GRINGO with respect to specifications expressed by first-order formulas. We define the concept of a locally tight program and prove that the verification process used by ANTHEM is applicable in this more general setting. Unlike tightness, the local tightness condition allows some forms of recursion. In particular, some programs describing effects of actions are locally tight. Under consideration for publication in Theory and Practice of Logic Programming