作者：常亮 高申 李德波 古天龙描述逻辑有序二叉决策图枚举算子可满足性判定
摘要：给定描述逻辑ALCIO中的任一知识库,应用NNF变换和FLAT规则对其进行预处理,通过一个重构过程将知识库中TBox模型转化为布尔函数,然后将布尔函数转换为有序二叉决策图（OBDD）表示形式,从而调用已有的OBDD软件包进行可满足性判定,实现描述逻辑ALCIO的判定算法。该算法在实现描述逻辑的推理方面与经典的Tableau判定算法在性能上可以相互弥补和配合。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
《广西科学院学报》（季刊）创刊于1982年，由广西科学院主办，CN刊号为：45-1075/N，自创刊以来，颇受业界和广大读者的关注和好评。 《广西科学院学报》始终坚持以马列主义、思想、邓小平理论和“三个代表”重要思想为指导，刊登了大量广西自然科学各领域的学术论文和具有创造性的科研成果，为活跃自然科学的理论研究，促进科技成果向生产力转化，繁荣科学技术事业，推动科技成果在国内外的交流作出了积极的贡献。
省级期刊
人气 238639 评论 36
人气 154232 评论 33
人气 151907 评论 53
人气 123247 评论 54
