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

Research on OBDD-based decision algorithm for εL^(￢) ontology

作　　者：高申[1] 古天龙[1] 

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

出　　处：《桂林电子科技大学学报》2010年第2期132-136,共5页Journal of Guilin University of Electronic Technology

基　　金：广西自然科学基金(0832006Z)

摘　　要：有序二叉决策图(OBDD)是一种新型的数据结构,在较大状态空间规模的模型检测和验证等领域中,已经得到了成功应用,并且在逻辑公式的可满足性判定方面也具有巨大的应用潜力。通过采用OBDD实现了描述逻辑εL(￢)判定算法。以基于OBDD的SHIQ判定算法为基础,针对描述逻辑εL(￢)进行了优化,应用标准化规则取代了FLAT规则,重构了知识库模型,进而将该模型转化为满足3CNF(每个从句含有3个变元的合取形式)约束的布尔函数并利用OBDD进行可满足性判定,并以实例对算法过程进行了演示。As a state-of-the-art data structure,Ordered Binary Decision Diagram （OBDD） has been successfully applied in large-scale state space of model checking and verification;there are some attractive potentials for it to be applied in the satisfiability-checking of logical formulas.In this paper,an OBDD-based decision algorithm for the description logic εL（￢） is presented.Taking an OBDD-based decision algorithm of the description logic SHIQ as the basis,some strategies for optimizing the algorithm were proposed for εL（￢）,and FLAT rules introduced in the former algorithm were replaced by some normalization rules,the model of knowledge bases is reconstructed,so that it could be transformed into Boolean formula in 3CNF（Conjunctive Normal Form with 3 Variables per Clause） forms,then,the satisfiability of Boolean formulas was checked by OBDD,and the algorithm procedure was carried out by an example.

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

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