Replacements in Non-Ground Answer-Set Programming
In this paper, the authors propose a formal framework for specifying rule replacements in non-monotonic logic programs within the answer-set programming paradigm. Of particular interest are replacement schemas retaining specific notions of equivalence, among them the prominent notions of strong and uniform equivalence, which have been introduced as theoretical tools for program optimization and verification. The authors derive some general properties of the replacement framework with respect to these notions of equivalence. Moreover, they generalize results about particular replacement schemas which have been established for ground programs to the non-ground case. Finally, they report a number of complexity results which address the problem of deciding how hard it is to apply a replacement to a given program.