The study of Description Logics have been historically mostly focused on features that can be translated to decidable fragments of first-order logic. In this paper, we leave this restriction behind and look for useful and decidable extensions outside first-order logic. We introduce universally quantified concepts, which take the form of variables that can be replaced with arbitrary concepts, and define two semantics of this extension. A schema semantics allows replacements of concept variables only by concepts from a particular language, giving us axiom schemata similar to modal logics. A second-order semantics allows replacement of concept variables with arbitrary subsets of the domain, which is similar to quantified predicates in second-order logic. To study the proposed semantics, we focus on the extension of the description logic $\mathcal{EL}$. We show that for a useful fragment of the extension, the conclusions entailed by the different semantics coincide, allowing us to use classical $\mathcal{EL}$ reasoning algorithms even for the second-order semantics. For a slightly smaller, but still useful, fragment, we were also able to show polynomial decidability of the extension. This fragment, in particular, can express a generalized form of role chain axioms, positive self restrictions, and some forms of (local) role-value-maps from KL-ONE, without requiring any additional constructors.

翻译：描述逻辑的研究在历史上主要集中于能够翻译为一阶逻辑可判定片段的特征。在本文中，我们摒弃了这一限制，转而探索一阶逻辑之外有用且可判定的扩展。我们引入全称量化概念，其形式为可被任意概念替换的变量，并为这一扩展定义了两种语义。模式语义允许概念变量仅由特定语言中的概念替换，从而产生类似于模态逻辑的公理模式。二阶语义允许概念变量由论域中的任意子集替换，这类似于二阶逻辑中的量化谓词。为研究所提出的语义，我们聚焦于描述逻辑$\mathcal{EL}$的扩展。我们证明，在该扩展的一个有用片段中，不同语义蕴含的结论是重合的，从而使得我们即使对于二阶语义也能使用经典的$\mathcal{EL}$推理算法。对于稍小但仍具有实用性的片段，我们还证明了该扩展的多项式可判定性。特别地，这一片段能表达KL-ONE中的广义角色链公理、正自限制以及某些形式的（局部）角色值映射，而无需额外添加任何构造子。