如何将命题公式转换为合取范式（CNF）？答案

【问题标题】：How to convert a propositional formula to conjunctive normal form (CNF)?如何将命题公式转换为合取范式（CNF）？
【发布时间】：2009-03-17 17:31:02
【问题描述】：

如何将此方程转换为 CNF？

¬((p ∨ ¬Q) ⊃ R) ⊃ (P ∧ R))

【问题讨论】：

【解决方案1】：

要将propositional formula 转换为conjunctive normal form，请执行以下两个步骤：

将否定推入公式，重复应用De Morgan's Law，直到所有否定仅适用于原子。您在negation normal form 中获得了一个公式。
- ¬(p ∨ q) 到 (¬p) ∧ (¬q)
- ¬(p ∧ q) 到 (¬p) ∨ (¬q)
重复应用distributive law，其中一个析取发生在一个连词上。一旦这不再可能，公式就在 CNF 中。
- p ∨ (q ∧ r) 到 (p ∨ q) ∧ (p ∨ r)

要获得析取范式的公式，只需在步骤 2 中应用 ∧ 对 ∨ 的分布即可。

问题中使用的子集符号 (⊂) 只是逻辑蕴含/蕴含的另一种表示法，通常写为箭头 (⇒)。

【讨论】：

【解决方案2】：

http://en.wikipedia.org/wiki/Conjunctive_normal_form

将一阶逻辑转换为 CNF：

转换为否定范式。

消除影响：将 x → y 转换为 ¬ x ∨ y

向内移动 NOT。

标准化变量

对声明进行梳理

删除通用量词

在 OR 上分配 AND。

（人工智能：现代方法 [1995...] Russel 和 Norvig）

【讨论】：

【解决方案3】：

我可以建议这个吗？页面上有转化算法。

【讨论】：

我会说它被称为算法有点高级。 “在 OR 上分配 AND”不足以描述该算法。
@jamie 这意味着应用分配律。这是一个非常准确的描述。
@ziggystar 那你是怎么做到的呢？很明显，您和其他任何对逻辑有任何理解的人都会发现这一步非常简单和明显，因为它需要天的搜索才能找到描述。顺便说一句，我找到的最终答案是谷歌上的付费答案。
@jamie 分配法是在德国数学五年级教授的（我刚刚查过）。我不认为有人在 SO 上问事情不知道。也许你没有理解答案中的短语。但是，如果您不理解我的重新表述（“应用分配律”） - 抱歉。

【解决方案4】：

我在 Java 中实现了一个小工具，可以将布尔表达式基本转换为 (C|D)NF。如果你有兴趣，你可能想看看https://github.com/julianthome/ctrans。该实现基于these lecture notes。更详细的描述可以在here 找到。任何反馈将不胜感激;-)。

【讨论】：