基于中介逻辑的时序逻辑系统

《基于中介逻辑的时序逻辑系统》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

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)(;