如何理解ASP中的否定失败？

Question

假设我们有以下程序:

human(socrates).
day(tomorrow).
die(X) :- human(X).
may_go_to_school(Y) :- day(Y), 
                       not holiday(Y).

如果我们运行clingo来获取程序的答案集,我们就会得到

Answer: 1
human(socrates) day(tomorrow) die(socrates) may_go_to_school(tomorrow)

我们知道地滚球将首先将所有变量实例化为常数,因此接地后的程序将是:

human(socrates).
day(tomorrow).
die(socrates) :- human(socrates).
may_go_to_school(tomorrow) :- day(tomorrow), 
                              not holiday(tomorrow).

我在Gelfond的书中读到它给出了3个获得答案集的规则:

1. 满足Π的规则.换句话说,如果你相信它的身体,相信一个规则的头.

2. 不要相信矛盾.

3. 坚持"理性原则",其中说:"相信没有你不会被迫相信."

在规则中:

may_go_to_school(tomorrow) :- day(tomorrow), 
                              not holiday(tomorrow).

我们因为失败而得到了否定 not holiday(tomorrow)

如本书所示:

符号not是一种新的逻辑连接,称为默认否定,(或否定为失败); 不是l经常被解读为"不相信我是真的."请注意,这并不意味着l被认为是假的.理所当然,理性推理者既不相信也不相信p否定,这是可以想象的¬p.

然后根据规则1,我应该相信believe in the head of a rule if you believe in its body身体,not holiday(tomorrow).因为我既不相信holiday(tomorrow).也不相信¬holiday(tomorrow).？

根据答案,我应该相信 ¬holiday(tomorrow).

• 那么为什么我们需要这种否定作为失败呢？
• 我们可以只使用经典否定吗？

Answer 1

假设我写了:

may_go_to_school(D) :- not holiday(D).

您期望哪些答案,即这是什么模型？实际给出了什么？

关键问题在于否定是失败是直接实现的,但并不完全捕捉我们在逻辑中对¬的意思.例如,怎么样D = hello？

Answer 2

我们可以只使用经典否定吗？

好吧,我们似乎不能.问题是我们无法实现逻辑否定.主要思想是Prolog为您的程序理论生成一个模型(Herbrand模型).当我们添加否定时,程序的语义会发生变化,因此Prolog可能无法使用sld分辨率找到模型.因此,作为失败的否定具有以下优点:我们可以得到否定(不完全是逻辑否定),并且仍然没有像经典否定那样存在程序语义问题.

您可以查看我的相关问题:Prolog中的逻辑否定.这个问题与这个问题并没有完全相同,但是@ j4n bur53在他的回答中描述了为什么我们不能有逻辑否定.