形式化方法幻灯片4
107页1、第四章 时态逻辑,时态逻辑,引入,命题逻辑和谓词逻辑表达的可能性 真和假 不能表达的可能性 必然为真 知道为真 将来为真 相信为真,例,奥巴马是美国总统 太阳系有九大行星 27的立方根是3,模态逻辑,本章内容,模态逻辑 时态逻辑 命题线性时态逻辑 一阶线性时态逻辑 计算树逻辑(CTL,CTL*),模态逻辑相关概念,模态(Modal) 谓词逻辑的扩展形式。基于命题逻辑的扩展称为模态命题逻辑,基于一阶谓词逻辑的扩展称为模态一阶逻辑。特点是通过引入“可能”和“必然”两个模态词,从而能够对可能世界中的命题进行描述和演算。 模态词 必然();可能() 例如,对于命题P:火星上有生命, P:火星上必然有生命 P:火星上可能有生命;,模态逻辑公式,原子命题是模态逻辑公式; 如果A是模态逻辑公式。那么A和A是模态逻辑公式; 如果A,B是模态逻辑合适公式,那么(A),(AB),(AB),AB),(AB)是模态逻辑公式; 当且仅当有限次地使用(1)(2)(3)所组成的符号串是模态逻辑公式。,考察(1),AA 必然A真则A真; AA A真则可能A真; AA 必然A真则可能A真; AA 必然A真当且仅当不可能
2、A; AA 可能A当且仅当并非必然 A; AA 可能A或者可能A;,考察(2),(AA) 不会既有必然A,又有必然A; (AA) 必然有A成立或者A成立; (AA) 不可能A与 A同时成立; (AB) AB 必然A并且B等价于必然A并且必然B;,考察(3),AB(AB) 如果必然A和必然B有一个为真,那么必然有A真或者B真; (AB) AB 可能A或者B当且仅当可能A或者可能B; (AB) AB 如果可能有A并且B,那么可能A并且B 。,模态一阶逻辑公式,原子谓词公式是模态逻辑公式; 如果A,B是模态一阶逻辑公式,那么(A),(A),(A),(AB),(AB),(AB),(AB)是模态逻辑公式; 如果A是模态一阶逻辑公式,x是A中出现的变量(个体变量),则x.A, x.A是模态逻辑公式; 当且仅当有限次地使用(1)(2)(3)所组成的符号串是模态一阶逻辑公式.,与量词相关的性质,xP(x. P) xP(x. P) (xP) (xP) xP(xP),模态词之间的关系,P P P P,模态逻辑语义,要区分真值的不同模式或程度 基本模态逻辑的模型(Kripke): 三元组M=(W,R,L)
3、W:可能世界的非空集合; R包含于 W W:可能世界W上的二元关系, L:W2p(P为原子公式集合):标记函数,对可能世界的真值指派。 例:R(w,w):世界w可从世界w到达,s1,s2,s0,用图来表现Kripke结构,圆圈:可能世界 有向线段:可能世界之间的关系 圆圈内:标记函数标识(该可能世界中成立的原子公式),p.q,q,r,r,标准模型,满足下面条件的三元组M=(W,R,L):对于p,q P和s,t W有: L(p,s) = 10 L(p,s) = L(p,s) L(pq,s) = L(p,s)L(q,s) L(pq,s) = L(p,s) L(q,s) L(p,s) = (t)(sRtL(p,t)=1 L(p,s) = (t)(sRtL(p,t)=1,定义的真值,设M=(W,R,L)是基本模态逻辑的一个模型。假设xW且是模态逻辑公式。通过对结构归纳,定义满足关系x|- 来定义在世界x中,的真值: x|-p当且仅当pL(x) x|-当且仅当x |= x|-当且仅当x |= 并且x|= x|-当且仅当x |= 或x|= x|-当且仅当只要x |= 则x|= x|- 当且仅当对R
4、(x,y)的每一yW,有y|= x|- 当且仅当存在yW,使得R(x,y)且y|=,定义,如果该模型中每个世界都满足该公式,称基本模态逻辑的模型M(W,R,L)满足一个公式。写M|=当且仅当对每个xW,x|-,x6,x5,x4,例,x1 |- q x1 |- q x1 |- q x5 |- p x5 |- q x5 |- pq x5 |- (pq) x2,x3,x4,x5,x6 |-pp,x1,x3,x2,p.q,q,p,q,q,q,模态公式之间的等价,基本模态逻辑的一个公式集语义导出基本模态逻辑公式,如果对任何模型M=(W,R,L)中的任何世界x,只要对所有均满足x|-,就有x|- 。在这种情况下,|=成立。 和是语义等价,如果|=和|=成立。记为,模态公式之间的等价(续),命题逻辑中的任何等价也是模态逻辑中的等价。 取命题逻辑中的任何等价,将原子一致地代换成任意的模态逻辑公式,结果还是模态逻辑中的等价。 例:pq, (pq) p: p (qp) q: r(qp) p (qp)(r(qp) (p (qp) (r(qp),有效公式,基本模态公式称为有效,如果它在任何模型的任何世界中都为
《形式化方法幻灯片4》由会员F****n分享,可在线阅读,更多相关《形式化方法幻灯片4》请在金锄头文库上搜索。
2024-04-18 25页
2024-04-18 29页
2024-04-18 38页
2024-04-18 16页
2024-04-09 21页
2024-04-09 26页
2024-04-09 28页
2024-04-09 19页
2024-04-09 26页
2024-04-09 23页