Abstract:Terminological cycles have been a very hard problem in description logics for a long time, and their essential problems, i.e. semantics and reasoning problem, have not been solved reasonably. Based on hybrid graded μ-calculus, the description logic μALCQO which may include terminological cycles is presented, and the μALCQO is derived form the description logic ALCQO which includes the nominal constructor by adding the least and greatest fixpoint constructors. The syntax, semantics and properties of the fixpoint constructors of description logic μALCQO are given. The equality between satisfiability of description logic μALCQO and that of hybrid graded μ-calculus is proved. Based on the satisfiability reasoning algorithm of hybrid graded μ-calculus, the satisfiability reasoning algorithm of description logic μALCQO is presented using fully enriched automata. The correctness of the satisfiability reasoning algorithm is proved, and the complexity property of the reasoning algorithm is given.The theoretical foundation for reasoning algorithms of more expressive description logics including fixpoint constructors and nominal constructor is provided through μALCQO.