我在处理布尔逻辑公式时看到的大多数事情首先将其转换为CNF或DNF格式。 Wikipedia说它“在自动化定理证明中很有用”，但不多。
想知道为什么有必要执行这个步骤，它的哪个方面正在利用哪个算法等等。不知道更多，似乎某些标准算法会利用这个特性，然后所有后续的论文都会有声明这是一项要求。但也许没有必要。
在许多领域中，如果输入首先被标准化，则算法更简单。
在逻辑公式的情况下，主要问题是它们可以任意嵌套。因此，直观地将它们展平并赋予它们规则的结构是有意义的。
事实证明，转换为clauses，特别是如果它们是Horn clauses，是最有用的。他们是像SDL resolution或DPLL这样的程序。这些是逻辑编程，自动定理证明，模型检查，规划等的基础工具。