On Negative Unfolding in the Answer Set Semantics
On Negative Unfolding in the Answer Set Semantics
复制标题
DOI：
10.1007/978-3-642-00515-2_12
复制
发表时间：
2009-03
期刊：
影响因子：
--
通讯作者：
H. Seki
中科院分区：
文献类型：
--
作者：
H. Seki
我们从保留答案集语义的角度研究逻辑程序的负展开。为此，我们根据 Lifschitz 等人的嵌套表达式来考虑负展开，并将其视为文字定义替换（称为“预负展开”）和双重否定消除的组合。我们给出了保留答案集语义的充分条件。然后，我们考虑局部分层程序的展开/折叠转换的框架，该框架除了负向展开之外，还包含替换规则，从而允许比 Pettorossi 和 Proietti 提出的形式更通用的形式。确定了正确性证明的新折叠条件，这对于确定程序或分层程序都不是必需的，但仅在局部分层程序的情况下才变得必要。还讨论了该框架超出本地分层计划类别的扩展。
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.