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

OBDD-Based Decision Algorithm for the Description Logic ALCIO

作　　者：常亮[1] 高申[1] 李德波[1] 古天龙[1] 

机构地区：[1]桂林电子科技大学计算机科学与工程学院,广西桂林541004

出　　处：《广西科学院学报》2010年第4期401-405,共5页Journal of Guangxi Academy of Sciences

基　　金：国家自然科学基金项目(60903079;60963010)资助

摘　　要：给定描述逻辑ALCIO中的任一知识库,应用NNF变换和FLAT规则对其进行预处理,通过一个重构过程将知识库中TBox模型转化为布尔函数,然后将布尔函数转换为有序二叉决策图(OBDD)表示形式,从而调用已有的OBDD软件包进行可满足性判定,实现描述逻辑ALCIO的判定算法。该算法在实现描述逻辑的推理方面与经典的Tableau判定算法在性能上可以相互弥补和配合。A satisfiability-checking algorithm based on Ordered Binary Decision Diagram（OBDD） is presented in this paper for the description logic ALCIO.Starting from an ALCIO ontology,the algorithm introduces the NNF transformation rule and the FLAT rule to do some preprocessing;then the TBox model of the knowledge base is reconstructed and transformed into some Boolean formulas;finally,these Boolean formulas are represented as OBDDs,based on the existing OBDD software package that can be called for deciding the satisfiability of ALCIO ontologies.The experimental results indicate that,according to the performance,the satisfiability-checking algorithm based on OBDD can complement the classical Tableau deciding algorithm.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]