基于OBDD的描述逻辑εL循环术语集推理

• 作者: 古天龙 吕思菁 常亮 徐周波
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 描述逻辑εL 循环术语集 有序二叉决策图 概念包含关系 不动点语义
• 年，卷（期）: 2014,（1）
• 所属期刊栏目: 模式识别与人工智能
• 页码范围: 64-77
• 页数: 14页
• 分类号: TP181
• 字数: 15200字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004403

摘要

循环术语集推理是描述逻辑研究中面临的难点问题,尚未得到很好的解决.有序二叉决策图(ordered binary decision diagram,简称OBDD)是一种对布尔函数进行紧凑表示和高效操作的数据结构,适用于表示和处理大规模问题.将OBDD应用于描述逻辑循环术语集的推理.首先,针对描述逻辑εL中的循环术语集,给出了描述图上关于最大模拟关系的重要性质,并借助集合表示和集合运算对该性质进行了表述和证明.在此基础上,应用布尔函数对描述图进行编码,给出了基于OBDD求解最大模拟关系的方法,进而给出了最大不动点语义下基于OBDD对概念包含关系进行判定的算法;接下来,基于OBDD给出了求解描述图中可以到达循环路径的所有结点的方法,进而给出了最小不动点语义下基于OBDD对概念包含关系进行判定的算法;最后,对算法的正确性、复杂度等进行了分析和证明,并对算法进行了编程实现,给出了关于计算性能的实验结果.该工作为循环术语集的推理提供了一条有效途径,也为OBDD在逻辑推理中的应用提供了新的案例.