Prolog 统一与 not()答案

【问题标题】：Prolog Unification with not()Prolog 统一与 not()
【发布时间】：2016-09-24 17:49:53
【问题描述】：

我只是在学习prolog，有件事我无法理解。

假设我有以下程序

value(v).

a(X) :- not(value(X)).

所以a(v). 给了我错误，因为value(v) 可以被证明是正确的。

a(w) 给了我真实的感觉，因为没有事实 value(w)，因此，即使尝试，也无法证明它是正确的。

在我的理解中，请求a(X). 应该给我第一个使value(X) 无法证明的可能值。应该有无数种可能性，因为只有value(v) 是正确的。

但为什么 Prolog 一直回复 false？

【问题讨论】：

看你怎么看falsification，什么是假的？你如何证明某事是假的？它的一种观点是所有不可证明的都是假的，这是一种你想象你生活在一个一切都是真的是可证明的（这当然是有争议的）。在序言中，\+ 运算符使用否定作为失败语义，这就是我在上面试图描述的。希望能提供一些线索。
是的，如果我们将 false 定义为不可证明，那么 Prolog 是否可以通过提供无法证明正确的示例来实现目标？
但我想问题是Prolog总是希望让事情变得真实，在这种情况下，我们基本上会反转引擎？

【解决方案1】：

首先，请使用 ISO 谓词 (\+)/1 而不是 not/1。

其次，请不要使用(\+)/1 表示术语的不等式：(\+)/1 在 Prolog 中不完整，因此在逻辑上不正确。它是非逻辑的否定，而是表示“不可证明”。

在你的情况下：?- value(X). 成功，所以它是可证明的，所以?- \+ value(X). 失败，尽管有使查询成功的实例化。

尤其是?- \+ value(a).成功。

所以我们有：

?- \+ 值（V）。错误。

但是更具体的查询会成功：

?- V = a，\+ 值（V）。 V = a。

这显然与我们期望的纯关系的逻辑属性背道而驰。见logical-purity。

要表示不等式项，请使用dif/2。如果您的 Prolog 系统不支持 dif/2，请要求将其包含在内，或使用 iso_dif/2 作为逻辑上合理的安全近似值。请参阅 prolog-dif 了解更多信息。

【讨论】：

好的，我明白了。因此，为了实现我想要的功能，Prolog 需要提出一个无法证明的示例，这是设计无法实现的。所以基本上，一个人可以在 Prolog 中实现这一点（尽管可能不是可取的）并得到我提到的行为？还是我遗漏了一些基本的逻辑概念？
在您的情况下，只需使用dif/2 或其他约束来表达不等式：dif(X, v) 表示X 与原子v 是不同。这成功了，只要不知道目标是否成立，就会留下 剩余目标。对于其他领域，也有类似的限制。例如，X #\= 3 声明 X 是一个不同于 3 的整数。

【解决方案2】：

Prolog 在“封闭世界假设”下运行——它只知道我们告诉它的内容。特别是，我们没有告诉它没有w、u 或任何其他东西，那么它怎么会向我们提供它们呢？为什么w 应该出现在u 之前，而不是相反？

唯一明智的可能是产生(X, dif(X,v))，但这将是一个不同问题的答案，即“如何制作@ 987654326@ provable?”，不是 Prolog 实际回答的那个，即 “a(X) 是否可以证明？”。

为了减轻您的认知负担，请将您脑海中的 Prolog 提示回复从 true 重命名为 Yes，并从 false 重命名为 No。

Yes 意味着 Prolog 告诉我们“是的，我可以证明它！”，而No – “不，我无法证明它。”

另外~~将“not”重命名为~~在心理上将\+读作not_provable。

【讨论】：