Enriching ℰℒ-Concepts with Greatest Fixpoints

We investigate the expressive power and computational complexity of ℰℒν, the extension of the lightweight description logic ℰℒ with concept constructors for greatest fixpoints. It is shown that ℰℒνhas the same expressive power as ℰℒ extended with simulation quantifiers and that it can be characterized as a largest fragment of monadic second-order logic that is preserved under simulations and has finite minimal models. As in basic ℰℒ, all standard reasoning problems for general TBoxes can be solved in polynomial time. ℰℒνhas a range of very desirable properties that ℰℒ itself is lacking. Firstly, least common subsumers w.r.t. general TBoxes as well as most specific concepts always exist and can be computed in polynomial time. Secondly, ℰℒνshares with ℰℒ the Craig interpolation property and the Beth definability property, but in contrast to ℰℒ allows the computation of interpolants and explicit concept definitions in polynomial time.