摘要
有序二叉决策图(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.
出处
《桂林电子科技大学学报》
2010年第2期132-136,共5页
Journal of Guilin University of Electronic Technology
基金
广西自然科学基金(0832006Z)