Verifying Strong Equivalence of Programs in the Input Language of GRINGO

摘要

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 prepositional 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.