Description Logic with part restrictions: PSPACE-complete expressiveness

Abstract

In this paper syntactic objects-concept constructors, called part restrictions-are considered in Description Logics (DLs). Being able to convey statements about a part of a set of successors, part restrictions essentially enrich the expressive capabilities of DLs. An extension of DL ALCQR with part restrictions is examined, and its PSPACE completeness is proven, what shows that the new expressiveness brings no extra cost to the complexity of reasoning in ALCQR. The proof uses completion calculus based on tableaux technique.