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

An OBDD-based decision algorithm for the description logic ALC

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

Description logic is the logic basic of semantic web, which has become a hot spot in computer science and artificial intelligence. Because the description logic ALC has the shortage of large-scale problems, but OBDD has an advantage in large-scale problems processing, a satisfiability-checking algorithm and correctness based on OBDD is presented. According to the form of the concept of the ALC, this algorithm computes the set of all the sub-concepts of this concept and their negative forms, constructs Boolean functions by the form of concepts in the set and represents all sub-set of the set by OBDD and check the satisfiability of the input concept by some operations on OBDD.