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.

PDF

In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR) 2007.

@inproceedings{lif07a, title={A Characterization of Strong Equivalence for Logic Programs with Variables}, author={Vladimir Lifschitz and David Pearce and Agustin Valverde}, booktitle={Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR)}, url="http://www.cs.utexas.edu/users/ai-lab?lif07a", year={2007} }