Reducing Strong Equivalence of Logic Programs to Entailment in Classical Propositional Logic
Fangzhen Lin · Rare & Special e-Zone (The Hong Kong University of Science and Technology) · 2002
Recently Lifschitz, Pearce, and Valverde (2001) introduced a notion of strong equivalence between two logic programs, and showed that it can be captured in a 3-valued logic. In this paper, first for propositional logic programs with default negation, constraints, and disjunctions, we show that there is a simple mapping from these programs to propositional theories that reduces this notion of strong equivalence to entailment in classical propositional logic. Furthermore, we also provide a mapping in the other direction thus show that the problem of checking strong equivalence is co-NP-complete. We then consider logic programs with variables. One surprising result is that while the problem of deciding whether two logic programs are equivalent goes from decidable to undecidable when we move from logic programs without variables to ones with, the problem of deciding whether two logic programs are strongly equivalent remains to be co-NP-complete for logic programs with variables and constants.