首页 | 本学科首页   官方微博 | 高级检索  
     

具有模态词□φ=1V2φ且可靠与完备的公理系统
引用本文:邓少波,黎敏,曹存根,眭跃飞.具有模态词□φ=1V2φ且可靠与完备的公理系统[J].软件学报,2015,26(9):2286-2296.
作者姓名:邓少波  黎敏  曹存根  眭跃飞
作者单位:中国科学院 计算技术研究所 智能信息处理重点实验室, 北京 100190;中国科学院大学, 北京 100049;南昌工程学院 信息工程学院, 江西 南昌 330099,南昌工程学院 信息工程学院, 江西 南昌 330099,中国科学院 计算技术研究所 智能信息处理重点实验室, 北京 100190,中国科学院 计算技术研究所 智能信息处理重点实验室, 北京 100190
基金项目:国家自然科学基金(61363047, 61173063, 60773059, 61035004); 江西省教育厅科技厅项目(GJJ14748); 江西省科技厅项目(20111BBE50008, 2011ZBBE50035, 20112BBE50052)
摘    要:提出具有模态词□φ=1V2φ的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,12是给定的模态词.该逻辑的公理化系统具有与公理系统S5相似的语言,但具有不同的语法与语义.对于任意的公式φ,□φ=1V2φ;框架定义为三元组W,R1,R2,模型定义为四元组W,R1,R2,I;在完备性定理证明过程中,需要在由所有极大协调集所构成的集合上构造出两个等价关系,其典型模型的构建方法与经典典型模型的构建方法不同.如果1的可达关系R1等于2的可达关系R2,那么该逻辑的公理化系统变成S5.

关 键 词:命题模态逻辑  模态词  公理系统
收稿时间:2014/6/23 0:00:00
修稿时间:2014/8/15 0:00:00
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号