使用 2 个冲突文字的比例逻辑中的解析反驳

Question

我已经完成了解决规则的消除过程并最终得到了集合。

{pq，不是 p，不是 q}。

根据我的教科书：引理：如果两个子句在多个文字上发生冲突，则它们的解决方案是微不足道的原因……然后继续说对此类子句执行解决方案并非完全不正确，但是由于微不足道的子句有贡献与我们同意删除它们的一组条款的可满足性或不可满足性无关...

但在其他地方我已经阅读过不要删除它们，因为没有理由这两个条款都可能是真的。

那么，able 子句是否会让我留下空集 {} 让我的最终答案是该集是不可满足的？还是我把它作为我的最终答案？问题说证明它是可满足的，所以我猜我应该将条款留在集合中，但教科书说要删除它们。

Answer 1

在您的示例中，没有任何两个子句会在两个文字中发生冲突。两个这样的子句可能是 {p,r,q} 和 {~p,~r,s}，你会得到总是可以满足的 {r,~r,q,s}（重言式）。所以，你会删除它我们没用。

在您的示例中，在对三个子句应用两个解析步骤后，您将得到一个空集：{pq}，~p 产生 q 和 {q}，{~q} 产生一个空集。所以，这组子句是不可满足的。

如果任务是证明某事是可满足的，那么推导的早期肯定有什么问题。