否定范式
| 否定范式 | |
|---|---|
| 术语名称 | 否定范式 |
| 英语名称 | negation normal form |
| 别名 | NNF |
否定范式(negation normal form, NNF)是命题公式的一种标准形式，其中否定逻辑联结词仅允许直接出现在命题变元之前，而不再出现在更复杂的子公式前，且公式中只允许出现基本逻辑连接词。
否定范式是比析取范式、合取范式还弱的约束，同样要求否定只作用于命题变元，但不要求析取和合取间的层级结构。
定义
若一个命题公式形式上满足以下两个条件：
- 否定仅直接作用于原子命题（命题变元）。
- 命题公式中只包含逻辑连接词合取、析取和否定。
则称其为一个否定范式(negation normal form)。
BNF 定义
否定范式构成的集合是命题语言的子集，也符合上下文无关文法，可以通过 BNF 定义。
<nnf> ::= <literal>
| ( <nnf> ∧ <nnf> )
| ( <nnf> ∨ <nnf> )
<literal> ::= <atomic> | ¬ <atomic>
<atomic> ::= "p" | "p₀" | "p₁" | "p₂" | ...
性质
- 对任意命题公式，都存在与其等价的否定范式。
- 与同一公式等价的否定范式不唯一。多个语法不同但逻辑等值的公式都可以是同一个原公式的否定范式。
- 否定范式的集合覆盖所有可能的真值函数，任意可能的真值函数都能通过其表达。
转换算法
任意命题公式都能通过以下步骤转换为否定范式。主要通过反复应用德摩根律和双重否定律来实现。
- 消除非基本逻辑联结词（主要指蕴含 [math]\displaystyle{ \rightarrow }[/math] 和等价 [math]\displaystyle{ \leftrightarrow }[/math] ）：将其他逻辑联结词替换为仅含 [math]\displaystyle{ \lnot,\land,\lor }[/math] 的表达方式。
- 消除否定 [math]\displaystyle{ \lnot }[/math] ：使用德摩根定律将限定对象不是原子公式的否定符号移到原子公式前。
- 消除可能产生的冗余双重否定，并对公式进行可能的整理。
例子
- [math]\displaystyle{ (A\land B)\lor (\lnot C\lor \lnot D) }[/math]
- [math]\displaystyle{ (A\land B)\lor (\lnot C\land \lnot D) }[/math] 进一步地是析取范式。
反例：
- [math]\displaystyle{ A\rightarrow B }[/math]
- [math]\displaystyle{ \lnot(A\land B) }[/math]