Satisfiability and reasoning mechanism of terminological cycles in description logic vL

The current research works and the existing problems of terminological cycles in description logics are analyzed in this paper. Referring to the works of Baader F and Nebel B, we aim in a new direction. Firstly, description logic vL is defined, and the description graphs GT and GJ are redefined. A syntax condition for the satisfiability of membership relation is given. By using this syntax condition, we prove the following： The subsumption reasoning in vL with respect to gfp-model, Ifp-model and descriptive model is polynomial.

描述逻辑εLN循环术语集的不动点语义及推理

循环术语集是描述逻辑长期以来的研究难点,其最基本的问题即语义及推理问题没有得到合理的解决分析了描述逻辑循环术语集的研究现状和存在的问题,将Baader的工作扩展到新的方向.针对更大的描述逻辑系统研究了循环术语集的语义及推理机制,即在描述逻辑εL的基础上添加数量约束构造算子,提出了描述逻辑εLN,给出了εLN的语义(包括不动点语义和描述语义).针对εLN的需要,重新定义了描述图(包括语法描述图和语义描述图).使用描述图之间的模拟关系给出了不动点语义下εLN循环术语集的可满足性和包含关系推理算法,并证明了推理算法是多项式时间复杂的.

基于描述逻辑的本体模型研究

本体原本是一个哲学概念 ,是指关于存在及其规律的学说 ,后来被人工智能所引入 ,特指对概念化的一个显式的规格说明 ,并应用在智能体间的通信、异构信息源的集成、语义 Web等领域。形式化的本体模型及其检验问题一直是人工智能中的研究热点。本文将描述逻辑应用到本体建模领域 ,建立基于逻辑的本体模型 ,分析本体术语检验与实例检验问题。

描述逻辑FL-循环术语集的语义及推理

循环术语集是描述逻辑长期以来的研究难点,它的最基本的问题即语义及推理问题没有得到合理的解决.文中分析了描述逻辑循环术语集的研究现状和存在的问题,在Baader的基础上进一步研究了描述逻辑FL^-循环术语集的语义及推理问题.给出了FL^-循环术语集的语法、语义和不动点模型的构造方法.针对FL^-循环术语集的需要,提出了一种新的有限自动机,使用有限自动机给出了不动点语义和描述语义下FL^-循环术语集的可满足性和包含推理算法,证明了推理算法的正确性,并给出了推理算法的复杂性定理.

描述逻辑εL混合循环术语集的LCS和MSC推理

分析了描述逻辑循环术语集的研究现状和存在的问题,在F.Baader工作的基础上进一步研究了描述逻辑εL混合循环术语集的LCS(least common subsumer)和MSC(most specific concept)推理问题.给出了εL混合循环术语集的语法和语义.针对εL混合循环术语集LCS和MSC推理的需要,提出了TBox-完全的概念,并重新定义了描述图.使用描述图和TBox-完全给出了最大不动点语义下εL混合循环术语集LCS和MSC的推理算法,证明了推理算法的正确性,并证明了推理算法是多项式时间复杂的.该推理算法为εL混合循环术语集的LCS和MSC推理提供了理论基础.

描述逻辑εL循环术语集的混合推理

循环术语集是描述逻辑长期以来的研究难点,它最基本的问题即语义及推理问题没有得到合理的解决.分析了描述逻辑循环术语集的研究现状和存在的问题,在Baader和Brandt的基础上进一步研究了描述逻辑εL循环术语集的混合推理问题.给出了εL的混合循环知识库的语法和语义(包括不动点语义和描述语义).针对εL循环术语集混合推理的需要,提出了TBox-完全的概念,并重新定义了描述图(包括语法描述图和语义描述图).使用描述图之间的模拟关系和TBox-完全概念给出了最大不动点语义和描述语义下εL混合循环知识库的实例检测推理算法,证明了推理算法的正确性,并给出了推理算法的复杂性定理.

基于OBDD的描述逻辑εL循环术语集推理

循环术语集推理是描述逻辑研究中面临的难点问题,尚未得到很好的解决.有序二叉决策图(ordered binary decision diagram,简称OBDD)是一种对布尔函数进行紧凑表示和高效操作的数据结构,适用于表示和处理大规模问题.将OBDD应用于描述逻辑循环术语集的推理.首先,针对描述逻辑εL中的循环术语集,给出了描述图上关于最大模拟关系的重要性质,并借助集合表示和集合运算对该性质进行了表述和证明.在此基础上,应用布尔函数对描述图进行编码,给出了基于OBDD求解最大模拟关系的方法,进而给出了最大不动点语义下基于OBDD对概念包含关系进行判定的算法;接下来,基于OBDD给出了求解描述图中可以到达循环路径的所有结点的方法,进而给出了最小不动点语义下基于OBDD对概念包含关系进行判定的算法;最后,对算法的正确性、复杂度等进行了分析和证明,并对算法进行了编程实现,给出了关于计算性能的实验结果.该工作为循环术语集的推理提供了一条有效途径,也为OBDD在逻辑推理中的应用提供了新的案例.

gfp-模型的描述逻辑FLε的循环术语集推理

描述逻辑(DL)一族知识表示形式系统,是人工智能领域的一个热门研究方向。循环定义下描述逻辑系统的表达在许多情况下更符合人们的直觉,而且具有更强的表达力,是非循环定义下的描述逻辑系统不可代替的。首先给出描述逻辑系统FLε有最大不动点模型的证明,然后初步探讨基于最大不动点语义下描述逻辑系统FLε循环定义的包含关系推理算法,并给出算法的可靠性和完全性证明。

带RVM的描述逻辑εL混合循环术语集的语义及推理

分析描述逻辑循环术语集的研究现状和存在的问题,在F.Baader和S.Brandt的基础上进一步研究带RVM的描述逻辑εL混合循环术语集的语义及推理问题.给出带RVM的εL混合循环术语集的语法和语义.针对带RVM的εL混合循环术语集包含推理的需要,提出TBox-完全的概念,并重新定义描述图,使用描述图之间的模拟关系和TBox-完全给出最大不动点语义和描述语义下带RVM的εL混合循环术语集的概念包含推理算法,证明推理算法的正确性,并证明推理算法是多项式时间复杂的.