prolog - 以系统的方式报告*为什么*查询在 Prolog 中失败

Question

我正在 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 之外寻找。

Answer 1

一些想法:
为什么逻辑程序会失败:“为什么”的答案当然是“因为没有满足 Prolog 程序给出的约束条件的变量赋值”。
这显然无济于事，但正是“蓝狗”的情况:没有这样的事情(至少在您建模的问题中)。
事实上，当系统进入完全定理证明模式并输出时，蓝狗问题的唯一可接受的答案是:

blue(X) <=> ~dog(X)

或者也许只是

dog(X) => ~blue(X)

或者也许只是

blue(X) => ~dog(X)

取决于假设。 “没有蓝狗的证据”。这是真的，因为这就是程序所说的。所以这个问题中的“为什么”是要求重写程序......
可能没有一个好的答案:“为什么没有 x 使得 x² < 0”是不适定的，并且答案可能是“仅仅因为”或“因为你将自己限制在实数中”或“因为在这个等式是错误的”……所以这在很大程度上取决于。
为了使“为什么”更有帮助，您必须以某种方式限定这个“为什么”。这可以通过构建程序和扩展查询来完成，以便在证明树构建期间收集的额外信息冒泡，但您必须事先决定哪些信息是:query(Sought, [Info1, Info2, Info3])并且此查询将始终成功(对于 query/2 ，“成功”不再意味着“成功找到建模问题的解决方案”而是“成功完成计算”)，
变量 Sought将是您想要回答的实际查询的具体答案，即原子之一 true或 false (也许 unknown 如果你已经受够了二值逻辑)和 Info1, Info2, Info3将提供更多详细信息，以帮助您回答为什么会出现某些情况 Sought是 false .
请注意，很多时候，询问“为什么”的愿望归结为两种不同失败之间的混淆:“未能找到建模问题的解决方案”和“未能完成计算”。比如你要申请maplist/3到两个列表并期望它可以工作但错误地两个列表的长度不同:您将得到 false - 但它会是 false来自计算(在这种情况下，由于错误)，而不是 false从建模。粗暴对待 assertion/1可能会在这里有所帮助，但这本身就是丑陋的。
事实上，与没有逻辑编程部分的命令式或函数式语言相比:如果发生故障(可能是异常(exception)？)，相应的“为什么”是什么？目前还不清楚。
附录
这是一个很好的问题，但我思考得越多，我就越认为它只能以特定于任务的方式来回答:您必须将逻辑程序构建为 why - 能够，你必须决定什么样的信息why实际上应该返回。这将是特定于任务的东西:关于缺少信息的东西，“如果只有这个或那个是真的”指示，其中“这个或那个”是从一组专用谓词中选择的。这当然是意料之中的，因为也没有通用的方法可以让命令式或函数式程序解释它们的结果(或缺乏结果)。
我已经查找了一些关于此的论文(包括 IEEE Xplore 和 ACM 库)，并且刚刚发现:

Reasoning about Explanations for Negative Query Answers in DL-Lite这实际上用于描述逻辑并使用 abductive reasoning .

WhyNot: Debugging Failed Queries in Large Knowledge Bases其中讨论了 Cyc 的工具.

我还随机查看了 Flora-2 的文档。但他们基本上似乎在说“使用调试器”。但是调试只是调试，而不是解释。

必须有更多。