用合取范式推理答案

【问题标题】：Reasoning with Conjunctive Normal Forms用合取范式推理
【发布时间】：2014-11-04 02:19:00
【问题描述】：

我有这段代码，我需要将其翻译成 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 是真的，不是吗？

【问题讨论】：

Prolog 中的多个子句通常表示“或”关系，所以我想你会想要，(p ^ q) v (r v ~q) ...。但是，不清楚这就是您的表达式列表的含义，因为它们并非都是格式正确的 Prolog 子句，并且不会以句点结尾。
如果您有足够的时间，我建议您在 SICStus、SWI 等中查看library(clpb)。
@j4nbur53 多个 谓词子句 表示“OR”而不是“AND”。也许您指的是逗号分隔的查询，即“AND”。例如，如果我写foo(X) :- bar(X). foo(X) :- bah(X).，那是两个谓词子句，如果bar(X) 为真或bah(X) 为真，则意味着foo(X) 为真。如果我写，foo(X) :- bar(X), bah(X). 那么这意味着如果bar(X) 为真且bah(X) 为真，foo(X) 为真。
@j4nbur53 如果我有一个谓词子句，foo(X) :- bar(X), bah(X). 那么它由一个规则头和主体组成。这是一个完整的谓词从句。我的理解是，如果我也有foo(X) :- framus(X).，那么这是谓词foo/1 的另一个“子句”。换句话说，谓词foo/1 由两个谓词子句 组成。也许这是我对术语的误解，但我对合取与析取并不混淆。你能指出一个定义谓词子句的文档吗？我不想继续对定义的错误理解。
这两个（谓词）子句通过连词连接形成确定逻辑程序（=无否定）的理论。它们已经包含析取，因为它们读取 (~bar(X) \/ ~bah(X) \/ foo(X)) 和 (~framus(X) \/ foo(X))。您不能再次以析取方式加入它们，这没有任何意义。另请参阅什么是 Horn 子句：en.wikipedia.org/wiki/Horn_clause（析取形式）

标签： prolog conjunctive-normal-form

【解决方案1】：

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

 Database |- Query

代替一个证明：

 Database, ~Query |- f

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

再见

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

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

【讨论】：

也可以编写一个谓词将 Prolog 公式转换为合取范式。
见编辑 14.02.2019