| 引用本文： |
-
常亮,高申,李德波,古天龙.基于OBDD的描述逻辑ALCIO判定算法[J].广西科学院学报,2010,26(4):401-405. [点击复制]
- CHANG Liang,GAO Shen,LI De-bo,GU Tian-long.OBDD-Based Decision Algorithm for the Description Logic ALCIO[J].Journal of Guangxi Academy of Sciences,2010,26(4):401-405. [点击复制]
|
|
| 摘要: |
| 给定描述逻辑ALCIO中的任一知识库,应用NNF变换和FLAT规则对其进行预处理,通过一个重构过程将知识库中TBox模型转化为布尔函数,然后将布尔函数转换为有序二叉决策图(OBDD)表示形式,从而调用已有的OBDD软件包进行可满足性判定,实现描述逻辑ALCIO的判定算法。该算法在实现描述逻辑的推理方面与经典的Tableau判定算法在性能上可以相互弥补和配合。 |
| 关键词: 描述逻辑 有序二叉决策图 枚举算子 可满足性判定 |
| DOI： |
| 投稿时间：2010-09-21 |
| 基金项目:国家自然科学基金项目(60903079,60963010)资助。 |
|
| OBDD-Based Decision Algorithm for the Description Logic ALCIO |
|
CHANG Liang, GAO Shen, LI De-bo, GU Tian-long
|
| (School of Computer Science and Technology, Guilin University of Electronic Technology, Guilin, Guangxi, 541004, China) |
| Abstract: |
| A satisfiability-checking algorithm based on Ordered Binary Decision Diagram (OBDD) is presented in this paper for the description logic ALCIO.Starting from an ALCIO ontology, the algorithm introduces the NNF transformation rule and the FLAT rule to do some preprocessing; then the TBox model of the knowledge base is reconstructed and transformed into some Boolean formulas; finally, these Boolean formulas are represented as OBDDs, based on the existing OBDD software package that can be called for deciding the satisfiability of ALCIO ontologies. The experimental results indicate that, according to the performance, the satisfiability-checking algorithm based on OBDD can complement the classical Tableau deciding algorithm. |
| Key words: description logic ordered binary decision diagram nominals satisfiability-checking |
