描述逻辑(DL)一族知识表示形式系统,是人工智能领域的一个热门研究方向。循环定义下描述逻辑系统的表达在许多情况下更符合人们的直觉,而且具有更强的表达力,是非循环定义下的描述逻辑系统不可代替的。首先给出描述逻辑系统FLε有最大不动点模型的证明,然后初步探讨基于最大不动点语义下描述逻辑系统FLε循环定义的包含关系推理算法,并给出算法的可靠性和完全性证明。
Description Logic(DL) is a family of knowledge representation formalisms and a hotpoint research direction of artificial intelligence.Description logic systems with cycle definition are more accord with people's intuition,with stronger expression ability and can not be replaced by other description logics in non-cycle definition.This article first presents the semantics and syntax of the description logic system FLε,also gives a proof of the theorem on existence of greatest fixpoint model.Based on the greatest fixpoint semantics,it discusses algorithms for reasoning about the subsumption in cyclic terminological Tbox of the description logic system FLε which has existential and value restrictions.