论文部分内容阅读
描述逻辑是一类刻画领域知识的形式化工具，在信息系统、软件工程、自然语言处理等领域已得到了成功应用。目前描述逻辑已成为语义Web本体语言OWL的逻辑基础，在语义 Web中起着更重要的作用。而当前的描述逻辑的推理算法却存在一些缺陷，尤其是在处理大规模问题时表现更为突出。Tableau算法是当前描述逻辑中最主要的推理方法，但其并不是在所有情况下都表现最好。因此，针对不同特征的本体，寻找合适的推理算法一直备受学者关注。 在现有的描述逻辑推理系统中，都要求描述逻辑知识库中的 TBo x中不包含有循环定义。但是，在很多场合下，不得不用循环定义来对知识进行刻画。如何解决有循环定义的推理问题也是备受关注。 有序二叉决策图(OBDD)是一种基于图的数据结构，是布尔函数的一种压缩表示形式，是信息的高效压缩，能高效地处理大规模问题，在模型检测和验证等领域已经得到了广泛应用。基于上述原因，本文做了基于OBDD的描述逻辑推理算法相关研究。其主要内容如下： (1)针对不允许循环定义的描述逻辑ALC，给出基于OBDD的可满足判定算法。首先根据待判定概念的形式，计算出其所有子概念和每个子概念的否定形式的集合；然后根据该集合里的每个概念的形式构造出其相应的布尔函数；最后将布尔函数转化为O BDD的表示形式来进行概念的可满足性判定；此外，并证明算法的正确性。 (2)针对允许循环定义的但不含有否定构造算子的描述逻辑εL循环术语集，给出基于OBDD的不动点语义下的概念包含判定算法。首先根据TBox的描述图和模拟关系，给出最大模拟关系的性质并证明其正确性；然后用 OBDD刻画描述图，进而利用OBDD计算最大模拟关系以及循环路径；最后通过OBDD的可满足操作来判定包含关系。 (3)针对允许循环定义并且包含否定构造算子的描述逻辑μALC，给出基于OBDD的概念可满足的判定算法。首先构造造出其准模型；然后利用布尔函数表示准模型，得到准模型的OBDD表示；最后利用基于OBDD的验证算法对准模型进行验证以判定概念可满足性。