The semantics of the input language of the ASP grounder gringo uses a translation that converts a logic program, which may contain variables and arithmetic operations, into a set of infinitary propositional formulas. In this note, we show that the result of that translation can be replaced in some cases by a finite set of first-order sentences. The translator anthem constructs that set of sentences and converts it to a format that can be processed by automated reasoning tools. anthem, in combination with the first-order theorem prover vampire, allows us to verify the strong equivalence of programs in the language of gringo.

PDF

In Proceedings of the 15th International Conference on Logic Programming and Non-monotonic Reasoning 2019.

@inproceedings{lif19, title={Verifying Strong Equivalence of Programs in the Input Language of gringo}, author={Vladimir Lifschitz and Patrick Lühne, and Torsten Schaub}, booktitle={Proceedings of the 15th International Conference on Logic Programming and Non-monotonic Reasoning}, url="http://www.cs.utexas.edu/users/ai-lab?verification", year={2019} }