为什么一个布尔逻辑语句需要是连接正规形式(CNF)

Question

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

想知道为什么有必要执行这一步骤，在哪种算法中利用了这一步骤的哪个方面，等等。如果不了解更多信息，似乎一些标准算法会利用这一功能，那么随后的所有论文都会将其作为一项要求。但也许没有必要。

Answer 1

在许多字段中，如果首先对输入进行规范化，则算法会更简单。

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

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