Semantics and reasoning of description logic μALCIO

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.