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].