版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
谓词逻辑与归结原理华北电力大学计算机系2/5/20231第三章谓词逻辑与归结原理归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理2/5/20232华北电力大学归结推理命题逻辑谓词逻辑Skolem标准型、子句集基本概念谓词逻辑归结原理合一和置换、控制策略数理逻辑命题逻辑归结Herbrand定理内容框架2/5/20233华北电力大学第三章谓词逻辑与归结原理归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略2/5/20234华北电力大学概述-推理技术推理按照某种策略从已有事实和知识推出结论的过程。推理是由程序实现的,称为推理机医疗诊断专家系统知识库中存储经验及医学常识数据库中存放病人的症状、化验结果等初始事实利用知识库中的知识及一定的控制策略,为病人诊治疾病、开出医疗处方就是推理过程2/5/20235华北电力大学概述推理的分类演绎推理、归纳推理、默认推理
确定性推理、不精确推理
单调推理、非单调推理
启发式推理、非启发式推理
2/5/20236华北电力大学概述从推出新判断的途径分演绎、归纳和默认推理演绎推理从全称判断推出特称判断或单称判断的过程,即从一般到个别的推理演绎推理中最常用的形式是三段论法(大前提和小前提,及结论)例如:所有的推理系统都是智能系统——一般的知识专家系统是推理系统——个体的判断所以,专家系统是智能系统——新判断
没有增加新的知识2/5/20237华北电力大学概述-演绎推理、归纳推理和默认推理归纳推理从足够多的事例中归纳出一般性结论的推理过程,是一种从个别到一般的推理过程常用的归纳推理有简单枚举法和类比法枚举法归纳推理是由已观察到的事物都有某属性,而没有观察到相反的事例,从而推出某类事物都有某属性,推理过程为:
S1是P S2是P …
Sn
是P(S1,S2,…Sn
是S类中的个别事物,在枚举中兼容)
S都是P
2/5/20238华北电力大学概述-演绎推理、归纳推理和默认推理归纳推理之枚举法枚举法归纳推理分完全归纳推理与不完全归纳推理完全归纳推理在进行归纳时考察了相应事物的全部对象,并根据这些对象是否都具有某种属性,从而推出这个事物是否具有这个属性完全归纳推理是必然性推理
不完全归纳推理只考察了相应事物的部分对象,就得出了结论不完全推理得出的结论不具有必然性,属于非必然性推理2/5/20239华北电力大学概述-演绎推理、归纳推理和默认推理归纳推理之类比法在两个或两类事物在许多属性上都相同的基础上,推出它们在其它属性上也相同,这就是类比法归纳推理类比法归纳可形式化地表示为:
A具有属性a,b,c,d,e B具有属性a,b,c,d,
B也具有属性e类比法的可靠程度决定于两个或两类事物的相同属性与推出的那个属性之间的相关程度,相关程度越高,则类比法的可靠性就越高归纳推理增加了知识(在机器学习部分称为归纳学习)
2/5/202310华北电力大学概述-演绎推理、归纳推理和默认推理默认推理又称为缺省推理,是在知识不完全的情况下假设某些条件已经具备所进行的推理如:在条件A已成立的情况下,如果没有足够的证据能证明条件B不成立,则就默认B是成立的,并在此默认的前提下进行推理,推导出某个结论知识不完全的情况下也能进行推理如果到某一时刻发现原先所作的默认不正确,则要撤消所作的默认以及由此默认推出的所有结论,重新按新情况进行推理
2/5/202311华北电力大学概述按推理时所用的知识的确定性分确定性推理推理中所用的知识都是精确的归结反演、基于规则的演绎系统等都是确定性推理不精确推理基于不确定的推理规则进行,形成的结论也是不确定的专家系统中主要使用的是不精确推理2/5/202312华北电力大学概述按推出的结论是否单调增加,或推出的结论是否越来越接近最终目标分:单调推理在推理过程中随着推理的向前推进及新知识的加入,推出的结论呈单调增加的趋势,并且越来越接近最终目标非单调推理在推理过程中随着推理的向前推进及新知识的加入,不仅没有加强已推出的结论,反而要否定它,使得推理退回到前面的某一步,重新开始一般非单调推理是在知识不完全的情况下进行的2/5/202313华北电力大学概述按推理中是否运用与问题有关的启发性知识分启发式推理推理过程中,运用与问题有关的启发性知识,以加快推理过程,提高搜索效率A*、AO*等算法就属于此类推理非启发式推理推理过程中,不运用启发性知识,只按照一般的控制逻辑进行推理这种方法缺乏对求解问题的针对性,所以推理效率较低,容易出现“组合爆炸”问题,如宽度优先搜索法2/5/202314华北电力大学概述推理的控制策略
主要是指推理方向的选择、推理时所用的搜索策略及冲突解决策略等一般推理的控制策略与知识表达方法有关推理方向推理方向用于确定推理的驱动方式根据推理方向的不同,可将推理分为正向推理、反向推理和正反向混合推理无论按哪种方式进行推理,一般都要求系统具有一个存放知识的知识库(KB)、一个存放初始事实和中间结果的数据库(DB)和一个用于推理的推理机2/5/202315华北电力大学概述-推理的控制策略推理方向正向推理(事实驱动推理)是由已知事实出发向结论方向的推理开始DB中是否包含问题的解?将用户提供的新事实加入DB中KB中是否有可适用的知识?把KB中所有适用的规则加入到RS中RS为空?按一定的冲突解决策略从RS中选择一条规则进行推理将推理结论加入DB中成功,退出用户可是否补充新事实?失败,退出将初始事实加入数据库DB中是否否是否是否2/5/202316华北电力大学概述-推理的控制策略推理方向反向推理——以某个假设目标作为出发点的一种推理,又称为目标驱动推理或逆向推理在KB中找出所有能导出该假设的规则,形成适用规则集RS该假设是否是事实?该假设在数据库DB?从RS中选择一条规则,并将该规则的一个条件作为新的假设目标该假设成立有假设?退出询问用户有事实?该假设成立,并将此假设作为事实存入DB提出假设开始是否是否否是是否2/5/202317华北电力大学概述-推理的控制策略推理方向正反混合推理是开始进行正向推理需要反向推理?以正向推理所得结果作为假设进行反向推理还需要正向推理吗?输出结果退出否是否2/5/202318华北电力大学概述-推理的控制策略搜索策略推理时,要反复用到知识库中的规则,而知识库中的规则又很多,这样就存在着如何在知识库中寻找可用规则的问题为有效控制规则的选取,可以采用各种搜索策略常用搜索策略:状态空间搜索(宽度优先搜索、深度优先搜索、有界深度优先搜索等)启发式搜索等(第三章)2/5/202319华北电力大学概述-推理的控制策略冲突解决策略
推理过程中,系统要不断地用数据库中的事实与知识库中的规则进行匹配,当有一个以上规则的条件部分和当前数据库相匹配时,就需要有一种策略来决定首先使用哪一条规则,这就是冲突解决策略冲突解决策略实际上就是确定规则的启用顺序
2/5/202320华北电力大学概述-推理的控制策略推理的控制策略
冲突解决策略
(1)
专一性排序 如果某一规则的条件部分规定的情况比另一规则的条件部分所规定的情况更专门,则这条规则具有较高的优先级
例,有如下规则: 规则1:IFAANDBANDCTHENE; 规则2:IFAANDBANDCANDDTHENF; 数据库中A、B、C、D均为真,这时规则1和规则2都与数据库相匹配,但因为规则2的条件部分包括了更多的限制,所以具有较高的优先级
本策略是优先使用针对性较强的产生式规则
2/5/202321华北电力大学概述-推理的控制策略推理的控制策略
3.冲突解决策略
(2)
规则排序 规则编排的顺序就表示了启用的优先级
(3)
数据排序 数据排序就是把规则条件部分的所有条件排序,按优先级次序编排,发生冲突时,首先使用在条件部分包含较高优先级数据的规则
(4)
就近排序 把最近使用的规则放在最优先的位置。如果某一规则经常使用,则倾向于更多地使用这条规则
(5)
上下文限制 上下文限制就是把产生式规则按它们所描述的上下文分组,在某种上下文条件下,只能从与其相对应的那组规则中选择可应用的规则2/5/202322华北电力大学概述-推理的控制策略推理的控制策略
3.冲突解决策略
(6)
按匹配度排序
在不精确匹配中,为了确定两个知识模式是否可以进行匹配,需要计算这两个模式的相似程度,当其相似度达到某个预先规定的值时,就认为它们是可匹配的。若有几条规则均可匹配成功,则可根据它们的匹配度来决定哪一个产生式规则可优先被应用
(7)按条件个数排序
如果有多条产生式规则生成的结论相同,则要求条件少的产生式规则被优先应用,因为要求条件少的规则匹配时花费的时间较少不同的系统,可使用上述这些策略的不同组合2/5/202323华北电力大学概述归结原理由J.A.Robinson于1965年提出定理证明的实质就是要对给出的(已知的)前提和结论,证明此前提推导出该结论这一事实是永恒的真理这是非常困难的,几乎是不可实现的要证明在一个论域上一个事件是永真的:就要证明在该域中的每一个点上该事实都成立论域是不可数时,该问题不可能解决即使可数,如果该论域是无限的,问题也无法简单地解决2/5/202324华北电力大学概述理论基础:Herbrand采用了反证法的思想,将永真性的证明问题转化成为不可满足性的证明问题实现方法:Robinson的归结原理使得自动定理证明得以实现归结推理方法在人工智能推理方法中有着很重要的历史地位,是机器定理证明的主要方法2/5/202325华北电力大学归结法的特点归结法是一阶逻辑中,至今为止的最有效的半可判定的算法。也是最适合计算机进行推理的逻辑演算方法半可判定一阶逻辑中任意恒真公式,使用归结原理,总可以在有限步内给以判定(证明其为永真式)当不知道该公式是否为恒真时,使用归结原理不能得到任何结论2/5/202326华北电力大学归结法基本原理采用反证法(反演推理方法)将待证明的表达式(定理)转换成为逻辑公式(谓词公式)然后再进行归结归结能够顺利完成,则证明原公式(定理)是正确的2/5/202327华北电力大学归结法基本原理—例例:由命题逻辑描述的命题:A1、A2、A3和B,要求证明:如果A1ΛA2ΛA3成立,则B成立,即:A1ΛA2ΛA3→B是重言式(永真式)归结法的思路A1ΛA2ΛA3→B是重言式等价于A1ΛA2ΛA3Λ~B是矛盾式,也就是永假式反证法:证明A1ΛA2ΛA3Λ~B是矛盾式(永假式)2/5/202328华北电力大学归结法和其它推理方法的比较语义网络、框架表示、产生式规则等知识表示方法的推理都是以逻辑推理方法为前提的也就是说如果有了规则和已知条件,就能够依据一定的规则和公理顺藤摸瓜找到结果归结方法是在一个规则指导下,进行自动推导。多用于计算机自动推理、自动推导证明注意:只讨论一阶谓词逻辑描述下的归结推理方法,不涉及高阶谓词逻辑问题2/5/202329华北电力大学第三章谓词逻辑与归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理2/5/202330华北电力大学第三章谓词逻辑与归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理2/5/202331华北电力大学命题描述事实、事物的状态、关系等性质的文字串,取值为真或假(表示是否成立)的句子称作命题命题:非真即假的简单陈述句能判断真假陈述句命题用小写字母p、q、r、s等表示2/5/202332华北电力大学命题例命题:能判断真假(不是既真又假)的陈述句
简单陈述句描述事实、事物的状态、关系等性质例如:1.
1+1=2 2.
雪是黑色的。
3.
北京是中国的首都。
4.
到冥王星去渡假。
判断一个句子是否是命题,有先要看它是否是陈述句,而后看它的真值是否唯一。以上4个例子都是命题。例如:1.
快点走吧!
2.
到哪儿去?
3.
x+y>10
都不是命题。2/5/202333华北电力大学命题表示公式(1)将陈述句转化成命题公式。如:设“下雨”为p,“骑车上班”为q,1.“只要不下雨,我骑自行车上班”。~p
是q的充分条件,因而,可得命题公式:~p→q2.“只有不下雨,我才骑自行车上班”。~p
是q的必要条件,因而,可得命题公式:q→~p2/5/202334华北电力大学命题表示公式(2)例如:1.
“如果我进城我就去看你,除非我很累。” 设:p,我进城,q,去看你,r,我很累。 则有命题公式:~r→(p→q)。2.“应届高中生,得过数学或物理竞赛的一等奖, 保送上北京大学。” 设:p,应届高中生,q,保送上北京大学上学,
r,是得过数学一等奖。t,是得过物理一等奖。 则有命题公式公式:p
∧(r∨t)→
q。
2/5/202335华北电力大学命题逻辑基础—数理逻辑的基本定义命题逻辑基础:定义:合取式:p与q,记做p∧
q析取式:
p或q,记做p∨
q蕴含式:如果p则q,记做p→
q等价式:p当且仅当q,记做p<=>
q
。。。。。。归结法的基础2/5/202336华北电力大学命题逻辑基础—数理逻辑的基本定义定义:若A无成假赋值,则称A为重言式或永真式若A无成真赋值,则称A为矛盾式或永假式若A至少有一个成真赋值,则称A为可满足的析取范式:仅由有限个简单合取式组成的析取式合取范式:仅由有限个简单析取式组成的合取式2/5/202337华北电力大学命题逻辑基础—基本等值式(1)基本等值式24个交换率:p∨q
<=>q
∨p
;
p∧q<=>q∧
p
结合率:(p∨q)∨
r<=>p∨(q
∨r); (p∧q)∧
r<=>p∧(q∧r)分配率:p∨(q
∧
r)<=>(p∨q)∧(p∨r)
;
p∧(q∨
r)<=>(p∧q)∨(p∧r)2/5/202338华北电力大学命题逻辑基础—基本等值式(2)摩根率:~
(p∨q)
<=>~
p∧
~
q
;
~
(p∧
q)
<=>~
p∨
~
q
吸收率:p∨(p
∧
q)<=>p
;
p∧(p∨q
)<=>p
同一律:p∨0
<=>p
;
p∧1
<=>p
蕴含等值式:p→
q
<=>~
p∨q
假言易位式:p→
q
<=>~p→~
q双重否定律p
<=>~
~
p零率律p∨0
<=>p;p∧1
<=>p2/5/202339华北电力大学命题逻辑基础-合取范式范式:公式的标准形式合取范式:单元子句、单元子句的或(∨)的与(∧)如:P∧(P∨Q)∧(~P∨Q)求合取范式的步骤求合取范式的基本原则利用∨对∧例:求取P∧(Q→R)→S的合取范式1.消去对于{→,∨,∧}来说冗余的连接词2.内移或消去否定号3.利用分配律2/5/202340华北电力大学命题逻辑基础-合取范式解:P∧(Q→R)→S
=~(P∧(~Q∨R)∨S
=~P∨~(~Q∨R)∨S
=~P∨(~~Q∧~R)∨S
=~P∨(Q∧~R)∨S
=~P∨S∨(Q∧~R)
=(~P∨S∨Q)∧(~P∨S∨~R)注意:将原有的命题公式整理、转换成为各个“或”语句的“与”,不然后续推导没有意义转换是基于数理逻辑的基本等值公式进行的,“或”转换到“与”中2/5/202341华北电力大学命题逻辑的推理规则逻辑结论(有效结论):A→B如A→B为重言式(永真式),则称A推结论B的推理正确。B是A的逻辑结论称A→B为由前件A推结论B的推理的形式结构可采用真值表法、等值演算法等证明逻辑结论逻辑结论也称为假言推理或演绎推理重言式表示为AB2/5/202342华北电力大学命题逻辑的推理规则——常用的推理定律附加:A(A∨B)简化:(A∧B)A假言推理:((A→B)∧A)B拒取式:((A→B)∧~B)~A析取三段论:((A∨B)∧~A)B假言三段论:((A→B)∧(B→C))A→C等价三段论:((AB)∧(BC))AC构造性二难:((A→B)∧(C→D)∧(A∨C))(B∨D)2/5/202343华北电力大学命题逻辑的推理规则——常用的推理规则前提引入规则:在证明的任何步骤上,都可以引入前提结论引入规则:在证明的任何步骤上,所证明的结论都可以作为后续证明的前提置换规则:在证明的任何步骤上,命题公式中的任何子命题都可以用与之等值的命题公式置换例如,可以用~p∨q置换p→q2/5/202344华北电力大学命题逻辑的演绎推理-例1例3.3:构造下列推理的证明。前提p∨q,p→~r,s→t,~s→r,~t结论q证明:
①s→t
前提引入 ②~t 前提引入 ③~s ①②拒取规则 ④~s→r
前提引入 ⑤r ③④假言推理 ⑥p→~r 前提引入 ⑦~p ⑤⑥拒取规则 ⑧p∨q
前提引入 ⑨q ⑦⑧析取三段论2/5/202345华北电力大学命题逻辑的演绎推理-例2例3.4写出对应下面推理的证明。如果今天是下雨天,则要带雨伞或带雨衣。如果走路上班,则不带雨衣。今天下雨,走路上班,所以带伞。解:p:今天下雨。q:带伞。r:带雨衣。s:走路上班。前提:p→(q∨r),s→~r,p,s结论:q证明:
①p→(q∨r) 前提引入 ②p 前提引入 ③q∨r ①②假言推理 ④s→~r
前提引入 ⑤s 前提引入 ⑥~r ④⑤假言推理 ⑦q ③⑥析取三段论2/5/202346华北电力大学命题逻辑的归结演绎推理:从一系列前提得出结论上两个例子归结方法:新推理方法理论基础是Herbrand定理将待证逻辑公式的结论,通过等值公式转换成附加前提,再证明该逻辑公式不可满足A1ΛA2ΛA3→B是重言式证明A1ΛA2ΛA3Λ~B不可满足建立在子句集基础上2/5/202347华北电力大学命题逻辑基础-子句集命题公式的子句集S是合取范式形式下的子命题(元素)的集合子句集是合取范式中各个合取分量的集合生成子句集的过程可以简单地理解为将命题公式的合取范式中的与符号“∧”,置换为逗号“,”上例的合取范式:(~P∨S∨Q)∧(~P∨S∨~R)其子句集为S={~P∨S∨Q,~P∨S∨~R}命题公式:P∧(P∨Q)∧(~P∨Q)其子句集S:S={P,P∨Q,~P∨Q}2/5/202348华北电力大学命题逻辑的归结—合取范式和子句集合取范式:命题、命题或的与,如:
P∧(P∨Q)∧(~P∨Q)子句集S:合取范式形式下的子命题(元素)的集合例:命题公式:P∧(P∨Q)∧(~P∨Q)子句集S:S={P,P∨Q,~P∨Q}2/5/202349华北电力大学命题逻辑的归结法——归结式归结式——归结法的核心设C1和C2是子句集中的任意两个子句,如果C1中的文字L1与C2中的文字L2互补,那么可从C1和C2中分别消去L1和L2,并将C1和C2中余下的部分按析取关系构成一个新子句C12,则称这一个过程为归结,称C12为C1和C2的归结式,称C1和C2为C12的亲本子句消去互补文字,用析取连接剩余部分例如:有子句:C1=P∨C1'
,C2=~P∨C2'
,存在互补对P和~P,则可得归结式:C12=C1'∨C2'2/5/202350华北电力大学命题逻辑的归结法——归结式性质归结式性质:归结式C12是亲本子句C1和C2的逻辑结论C1ΛC2→C12任一使C1,C2
为真的解释I下必有归结式C12为真注意:C1ΛC2→C12,反之不一定成立。C1=P∨C1'
,C2=~P∨C2'
,C12=C1'∨C2'因为存在一个使C1'∨C2'为真的解释I,不妨设C1'为真,C2'为假。若P为真,则~P∨C2'就为假了。因此反之不一定成立2/5/202351华北电力大学命题逻辑的归结法——归结过程
建立待归结命题公式:根据反证法将所求证的问题转化成为命题公式,求证其是矛盾式(永假式)求取合取范式建立子句集归结对子句集中的子句使用归结规则归结式作为新子句加入子句集参加归结归结式为空子句□为止(说明子句集不可满足,即定理成立)。归结完毕 谓词归结:除有量词和函数以外,其余和命题归结一样2/5/202352华北电力大学命题逻辑归结例题(1)例题,证明公式:(P→Q)→(~Q→~P)证明:(1)根据归结原理,将待证明公式转化成待归结命题公式:
(P→Q)∧~(~Q→~P)(2)分别将公式前项化为合取范式:
P→Q=~P∨Q
结论求~后的后项化为合取范式: ~(~Q→~P)=~(Q∨~P)=~Q∧P
两项合并后化为合取范式: (~P∨Q)∧~Q∧P(3)则子句集为:
{~P∨Q,~Q,P}2/5/202353华北电力大学命题逻辑归结例题(2)
子句集为: {~P∨Q,~Q,P}(4)对子句集中的子句进行归结可得:1.
~P∨Q2.
~Q3.
P4.
Q, (1,3归结)5.
, (2,4归结)
由上可得原公式成立。2/5/202354华北电力大学第三章谓词逻辑与归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理2/5/202355华北电力大学第三章谓词逻辑与归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理2/5/202356华北电力大学谓词逻辑归结基础—基本概念一阶逻辑逻辑的基本定义基本概念个体词:表示主语的词个体常量:具体的或特定的个体个体变量:抽象的或泛指的个体谓词:刻画个体性质或个体之间关系的词谓词常量:具体性质或关系的谓词谓词变量:抽象或泛指的谓词量词:表示数量的词量词符号:全称、存在量词2/5/202357华北电力大学谓词逻辑归结基础—基本概念-例小王是个工程师。8是个自然数。我去买花。小丽和小华是朋友。个体词:“小王”、“工程师”、“我”、“花”、“8”、“小丽”、“小华”谓词:“是个工程师”、“是个自然数”、“去买”、“是朋友”都是谓词前两个谓词表示的是事物的性质第三个谓词“去买”表示的一个动作也表示了主、宾两个个体词的关系最后一个谓词“是朋友”表示两个个体词之间的关系2/5/202358华北电力大学谓词逻辑归结基础—基本概念一阶逻辑逻辑:以谓词的形式来表示动作的主体、客体公式及其解释个体常量:a,b,c个体变量:x,y,z谓词常量:P,Q,R谓词变量:P(x),Q(x,y),R(x,b)量词符号:
,,xP(x),xP(x)2/5/202359华北电力大学谓词逻辑归结基础—基本概念原子公式:设P(x1,x2,…,xn)是任意n元谓词,t1,t2,……,tn是项,则P(t1,t2,…,tn)为原子公式谓词公式:原子公式是谓词公式若A是谓词公式,则(~A)也是谓词公式若A、B是谓词公式,则(A∧B)、(A∨B)、(A→B)、(A↔B)也是谓词公式若A是谓词公式,则xA
,xA也是谓词公式只有有限次的应用①~④构成的符号串才是谓词公式2/5/202360华北电力大学谓词逻辑归结基础—基本概念指导变量:xA,xA中的x为指导变量辖域:xA,xA中的A成为相应量词的辖域约束出现:在辖域(A)中,x的所有出现称为约束出现自由出现:在辖域(A)中,不是约束出现的其他变量的出现,称为自由出现2/5/202361华北电力大学谓词逻辑归结基础—基本概念-例例如:(1)所有的人都是要死的。(2)
有的人活到一百岁以上。在个体域D为人类集合时,可符号化为:(1)xP(x),其中P(x)表示x是要死的。(2)xQ(x),其中Q(x)表示x活到一百岁以上。在个体域D是全总个体域时,引入特殊谓词R(x)表示x是人,可符号化为:(1)x(R(x)→P(x)),
其中,R(x)表示x是人;P(x)表示x是要死的。(2)x(R(x)∧Q(x)) 其中,R(x)表示x是人;Q(x)表示x活到一百岁以上。2/5/202362华北电力大学谓词逻辑归结基础——谓词公式等值式量词否定等值式:~(x
)
M(x)<=>(
y
)~
M(y)~(x
)
M(x)<=>(
y
)~
M(y)量词分配等值式:(x
)(
P(x)∧
Q(x))<=>(x
)
P(x)∧
(x
)
Q(x)(x
)(
P(x)∨
Q(x))<=>(x
)
P(x)∨
(x
)
Q(x)消去量词等值式:设个体域为有穷集合(a1,a2,…an)(x
)
P(x)<=>P(a1
)∧
P(a2
)∧
…∧
P(an
)(x
)P(x)<=>P(a1
)∨
P(a2
)∨
…∨
P(an
)2/5/202363华北电力大学谓词逻辑归结基础——谓词公式等值式量词辖域收缩与扩张等值式:(x
)(
P(x)∨Q)<=>(x
)
P(x)∨Q(x
)(
P(x)∧
Q)<=>(x
)
P(x)∧
Q
(x
)(
P(x)→Q)<=>(x
)
P(x)→Q
(x
)(Q
→P(x))<=>Q
→(x
)
P(x)(x
)(
P(x)∨Q)<=>(x
)
P(x)∨Q(x
)(
P(x)∧
Q)<=>(x
)
P(x)∧
Q
(x
)(
P(x)→Q)<=>(x
)
P(x)→Q
(x
)(Q
→P(x))<=>Q
→(x
)
P(x)2/5/202364华北电力大学Skolem
标准型——前束范式SKolem标准型是在前束范式的基础上进行变量映射的前束范式定义:说公式A是一个前束范式,如果A中的一切量词都位于该公式的最左边(不含否定词),且这些量词的辖域都延伸到公式的末端。
(Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn)将量词提到公式最前端时存在约束变量换名问题。要严守约束变元的换名规则(Qx)M(x)(Qy
)M(y)(Qx)M(x,z)(Qy
)M(y,z)
例题Qi:量词,M:母式2/5/202365华北电力大学例(w)P(w)→((x)((y)((z)(P(x,y,z)→(u)R(x,y,z,u)))))(w)~P(w)∨(x)((y)((z)(~P(x,y,z)∨(u)R(x,y,z,u))))(w)(x)(y)(z)(u)(~P(w)∨~P(x,y,z)∨R(x,y,z,u))2/5/202366华北电力大学Skolem
标准型前束范式中消去所有的量词,则称这种形式的谓词公式为Skolem标准型Skolem标准型必须满足合取范式的条件任何一个谓词公式都可以化成与之对应的Skolem标准型。但Skolem标准型不唯一2/5/202367华北电力大学Skolem
标准型——转化过程将谓词公式G转换成为前束范式消去量词量词消去原则:消去存在量词“”如果存在量词左边没有任何全称量词,则只将其改写成为常量(a,b等)如果是左边有全称量词的存在量词,消去时该变量改写成为全称量词的函数(f(x),g(y)等)略去全称量词“”,简单地省略掉该量词2/5/202368华北电力大学Skolem
标准型——例将下式化为Skolem标准型: ~((x)(y)P(a,x,y)→(x)(~(y)Q(y,b)→R(x)))解:第一步,消去→号,得:
~(~(x)(y)P(a,x,y)∨(x)(~~(y)Q(y,b)∨R(x)))第二步,~深入到量词内部,得:
(x)(y)P(a,x,y)∧~((x)((y)Q(y,b)∨R(x)))=(x)(y)P(a,x,y)∧(x)((y)~Q(y,b)∧~R(x))第三步,任意量词左移,利用分配律,得到
(x)((y)P(a,x,y)∧(y)(~Q(y,b)∧~R(x)))第四步,变元易名,存在量词左移,直至所有的量词移到前面,得:
(x)((y)P(a,x,y)∧(y)(~Q(y,b)∧~R(x)))=(x)((y)P(a,x,y)∧(z)(~Q(z,b)∧~R(x)))=(x)(y)(z)(P(a,x,y)∧(~Q(z,b)∧~R(x))
由此得到前述范式2/5/202369华北电力大学Skolem
标准型——例上页:(x)(y)(z)(P(a,x,y)∧(~Q(z,b)∧~R(x))第五步,消去“”,略去“” 消去(y),因为它左边只有(x),所以使用x的函数f(x)代替之,这样得到:
(x)(z)(P(a,x,f(x))∧~Q(z,b)∧~R(x))
消去(z),同理使用g(x)代替之,这样得到:
(x)(P(a,x,f(x))∧~Q(g(x),b)∧~R(x))
略去全称变量,原式的Skolem标准型为:
P(a,x,f(x))∧~Q(g(x),b)∧~R(x)
例2:
((x)p(x)∨(x)Q(x))→(x)(p(x)∨Q(x))2/5/202370华北电力大学Skolem定理SKOLEM标准型定义: 消去量词后的前束范式Skolem定理:
谓词逻辑的任意公式都可以化为与之等价的前束范式,但其前束范式不唯一注意:
谓词公式G的SKOLEM标准型同G并不等值例如有谓词公式G=(x)p(x),其skolem标准型G’=P(a)
解释I:个体域DI={0,1},常数a=0,谓词P(x)为P(0)=F,P(1)=T,则在解释I下G=T,G’=F2/5/202371华北电力大学子句集——定义子句与子句集文字:不含任何连接词的谓词公式子句:一些文字的析取(谓词的和)空子句:不含任何文字的子句,子句集:所有子句的集合对于任一个公式G,都可以通过Skolem标准型,标准化建立起一个子句集与之相对应2/5/202372华北电力大学子句集——求取步骤子句集S的求取:通过Skolem标准型求取
G→前束范式 →消去量词生成Skolem标准型→将Skolem标准型中的子句提出,表示为集合形式,即以“,”取代∧”,并表示为集合形式注意Skolem标准型必须满足合取范式的条件2/5/202373华北电力大学子句集与谓词公式的不可满足性G是不可满足的<=>S是不可满足的G与S不等价,但在不可满足的意义下是一致的
定理3.1: 若G是给定的公式,而S是相应的子句集,则G是不可满足的,当且仅当S是不可满足的。
注意:G真不一定S真,而S真必有G真 即:S=>G2/5/202374华北电力大学子句集与谓词公式的不可满足性
——定理3.1的推广谓词公式G=G1ΛG2ΛG3Λ…ΛGn,G的子句集S的求取可以分解成几个部分单独处理。如果Gi的子句集为Si,则有:
S'=S1∪S2∪S3∪…∪Sn。虽然G的子句集不为S',但是可以证明:
SG与S'
在不可满足的意义上是一致的。即SG不可满足
S1∪S2∪S3∪…∪Sn不可满足2/5/202375华北电力大学求取子句集例(1)例:对所有的x,y,z来说,如果y是x的父亲,z又是y的父亲,则z是x的祖父。又知每个人都有父亲,试问对某个人来说谁是它的祖父?求:用一阶逻辑表示这个问题,并建立子句集。解:这里我们首先引入谓词:
P(x,y)表示x是y的父亲
Q(x,y)表示x是y的祖父
ANS(x)表示问题的解答2/5/202376华北电力大学求取子句集例(2)对于第一个条件,“如果x是y的父亲,y又是z的父亲,则x是z的祖父”,一阶逻辑表达式如下:
A1:(x)(y)(z)(P(x,y)∧P(y,z)→Q(x,z)) SA1:~P(x,y)∨~P(y,z)∨Q(x,z)对于第二个条件:“每个人都有父亲”,一阶逻辑表达式:
A2:(y)(x)P(x,y) SA2:P(f(y),y)对于结论:某个人是他的祖父
B:(x)(y)Q(x,y)
否定后得到子句:~((x)(y)Q(x,y))∨ANS(x) S~B:~Q(x,y)∨ANS(x)则得到的相应的子句集为:{SA1,SA2,S~B}2/5/202377华北电力大学第三章谓词逻辑与归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理2/5/202378华北电力大学第三章谓词逻辑与归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结过程的控制策略Herbrand定理2/5/202379华北电力大学归结原理归结原理正确性的根本在于,如果在子句集中找到矛盾可以肯定命题是不可满足的(不真)方法:和命题逻辑一样但由于有函数,所以要考虑合一和置换
2/5/202380华北电力大学置换置换:在一个谓词公式中用置换项去置换变量定义: 置换是形如{t1/x1,t2/x2,…,tn/xn}的有限集合。其中,x1,x2,…,xn是互不相同的变量,t1,t2,…,tn是不同于xi的项(常量、变量、函数);ti/xi表示用ti置换xi,并且要求ti与xi不能相同,而且xi不能循环地出现在另一个ti中。例如
{a/x,c/y,f(b)/z}是一个置换
{g(y)/x,f(x)/y}不是一个置换2/5/202381华北电力大学置换定义:设是一个置换,E是一个表达式,把对E施行置换,即把E中出现的个体变元xi用ti替换,记为E例:={a/x,f(b)/y,c/z},G=P(x,y,z),求G
G=P(a,f(b),c)2/5/202382华北电力大学置换的合成
设={t1/x1,t2/x2,…,tn/xn}, ={u1/y1,u2/y2,…,um/ym},是两个置换。则与的合成也是一个置换,记作·。它是从集合
{t1·/x1,t2·/x2,…,tn·/xn,u1/y1,u2/y2,…,um/ym}
中删去以下两种元素:当ti=xi时,删去ti/xi(i=1,2,…,n)
当yi{x1,x2,…,xn}时,删去uj/yj
(j=1,2,…,m)
最后剩下的元素所构成的集合合成即是对ti先做置换然后再做置换,置换xi2/5/202383华北电力大学置换的合成例:设:={f(y)/x,z/y},={a/x,b/y,y/z},求与的合成解:先求出集合
{f(b/y)/x,(y/z)/y,a/x,b/y,y/z}={f(b)/x,y/y,a/x,b/y,y/z}
其中,f(b)/x中的f(b)是置换作用于f(y)的结果;y/y中的y是置换作用于z的结果。在该集合中,y/y满足定义中的条件i,需要删除;a/x,b/y满足定义中的条件ii,也需要删除。最后得 ·={f(b)/x,y/z}2/5/202384华北电力大学合一合一可以简单地理解为“寻找相对变量的置换,使两个谓词公式一致”定义:设有公式集F={F1,F2,…,Fn},若存在一个置换,可使F1=F2=…=Fn,则称是F的一个合一。同时称F1,F2,...,Fn是可合一的2/5/202385华北电力大学合一——例子例: 设有公式集F={P(x,y,f(y)),P(a,g(x),z)},则={a/x,g(a)/y,f(g(a))/z}是它的一个合一。注意:一般说来,一个公式集的合一不是唯一的2/5/202386华北电力大学最一般合一定义:最一般合一设σ是公式集F的一个合一,如果对F的任意一个合一θ都存在一个置换λ,使得θ=σ·λ,则称σ是一个最一般合一(MostGeneralUnifier,简记为mgu)2/5/202387华北电力大学最一般合一一个公式集的最一般合一是唯一的若用最一般合一去置换那些可合一的谓词公式,可使它们变成完全一致的谓词公式(——用途)mgu的求取方法对于给定谓词公式F1和F2,采用逐一比较找出不一致,并作出相应的合一置换,可求得mgu2/5/202388华北电力大学mgu求取方法令w={F1,F2}令k=0,w0=w,σ0=ε如果wk已合一,停止,σk=mgu,否则,找不一致集Dk若Dk中存在元素vk和tk,其中vk不出现于tk中,转5,否则,不可合一令σk+1=σk{tk/vk},wk+1=wk{tk/vk}=wσk+1k=k+1,转3若F1和F2可合一,算法必停止与32/5/202389华北电力大学mgu的例子例:W={P(a,x,f(g(y))),P(z,f(a),f(u))},
其中F1=P(a,x,f(g(y))),F2=P(z,f(a),f(u))
求F1和F2的最一般合一。2/5/202390华北电力大学mgu的例子2/5/202391华北电力大学mgu的例子2/5/202392华北电力大学归结式和命题逻辑一样消去互补对,但要考虑变量的合一与置换设C1、C2是两个无公共变量的子句,L1和L2分别是C1和C2的文字,如果L1、~L2有最一般合一σ,则
R=(C1
σ-{L1σ})∪(C2
σ-{L2σ})称作子句C1、C2的一个二元归结式,而L1和L2为被归结的文字例子2/5/202393华北电力大学P(x)∨Q(x,y)与~P(a)∨R(b,z)的归结式
Q(a,y)∨R(b,z)σ={a/x}
P(x,y)∨Q(x)∨R(x)与~P(a,z)∨~Q(b)的归结式
Q(a)∨R(a)∨~Q(b)σ={a/x,y/z}
P(b,y)∨R(b)∨~P(a,z)σ={b/x}归结式-例2/5/202394华北电力大学归结原理——归结的注意事项谓词的一致性,P()与~Q(),不可以常量的一致性,P(a,…)与~
P(b,….),不可以;变量,P(a,….)与~P(x,…),可以变量与函数,
P(x,x,….)与~P(x,f(x),…),不可以;
P(x,x,….)与~P(x,f(y),…),可以;不能同时消去两个互补对,P∨Q与~P∨~Q得空,不可以先进行内部简化(置换、合并)
例子2/5/202395华北电力大学归结原理——归结的过程归结的过程写出谓词关系公式→用反演法写出谓词表达式→SKOLEM标准型→子句集S→对S中可归结的子句做归结→归结式仍放入S中,反复归结过程→得到空子句→
▯得证2/5/202396华北电力大学例题“快乐学生”问题假设任何通过计算机考试并获奖的人都是快乐的,任何肯学习或幸运的人都可以通过所有的考试,张不肯学习但他是幸运的,任何幸运的人都能获奖。求证:张是快乐的。证明:先将问题用谓词表示如下:R1:“任何通过计算机考试并获奖的人都是快乐的”
(x)((Pass(x,computer)∧Win(x,prize))→Happy(x))R2:“任何肯学习或幸运的人都可以通过所有考试”
(x)(y)(Study(x)∨Lucky(x)→Pass(x,y))R3:“张不肯学习但他是幸运的” ~Study(zhang)∧Lucky(zhang)R4:“任何幸运的人都能获奖”
(x)(Luck(x)→Win(x,prize))结论:“张是快乐的”的否定~Happy(zhang)2/5/202397华北电力大学例题“快乐学生”问题由R1及逻辑转换公式:P∧W→H=~(P∧W)∨H,可得
(1)~Pass(x,computer)∨~Win(x,prize)∨Happy(x)由R2:(2)~Study(y)∨Pass(y,z)(3)~Lucky(u)∨Pass(u,v)由R3:(4)~Study(zhang)(5)Lucky(zhang)由R4:(6)~Lucky(w)∨Win(w,prize)由结论:(7)~Happy(zhang) (结论的否定)(8)~Pass(w,computer)∨Happy(w)∨~Lucky(w)(1)(6),{w/x}(9)~Pass(zhang,computer)∨~Lucky(zhang)(8)(7),{zhang/w}(10)
~Pass(zhang,computer) (9)(5)(11)
~Lucky(zhang)(10)(3),{zhang/u,computer/v}(12)
(11)(5)
2/5/202398华北电力大学例题某些患者喜欢所有医生,没有患者喜欢庸医,所以没有医生是庸医。2/5/202399华北电力大学第三章谓词逻辑与归结原理概述命题逻辑的归结法谓词逻辑归结基础归结原理归结
温馨提示
- 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
- 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
- 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
- 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
- 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
- 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
- 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
最新文档
- GB/T 13465.1-2024不透性石墨材料试验方法第1部分:总则
- 废旧家电回收利用行业营销策略方案
- 离心碾磨机细分市场深度研究报告
- 人力资源流程再造行业市场调研分析报告
- 相框边条项目运营指导方案
- 乐器销售行业营销策略方案
- 数据管理用计算机产品供应链分析
- 纺织品制壁挂细分市场深度研究报告
- 书法培训行业相关项目经营管理报告
- 茶壶项目运营指导方案
- 喉痹(咽炎)中医护理方案
- DBJ33_T 1268-2022 工程建设工法编制标准
- 压力容器产品质量证明书样表简版
- 11工作审批流程及权限
- 综合组教研活动记录【精选文档】
- 上册文字表达式-符号表达式-化学式
- 专业技术职称等级分类
- 江苏省城市设计编制导则
- 2022年铁路货运员考试题库(汇总版)
- 《基坑支护》PPT课件.ppt
- 探究如何提高机电工程施工质量的方法
评论
0/150
提交评论