$$\boldsymbol{\mathcal{ALCQPI}}_{\boldsymbol{R}^{\mathbf{+}}}$$ : Rational Grading in an Expressive Description Logic with Inverse and Transitive Roles and Counting

In this paper, we consider the expressive Description Logic (DL) $$\mathcal{ALCQPI}_{R^{+}}$$ having concept constructors called part restrictions that realize rational grading. Part restrictions are able to convey statements about a rational part of a set of successors, and they essentially enrich the expressive capabilities of DLs. That is why it is important to evaluate the cost of their use with respect to the reasoning complexity. We modify the tableaux algorithm used for $$\mathcal{ALCNI}_{R^{+}}$$ (a DL with just number restrictions instead of qualified number ones), and augment it with a specific technique for dealing with part restrictions to prove that concept satisfiability and subsumption in the considered DL are still in PSPACE.