命题模态逻辑的模型构造和完备性证明

• 作者: 李小燕 柳欣欣
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: Fisher-Ladner闭包 canonical model R规则 可满足性 完备性
• 年，卷（期）: 2014,（8）
• 所属期刊栏目: 软件技术与研究
• 页码范围: 9-12,24
• 页数: 5页
• 分类号: TP301
• 字数: 5724字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2014.08.003

摘要

模态逻辑是研究必然、可能及其相关概念的逻辑.模态公式的可满足性问题和证明系统的完备性问题是模态逻辑中的两个经典的问题.为了解决这两个问题,提出一个构造模态公式的canonical model的方法.通过这个方法,对于给定模态公式(φ),如果(φ)是可满足的,可以得到(φ)的一个canonical model;如果(φ)是不可满足的,可以得到(Γ)(φ)的证明.此外,还给出命题模态逻辑完备性的一个构造性证明方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李小燕	中国科学院软件研究所计算机科学国家重点实验室	18	310	7.0	17.0
10	柳欣欣	中国科学院软件研究所计算机科学国家重点实验室	2	0	0.0	0.0