Strong equivalence for LP^MLN programs

LP^MLN is a probabilistic extension of answer set programs with the weight scheme adapted from Markov Logic. We study the concept of strong equivalence in LP^MLN, which is a useful mathematical tool for simplifying a part of an LP^MLN program without looking at the rest of it. We show that the verification of strong equivalence in LP^MLN can be reduced to equivalence checking in classical logic via a reduct and choice rules as well as to equivalence checking under the “soft” logic of here-and-there. The result allows us to leverage an answer set solver for LP^MLN strong equivalence checking. The study also suggests us a few reformulations of the LP^MLN semantics using choice rules, the logic of here-and-there, and classical logic.