On the complexity of (restricted) \(\mathcal{ALCI}r\) (Q2815247)

The logic \(\mathcal{ALCI}r\) extends the description logic \(\mathcal{ALCI}\) with axioms of the form \(R\sqsubseteq QR_1\ldots R_m\) satisfying the same regularity condition as \(\mathcal{SR+OIQ}\), while \(\mathcal{ALCI}r^-\) denotes the fragment of \(\mathcal{ALCI}r\) in which no \(P_i\) appears on the left-hand side of the role inclusion axioms from the set \(\mathrm{RI}=\{R_i\sqsubseteq Q_iP_i\}\). It is proven that concept satisfiability with respect to RBoxes in \(\mathcal{ALCI}r\) is ExpTime-hard. Then, a tableau-based PSpace decision procedure for the same problem is given for \(\mathcal{ALCI}r^-\). The question of the concept satisfiability upper bound for \(\mathcal{ALCI}r\) remains open.