T. Eiter, M. Fink, S. Woltran:
"Semantical Characterizations and Complexity of Equivalences in Answer Set Programming";
Report for TU Wien, Institut fuer Informationssysteme, INFSYS RR-1843-05-01;
In recent research on non-monotonic logic programming, repeatedly
strong equivalence of logic programs P and Q has been considered,
which holds if the programs P union R and Q union R have the same
answer sets for any other program R. This property strengthens
equivalence of P and Q with respect to answer sets (which is the
particular case for R is the empty set), and has its applications
in program optimization, verification, and modular logic programming.
In this paper, we consider more liberal notions of strong equivalence,
in which the actual form of R may be syntactically restricted.
On the one hand, we consider uniform equivalence, where R is a set of
facts rather than a set of rules. This notion, which is well known
in the area of deductive databases, is particularly useful for assessing
whether programs P and Q are equivalent as components of a logic program
which is modularly structured.
On the other hand, we consider relativized notions of equivalence,
where R ranges over rules over a fixed alphabet, and thus generalize our
results to relativized notions of strong and uniform equivalence.
For all these notions, we consider disjunctive logic programs
in the propositional (ground) case, as well as some restricted classes,
provide semantical characterizations and analyze the computational
complexity. Our results, which naturally extend to answer set semantics for
programs with strong negation, complement the results on strong equivalence
of logic programs and pave the way for optimizations in answer set solvers
as a tool for input-based problem solving.
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.