Manuals written by the designers of answer set solvers usually describe the semantics of the input languages of their systems using examples and informal comments that appeal to the user’s intuition, without references to any precise semantics.We would like to describe a precise semantics for a large subset of the input language of the solver GRINGO based on representing GRINGO rules as infinitary propositional formulas. To prove strong equivalence of programs in this language we need a system of natural deduction for infinitary formulas, similar to intuitionistic propositional logic.

PDF

TPLP, Online Supplement (2013). http://journals.cambridge.org/downloadsup.php?file=/tlp2013035.pdf.

@article{harrison:tplp13b, title={The Semantics of Gringo and Proving Strong Equivalence}, author={Amelia Harrison}, journal={TPLP, Online Supplement}, note={http://journals.cambridge.org/downloadsup.php?file=/tlp2013035.pdf}, url="http://www.cs.utexas.edu/users/ai-lab?dc_ajh", year={2013} }