# Adding the Power-Set to Description Logics

## TL;DR

This paper introduces ALC^Omega, an extension of Description Logics incorporating set-theoretic constructs like the power-set, enabling metamodeling and circularity, with complexity and translation analyses.

## Contribution

It defines ALC^Omega, integrating set-theoretic power-set into Description Logics, and analyzes its properties, translations, and expressive power.

## Key findings

- Polynomial encoding of ALC^Omega in ALCIO confirms finite model property.
- Complexity of concept satisfiability is ExpTime.
- Fragment LC^Omega is as expressive as ALC^Omega.

## Abstract

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 Omega, consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set. An extension of ALC, ALC^Omega, is then defined in which concepts are naturally interpreted as sets living in Omega-models. In ALC^Omega not only membership between concepts is allowed---even admitting circularity---but also the power-set construct is exploited to add metamodeling capabilities. We investigate translations of ALC^Omega into standard description logics as well as a set-theoretic translation. A polynomial encoding of ALC^Omega in ALCIO 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^Omega in the theory Omega, exploiting a technique originally proposed for translating normal modal and polymodal logics into Omega. Finally, we show that the fragment LC^Omega of ALC^Omega, which does not admit roles and individual names, is as expressive as ALC^Omega.