Terminological Cycles and the Propositional μ-Calculus

Klaus Schild

DFKI DFKI Research Reports (RR) 93-18 1993.


We investigate terminological cycles in the terminological standard logic 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 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 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 ALC augmented by regular role expressions. These results are obtained by a direct correspondence to the so-called propositional μ-calculus which allows to express least and greatest fixpoints explicitly. We propose ALC augmented by the fixpoint operators of the μ-calculus as a unifying framework for all three kinds of semantics.

RR-93-18.pdf (pdf, 43 MB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence