%0 Journal Article
%T 基于obdd的描述逻辑εl循环术语集推理
%A 古天龙？
%A 吕思菁？
%A 常亮？
%A 徐周波？
%J 软件学报
%P 64-77
%D 2014
%R 10.13328/j.cnki.jos.004403
%X 循环术语集推理是描述逻辑研究中面临的难点问题，尚未得到很好的解决.有序二叉决策图（orderedbinarydecisiondiagram，简称obdd）是一种对布尔函数进行紧凑表示和高效操作的数据结构，适用于表示和处理大规模问题.将obdd应用于描述逻辑循环术语集的推理.首先，针对描述逻辑εl中的循环术语集，给出了描述图上关于最大模拟关系的重要性质，并借助集合表示和集合运算对该性质进行了表述和证明.在此基础上，应用布尔函数对描述图进行编码，给出了基于obdd求解最大模拟关系的方法，进而给出了最大不动点语义下基于obdd对概念包含关系进行判定的算法；接下来，基于obdd给出了求解描述图中可以到达循环路径的所有结点的方法，进而给出了最小不动点语义下基于obdd对概念包含关系进行判定的算法；最后，对算法的正确性、复杂度等进行了分析和证明，并对算法进行了编程实现，给出了关于计算性能的实验结果.该工作为循环术语集的推理提供了一条有效途径，也为obdd在逻辑推理中的应用提供了新的案例.
%K 描述逻辑εl
%K 循环术语集
%K 有序二叉决策图
%K 概念包含关系
%K 不动点语义
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4403&flag=1