Research On Extension Of Description Logic ALCN And ALCQ

Ontology vocabulary, which lies in key layer of the semantic web architecture, is used to describe concept and semantics of information abstractly and description logic(DL) underpins the OWL. As subset of first order logic, DL has decidable computational property, which leads to its wide application. The dissertation does research on two basic DLs ALCN and ALCQ, aiming to extend expressiveness and solve reasoning and decidability problems.Firstly, background of research is introduced and research status of extension to expressiveness and reasoning of DL is summarized.Secondly, the consistency of ALCN Abox is studied. By using graph theory, some role assertions are eliminated according to the necessary condition that ALCN concept tableau algorithm’s direct application to Abox does not terminate. Then, expansion rules are proposed to expand the rest assertions to a complete forest and the proof of termination, soundness, completeness and decidability of the algorithm is given. At last, trace rules are presented to optimize the algorithm, such that its non-determinism is minimized while preserving inference complexity.Thirdly, epistemic query of ALCNK is discussed. The syntax and semantics of ALCNK which is obtained by embedding epistemic operator K into DL ALCN is given. Then tableau algorithm of epistemic query of ALCNK is designed on condition that Tbox is empty and Abox is K-free. At last, soundness, completeness and decidability of the algorithm is proved and its computational complexity is also analyzed.Finally, a kind of decidable extension to ALCQ is investigated. The DL ALCQs(°,∪,∩), which is sublanguage of ALCQ((°,∪,∩), is obtained by restricting role chains connected by and/or constructors of complex role to have the same length. Then, tableau algorithm of ALCQs((°,∪,∩) concept satisfiability is presented and the proof of termination, soundness, completeness and decidability of the algorithm is given. At last, an untight upper bound of computational complexity is obtained by analyzing the property of ALCQs((°,∪,∩) concept.