ASP中的否定

ASP遵循“失败即否定（negation as failure, NAF）”原则，即尝试推导某个原子失败时，就否定该原子。

NAF否定（默认否定）

NAF否定是ASP的默认否定，通过在Atom前加not实现。NAF否定的含义是， $not A$ 为真，当且仅当无法推出 $A$ 为真。

a :- not b.

这个程序有一个回答集：a。因为没有任何一个规则能够推出b为真，所以not b为真，从而a为真。

值得强调，尽管逻辑上可以由约束（即头部为空的规则）或规则体中的aggregates来隐式地推导出某些Atom的真伪，但是NAF规则中的推导是显式的推导，即必须由规则头部来证明。例如：

:- a, not b.
a.

这个程序是unsatisfiable的，因为b没有在任何一个规则的头部出现，也就没有证据证明b是真。根据NAF规则，not b应该为真，从而使第一行的约束无法满足。当运行这样的程序时，clingo会警告某些原子没有在规则头部出现过，这样的原子是underivable的。

经典否定通过在原子前加-来表示。含经典否定的原子必须能够显式地推导，才会被认为是真。事实上，可以认为经典否定-a是一个独立的原子neg_a，加上下面的约束：

:- a, neg_a.

由于经典否定可以看作独立的原子，因此含经典否定的原子必须在规则头部出现，否则将是underivable的。

双重否定的形式是 $not not A$ 。它为真当 $A$ 为真。但不同的是，它不要求推断是无循环的。

看这个例子：

a :- b.
b :- a.

（空）和a b都满足这两条规则，但后者存在循环依赖，因此不能作为答案集。如果用gringo处理这个程序，可以看到两条规则都被删去了。而

a :- not not b.
b :- not not a.

则保留了两个答案集，使用gringo处理可以看到两条规则依原样被保留了下来。

事实上，双重否定等效于一个额外的原子来代表原始原子的NAF否定。考虑下面的程序：

p :- not not p.

如果我们令q :- not p，即：

p :- not q.
q :- not p.

很容易得到两个答案集：p和q。所以原始程序的答案集是（空）和p。

规则头部可以出现not或not not，且可以和双重否定相互等价。在不考虑头部为析取的情况下，有：

not A \leftarrow L . ⟺ \emptyset \leftarrow L, not not A .

以及

not not A \leftarrow L . ⟺ \emptyset \leftarrow L, not A .

头部包含析取的情况下，也可以进行类似的等价^[1]。更深入地理解头部否定和双重否定，需要理解ASP的语义。下一篇再写吧。

Lifschitz V, Tang L R, Turner H. Nested expressions in logic programs[J]. Annals of Mathematics and Artificial Intelligence, 1999, 25: 369-389. ↩︎