极小非正规时序逻辑的矢列式演算系统

摘要：

本文对关系语义(或Kripke语义)下极小非正规模态逻辑C2进行时序化处理,得到极小非正规时序逻辑C2t,并建立了C2t的Hilbert式公理系统HC2t,证明了其可靠性和完全性,C2t比极小时序逻辑Kt更具有一般性,本文还从证明论的角度对C2t进行了研究,建立了C2t的一个加标矢列式演算系统GC2t,并且证明了GC2t的可靠性和完全性,同时还证明了GC2t的切割消除定理(cut elimination),然后得到C2t的可判定性.在GC2t中还可以进行证明搜索.

关键词：非正规时序逻辑、公理系统、矢列式演算、完全性、可判定性

所属期刊栏目：47

分类号：TP18;TP301;O142

资助基金：国家社会科学基金16CZX049

在线出版日期：2017-03-03（万方平台首次上网日期，不代表论文的发表时间）

页码：31-46