Strongly Equivalent Logic Programs (2001)
Vladimir Lifschitz, David Pearce and Agustin Valverde
A logic program PI_1 is said to be equivalent to a logic program PI_2 in the sense of the answer set semantics if PI_1 and PI_2 have the same answer sets. We are interested in the following stronger condition: for every logic program PI, PI_1 union PI has the same answer sets as PI_2 union PI. The study of strong equivalence is important, because we learn from it how one can simplify a part of a logic program without looking at the rest of it. The main theorem shows that the verification of strong equivalence can be accomplished by checking the equivalence of formulas in a monotonic logic, called the logic of here-and-there, which is intermediate between classical logic and intuitionistic logic.
ACM Transactions on Computational Logic, Vol. 2 (2001), pp. 526-541.

Vladimir Lifschitz Faculty vl [at] cs utexas edu