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语句时,有Ф的子句满足:所有Pj已被标记,而P’尚未被标记。记v是任一使Ф取值为真的一次求值。根据归纳假设,v使所有pj为TRUE,从而子句左边为TRUE。又子句为TRUE。于是P’必为TRUE。其次我们对算法HORN中的if语句作分析。
[1]若┴被标记,如果有使Ф取值TRUE的求值v, 由(*)可知,该子句必在v中取值为FALSE。这是不可能的。于是Ф不可满足。
[2]若┴始终没有被标记,此时,令被标记的命题原子取T而未被标记的原子取F。则Ф在此求值中必取值TRUE。
事实此时Ф中任一子句中要么所有的Pj连同P’已被标记,因而取值TRUE;要么中存在有尚未被标记的Pj, 由此得取值FALSE,由”→”的语义定义可知,取值TRUE。
相关推荐
文档介绍了Horn集的概念和Horn逻辑的详细介绍,对了解Horn集上的语义归结和调换有一定帮助。
作为ARTIGENCE的描述逻辑组件,这是迄今为止具有可确定的推理过程的最具表现力的描述逻辑之一。 我们还表明,在我们提出的框架中使用的特定描述逻辑ACLNR不是强制性的,其他可确定的描述逻辑,甚至它们的概率版本也...
光流算法:Horn-Schunck方法,效果不错。
The horn antenna is widely used in thetransmission and reception of RF microwave signals. It isusually an assembly of flaring metal waveguide andantenna. Beyond the fundamental knowledge of ...
Horn-Schunck 光流场 的经典算法,matlab程序,可直接用 联合开发网...
Horn R A, Johnson C R, Matrix Analysis
Aroon Horn 指标
矩阵分析-horn 中文版 经典书籍 ,已经绝版 中文扫描版
Matlab code for Horn-Schunck method
矩阵分析-horn,控制科学与工程一本不可或缺的书。其中涉及了,数值分析和矩阵处理内容,是交我自适应控制老师推荐给我的,拿来和大家分享!
金字塔Horn-Schunck光流算法的实现,能够较好地解决大位移的问题。在VS2017下实现,并使用了OpenCV库,运行时,请自己设置项目的属性,添加OpenCV库。
矩阵分析 Horn 原书第二版 需要的朋友可以下载 大家一起学习
1.领域:matlab,Lucas-Kanade和Horn-Schunck算法 2.内容:对视频目标进行光流提取,对比Lucas-Kanade和Horn-Schunck+matlab操作视频 3.用处:用于Lucas-Kanade和Horn-Schunck算法编程学习 4.指向人群:本硕博等...
Big Horn Audio Project and drawings
矩阵分析 第2版 Matrix_Analysis_2nd_Horn.pdf Horn编写 机器学习必备
Matrix+Analysis+(Horn,Johnson).part1.rar 下下看吧
Horn-Schunck 法实现的光流法
【EN】【Matrix analysis】【矩阵分析】【R. A. Horn & C. R. Johnson】【Cambridge University Press】【1990】
数学基础课矩阵分析Roger.A.Horn版本经典教材讲义,值得推荐!
论文Determining Optical flow 的代码实现,使用了OpenCV库,效果较好。 实现环境为:VS2017