Extending ALCQ with Bounded Self-Reference.
Daniel Gorín, Lutz Schröder · 2012
Self-reference has been recognized as a useful feature in description logics but is known to cause substantial problems with decidability. We have shown in previous work that the basic description logic ALC remains decidable, and in fact retains its low complexity, when extended with a bounded form of self-reference where only one variable (denoted me following previous work by Marx) is allowed, and no more than two relational steps are allowed to intercede between binding and use of me (this result is optimal in the sense that already allowing three steps leads to undecidability). Here, we extend these results to ALCQ, i.e. ALC extended with qualified number restrictions, and analyse the expressivity of the arising logic, ALCQme2. In fact it turns out the expressive power of ALCQme2 is identical to that of ALCHIQbe, the extension of ALCQ with role inverses, role hierarchies, safe Boolean combinations of roles, and a simple self-loop construct. However, while there is a straightforwardly defined polynomial translation from ALCHIQbe to ALCQme2, the translation from ALCQme2 to ALCHIQbe has an exponential blowup in the formula size. To establish the desired complexity bounds, we therefore provide a polynomial satisfiability-preserving encoding of ALCQme2 into ALCHIQbe and prove that the latter is decidable in EXPTIME.