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中广义形式的角色链公理、正自限制以及某些形式的（局部）角色值映射，而无需额外构造子。