查看“︁否定范式”︁的源代码

[[分类:命题逻辑]]
[[分类:形式语言实例]]{{DEFAULTSORT:fou3ding4fan4shi4}}
{{#seo:
|keywords=代数范式, ANF, Zhegalkin范式, Жегалкина范式, Zhegalkin多项式, Жегалкина多项式, 里德-马勒展开式
|description=代数范式(ANF)是命题公式的标准表示形式，仅使用合取和异或运算。每个布尔函数都有唯一的代数范式，在密码学、电路设计和编码理论中有重要应用，也称为Zhegalkin多项式或里德-马勒展开式。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2025-11-09
}}
{{InfoBox
|name=否定范式
|eng_name=negation normal form
|aliases=NNF
}}
'''否定范式'''('''negation normal form''', '''NNF''')是[[命题公式]]的一种标准形式，其中[[否定]][[逻辑联结词]]仅允许直接出现在[[命题变元]]之前，而不再出现在更复杂的子公式前，且公式中只允许出现基本逻辑连接词。

否定范式是比[[析取范式、合取范式]]还弱的约束，同样要求否定只作用于命题变元，但不要求析取和合取间的层级结构。

== 定义 ==

若一个命题公式形式上满足以下两个条件：
* 否定仅直接作用于原子命题（命题变元）。
* 命题公式中只包含逻辑连接词合取、析取和否定。
则称其为一个'''否定范式'''('''negation normal form''')。

=== BNF 定义 ===

否定范式构成的集合是[[命题语言]]的子集，也符合[[上下文无关文法]]，可以通过 [[BNF]] 定义。

<syntaxhighlight lang="bnf">
<nnf>      ::= <literal>
             | ( <nnf> ∧ <nnf> )
             | ( <nnf> ∨ <nnf> )
<literal>  ::= <atomic> | ¬ <atomic>
<atomic>   ::= "p" | "p₀" | "p₁" | "p₂" | ...
</syntaxhighlight>

== 性质 ==

* 对任意命题公式，都存在与其等价的否定范式。
* 与同一公式等价的否定范式不唯一。多个语法不同但逻辑等值的公式都可以是同一个原公式的否定范式。
* 否定范式的集合覆盖所有可能的真值函数，任意可能的真值函数都能通过其表达。

== 转换算法 ==

任意命题公式都能通过以下步骤转换为否定范式。主要通过反复应用[[德摩根律]]和[[双重否定律]]来实现。

# 消除非基本逻辑联结词（主要指[[蕴含]] <math>\rightarrow</math> 和[[等价（逻辑）|等价]] <math>\leftrightarrow</math> ）：将其他逻辑联结词替换为仅含 <math>\lnot,\land,\lor</math> 的表达方式。
# 消除否定 <math>\lnot</math> ：使用德摩根定律将限定对象不是原子公式的否定符号移到原子公式前。
# 消除可能产生的冗余双重否定，并对公式进行可能的整理。

== 例子 ==

* <math>(A\land B)\lor (\lnot C\lor \lnot D)</math>
* <math>(A\land B)\lor (\lnot C\land \lnot D)</math> 进一步地是析取范式。
反例：
* <math>A\rightarrow B</math>
* <math>\lnot(A\land B)</math>


{{命题逻辑}}