循环术语集是描述逻辑长期以来的研究难点,它的最基本的问题即语义及推理问题没有得到合理的解决,文中分析了描述逻辑循环术语集的研究现状和存在的问题,在Baader的基础上进一步研究了描述逻辑FL^-循环术语集的语义及推理问题.给出了FL^-循环术语集的语法、语义和不动点模型的构造方法.针对FL^-循环术语集的需要,提出了一种新的有限自动机,使用有限自动机给出了不动点语义和描述语义下FL^-循环术语集的可满足性和包含推理算法,证明了推理算法的正确性,并给出了推理算法的复杂性定理。
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 the work of Baader F, the semantics and reasoning of terminological cycles in description logic FL- are further studied. The syntax, semantics, and construction method of fixpoint models of terminololgical cycles in FL^- are given. Aiming at the requirement of terminololgical cycles in FL^-, a kind of new finite automata is presented, and the satisfiability and subsumption reasoning algorithms of terminological cycles in FL^- w. r. t. fixpoint semantics and descriptive semantics are presented using finite automata. The correctness of reasoning algorithms is proved, and the complexity property of reasoning algorithms is given.