Research On OBDD-based Decision Algorithm For Description Logics

As a family of knowledge representation formalisms, description logic has beensuccessfully applied in information systems, software engineering, natural languageprocessing and other fields. Especially with the recent development of Semantic Web,description logic, playing an important role, has become the logical basis of the SemanticWeb Ontology Language (OWL). With the wide range of applications the description logicbased ontology in semantics in e-Science and Semantic Web, the reasoning algorithms ofthe description logic is encountering a series of challenges for dealing with large-scaleproblems. Tableau algorithm is the most important method in description logic reasoning,but not the best in all cases. Therefore, it is necessary to look for suitable reasoningalgorithms for ontologies about different characteristics.Ordered Binary Decision Diagram (OBDD) as a graph-based data structure arecompact representations of Boolean functions. As the OBDD can effectively represent thecompression of information and handle large-scale problems, it has been successfullyapplied in the domain of large-scale model checking and verification.According tocharacteristics of OBDD and the advantages of Tableau algorithm in processing numerousrole names, this paper has done research of description logic reasoning algorithm based onOBDD and Tableau. There are main contents as following:(1) According to characteristics of OBDD, decision algorithm consistency of thedescription logic SHOIQ-TBox on OBDD-based is given. The algorithm will convert anSHOIQ knowledge base into an equisat- isfiable ALCIb knowledge base. Firstly, Startingfrom an ALCIb knowledge base, the algorithm introduces the FLAT rule to do somepreprocessing; Secondly, the model of the dominos set is constructed about the TBox of theknowledge base and then the model is transformed into Boolean function; Finally, theseBoolean functions are represented as OBDDs and then decide the consistency of the TBox.(2) According to the decision algorithm on OBDD-based for description logic exeitedthe limitations in dealing with ontologies with the many of role names, with Tableaualgorithm advantage in this case, decision algorithm consistency of the description logicALCIO-TBox on OBDD-Tableau-based is given. Firstly, the ALCIO-TBox is mapped topropositional level and mode level. Secondly, determ- ining the satisfiability of propositionlevel by OBDD, and deciding the satisfiability of modal level by Tableau, then todetermine the consistency of ALCIO-TBox . Finally, reliability, completeness and termina tion of the algorithm are proved.(3) Based on the two reasoning algorithms above, we develop the correspondingprototype reasoning system: DLR_SHOIQ and DLR_ALCIO (OBDD-Tableau). Theresults of experiment show that pure OBDD reasoning algorithm outperforms purereasoning algorithm Tableau in the larger ontology but less role name. Pure OBDDreasoning algorithm is inferior to pure Tableau reasoning algorithm in larger ontology butthe number of role names, OBDD-Tableau reasoning algorithm is better than purereasoning algorithms and pure OBDD Tableau reasoning algorithm. In other cases,OBDD-Tableau algorithm is less than pure Tableau reasoning algorithms because the timecost of building OBDD.