ALC_ALC: A context description logic

We develop a novel description logic (DL) for representing and reasoning with contextual knowledge. Our approach descends from McCarthy’s tradition of treating contexts as formal objects over which one can quantify and express first-order properties. As a foundation we consider several common product-like combinations of DLs with multimodal logics and adopt the prominent (Kn)ALC. We then extend it with a second sort of vocabulary for describing contexts, i.e., objects of the second dimension. In this way, we obtain a two-sorted, two-dimensional combination of a pair of DLs ALC, called ALCALC. As our main technical result, we show that the satisfiability problem in this logic, as well as in its proper fragment (Kn)ALC with global TBoxes and local roles, is 2ExpTime- complete. Hence, the surprising conclusion is that the significant increase in the expressiveness of ALCALC due to adding the vocabulary comes for no substantial price in terms of its worst-case complexity