基于OBDD的描述逻辑ALCIO判定算法

摘要：

　　本文对基于OBDD的描述逻辑ALCIO判定算法进行了研究。给定描述逻辑ALCJO中的任一知识库，应用NNF变换和FLAT规则对其进行预处理，通过一个重构过程将知识库中TBox模型转化为布尔函数，然后将布尔函数转换为有序二叉决策图(OBDD)表示形式，从而调用已有的OBDD软件包进行可满足性判定，实现描述逻辑ALCJ0的判定算法。该算法在实现描述逻辑的推理方面与经典的Tableau判定算法在性能上可以相互弥补和配合。

关键词： 描述逻辑 有序二叉决策图 枚举算子 可满足性判定

作者: 常亮 高申 李德波 古天龙

作者单位: 桂林电子科技大学计算机科学与工程学院,广西桂林 541004

会议类型: 国内会议

会议名称: 广西计算机学会2010年年会

会议地点: 南宁

会议语种:中文

页码: 401-405

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