Extending ALC with the Power-Set Construct

We continue our exploration of the relationships between Description Logics and Set Theory, which started with the definition of the description logic ALCΩ. We develop a set-theoretic translation of the description logic ALCΩ in the set theory Ω, exploiting a technique originally proposed for translating normal modal and polymodal logics into Ω. We first define a set-theoretic translation of ALC based on Schild’s correspondence with polymodal logics. Then we propose a translation of the fragment LCΩ of ALCΩ without roles and individual names. In this—simple—case the power-set concept is mapped, as expected, to the set-theoretic power-set, making clearer the real nature of the power-set concept in ALCΩ. Finally, we encode the whole language of ALCΩ into its fragment without roles, showing that such a fragment is as expres- sive as ALCΩ. The encoding provides, as a by-product, a set-theoretic translation of ALCΩ into the theory Ω, which can be used as basis for extending other, more expressive, DLs with the power-set construct. The research that led to the present paper was partially supported by a grant of the group GNCS of INdAM.