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

OBDD-Based Decision Algorithm for the Description Logic ALCIO

给定描述逻辑ALCIO中的任一知识库,应用NNF变换和FLAT规则对其进行预处理,通过一个重构过程将知识库中TBox模型转化为布尔函数,然后将布尔函数转换为有序二叉决策图(OBDD)表示形式,从而调用已有的OBDD软件包进行可满足性判定,实现描述逻辑ALCIO的判定算法。该算法在实现描述逻辑的推理方面与经典的Tableau判定算法在性能上可以相互弥补和配合。

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.