时态数据库时间轴的动态逻辑模型  

Dynamic Logic Model of Time Axes in Temporal Database

作　　者：刘冬宁[1,2] 汤庸[2] 

机构地区：[1]广东工业大学计算机学院,广东广州510006 [2]中山大学计算机科学系,广东广州510275

出　　处：《软件学报》2010年第4期694-701,共8页Journal of Software

基　　金：国家自然科学基金Nos.60673135;60736020;新世纪优秀人才支持计划No.NCET-04-0805;广东省自然科学基金Nos.7003721;04105503;广东省科技攻关计划Nos.2005B10101041;2007B010200052~~

摘　　要：尽管在1994年,Gabbay等人论证了时态逻辑的公理化系统和证明论方法是不适合于时态数据库查询语言建模的,但是仍需要通过对时间轴的公理化建模,利用公理化系统的可靠和完全等性质对时间轴作"细精度"的语义刻画.只有这样才能准确地在数据库中反映时间和时间属性的本质特点,并应用于与时间轴模型直接相关的时态查询语言.因此,从分析时间轴的性质出发,对时间轴的序关系和谓词逻辑性质进行了研究和阐述.随后分别用经典的时态逻辑Tense Logic和动态逻辑对时态数据库的时间轴进行了公理化建模,这样刻画的目的是为了"细精度"地体现时间轴的特点,并借助逻辑的方法对其分析.在TDB(temporal database)时间轴的动态逻辑建模部分,相对于原时态逻辑系统较为静态,着重处理了时间的动态性,并参照了TenseLogic中的Lin.Z系统,将其转化为动态Lin.Z系统,在其中添加了参数化处理.该参数化的处理是基于动作执行的,主要工作在动作指数的数值化和函数化两个方面,其结果体现了时态数据库中规则生存周期和"Now"节点的一些特点以及知识表达和解决方法,研究结果将对后续时态知识表达和时态数据库查询语言的研究起到积极的作用.Although axiomatic systems and proof method for temporal logic have found so far relatively few applications in the query language modeling of temporal database and that was proved by Gabbay, et al in 1994, the model of time＇ axes still must be built axiomatically, which owns soundness and completeness and depicts the time axes in fine grain. Thus the essential characteristics of time and temporal attributes in database can be described exactly, and the result is used in the temporal querying. So the research starts from essential characteristics of time attributes. At first, this paper expounds the order relation and first order logic properties of time axes. Secondly, this paper axiomatically models that using Tense Logic and dynamic logic, which aims at reflecting the properties of axes in fine grain by logical analysis. In the part of dynamic logic modeling, respecting to the static of temporal logic system, this paper mostly deals with the dynamics in the new system. Based on Lin.Z system in Tense Logic, this paper makes out the dynamic Lin.Z system, which has some parameters and functions. The parameters of this system are based on the action, which helps the action exponential numerical and functional. The results of that embody the properties and representation method of the rule＇s lifecycle and point ＂Now＂ in temporal database, which positively helps the research in the field of temporal knowledge representation and temporal querying subsequently.

关 键 词：时态数据库 时间轴 TENSE LOGIC 动态逻辑 动作参数 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]