OBDD-Based Decision Algorithm for the Description Logic ALCIO
Tianlong Gu · Journal of Guangxi Academy of Sciences · 2010
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.