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

摘要：

针对描述逻辑ALC的经典判定算法在处理大规模问题上的不足,而OBDD对于处理大规模问题有高效性,给出了一种基于OBDD的ALC判定算法并证明正确性.该算法根据ALC的概念的形式,计算所有子概念和每个子概念的否定形式的集合,然后根据该集合里的每个概念的形式构造出其相应的布尔函数,将布尔函数转化为OBDD的表示形式来进行概念的可满足性判定.

关键词：描述逻辑、ALC、布尔函数、OBDD、可满足性

所属期刊栏目：32

分类号：TP301(计算技术、计算机技术)

资助基金：广西研究生教育创新计划2010105950812M24

在线出版日期：2012-09-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：213-216