Description Logics with Transitive Roles
Ian Horrocks, Graham Gough · 1997
This paper describes the logic ALCHR +, which extends ALCR + with a primitive role hierarchy, and presents an appropriate extension to the ALCR + satisfiability testing algorithm. ALCHR + is of interest because it provides useful additional expressive power and, although its satisfiability problem is Exptimecomplete, the algorithm is relatively simple and is amenable to optimisation. 1