Simplifying Logic Programs Under Uniform and Strong Equivalence

Abstract. We consider the simplification of logic programs under the stablemodel semantics, with respect to the notions of strong and uniform equivalence between logic programs, respectively. Both notions have recently been considered for nonmonotonic logic programs (the latter dates back to the 1980s, though) and provide semantic foundations for optimizing programs with input. Extending previous work, we investigate syntactic and semantic rules for program transformation, based on proper notions of consequence. We furthermore provide encodings of these notions in answer-set programming, and give characterizations of programs which are semantically equivalent to positive and Horn programs, respectively. Finally, we investigate the complexity of program simplification and determining semantical equivalence, showing that the problems range between coNP and ΠP 2 complexity, and we present some tractable cases.

• Type: Conference
• Year: 2004
• Where: LPNMR
• Authors: Thomas Eiter, Michael Fink, Hans Tompits, Stefan Woltran
• Keywords: Logic Programs, LPNMR 2004, Nonmonotonic Logic Programs, Uniform Equivalence