极小非正规时态逻辑研究
本文选题：非正规时态逻辑 切入点：矢列式系统 出处：《西南大学》2017年博士论文
【摘要】：时态逻辑是模态逻辑的一个重要分支。随着人工智能、软件工程、模型检测等领域的产生和发展,时态逻辑在计算机科中越来越重要。本文研究的对象是极小非正规时态逻辑C2t,该逻辑是对E.J.Lemmon提出的极小非正规模态逻辑C2时态化处理后得到的。针对极小非正规时态逻辑C2t,本文从证明论、模型论和代数的角度开展了以下5个方面的创新性工作:1.建立C2t的希尔伯特式公理系统HC2t。首先给出了C2t的语言和语义,C2t的语言和极小正规时态逻辑Kt的语言是相同的,但是在正则模型进行解释的。正则模型是非正规模态逻辑的模型,这种模型的特点在于模型中可以包含非正规世界。然后定义了公式在正则模型上的世界上是真的概念,与经典模态逻辑不同的是:一个模态公式在某个世界上的真值不仅仅依赖于与该世界可及的其他世界上的信息,并且还依赖于该世界是否是正规世界。最后给出了HC2t的公理和推理规则,构造了HC2t的典范模型,并利用典范模型证明了HC2t的完全性。2.建立C2t的加标矢列式演算系统GC2t。加标矢列式系统是近年来出现的一种证明系统,其特点是将模态算子的语义改写成自然演绎规则,然后从自然演绎系统转化为矢列式系统。首先定义矢列式的概念,建立GC2t的公理和推理规则。推理规则包括命题联接词规则、时序算子规则和关系规则。其次,证明了一些结构规则在GC2t中是可允许的,例如弱化规则、收缩规则和切割规则,其中最重要的结构规则是切割规则(cut rule)。然后,定义了正则模型的加标扩张,并证明GC2t(相对于正则模型的加标扩张)是可靠的和完全性。最后,证明了GC2t中的推导的可判定性。3.建立正则模型类在时态语言下可定义的刻画定理。可定义性是模型论的核心问题,它是研究模型类或模型的性质在一个逻辑语言中可定义或可表达的问题。首先定义了正则模型上的一些关系,例如时态等价关系、同态、强同态和有界态射等。证明了满足关系在强同态和有界态射下是保持不变的。其次定义了C2t-互模拟的概念,证明了满足关系在C2t-互模拟下是保持不变的。定义了“C2t-像有穷”(C2t-image finite)的概念,证明了如果两个正则模型是C2t-像有穷的,那么这两个正则模型上的时态等价关系和C2t-互模拟关系是相等的。然后定义了正则模型的不相交并、生成子模型等概念,并证明了如果一个正则模型类是时态可定义的,那么它在满C2t-互模拟像,不相交并、生成子模型等运算下是封闭的。定义了时态饱和的概念,并证明在时态饱和的正则模型类上,时态等价蕴含C2t-互模拟。定义了正则模型的C2t-超滤扩张,证明了任何正则模型的C2t-超滤扩张都是时态饱和的,并且时态可定义的正则模型类在C2t-超滤扩张下封闭。最后,证明了一个正则模型类是时态可定义的当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下是封闭的,并且它的补类在C2t-超滤扩张下也是封闭的。该刻画定理解释了时态语言在正则模型类上的表达力。4.建立C2t语言与一阶语言的对应理论和C2t语言的有穷模型性。首先定义了C2t语言的标准翻译,并证明了任意时态公式和其在标准翻译下的一阶公式是等值的。同时,利用标准翻译证明了C2t语言的紧致性。其次定义了正则模型的过滤的概念,并证明对任意正则模型和任意满足一定条件的公式集,正则模型通过公式集的过滤总是存在的。最后,利用过滤的方法证明了C2t语言具有有穷模型性。5.建立C2t的代数语义学。首先定义了正则时态代数,证明了正则时态代数的一些基本性质。定义了正则框架的复代数,并证明任意正则框架的复代数是一个正则时态代数。这表明从正则框架可以构造出一个正则时态代数。其次定义了一个等式在正则时态代数上是真的概念,证明了一个等式在正则框架的复代数上是真的当且仅当该等式对应的时态公式在正则框架上是有效的。然后,定义了C2t的林登博姆-塔斯基代数(Lindenbaum-Tarski Algebra),证明了它是正则时态代数,在某种意义上,它是一种“典范的”正则时态代数,即证明了C2t的定理所对应的等式都在C2t的林登博姆-塔斯基代数上是真的。反之,在林登博姆-塔斯基代数上是真的等式所对应的时态公式都是C2t的定理。利用上述结果,证明了C2t(相对于正则时态代数)的代数完全性。最后,建立了正则时态代数的一个表示定理。具体来说,定义正则时态代数的超滤框架,并证明任意正则时态代数都可以嵌入到它的超滤框架的复代数上,同时证明了C2t的典范框架和和它的林登保姆-塔斯基代数的超滤框架是同构的。本文开展的上述工作,从理论上丰富了现有的时态逻辑系统,并建立了一些重要的结论。这些结论在软件规约、自动定理证明和模型检测等方面都有一定的指导意义。因此本文的研究,不仅具有理论意义,而且具有应用价值。
[Abstract]:......
【学位授予单位】：西南大学
【学位级别】：博士
【学位授予年份】：2017
【分类号】：B81
【相似文献】
相关期刊论文 前10条
1 周文华;;基于区间的三值时态逻辑[J];湖北社会科学;2009年03期
2 刘虎;;开放系统中智能体竞争的时态逻辑[J];中山大学学报(社会科学版);2008年02期
3 王辉;;混合语言与时态逻辑[J];湖南科技大学学报(社会科学版);2009年02期
4 张家龙;;略谈时态逻辑[J];国内哲学动态;1979年12期
5 冯彦波;;论时态逻辑的新发展[J];郑州航空工业管理学院学报(社会科学版);2008年04期
6 白金山;李祥;;具有自反性质的线序时态逻辑研究[J];计算机工程与设计;2011年04期
7 杜国平;;知识蕴涵时态逻辑系统[J];安徽大学学报(哲学社会科学版);2009年05期
8 唐同诰;;程序算子与逻辑算子的统一——一阶时态逻辑(关系逻辑)[J];贵州大学学报(自然科学版);1986年03期
9 冯彦波;;决定论、逻辑决定论与时态逻辑[J];内蒙古农业大学学报(社会科学版);2008年01期
10 吴新民;;时态逻辑与时间思想的语言哲学维度[J];湖南社会科学;2011年04期
相关会议论文 前5条
1 田国会;刘长有;徐心和;;离散事件动态系统理论的时态逻辑研究方法[A];1996中国控制与决策学术年会论文集[C];1996年
2 田国会;刘长有;徐心和;;电梯服务系统的时态逻辑描述、分析与控制[A];1996年中国控制会议论文集[C];1996年
3 陈玉泉;陈宣;陆汝占;;内涵时态逻辑的语义解释系统[A];自然语言理解与机器翻译——全国第六届计算语言学联合学术会议论文集[C];2001年
4 李晓鸥;郭令忠;徐心和;;Petri网监控的时态逻辑框架[A];1994中国控制与决策学术年会论文集[C];1994年
5 刘新;邹丽;;直觉模糊时态逻辑[A];模糊集理论与应用——98年中国模糊数学与模糊系统委员会第九届年会论文选集[C];1998年
相关博士学位论文 前2条
1 王善侠;极小非正规时态逻辑研究[D];西南大学;2017年
2 吕嘉;基于开放时态逻辑的面向方面程序形式化验证和模块推理研究[D];浙江大学;2009年
相关硕士学位论文 前8条
1 田洁;基于时态逻辑的管制员响应执行差错建模与分析方法研究[D];中国民航大学;2016年
2 刘冬宁;时态逻辑及其对知识库的构架与研究[D];广东工业大学;2004年
3 李岚;略论时态逻辑在计算机科学中的发展[D];华东师范大学;2013年
4 李学军;基于时态逻辑的迁移实例运行时安全研究[D];山东大学;2009年
5 王胜;基于SystemC的时态逻辑属性验证方法研究[D];北京化工大学;2009年
6 赵峗;基于时态逻辑的UML交互模型检测研究[D];青岛大学;2008年
7 白金山;二元判断图BDD及其JAVA实现的应用与研究[D];贵州大学;2008年
8 张红军;一类对象Petri网建模与验证方法研究[D];郑州大学;2006年
，本文编号：1669646
本文链接：https://www.wllwen.com/shekelunwen/ljx/1669646.html
