In this paper we consider an expressive description logic, which we
believe has not been considered in the literature on description
logics or modal logics. We call the logic ALB which is short for
`attribute language with boolean algebras on concepts and
roles'. ALB extends ALC with the top role, full role
negation, role intersection, role disjunction, role converse, domain
restriction, and range restriction.
We describe two methods on the basis of which efficient resolution decision procedures can be developed for a range of description logics. The first method uses an ordering restriction and applies to ALB and its reducts. The second method is based solely on a selection restriction and applies to reducts of ALB without the top role and role negation. On ALC, the latter method can be viewed as a polynomial simulation of tableaux-based theorem proving. This result is a first contribution towards a better understanding of the relationship of tableaux-based and resolution-based reasoning for description logics, similar to our understanding of the relationship of various calculi for propositional logic [Urquhart95].