数理逻辑之 范式

从上一篇文章数理逻辑之 命题逻辑完备性终于到现在找到了满意的工作：一家大型外企，各方面都很满意。

 

今天开始说范式。先介绍几个概念。

语义等值：令Ф和ψ是命题逻辑公式，我们称Ф和ψ语义等值当且仅当Ф ╞ ψ 且ψ ╞ Ф成立。记为Ф≡ψ。

可满足公式：给定命题逻辑公式Ф，我们说Ф是可满足的，如果存在Ф的一次求值使得Ф取值TRUE. 

 

文字：文字L是指命题原子p或¬p。 L ::= p | ¬p

析取子句：析取子句D是若干个文字的析取 D::= L | L∨D 

合取范式（CNF）：合取范式是若干个析取子句的合取C::=D|DΛC

否定范式（NNF）：如果否定联结符的联结对象只是命题原子的公式称为否定范式

 

 

CNF的构造过程：从Ф的真值表求与之语义等价的CNF

设Ф所含的命题原子为 p1,p2,...,pn。在Ф的真值表中，对于使Ф取值F的任一行l，我们构造一个析取子句Dl（称为最大和）：

Dl = ˆp1∨ˆp2∨ . . . ∨ ˆpn,对于任意1<=i<=n，在第 l 行中若pi为T，则ˆpi取pi，否则取┐pi。

对这样构造得到的所有析取子句进行合取即可得到Ф的CNF。

 

 

例：Ф = (p->┐q)->(q∨┐p)，其真值表如下：

 有三行结果为T的，则Ф≡（pΛq）∨（┐pΛ┐q）∨（┐pΛq）≡（┐pΛq）

CNF 的构造算法叫蕴含释放算法，如下：

 

 

否定范式相对简单，比如p, ¬p, ¬pΛ(pΛq), ¬pΛ(p→q)是NNF实例（注意第一个），¬(pΛq), ¬ ¬p, r→pΛ(¬(p→q))不是NNF实例。

 

NNF的构造算法也基于蕴含释放算法：