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.
CITATION STYLE
Lifschitz, V., Lühne, P., & Schaub, T. (2019). Verifying Strong Equivalence of Programs in the Input Language of gringo. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11481 LNAI, pp. 270–283). Springer Verlag. https://doi.org/10.1007/978-3-030-20528-7_20
Mendeley helps you to discover research relevant for your work.