| 基于OBDD的描述逻辑εL循环术语集推理 |
| |
| 作者姓名： | 古天龙 吕思菁 常亮 徐周波 |
| |
| 作者单位： | 广西可信软件重点实验室(桂林电子科技大学), 广西 桂林 541004;广西可信软件重点实验室(桂林电子科技大学), 广西 桂林 541004;广西可信软件重点实验室(桂林电子科技大学), 广西 桂林 541004;广西可信软件重点实验室(桂林电子科技大学), 广西 桂林 541004 |
| |
| 基金项目： | 国家自然科学基金（60963010，60903079，61100025，61262030，61363030）；广西自然科学基金（2012GXNSFBA053169） |
| |
| 摘 要： | 循环术语集推理是描述逻辑研究中面临的难点问题，尚未得到很好的解决.有序二叉决策图（ordered binary decision diagram，简称OBDD）是一种对布尔函数进行紧凑表示和高效操作的数据结构，适用于表示和处理大规模问题.将OBDD应用于描述逻辑循环术语集的推理.首先，针对描述逻辑εL中的循环术语集，给出了描述图上关于最大模拟关系的重要性质，并借助集合表示和集合运算对该性质进行了表述和证明.在此基础上，应用布尔函数对描述图进行编码，给出了基于OBDD求解最大模拟关系的方法，进而给出了最大不动点语义下基于OBDD对概念包含关系进行判定的算法；接下来，基于OBDD给出了求解描述图中可以到达循环路径的所有结点的方法，进而给出了最小不动点语义下基于OBDD对概念包含关系进行判定的算法；最后，对算法的正确性、复杂度等进行了分析和证明，并对算法进行了编程实现，给出了关于计算性能的实验结果.该工作为循环术语集的推理提供了一条有效途径，也为OBDD在逻辑推理中的应用提供了新的案例.
|
| 关 键 词： | 描述逻辑εL 循环术语集 有序二叉决策图 概念包含关系 不动点语义 |
| 收稿时间： | 2012-09-06 |
| 修稿时间： | 2013-03-27 |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
