Issues of decidability for description logics in the framework of resolution

We describe two methods on the basis of which efficient resolution decision procedures can be developed for a range of description logics. The first m ethod uses an ordering restriction and applies to the description logic ALB , which extends ALC with the top role, full role negation, role intersectio n, role disjunction, role converse, domain restriction, range restriction, and role hierarchies. The second method is based solely on a selection rest riction and applies to reducts of ALB without the top (r) over bar ole and role negation. The latter method can be viewed as a polynomial simulation o f familiar tableaux-based decision procedures. It can also be employed for automated model generation.