需要关于解决方案规则的一些提示证明

Question

这是一项家庭作业。我试图证明（一个V B）^（〜B）（V C）| =（为V C）

这是一个正确的解决规则。而且我不允许使用解析规则来证明它。 获取有点混乱，不知道我应该在第一个地方做..

而另外一个问题，老师让我们来证明KB | =一个，当KB ^〜一是不可满足的。据我所知，我可能需要建立一个包含几个句子的知识库，然后我可以证明 KB^a是不可满足的。但老师告诉我如果我想要举一个例子，我必须让它适合每一种情况。我想知道有没有一个通用的例子来证明这一点？我必须使用示例吗？

希望有人可以给我一些提示或有用的链接..谢谢..

Answer 1

你可以用你的第三段描述规则做到这一点：

首先，构建所有的知识库你知道：即a v b和~b v c。

然后添加你想证明声明的否定：~(a v c)。您可以在CNF中重写该文件并将其添加到KB中。

现在显示这个KB是不可满足的。有两种方法可以做到这一点：

• 只是做一个真值表。有8个可能的作业a,b,c，所以它会有八行;您可以显示KB中至少有一条语句对于任何可能的分配都是错误的。这不是一个“例子”，因为你正在考虑所有可能的情况。

• 根据您所使用的模型，可以使KB本身的一些推断。你会有一些陈述，只是断言某个变量是真或假;那么您可以使用该事实来简化KB中的其他语句。尽管如此，你仍然希望检查你是否以适合你的形式来做这件事。

---

所以，为了证明KB^~a是不可满足的暗示KB |= a，由矛盾做一个证明：

• 你有KB。
• 假设，给出KB，~a是满足的。
• 但是，如果这是真的，那么KB^~a可满足 - 这你证明是虚假的，即KB^~a是不可满足的。
• 因此，我们必须假设错了，所以~a是不可满足给定KB。

现在，你几乎没有。