prolog - 双重否定的输出混淆为失败

Question

我正在尝试学习序言，但遇到了以下问题：

鉴于 -

try(X):-not(not((member(X,[a,b,c])))),write(X). 

我希望查询?- try(X).，因为以下查询类似于

X=a
a;
X=b
b;
X=c
c.

但实际上，输出是：

?- try(X).
_12010
true.

这是为什么？为什么变量没有初始化为某个值？

Answer 1

除了@VictoriaRuiz 所说的，请注意其他一些事情：

?- \+ member(X, [a,b,c]).
false.

这是错误的，因为member(X, [a,b,c])有解决方案，但是当您否定它时，变量绑定会丢失。所以这意味着

?- \+ \+ member(X, [a,b,c]).
true.

是相同的

?- \+ false.
true.

换句话说，X 无处实现。您write(X)发生在 X 的变量绑定范围之外，就好像您这样做了：

?- \+ false, write(X).
_4082
true.

这基本上与

?- write(X).
_4014
true.

如果您想在否定中查看回溯的证据，您可能希望通过以下查询看到它：

?- \+ \+ (member(X, [a,b,c]), write(X), nl).
a
true.

但是因为你第一次尝试就得到了真解，所以否定它是错误的。那么这个否定是真的。所以我们看到它在目标内部产生了一个解决方案(member(X, [a,b,c]), write(X), nl)，这足以知道对它的否定是错误的。再次否定 false 给你 true，但没有变量绑定。

Answer 2

Prolog 以封闭世界假设运行。您提供了一个知识库，只有其中的内容才是真实的。

当你否定时，Prolog 不知道要检查什么值。它不能添加“a”作为值得检查的这个宇宙的一部分。而且由于它不能检查任何东西，它只会返回废话。