Description Logics Go Second-Order -- Extending EL with Universally Quantified Concepts

TL;DR

This paper extends the description logic EL with universally quantified concepts, exploring semantics beyond first-order logic, and demonstrates decidability and reasoning capabilities for certain fragments.

Contribution

It introduces universally quantified concepts into EL with two semantics and shows that some extensions remain decidable and compatible with existing reasoning algorithms.

Findings

Entails coincide under schema and second-order semantics for a useful fragment.

Polynomial decidability is achieved for a smaller, still expressive fragment.

The extension can express complex role axioms without additional constructors.

Abstract

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.