分支时态描述逻辑ALC-CTL及其可满足性判定

• 作者: 孟瑜 常亮 李凤英 李屾
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 时态描述逻辑 分支时态逻辑 可满足性问题 Tableau算法 复杂度
• 年，卷（期）: 2014,（3）
• 所属期刊栏目: 人工智能
• 页码范围: 205-211
• 页数: 7页
• 分类号: TP301
• 字数: 12300字
• 语种: 中文

摘要

时态描述逻辑是将描述逻辑与时态逻辑相结合后得到的逻辑系统,具有较强的描述能力;但是大部分的时态描述逻辑都是将时态算子同时引入到概念和公式中,使得公式可满足性问题的计算复杂度过高.将描述逻辑ALC与分支时态逻辑CTL相结合,提出新的分支时态描述逻辑ALC-CTL.该逻辑没有将时态算子用于概念的构造过程,而是将时态算子引入到公式的构造中;从分支时态逻辑的角度看,相当于将CTL中的原子命题提升为描述逻辑中的个体断言.最终得到的逻辑系统不仅具有较强的刻画能力,还使得公式可满足性问题的复杂度保持在EXPTIME-完全这个级别.通过将CTL的Tableau判定算法与描述逻辑ALC的推理机制有机结合,给出了ALC-CTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	常亮	桂林电子科技大学广西可信软件重点实验室	77	450	12.0	17.0
2	孟瑜	桂林电子科技大学广西可信软件重点实验室	11	20	2.0	4.0
3	李凤英	桂林电子科技大学广西可信软件重点实验室	22	88	5.0	8.0
4	李屾	桂林电子科技大学广西可信软件重点实验室	1	2	1.0	1.0