描述逻辑μALCQO的语义及推理

• 作者: 汤庸 王驹 蒋运承 邓培民
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 描述逻辑 μALCQO 混合分级μ-演算 完全强化自动机 不动点构造算子
• 年，卷（期）: 2009,（3）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 491-504
• 页数: 14页
• 分类号: TP301
• 字数: 14739字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2009.03255

摘要

循环术语集是描述逻辑长期以来的研究难点,其最基本的问题即语义及推理问题没有得到合理的解决.基于混合分级μ-演算将不动点构造算子引入到含有枚举构造算子的描述逻辑ALCQO中,提出了一种允许包含循环术语集的描述逻辑μALCQO.给出了μALCQO的语法、语义和不动点构造算子的性质,证明了μALCQO的可满足性推理等价于混合分级μ-演算的可满足性推理.基于混合分级μ-演算可满足性推理算法,并利用完全强化自动机给出了μALCQO的可满足性推理算法,以及给出了推理算法正确性证明和复杂性定理.μALCQO为进一步给出同时含有不动点构造算子和枚举构造算子的表达能力强的描述逻辑推理算法提供了理论基础.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王驹	广西师范大学计算机科学与信息工程学院	53	458	11.0	19.0
2	蒋运承	广西师范大学计算机科学与信息工程学院	44	591	15.0	23.0
4	汤庸	中山大学计算机科学系	95	1243	20.0	30.0
7	邓培民	广西师范大学计算机科学与信息工程学院	61	278	9.0	13.0