| 描述逻辑μALCQO 的语义及推理 |
| |
| 引用本文： | 蒋运承,王驹,汤庸,邓培民.描述逻辑μALCQO 的语义及推理[J].软件学报,2009,20(3):491-504. |
| |
| 作者姓名： | 蒋运承 王驹 汤庸 邓培民 |
| |
| 作者单位： | 1. 广西师范大学,计算机科学与信息工程学院,广西,桂林,541004;中山大学,计算机科学系,广东,广州,510275
2. 广西师范大学,计算机科学与信息工程学院,广西,桂林,541004
3. 中山大学,计算机科学系,广东,广州,510275 |
| |
| 基金项目： | Supported by the National Natural Science Foundation of China under Grant Nos.60663001, 60573010, 60673135, 60373081 (国家自然科学基金); the Postdoctoral Science Foundation of China under Grant No.20060400226 (中国博士后科学基金); the NaturalScience Key Foundation of Guangdong Province of China under Grant No.04105503 (广东省自然科学重点基金); the Natural ScienceFoundation of Guangxi Province of China under Grant Nos.0640030, 0832103 (广西自然科学基金) |
| |
| 摘 要： | 循环术语集是描述逻辑长期以来的研究难点,其最基本的问题即语义及推理问题没有得到合理的解决.基于混合分级μ-演算将不动点构造算子引入到含有枚举构造算子的描述逻辑ALCQO 中,提出了一种允许包含循环术语集的描述逻辑μALCQO.给出了μALCQO 的语法、语义和不动点构造算子的性质,证明了μALCQO 的可满足性推理等价于混合分级μ-演算的可满足性推理.基于混合分级μ-演算可满足性推理算法,并利用完全强化自动机给出了μALCQO的可满足性推理算法,以及给出了推理算法正确性证明和复杂性定理.μALCQO为进一步给出同时含有不动点构造算子和枚举构造算子的表达能力强的描述逻辑推理算法提供了理论基础.
|
| 关 键 词： | 描述逻辑 μALCQO 混合分级μ-演算 完全强化自动机 不动点构造算子 |
| 收稿时间： | 2007/7/23 0:00:00 |
| 修稿时间： | 2008/1/10 0:00:00 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
