摘要
为了能够有效的描述现实世界中的相对静止状态,分析了在哲学逻辑理论中的线序时态逻辑定理系统中引入自反性质的可行性,在此基础上建立了具有自反性质的线序时态逻辑系统TA。叙述了TA时态系统的主要定理以及该系统具有无端稠密线序性质,并表明了该系统的紧致性、可靠性和完全性。运用状态重命名方法说明了TA系统与行为时序逻辑TLA系统之间的联系,从而将TA的定理系统运用到行为时序逻辑的研究中。
In order to effectively describe the relatively static state of the real world,the feasibility of introducing the reflexive property into linear tense logic theorem system of philosophical logic is analyzed.And based on it,a linear tense logic system TA with reflexive property is put forward and the main theorem of TA system is proved.The result shows that the system has a dense linear ordered nature.Beside,we prove the compactness,soundness and completeness of this system and show the relationship between the TA system and the temporal logic of action.Through it,the TA system is applied to the research of the temporal logic of action.
出处
《计算机工程与设计》
CSCD
北大核心
2011年第4期1338-1341,共4页
Computer Engineering and Design
关键词
模型检测
时态逻辑
自反性
可靠性
完全性
model checking
tense logic
reflexive property
soundness
completeness
