prolog - 实践中的一阶逻辑，如何处理不可判定性？

Question

我对这些东西很陌生。希望这不是一个非常幼稚的问题。

我在 Prolog 中尝试了以下公式: A ⇒ B

鉴于 乙是真的，我评价一个 它说假。

我的问题是为什么 FALSE？ (为什么不是 TRUE？)鉴于当前信息，我们对 一无所知。乙 . Prolog 是否基于以下假设工作​​:对于任何未知事物，它会输出 FALSE？

如果这是一个假设，这有多普遍？

想到的另一件事是，它正在寻找输入查询和公理的结合的分配(基本上是 SAT 求解)。由于结果输出为 TRUE，无论 是什么值一个 有，它只是随机选择一个(或默认为零？)。

基于一阶逻辑的性质，它是半可判定的。如果一句话一个 逻辑上暗示一个句子乙那么这可以被发现，但不能反过来。那么，在没有 TRUTH 证明的情况下，后一种情况在实践中是如何处理的呢？

PS1。关于 Prolog 如何工作的一点解释，也可能有用。它是否使用 SAT 求解器作为黑匣子？还是贪心搜索算法？

Answer 1

Does Prolog work based on the assumption that for anything unknown, it outputs FALSE?

是的，确实如此。此行为反射(reflect)了 Closed-World Assumption (CWA)因为如果一个事实没有明确说明，它被认为是错误的。

If this is an assumption, how common is this?

很常见——大多数数据库都使用这个假设。

它可以帮助你了解 Prolog 的推理方法: SLD Resolution .