Terminological cycles and the ropositional μ-calculus

We investigate terminological cycles in the terminological standard logic mathcal{ALC} with the only restriction that recursively defined concepts must occur in their definition positively. This restriction, called syntactic monotonicity, ensures the existence of least and greatest fixpoint models. It turns out that as far as syntactically monotone terminologies of mathcal{ALC} are concerned, the descriptive semantics as well as the least and greatest fixpoint semantics do not differ in the computational complexity of the corresponding subsumption relation. In fact, we prove that in each case subsumption is complete for deterministic exponential time. We then show that the expressive power of finite sets of syntactically monotone terminologies of mathcal{ALC} is the very same for the least and the greatest fixpoint semantics and, moreover, in both cases they are strictly stronger in expressive power than mathcal{ALC} augmented by regular role expressions. These results are obtained by a direct correspondence to the so-called propositional mu-calculus which allows to express least and greatest fixpoints explicitly. We propose ALC augmented by the fixpoint operators of the mu-calculus as a unifying framework for all three kinds of semantics