Uniform Equivalence of Logic Programs under the Stable Model Semantics

In recent research on nonmonotonic logic programming, repeatedly strong equivalence of logic programs P and Q has been considered, which holds if the programs P ∪ R and Q∪ R have the same stable models for any other program R. This property strengthens equivalence of P and Q with respect to stable models (which is the particular case for R= ∅), and has an application in program optimization. In this paper, we consider the more liberal notion of uniform equivalence, in which R ranges only over the sets of facts rather than all sets of rules. This notion, which is well-known, is particularly useful for assessing whether programs P and Q are equivalent as components in a logic program which is modularly structured. We provide semantical characterizations of uniform equivalence for disjunctive logic programs and some restricted classes, and analyze the computational cost of uniform equivalence in the propositional (ground) case. Our results, which naturally extend to answer set semantics, complement the results on strong equivalence of logic programs and pave the way for optimizations in answer set solvers as a tool for input-based problem solving.