Eri*_*nda 6 prolog first-order-logic
我正在 Prolog 中寻找一种方法、模式或内置功能，我可以用它来返回原因，至少就数据库中的谓词而言。当用户在系统中提出查询时，我试图能够说的不仅仅是“那是错误的”。
例如，假设我有两个谓词。 blue/1如果某物是蓝色，则为真；dog/1如果某物是狗，则为真：
blue(X) :- ...
dog(X) :- ...
如果我向 Prolog 提出以下查询并且foo是一只狗，但不是蓝色，Prolog 通常只会返回“false”：
? blue(foo), dog(foo)
false.
我想要的是找出为什么谓词的合取不正确，即使它是带外调用，例如：
? getReasonForFailure(X)
X = not(blue(foo))
如果谓词必须以某种方式编写，我没关系，我只是在寻找人们使用过的任何方法。
迄今为止，我完成此操作并取得了一些成功的方法是以程式化的方式编写谓词，并使用一些辅助谓词来找出事后的原因。例如：
blue(X) :-
recordFailureReason(not(blue(X))),
isBlue(X).
然后实现 recordFailureReason/1 ，以便它始终记住堆栈最深处发生的“原因”。如果查询失败，则发生最深的任何失败都会被记录为失败的“最佳”原因。这种启发式方法在许多情况下都出奇地有效，但确实需要仔细构建谓词才能正常工作。
有任何想法吗？我愿意看看 Prolog 之外是否有专为此类分析而设计的谓词逻辑系统。
一些想法：
\n为什么逻辑程序失败：“为什么”的答案当然是“因为没有满足Prolog程序给出的约束的变量赋值”。
\n这显然毫无帮助，但这正是“蓝狗”的情况：不存在这样的东西（至少在您建模的问题中）。
\n事实上，当系统进入完整的定理证明模式并输出时，蓝狗问题的唯一可接受的答案是获得的：
\nblue(X) <=> ~dog(X)\n或者也许只是
\ndog(X) => ~blue(X)\n或者也许只是
\nblue(X) => ~dog(X)\n取决于假设。“没有证据表明有蓝狗”。这是真的，因为程序就是这么说的。所以这个问题中的“为什么”是要求重写程序......
\n可能没有一个好的答案：“为什么没有 x 使得 x\xc2\xb2 < 0”是不适定的，并且可能有答案“只是因为”或“因为你将自己限制为实数”或“因为等式中的 0 就是错误的” ……所以这取决于很多因素。
\n为了使“为什么”更有帮助，您必须以某种方式限定这个“为什么”。这可以通过构建程序并扩展查询来完成，以便在证明树构建期间收集的附加信息不断涌现，但您必须事先决定哪些信息是：
\nquery(Sought, [Info1, Info2, Info3])
并且这个查询总是会成功（对于query/2，“成功”不再意味着“成功找到建模问题的解决方案”而是“成功完成计算”），
变量Sought将是您想要回答的实际查询的具体答案，即原子之一true或false（也许unknown如果您已经受够了二值逻辑），并且Info1, Info2, Info3将是额外的详细信息，以帮助您回答为什么某件事Sought是这样的false。
请注意，大多数时候，询问“为什么”的愿望归因于两种不同失败之间的混淆：“未能找到建模问题的解决方案”和“未能完成计算”。例如，您想要应用于maplist/3两个列表并期望它能够工作，但错误地这两个列表的长度不同：您将得到false- 但它将是一个falsefrom 计算（在本例中，由于错误），而不是一个falsefrom造型。采取严厉措施assertion/1可能会有所帮助，但这本身就是丑陋的。
事实上，与没有逻辑编程部分的命令式或函数式语言相比：如果发生故障（也许是例外？），相应的“为什么”是什么？目前还不清楚。
\n附录
\n这是一个很好的问题，但我越思考它，我就越认为它只能以特定于任务的方式来回答：你必须构建你的逻辑程序，并且你必须决定实际上应该why包含什么样的信息why返回。它将是特定于任务的东西：关于缺失信息的东西，“如果只有这个或那个是真的”指示，其中“这个或那个”是从一组专用谓词中选择的。这当然是预期的，因为也没有通用的方法可以使命令式或函数式程序解释其结果（或缺乏结果）。
我查了一些关于这方面的论文（包括 IEEE Xplore 和 ACM Library），并且刚刚发现：
\n一定还有更多。
\n