Strong and Uniform Equivalence in Answer-Set Programming: Characterizations and Complexity Results for the Non-Ground Case

Abstract

Recent research in nonmonotonic logic programming under the answer-set semantics studies different notions of equiva-lence. In particular, strong and uniform equivalence are pro-posed as useful tools for optimizing (parts of) a logic pro-gram. While previous research mainly addressed proposi-tional (i.e., ground) programs, we deal here with the more general case of non-ground programs, and provide semantical characterizations capturing the essence of equivalence, gen-eralizing the concepts of SE-models and UE-models, respec-tively, as originally introduced for propositional programs. We show that uniform equivalence is undecidable, and we give decidability results and precise complexity bounds for strong equivalence (thereby correcting a previous complexity bound for strong equivalence from the literature) as well as for uniform equivalence for nite vocabularies.