摘要
本文对关系语义(或Kripke语义)下极小非正规模态逻辑C2进行时序化处理,得到极小非正规时序逻辑C2t,并建立了C2t的Hilbert式公理系统HC2t,证明了其可靠性和完全性,C2t比极小时序逻辑Kt更具有一般性.本文还从证明论的角度对C2t进行了研究,建立了C2t的一个加标矢列式演算系统GC2t,并且证明了GC2t的可靠性和完全性,同时还证明了GC2t的切割消除定理(cut elimination),然后得到C2t的可判定性.在GC2t中还可以进行证明搜索.
The minimal non-normal modal logic C2 is temporalized, and the minimal non-normal temporal logic C2t is obtained. The Hilbert-style axiomatic system HC2t, which is sound and complete, is established for C2t.The logic C2t is more general than the minimal temporal logic Kt. The proof theory of C2t is approached by introducing the labelled sequent calculus GC2t. The calculus GC2t is sound and complete, and involves cut elimination. The decidability of GC2t is obtained, and the proof search can be performed in GC2t.
作者
马明辉
王善侠
邓辉文
Minghui MA Shanxia WANG Huiwen DENG(Institute for Logic and Intelligence, Southwest University, Chongqing 400715, China School of Computer and Information Science, Southwest University, Chongqing 400715, China School of Computer and Information Engineering, Henan Normal University, Xinxiang 453007, China)
出处
《中国科学：信息科学》
CSCD
北大核心
2017年第1期31-46,共16页
Scientia Sinica(Informationis)
基金
国家社会科学基金项目(批准号:16CZX049)资助
关键词
非正规时序逻辑
公理系统
矢列式演算
完全性
可判定性
non-normal temporal logic
axiomatic system
sequent calculus
completeness
decidability
