prolog - 用合取范式推理

Question

我有这段代码，我需要将其翻译成 CNF（这是为考试做准备，所以不是家庭作业！）：

p,q
r :- q
false :- p , s 
s :- t
t

这是我所做的：

p ^ q ^ (r V ~q) ^ (~p V ~s) ^ (s V ~t) ^ t

=  r

我的推理正确吗？

这里还有一个问题：

你想用 r 查询数据库。您应该将什么子句添加到您的数据库中？

我完全不明白这一点。简化后的数据库基本上是r。r 是真的，不是吗？

Answer 1

问题“您想用 r 查询数据库。应该将什么子句添加到数据库中？” 指所谓的反驳证明。在反驳证明中，不证明：

 Database |- Query

而是一个证明：

 Database, ~Query |- f

在经典逻辑中，两者是相同的。因此，在您的示例中，您需要证明 p ^ q ^ (r V ~q) ^ (~p V ~s) ^ (s V ~t) ^ t ^ ~r 会导致矛盾。

再见

编辑 14.02.2019：
如果有人对 Prolog 代码感兴趣，用于将提议公式转换为 CNF，请参见此处https://gist.github.com/jburse/ca8d01e26c7cf176ea65eeb1bf916ea0#file-aspsat-p（第 43-87 行，需要 Prolog Commons列表和排序集），您可以通过调用将公式F转换为 CNF 。Cnorm(F,H), cnf(H,C)

获得的 CNF 已经从琐碎和包含的子句中清除。如果有人对 CNF 测试用例进一步感兴趣，请参见此处http://gist.github.com/jburse/bf992 ​​39903847322321fabf6f49a5b84#file-casescls-p ，它包含来自 Principia Mathematica 的数百个重言式，另外还收集了十分之一的谬误。