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

• 作者: 王善侠 邓辉文 马明辉
• 来源期刊: 中国科学（信息科学）
• 关键词: 非正规时序逻辑 公理系统 矢列式演算 完全性 可判定性
• 年，卷（期）: 2017,（1）
• 所属期刊栏目: 论文
• 页码范围: 31-46
• 页数: 16页
• 语种: 中文
• DOI: 10.1360/N112015-00320

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	邓辉文	西南大学逻辑与智能研究中心	34	339	12.0	17.0
5	马明辉	西南大学逻辑与智能研究中心	20	10	1.0	2.0
6	王善侠	西南大学逻辑与智能研究中心	5	9	2.0	2.0