资源描述:
《基于中介逻辑的时序逻辑系统》由会员上传分享,免费在线阅读,更多相关内容在教育资源-天天文库。
1、第18卷第3期数学研究与评论Vol.18No.31998年8月JOURNALOFMATHEMATICALRESEARCHANDEXPOSITIONAug.1998基于中介逻辑的时序逻辑系统X1,21,31,3施庆生 张东摩 朱梧木贾1(南京航空航天大学计算机科学与工程系 南京,210016)2(南京建筑工程学院基础部 南京,210009)3(南京大学软件高技术国家重点实验室 南京,210008)摘 要 本文基于中介逻辑建立了一种中介时序逻辑系统MTL(MediumTemporalLogic),文中着重讨论了MTL的形式系统并给出了它的语义解释,证明了
2、MTL系统的可靠性.最后对MTL系统和经典时序命题逻辑系统进行对比,指出经典时序命题逻辑系统是MTL的子系统.关键词中介逻辑,时序逻辑,命题逻辑,中介时序逻辑.分类号AMS(1991)03B55/CCLO1411 引 言时序逻辑作为一种把时间概念直接引入其形式系统的逻辑系统,它对于变化的世界具有[1]很强的描述能力,因而常被用作程序或并发程序的描述工具及验证系统,故近年来时序逻辑在计算机领域取得了广泛地应用,这些应用反过来又促进了时序逻辑本身的研究与发展.本文将基于中介逻辑建立一种中介时序逻辑系统MTL(MediumTemporalLogic).由于
3、中介逻辑是一种特殊的三值逻辑系统,因此本文建立的系统可以看成是对时序逻辑的三值扩充.2 中介时序逻辑的语言构成MTL3[2]设L为由MP中所有逻辑符号及模态词□,◇,○,þ构成的语言,它包括:(1) 命题变元:p1,p2,⋯;(2) 逻辑联结词:~,Ò,µ,∧,∨,→,;,],N;(3) 模态词:□,◇,○,þ;(4) 技术符号:(、),[、].MTLL中的合式公式由下列规则生成:(1)pi为合式公式(i=1,2,⋯);(2) 如果A为合式公式,则~A,ÒA,µA,A∧B,A∨B,A→B,A;B,A]B,ANB,□A,◇A,○A,AþB也为合式公式;
4、X1995年3月16日收到.国家高技术研究发展计划(863-05-04-3)及国家自然科学基金资助项目.—465—©1995-2005TsinghuaTongfangOpticalDiscCo.,Ltd.Allrightsreserved.MTL(3)L中的合式公式均由(1),(2)生成.3 中介时序逻辑系统MTLMTL中介时序逻辑系统MTL为语言L上的一种时序逻辑系统,它由下列公理及推理规则组成:3MTLⅠ.MP中的所有推理规则对L中的所有合式公式均成立.Ⅱ.若3A,则3□A.Ⅲ.(K1)□(A;B)3□A;□B;(K2)○(A;B)3○A;○B;
5、(K3)□(A]○A)3A]□A;(R1)◇A—Ò□ÒA;(R2)~□A—□µÒA∧◇~A;(R3)~◇A—□µA∧◇~A;(R4)~○A—○~A;(R5)Ò○A—○ÒA;(R6)AþB—B∨(A∧○(AþB));(R7)Ò(AþB)—ÒB∧(ÒA∨○Ò(AþB));(T1)3□A;○A;(T2)3□A;A∧○□A;(T3)3AþB;◇B;由文[3]可知在MTL中下列引理1—引理3成立:引理1 若A=B,则□A=□B.引理2◇A=Ò□ÒA.引理3 若A=B,则◇A=◇B.引理4 若A=B,则○A=○B证明因A=B,故3ANB,从而有3A;B及3B;A
6、,由前者3□(A;B),由(T1)3○(A;B),由(K2)3○A;○B.同理可得3○B;○A),故3○AN○B,从而○A=○B.引理5[1] 对任何公式A,若3A,则3○A.[2] 对任何公式A,有3○A;◇A.[3] 对任何公式A、B,若A3B,则○A3○B.[4] 对任何公式A,若A3○A,则A3□A.证明 选证[3](1)A]B题设(2)A;(A;B)“]”定义—466—©1995-2005TsinghuaTongfangOpticalDiscCo.,Ltd.Allrightsreserved.(3)○(A;(A;B))(2)[1](4)○A
7、;○(A;B)(3)(K2)(5)○A](○A]○B)(4)MP3定理及(K2)(6)(○A](○A]○B))](○A]○B)(5)MP3重言式(7)○A]○B引理6在MTL中有:[1]□(A]B)3□A]□B.[2]○(A]B)3○A]○B.[3]○(A∧B)—○A∧○B[4]○(A∨B)—○A∨○B.[5]□(A∧B)—□A∧□B.[6]□(A∨B)3□A∨□B.[7]◇(A∨B)—◇A∨◇B.[8]◇(A∧B)3◇A∧◇B.[9]µ□A—◇µA[10]µ◇A—□µA.证明 选证[4](1)○(A∨B)假设(2)A∨B;ÒÒA∨ÒÒBMP3定理(
8、3)○(A∨B);○(ÒÒA∨ÒÒB)(2)引理5[1]及(K2)(4)○(ÒÒA∨ÒÒB)(1)(3)(;