Strong equivalence is an important concept in the theory of answer set programming. Informally speaking, two sets of rules are strongly equivalent if they have the same meaning in any context. Equilibrium logic was used to prove that sets of rules expressed as propositional formulas are strongly equivalent if and only if they are equivalent in the logic of here-and-there. We extend this line of work to formulas with infinitely long conjunctions and disjunctions. This is useful because of the relationship between infinitary formulas and logic programs with local variables.

PDF

Artificial Intelligence, Vol. 246 (2017).

@article{harrison:aij16, title={Infinitary Equilibrium Logic and Strongly Equivalent Logic Programs}, author={Amelia Harrison and Vladimir Lifschitz and David Pearce and Agustín Valverde}, volume={246}, journal={Artificial Intelligence}, url="http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=127548", year={2017} }