在 Prolog 中，谓词答案

【问题标题】：In Prolog, predicate在 Prolog 中，谓词
【发布时间】：2017-11-30 00:00:56
【问题描述】：

以下 Prolog 目标是否令人满意？

croire(X, aime(lila, pizza)) = croire(ali, aime(Y, pizza))?

我发现一个 Prolog 文档问这个问题，答案是：“不，这个目标在语法上不正确”但是当我在 SWI-Prolog 中尝试它时，它没有显示任何错误，它给了我这个作为我认为合乎逻辑的答案：

X = ali,
Y = lila.

那么有什么我错过的吗？还是文档的答案是错误的？

【问题讨论】：

你能发布一个链接到声明这个文件的链接吗？
我认为这似乎与认知逻辑有关。这是一种可以在 Prolog 中模拟的逻辑形式，但可能需要一些额外的基础设施。
是法语的，你可以吗？
问号是语法错误的原因
@CapelliC 因为 OP 运行它并得到了结果，我认为这只是问题中的一个符号错误。但是，如果引用的（但未显示）文本确实包含一个问号作为输入语法的一部分，那么它确实是错误的。

标签： prolog functor

【解决方案1】：

首先，查询在 GNU Prolog 中也可以满足（请注意，Prolog 查询总是以点结尾，而不是问号）：

GNU Prolog 1.4.4 (64 bits)
Compiled Aug  3 2017, 08:15:35 with gcc
By Daniel Diaz
Copyright (C) 1999-2013 Daniel Diaz
| ?- croire(X, aime(lila, pizza)) = croire(ali, aime(Y, pizza)).

X = ali
Y = lila

(1 ms) yes

那是什么意思？我们询问变量X 和Y 是否存在赋值，使得croire(X, aime(lila, pizza)) 和croire(ali, aime(Y, pizza)) 相等。 GNU Prolog 返回一个答案，即X = ali, Y = lila。让我们看看当我们应用这个替换时我们得到了哪些术语：

croire(ali, aime(lila, pizza)) = croire(ali, aime(lila, pizza))

因为一个词项肯定等于它自己，所以这个替换满足相等谓词。另一方面，X = reine, Y = grenouille 导致

croire(reine, aime(lila, pizza)) = croire(ali, aime(grenouille, pizza))

这是 -- 没有进一步的假设 -- 错误。

备注：我发现在这种情况下可以满足的术语非常令人困惑。尽管我应该知道得更多，但我仍在努力对正在发生的事情进行良好的描述，但我会尝试：

Prolog 的推理机制是解决，旨在导出矛盾，但矛盾是一个不可满足的公式。在这种特殊情况下，我们将 Z != Z 解析为 croire(X, aime(lila, pizza)) = croire(ali, aime(Y, pizza)) 以获得（不可满足的）空子句。

如果我们以积极的方式写下子句集，它看起来像这样：

∀Z (Z=Z) ⊃ ∃X ∃Y (croire(X, aime(lila, pizza)) = croire(ali, aime(Y, pizza)))

将量词拉到前面，我们得到：

∃Z ∃X ∃Y ( Z=Z ⊃  (croire(X, aime(lila, pizza)) = croire(ali, aime(Y, pizza))) )

现在，如果Z=Z ⊃ (croire(X, aime(lila, pizza)) = croire(ali, aime(Y, pizza))) 是可满足的，那么它的存在闭包是有效的。我发现很难以这种方式精确，通常只说查询的答案（替代）。然后我可以将通过应用答案替换获得的子句集称为不可满足而不会混淆。

【讨论】：

你的反例有点混乱：替换 X = reine, Y = grenouille 导致 croire(reine, aime(lila, pizza)) = croire(ali, aime(grenouille, pizza)). ;-)
您说的完全正确，谢谢！现在应该纠正这个错误。还要感谢 @false 纠正我的法语拼写。
从逻辑上讲，查询首先被否定。如果找到否定查询的反驳，则表示肯定（原始）查询是可满足的！
en.m.wikipedia.org/wiki/… 表达得很好。归结为：罗宾逊对子句集的解析不是强完备的，但它是驳斥完备的。