欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
循环术语集是描述逻辑长期以来的研究难点，它的最基本的问题即语义及推理问题没有得到合理的解决．分析了描述逻辑循环术语集的研究现状和存在的问题，基于混合“一演算将不动点构造算子引入到含有枚举构造算子的描述逻辑ALCIO中，提出了一种允许包含循环术语集的描述逻辑μALCIO．给出了μALCIO的语法和语义，证明了μALCIO的可满足性推理等价于混合旷演算的可满足性推理，并利用树自动机理论给出了μALCIO的可满足性推理算法以及给出了推理算法正确性证明和复杂性定理．
英文摘要：
Terminological cycles have been a difficult spot in the study of description logics for quite a few years. The basic problems, such as their semantics and reasoning mechanisms, have not been reasonably well settled. The current research progresses and the existing problems of terminological cycles in description logics are analyzed in this paper. Based on hybrid μ-calculus, description logic μALCIO which may include terminlolgical cycles is presented, and μALCIO is derived form description logic ALCIO which includes nominal constructors by adding least and greatest fixpoint constructors. The syntax and semantics of description logic μALCIO are given. The equality between satisfiability of description logic μALCIO and satisfiability of hybrid μ-calculus is proved. The satisfiability reasoning algorithm of description logic μALCIO is presented using tree automata. The correctness of the satisfiability reasoning algorithm is proved, and the complexity property of the reasoning algorithm is given.
同期刊论文项目
同项目期刊论文
期刊信息
位置：