具有模态词□φ=□_(1φ)∨□_(2φ)且可靠与完备的公理系统

作     者：邓少波 黎敏 曹存根 眭跃飞 DENG Shao-Bo;LI Min;CAO Cun-Gen;SUI Yue-Fei

作者机构：中国科学院计算技术研究所智能信息处理重点实验室北京100190 中国科学院大学北京100049 南昌工程学院信息工程学院江西南昌330099 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2015年第26卷第9期

页      面：2286-2296页

核心收录：

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金(61363047 61173063 60773059 61035004) 江西省教育厅科技厅项目(GJJ14748) 江西省科技厅项目(20111BBE50008 2011ZBBE50035 20112BBE50052) 

主　　题：命题模态逻辑 模态词 公理系统 

摘      要：提出具有模态词□φ=□_(1φ)∨□_(2φ)的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,□_1与□_2是给定的模态词.该逻辑的公理化系统具有与公理系统S5相似的语言,但具有不同的语法与语义.对于任意的公式φ,□φ=□_(1φ)∨□_(2φ);框架定义为三元组,模型定义为四元组;在完备性定理证明过程中,需要在由所有极大协调集所构成的集合上构造出两个等价关系,其典型模型的构建方法与经典典型模型的构建方法不同.如果□_1的可达关系R_1等于□_2的可达关系R_2,那么该逻辑的公理化系统变成S5.