  LPMLN is a probabilistic extension of answer set programs with the weight
scheme adapted from Markov Logic. We study the concept of strong equivalence in
LPMLN, which is a useful mathematical tool for simplifying a part of an LPMLN
program without looking at the rest of it. We show that the verification of
strong equivalence in LPMLN 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 LPMLN strong equivalence checking. The study also suggests us a
few reformulations of the LPMLN semantics using choice rules, the logic of
here-and-there, and classical logic.
