Vladimir Lifschitz, David Pearce and Agustin Valverde
Two sets of rules are said to be strongly equivalent to each other if replacing one by the other within any logic program preserves the program's stable models. The familiar characterization of strong equivalence of grounded programs in terms of the propositional logic of here-and-there is extended in this paper to a large class of logic programs with variables. This class includes, in particular, programs with conditional literals and cardinality constraints. The first-order version of the logic of here-and-there required for this purpose involves two additional non-intuitionistic axiom schemas.
In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR) 2007.

Vladimir Lifschitz Faculty vl [at] cs utexas edu