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

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

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.