极小非正规时序逻辑的矢列式演算系统
本文对关系语义(或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