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

发布时间：2018-03-24 14:13

  本文选题：非正规时序逻辑　切入点：公理系统　出处：《中国科学:信息科学》2017年01期

【摘要】：本文对关系语义(或Kripke语义)下极小非正规模态逻辑C2进行时序化处理,得到极小非正规时序逻辑C2t,并建立了C2t的Hilbert式公理系统HC2t,证明了其可靠性和完全性,C2t比极小时序逻辑Kt更具有一般性.本文还从证明论的角度对C2t进行了研究,建立了C2t的一个加标矢列式演算系统GC2t,并且证明了GC2t的可靠性和完全性,同时还证明了GC2t的切割消除定理(cut elimination),然后得到C2t的可判定性.在GC2t中还可以进行证明搜索.
[Abstract]:In this paper, the minimal informal modal logic C2 under relational semantics (or Kripke semantics) is sequenced. The minimal informal sequential logic C2t is obtained, and the Hilbert axiomatic system HC2t is established. It is proved that the reliability and completeness of C2t are more general than that of minimal temporal logic Kt. In this paper, we also study C2t from the point of view of proof theory. A scalar vector calculus system GC2t of C2t is established, and the reliability and completeness of GC2t are proved. At the same time, the cut elimination theorem of GC2t is proved, and the determinability of C2t is obtained.
【作者单位】： 西南大学逻辑与智能研究中心;河南师范大学计算机与信息工程学院;西南大学计算机与信息科学学院;
【基金】：国家社会科学基金项目(批准号:16CZX049)资助
【分类号】：O141
，

本文编号：1658651