Expressive Description Logic with Instantiation Metamodelling

We investigate a higher-order extension of the description logic (DL) SROIQ that provides a fixedly interpreted role semantically coupled with instantiation. It is useful to express interesting meta-level constraints on the modelled ontology. We provide a model-theoretic characterization of the semantics, and we show the decidability by means of reduction.