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

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 20

Logic Programming

Recent research in nonmonotonic logic programming under the answer-set semantics focuses on different notions of equivalence. In particular, strong and uniform equivalence are proposed as useful tools for optimizing (parts of) a logic program. Whereas most previous research in this direction addressed only ground logic programs (i.e., programs without variables), in this paper, we deal with the more general case of non-ground programs. More specifically, we discuss languages with both finite and infinite vocabularies and provide semantical characterizations capturing the essence of equivalence, generalizing the concepts of SE-models and UE-models, respectively, as originally introduced for propositional programs. We furthermore show that, for infinite vocabularies, uniform equivalence between disjunctive programs is undecidable, and we provide decidability results and precise complexity bounds for strong equivalence, for both finite and infinite vocabularies, and for uniform equivalence for finite vocabularies, thereby correcting a previous complexity bound for strong equivalence from the literature.