On Negative Unfolding in the Answer Set Semantics

摘要

We study negative unfolding for logic programs from a viewpoint of preservation of the answer set semantics. To this end, we consider negative unfolding in terms of nested expressions by Lifschitz et al., and regard it as a combination of the replacement of a literal by its definition (called "pre-negative unfolding") and double negation elimination. We give sufficient conditions for preserving the answer set semantics. We then consider a framework for unfold/fold transformation of locally stratified programs, which, besides negative unfolding, contains replacement rules, allowing a more general form than those proposed by Pettorossi and Proietti. A new folding condition for the correctness proof is identified, which is not required either for definite or stratified programs, but becomes necessary only in case of locally stratified programs. An extension of the framework beyond the class of locally stratified programs is also discussed.