基于OBDD的εL(-)本体判定算法

摘要：

有序二叉决策图(OBDD)是一种新型的数据结构,在较大状态空间规模的模型检测和验证等领域中,已经得到了成功应用,并且在逻辑公式的可满足性判定方面也具有巨大的应用潜力.通过采用OBDD实现了描述逻辑εL(一)判定算法.以基于OBDD的SHIQ判定算法为基础,针对描述逻辑εL(一)进行了优化,应用标准化规则取代了FLAT规则,重构了知识库模型,进而将该模型转化为满足3CNF(每个从句含有3个变元的合取形式)约束的布尔函数并利用OBDD进行可满足性判定,并以实例对算法过程进行了演示.

关键词：描述逻辑、一致性、Tableau-算法、有序二叉决策图

所属期刊栏目：30

分类号：TP301.6(计算技术、计算机技术)

资助基金：广西自然科学基金0832006Z

在线出版日期：2010-06-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：132-136