数理逻辑之 horn公式

Horn公式，中文名一般翻译成“霍恩公式”，也是范式的一种。

Horn原子有三：

P::= ┴ | T |p       Horn原子

 分别是底公式、顶公式和命题原子。

Horn原子合取后的蕴含称为Horn字句：

A::= P | PΛA 
C::= A → P        Horn子句

 继续合取就是Horn公式：

H::= C | CΛH         Horn公式

下面的都是Horn公式例子：

(pΛqΛr->p)Λ(pΛqΛr->q)Λ(pΛqΛr->r)
(pΛqΛr->┴)Λ(pΛr->q)Λ(T->r)
(p1Λq2Λr3->p13)Λ(T->q)Λ(p4Λq5->┴)

 下面的都不是Horn公式实例：

(pΛqΛr->┐p)Λ(pΛqΛr->q)Λ(pΛqΛr->r)   包含了命题原子否定
(pΛqΛr->┴)Λ(pΛ┐r->q)Λ(T->r)
(p1Λq2Λr3->p13Λr30)Λ(T->q)Λ(p4Λq5->┴)  蕴含右边是合取公式而非命题原子
(T->q)Λ(p4Λq5)                             字句有不是蕴含关系的

对于给定的Horn公式，是否是可满足的（还记得这个概念吗），我们有一个简单的算法：

 Horn公式的可满足判定算法HORN是正确的且算法HORN的执行过程中，while语句至多被执行的次数不超过n+1次。其中n是Ф中所含的命题原子数目。

先来证明第二个论断：算法HORN执行过程中while语句被执行的次数不超过n+1次。

由于在执行while语句之前已对T作标记，且执行while语句的语句体一次就标记一个尚未标记的P（P可能是命题原子或┴）于是只能进行不超过n+1次标记。

再来证明它的正确性。为了证明算法HORN的正确性，我们先需证明以下论断：

“对于所有使Ф取值T的求值v必使所有被标记的P为T。”  ------（*）

我们对while语句的执行次数k作数学归纳法。

归纳基本步：k=0时，此时被标记的仅是T，于是（*）成立。

归纳假设：假设在执行while语句k次后（*）成立，要证明执行while语句（k+1）次后（*）也成立。

设在第k+1次执行while语句时，有Ф的子句满足：所有P_j已被标记，而P’尚未被标记。记v是任一使Ф取值为真的一次求值。根据归纳假设，v使所有p_j为TRUE，从而子句左边为TRUE。又子句为TRUE。于是P’必为TRUE。其次我们对算法HORN中的if语句作分析。

[1]若┴被标记，如果有使Ф取值TRUE的求值v, 由（*）可知，该子句必在v中取值为FALSE。这是不可能的。于是Ф不可满足。

[2]若┴始终没有被标记，此时，令被标记的命题原子取T而未被标记的原子取F。则Ф在此求值中必取值TRUE。

事实此时Ф中任一子句中要么所有的P_j连同P’已被标记，因而取值TRUE；要么中存在有尚未被标记的P_j, 由此得取值FALSE，由”→”的语义定义可知，取值TRUE。