Adding the power-set to description logics

We explore the relationships between Description Logics and Set Theory. The study is carried on using, on the set-theoretic side, a very rudimentary axiomatic set theory Ω, consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set. An extension of ALC, dubbed ALC^Ω, is defined in which concepts are naturally interpreted as sets living in Ω-models. In ALC^Ω not only membership between concepts is allowed—even admitting membership circularity—but also the power-set construct is exploited to add metamodelling capabilities. We investigate translations of ALC^Ω into standard description logics as well as a set-theoretic translation. A polynomial encoding of ALC^Ω in ALCOI proves the validity of the finite model property as well as an EXPTIME upper bound on the complexity of concept satisfiability. We develop a set-theoretic translation of ALC^Ω in the theory Ω, exploiting a technique proposed for translating normal modal and polymodal logics into Ω. Finally, we show that the fragment LC^Ω of ALC^Ω not admitting roles and individual names, is as expressive as ALC^Ω.