需要一些有关解决规则证明的提示
这是一份家庭作业。我试图证明 (avb) ^(~b V c) |= (a V c)
这是一个正确的解析规则。而且我不允许使用解析规则来证明这一点。 有点困惑，不知道我首先应该做什么。.
还有一个问题，老师让我们证明KB |= a，当KB ^ ~a > 无法满足。据我所知，我可能需要构建一个包含几个句子的知识库，然后我可以证明 KB ^ ~a 是不可满足的。但老师告诉我，如果我想推导出一个例子，我必须让它适合每一种情况。我想知道是否有一个通用的例子可以证明这一点？我必须使用示例吗？
希望有人能给我一些提示或有用的链接..谢谢..
It's a homework. I'm trying to prove that (a v b) ^(~b V c) |= (a V c)
it's a correct resolution rule. And I'm not allowed to use resolution rule to prove it.
Get little confusing, don't know what should I do at the first place..
And another problem, teacher let us to prove KB |= a, when KB ^ ~a is unsatisfiable. as far as I know , I may need to build a KB which includes several sentences, then I can prove
KB ^ ~a is unsatisfiable. but teacher told to me If I want to derive an example, I have to let it suit for every cases. I want to know is there an universal example to prove that? Do I have to use example?
Hope somebody can give me some hints or useful links.. Thanks..
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您可以按照第三段中描述的规则来做到这一点：
首先，构建您所知道的所有内容的知识库：即
av b和~bv c。然后添加您要证明的命题的否定：
~(avc)。您可以在 CNF 中重写它并将其添加到 KB 中。现在证明这个知识库是不可满足的。有两种方法可以做到这一点：
只需制作一个真值表。
a、b、c有八种可能的分配方式，因此它有八行；您可以证明知识库中至少有一个语句对于任何可能的分配都是错误的。这不是一个“示例”，因为您正在考虑所有可能的情况。根据您使用的模型，您可以在知识库本身中进行一些推断。您将得到一些简单断言某个变量为真或假的语句；然后，您可以使用该事实来简化知识库中的其他语句。不过，您需要检查是否以适合您的形式主义的方式执行此操作。
因此，要证明
KB ^ ~a不可满足意味着KB |= a，请进行反证法：KB。KB，~a是可满足的。KB时~a是不可满足的。现在你已经差不多了。
You can do it with the rule you describe in the third paragraph:
First, build a knowledge base of everything you know: namely
a v band~b v c.Then add the negation of the statement you're trying to prove:
~(a v c). You can rewrite this in CNF and add it to the KB.Now show that this KB is unsatisfiable. There are two ways you can do this:
Just make a truth table. There are eight possible assignments to
a,b,c, so it'll have eight rows; you can show that at least one statement in the KB is false for any possible assignment. This isn't an "example", because you're considering all possible cases.Depending on the models you're using, you can make some inference within the KB itself. You'll have some statements that simply assert that a certain variable is true or false; you can then use that fact to simplify other statements in the KB. You'll want to check that you're doing this in a way that's appropriate in your formalism, though.
So, to prove that
KB ^ ~abeing unsatisfiable impliesKB |= a, do a proof by contradiction:KB.KB,~ais satisfiable.KB ^ ~ais satisfiable -- which you're proving is false, ieKB ^ ~ais unsatisfiable.~ais unsatisfiable givenKB.Now you're pretty much there.