Decidable and Undecidable Extensions of ALC with Composition-Based Role Inclusion Axioms
Michael Wessel · 2007
This paper continues our investigation on the extension of the standard description logic ALC with role axioms of the form S #T # R 1 # #R n . We consider the concept satisfiability problem of ALC w.r.t. a set of role axioms of the proposed form. A set of these role axioms is called a role box. The original motivation for this kind of role axioms comes from foreseen applications in the field of qualitative spatial reasoning with description logics. In this paper, we define the logics ALC RA # , ALCRA , and ALCRASG . Basically, both ALC RA # and ALCRA allow arbitrary role boxes containing axioms of the general form S # T # R 1 # # R n . In contrast to ALC RA # , ALCRA requires additionally that all roles have to be interpreted as disjoint. This requirement is also originally motivated by qualitative spatial reasoning applications with ALCRA . Recently it turned out that ALC RA # is undecidable. In fact, already ALU RA # with role boxes containing axioms of the form R#S # T is undecidable. A very similar result has also been obtained independently in a branch of normal multimodal logics, called grammar logics. Since role disjointness is a very severe restriction it is currently still unknown whether ALCRA might be decidable or not. In this paper we go back one step before ALCRA and discuss a common fragment of ALCRA and ALC RA # , called ALCRASG . Like in ALCRA , ALCRASG requires role disjointness, but the set of admissible role boxes is further pruned. It turned out that associativity of role boxes is an important requirement -- exploiting associativity we were able to show the decidability and EXPTIME-completeness of ALCRASG . Surprisingly, satisfiability of ALCRASG -concepts w.r.t. admissible role boxes can...