Chinese Journal of Computers   Full Text
  TitleSemantics and Reasoning of Description Logic μALCIO
  AuthorsJIANG Yun-Cheng1),2) WANG Ju3) DENG Pei-Min3) TANG Yong4) ZHOU Sheng-Ming3)
  Address1)(School of Computer Science, South China Normal University, Guangzhou 510631) 2)(Sate Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190) 3)(College of Computer Science and Information Engineering, Guangxi Normal University, Guilin, Guangxi 541004) 4)(Department of Computer Science, Sun Yat-Sen University, Guangzhou 510275)
  Year2009
  IssueNo.7(1280—1290)
  Abstract &
  Background 		Abstract Terminological cycles have been a difficult spot in the study of description logics for quite a few years. The basic problems, such as their semantics and reasoning mechanisms, have not been reasonably well settled. The current research progresses and the existing problems of terminological cycles in description logics are analyzed in this paper. Based on hybrid μ-calculus, description logic μALCIO which may include terminlolgical cycles is presented, and μALCIO is derived form description logic ALCIO which includes nominal constructors by adding least and greatest fixpoint constructors. The syntax and semantics of description logic μALCIO are given. The equality between satisfiability of description logic μALCIO and satisfiability of hybrid μ-calculus is proved. The satisfiability reasoning algorithm of description logic μALCIO is presented using tree automata. The correctness of the satisfiability reasoning algorithm is proved, and the complexity property of the reasoning algorithm is given. Keywords description logic; μALCIO; hybrid μ-calculus; tree automata; fixpoint constructors Background Description logics are a logical reconstruction of the frame-based knowledge representation languages, with the aim of providing a simple well-established declarative semantics to capture the meaning of structured representation of knowledge. Terminological cycles (or cyclic definitions) have been a difficult spot in the study of description logics for quite a few years. The basic problems, such as their semantics and reasoning mechanisms, have not been reasonably well settled. However, terminological cycles may greatly extend the expressive capability of the language. In some applications, terminological cycles are indispensable. Also, by using terminological cycles, one can establish a description logic knowledge base more conveniently because it would give the people an intuitive understanding of the axioms, sentences of the knowledge base. If we do not accept terminological cycles in the knowledge base, when a cyclic concept occurs in the application, it would make the system specification overly complex and hard to understand by a user. For these reasons, it is significant to study the semantics and the algorithmic nature of terminological cycles. Based on hybrid μ-calculus, description logic μALCIO which may include terminlolgical cycles is presented, and μALCIO is derived form description logic ALCIO which includes nominal constructors by adding least and greatest fixpoint constructors. The syntax and semantics of description logic μALCIO are given. The equality between satisfiability of description logic μALCIO and satisfiability of hybrid μ-calculus is proved. The satisfiability reasoning algorithm of description logic μALCIO is presented by using tree automata. The correctness of the satisfiability reasoning algorithm is proved, and the complexity property of the reasoning algorithm is given. The work is supported by the National Natural Science Foundation of China under grant Nos.60663001, 60573010, 60673135 and 60373081, the Open Foundation of the State Key Laboratory of Computer Science of Chinese Academy of Sciences under grant No.SYSKF0904, and the Natural Science Foundation of Guangxi Province of China under grant Nos.0640030, 0991100 and 0832103.