Issues of Decidability for Description Logics in the Framework of Resolution

Hustadt, U. and Schmidt, R. A. (1998)

In Caferra, R. and Salzer, G. (eds), First-order Theorem Proving - FTP'98, Technical Report E1852-GS-981, Technische Universität Wien, Vienna, Austria, 152-161. BiBTeX, PostScript

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


Renate A. Schmidt
Home | Publications | FM Group | School | Man Univ

Last modified: 27 Apr 2001
Copyright © 1996,7,8 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk