解决方案是完整的还是仅反驳的？

Question

经历 一些知识代表教程 目前解决，我遇到了 幻灯片05.KR，第77号.

那里提到“过程也完成”。

我认为这种完整性并不意味着如果句子是KB的，那么它将通过解决方案得出。例如，分辨率无法从具有单一条款$ neg p $的KB中得出$（q lor neg Q）$。 （例如KRR，Brachman和Levesque，第53页）。

谁能帮我弄清楚这张幻灯片的含义？幻灯片的完整性是指排斥统一而不是完整的证明程序吗？

Answer 1

解决方案是驳斥系统的完整。也就是说，如果$ s $是一组矛盾的条款，则分辨率可以反驳$ s $，即$ s vdash bot $。

这足够了，因为$ t vdash a $等于$ t cup { lnot a } vdash bot $。因此，如果我们想看到$ t $的公式$ a $是$ t $的，我们只需要检查是否有$ t cup { lnot a } $的反驳证明，可以使用分辨率检查。

Answer 2

正如您提到的，只有反驳才能完成。这是 故意的 而且非常有用，因为它大大降低了搜索空间。分辨率不必最终得出所有可能的后果（要找到某种猜想的证明），而是试图得出空句。

Answer 3

从以下意义上讲，这也是含义完整的：

如果一组条款$ f $意味着非重言式条款$ c $，那么始终可以得出一个单一条款$ c'$，该$ c'$包含$ c $（即$ c' subseteq c $）。

资源：
ChristianG.Fermüller，《签名决议的暗示完整性》，2002年

请注意，原始结果参考：
RCT Lee。一个完整的定理和计算机程序，用于从给定的公理衍生的定理。博士论文，加利福尼亚大学，伯克利分校，1967年。