否定只作用于变量或原子，公式为文字（literal）由合取、析取所联结。
将公式转换为 NNF 不影响计算属性，公式大小为线性。做法是用 De Morgan 律并消去双重否定。
Related
- Tseytin transformation 如果进一步应用分配律转为 CNF 或 DNF，公式规模为指数。对于 CNF，可通过引入辅助变量限制在线性大小。
否定只作用于变量或原子，公式为文字（literal）由合取、析取所联结。
将公式转换为 NNF 不影响计算属性，公式大小为线性。做法是用 De Morgan 律并消去双重否定。