boolean-logic - 为什么布尔逻辑语句需要采用联合范式 (CNF)

Question

我在处理布尔逻辑公式时看到的大多数事情都是首先将其转换为 CNF 或 DNF 形式。维基百科说它“在自动定理证明中很有用”，但仅此而已。

想知道为什么需要执行这一步，在哪个算法中利用了它的哪个方面等等。如果不知道更多，似乎一些标准算法会利用这个特性，那么所有后续论文都会有将其声明为一项要求。但也许没有必要。

Answer 1

在许多领域，如果首先对输入进行归一化，算法会更简单。

在逻辑公式的情况下，主要问题是它们可以任意深度嵌套。因此，将它们展平并赋予它们规则的结构在直觉上是有意义的。

事实证明，转换为从句，特别是如果它们是Horn 从句，是最有用的。它们是SDL 解析或DPLL等程序使用的。这些是逻辑编程、自动定理证明、模型检查、规划等方面的基本工具。