Thomas Eiter, Michael Fink, Hans Tompits, Stefan Woltran
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.
Content Area: 11. Logic Programming
Subjects: 9.2 Computational Complexity; 3.3 Nonmonotonic Reasoning
Submitted: May 10, 2005