On the Decidability of Expressive Description Logics with Transitive Closure and Regular Role Expressions.

We consider fragments of the description logic SHOIF extended with regular expressions on roles. Our main result is that satisfiability and finite satisfiability are decidable in two fragments SHOIFreg1 and SHOIFreg2, NEXPTIME-complete for the former and in 2NEXPTIME for the more expressive latter fragment. Both fragments impose restrictions on regular role expressions of the form alpha(*). SHOIF(reg)(1)encompasses the extension of SHOIF with transitive closure of roles (when functional roles have no subroles) and the modal logic of linear orders and successor, with converse. Consequently, these logics are also decidable and NEXP-TIME-complete.