Under some conditions, a rule in the input language of the ASP grounder gringo can be transformed into a first-order sentence that has the same meaning under the stable model semantics. Such translations can be used for proving strong equivalence of logic programs and for verifying their correctness with respect to specifications expressed by first-order formulas. This paper defines a translation of this kind that is applicable to some rules containing both arithmetic operations and aggregate expressions.

PDF

Theory and Practice of Logic Programming, Vol. 22 (2022).

@article{lif22a, title={Strong Equivalence of Logic Programs with Counting}, author={Vladimir Lifschitz}, volume={22}, journal={Theory and Practice of Logic Programming}, month={ }, url="http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=127940", year={2022} }