论文部分内容阅读
时态逻辑是模态逻辑的一个重要分支。随着人工智能、软件工程、模型检测等领域的产生和发展,时态逻辑在计算机科中越来越重要。本文研究的对象是极小非正规时态逻辑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的典范框架和和它的林登保姆-塔斯基代数的超滤框架是同构的。本文开展的上述工作,从理论上丰富了现有的时态逻辑系统,并建立了一些重要的结论。这些结论在软件规约、自动定理证明和模型检测等方面都有一定的指导意义。因此本文的研究,不仅具有理论意义,而且具有应用价值。