On the Semantics of Gringo (2013)
Input languages of answer set solvers are based on the mathematically simple concept of a stable model. But many useful constructs available in these languages, including local variables, conditional literals, and aggregates, cannot be easily explained in terms of stable models in the sense of the original de finition of this concept and its straightforward generalizations. Manuals written by designers of answer set solvers usually explain such constructs using examples and informal comments that appeal to the user's intuition, without references to any precise semantics. We propose to approach the problem of defi ning the semantics of Gringo programs by translating them into the language of in finitary propositional formulas. This semantics allows us to study equivalent transformations of Gringo programs using natural deduction in in finitary propositional logic.
In Answer Set Programming and Other Computing Paradigms (ASPOCP 2013), Istanbul, Turkey, August 2013.

Amelia Harrison Postdoctoral Fellow ameliaj [at] cs utexas edu
Vladimir Lifschitz Faculty vl [at] cs utexas edu
Fangkai Yang Ph.D. Alumni fkyang [at] cs utexas edu