Decidability of Description Logics with Transitive Closure of Roles in Concept and Role Inclusion Axioms

Abstract. This paper investigates Description Logics which allow transitive closure of roles to occur not only in concept inclusion axioms but also in role inclusion axioms. First, we propose a decision procedure for the description logic SHIO+, which is obtained from SHIO by adding transitive closure of roles. Next, we show that SHIO+ has the finite model property by providing a upper bound on the size of models of satisfiable SHIO+-concepts with respect to sets of concept and role inclusion axioms. Additionally, we prove that if we add number restrictions to SHI+ then the satisfiability problem is undecidable.