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