Complexity Results for Checking Equivalence of Stratified Logic Programs

Thomas Eiter, Michael Fink, Hans Tompits, Stefan Woltran

Recent research in nonmonotonic logic programming under the answer-set semantics focuses on different notions of program equivalence. However, previous results do not address the important classes of stratified programs and its subclass of acyclic (i.e., recursion-free) programs, although they are recognized as important tools for knowledge representation and reasoning. In this paper, we consider such programs, possibly augmented with constraints. Our results show that in the propositional setting, where reasoning is well-known to be polynomial, deciding strong and uniform equivalence is as hard as for arbitrary normal logic programs (and thus coNP-complete), but is polynomial in some restricted cases. Non-ground programs behave similarly. However, exponential lower bounds already hold for small programs (i.e., with constantly many rules). In particular, uniform equivalence is undecidable even for small Horn programs plus a single negative constraint.

Subjects: 3.3 Nonmonotonic Reasoning; 9.2 Computational Complexity

Submitted: Oct 16, 2006

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.