arxiv

Copyright for this paper by its authors. Use permitted under Creative Commons
License Attribution 4.0 International (CC BY 4.0).

dl  DL 2023: 36th International Workshop on Description Logics, September 2–4,
2023, Rhodes, Greece arxiv

<EMAIL_ADDRESS>]<EMAIL_ADDRESS>]

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

Joshua Hirschbrunn  University of Ulm, James-Franck-Ring, 89081 Ulm, Germany
Yevgeny Kazakov

(2023)

###### 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.

###### keywords:

EL Quantified Concepts Concept Variables Second-Order Logic Modal Logic
Ontology Design Patterns

##  1 Introduction and Motivation

After the famous undecidability result of the early knowledge representation
language used in the KL-ONE system [1], it has been commonly agreed that
Description Logics should be restricted to decidable fragments of First-Order
Logic (FOL), preferably of lower complexity. The subsequent search for
suitable languages has resulted in a large spectrum of DLs ranging from simple
tractable languages, such as $\mathcal{EL}$ [2] and DL-Lite [3] to very
expressive languages, such as $\mathcal{SROIQ}$ [4], used as the basis of the
Web ontology language OWL 2 [5]. After these extensive studies, finding new
interesting fragments of FOL, has become increasingly difficult. That is why,
in this paper, we look at some features from Second-Order Logic (SOL),
specifically at _universally quantified concepts_. Syntactically, we introduce
new _concept variables_ , which can be used in place of classical concepts.
For example, an axiom
$\exists{\textsf{owns}}.(X\sqcap\textsf{Pet})\sqsubseteq\exists{\textsf{feeds}}.X$
expresses that everyone who owns a pet from a set of objects $X$ must feed
someone from this set. Such concept variables $X$ are assumed to be implicitly
_universally quantified_ , that is, the above property should hold for _every
reasonable choice_ of a set $X$.

One possible way of defining semantics of our language extension, is to regard
axioms with concept variables as _axiom schemata_. Under this reading, the
reasonable choices of $X$ in the above axiom, are sets defined by _concepts_
of a specific form, for example, all (atomic) concepts from an ontology, or
all concepts that can be built in a particular DL, such as $\mathcal{EL}$.
After replacing each variable with every possible concept, one obtains a
(possibly infinite) set of ordinary DL axioms, for which the logical
entailment is defined in the standard way.

Axiom schemata is certainly not a new concept. In fact, most logic languages,
including Propositional Logic (PL), FOL, and Modal Logics were originally
defined _axiomatically_. For example, PL can be defined using 3 axiom
schemata: $X\to X$, $X\to(Y\to X)$, and $(X\to(Y\to Z))\to((X\to Y)\to(X\to
Z))$, in which every variable can be replaced with any propositional formula.
Many MLs were defined by extending PL with new axiom schemata, for example,
K4: $\Box X\to\Box\Box X$ (see, e.g., [6]). In the context of DLs, axiom
schemata occur in different contexts: Nominal Schemas [7, 8, 9] introduce
(nominal) variables that can be replaced with individual names. Ontology
Design Patterns [10, 11, 12, 13, 14, 15, 16], use concept variables to define
axiom templates, which can be used to generate ordinary axioms for specific
applications. Axiom schemata with existentially-quantified concepts can be
also used to define operations, such as interpolants or most-common subsumer
[17]. To obtain decidability results, most works restrict the set of values
that can be used for replacement of variables so that the resulting set of
(ordinary) axioms is _finite_. However, even for unrestricted axiom schemata,
such as those found in PLs and MLs, it can be often shown that it is
sufficient to replace variables with only finitely-many formulas found in (or
built using) the entailment to be proved. For MLs, this _sub-formula property_
usually follows from _cut-free sequent-style_ calculi (see, e.g., [18]).

The main advantage of the schema semantics for concept variables, is that any
DL reasoning procedure could, in principle, be used for checking entailment in
the corresponding DL extension, by systematically generating instances of
axiom schemata and checking entailment from the resulting increasing sets of
ordinary axioms. This immediately implies _semi-decidability_ of the schema
extension and, in the cases when a form of sub-formula property can be proved,
also _decidability_ and _complexity_ results. Schema semantics, however, also
has disadvantages, one of which, is that the entailments depend on the choices
of concepts used for variable replacements. Consider, for example, axiom
schema $\top\sqsubseteq\exists r.X$. If we only allow $\mathcal{EL}$ concepts
$C$ for variable replacements, the resulting set of axioms is satisfiable
since there is a model (with one element) that interprets every $\mathcal{EL}$
concept (including every $\exists r.C$) by the whole domain. If, however, we
additionally allow $X$ to be replaced by $\bot$, i.e., by taking concepts from
$\mathcal{EL}^{\bot}$, then, clearly, this schema becomes unsatisfiable. As a
consequence, the $\mathcal{EL}$ axiom schema obtains new $\mathcal{EL}$
logical conclusions (e.g., $A\sqsubseteq B$) when viewing it in a context of a
larger language (e.g., $\mathcal{EL}^{\bot}$). In the next section we give a
similar example when an $\mathcal{EL}$ schema obtains new $\mathcal{EL}$
consequences with $\mathcal{ALC}$ concept replacements, this time, without
making axioms inconsistent.111To see why this could be a concern, imagine that
the axiom schemata of PL would obtain new logical consequences in the language
of PL when allowing variables to be replaced by modal formulas!

Motivated by the above consideration, we define another, _language-
independent_ semantics of concept variables. Specifically, an axiom with
concept variables is satisfied by an interpretation if for _every_ assignment
of concept variables to _subsets_ of its domain, the axiom is satisfied in the
extension of this interpretation in which the variables are interpreted by
these subsets (as ordinary concept names). For example, axiom
$\top\sqsubseteq\exists r.X$ is _not_ satisfied in any interpretation
$\mathcal{I}$ since for the assignment of $X\mapsto\emptyset$, this axiom does
not hold if we extend $\mathcal{I}$ by $X^{\mathcal{I}}=\emptyset$. On the
other hand, axiom $X\sqsubseteq\exists r.X$ is satisfied in exactly those
interpretations $\mathcal{I}$ such that $r^{\mathcal{I}}$ is a reflexive
relation. Similarly, axiom
$\exists{\textsf{owns}}.(X\sqcap\textsf{Pet})\sqsubseteq\exists{\textsf{feeds}}.X$
is satisfied in exactly those interpretations $\mathcal{I}$ such that $\langle
x,y\rangle\in\textsf{owns}^{\mathcal{I}}$ and $y\in\textsf{Pet}^{\mathcal{I}}$
imply ${\langle x,y\rangle}\in\textsf{feeds}^{\mathcal{I}}$.222Note that this
property can be expressed in $\mathcal{SROIQ}$ using a fresh role pet:
$\textsf{Pet}\sqsubseteq\exists\textsf{pet}.\textsf{Self}$ and
$\textsf{pet}\circ\textsf{owns}\sqsubseteq\textsf{feeds}$ Essentially, under
this semantics, concept variables correspond to universally-quantified second-
order (unary) predicates. Hence, we refer to this semantics as _second-order
semantics_.

It is easy to see that the second-order semantics is _stronger_ than the
schema semantics. Indeed, if an axiom is satisfied in an interpretation under
the second-order semantics, then for every replacement of variables by
concepts, the resulting axioms are also (classically) satisfied in this
interpretation because variables can be assigned to interpretations of these
concepts in the second-order semantics. The converse is not true, as has been
shown on the example of axiom $\top\sqsubseteq\exists r.X$ for the
$\mathcal{EL}$-schema semantics. Furthermore, whereas schema entailment can be
always reduced to first-order entailment (from a possibly infinite set of
formulas), there are axioms whose models under second-order semantics cannot
be expressed by first-order formulas. For example, the well-known ML _McKinsey
axiom_ $\Box\Diamond X\rightarrow\Diamond\Box X$, which can be written in the
DL $\mathcal{ALC}$ as $\forall r.\exists r.X\sqsubseteq\exists r.\forall r.X$,
cannot be translated into even an infinite set of first-order formulas that
holds in exactly the same interpretations (of $r$) [19]. Hence, even semi-
decidability for the second-order extension of $\mathcal{ALC}$ seems to be an
open question.

To combine advantages of the two proposed semantics (semi-decidability and
schema language independence), it makes sense to look for restricted use of
concept variables in DLs for which the entailment under two semantics
_coincide_. In this paper, we describe a useful extension of the DL
$\mathcal{EL}$ with concept variables for which this is the case (Section 3),
and a further restriction, for which these (equivalent) entailments are
_polynomially decidable_ (Section 4). Even though the use of concept variables
in this fragment is restricted, it can express several other DL features, such
as role chain axioms, positive self restrictions, reflexive roles, some forms
of (local) role-value-maps from KL-ONE, and their generalizations (see Section
5).

The main idea for proving these results, is to show that the standard
$\mathcal{EL}$ canonical model [2] for axioms obtained by replacing concept
variables with certain _relevant_ $\mathcal{EL}$ concepts, is also a model of
the original axioms under the second-order semantics. This property holds
because for our restricted form of axioms, it is sufficient to replace concept
variables with only _singleton subsets_ of the domain to capture the second-
order semantics.333This means, in particular, that our restricted axioms can
be translated to FOL. Note that any fragment for which the second-order
entailment coincides with the schema entailment can be translated to FOL using
the standard FOL translation for the schema instances. For example, if
$X\sqsubseteq\exists r.X$ holds for all replacements of $X$ with singleton
subsets of the domain (that is, when $r$ is reflexive) then this axiom also
holds for replacements of $X$ with any larger set. To obtain the decidability
and complexity result, we define a further restriction for which it is
sufficient to use only polynomially-many relevant concepts for checking the
schema entailment.

dl Because of limited space, we omit most proofs in this paper. They can be
found in the accompanying technical report [hirshbrunn2023elx-tr].

##  2 Schema Semantics and Second-Order Semantics

We start by formally defining our extension of DLs with concept variables:

######  Definition 1 (Syntax).

The _syntax_ of DLs with concept variables consists of disjoint and countably
infinite sets $N_{C}$ of _concept names_ , $N_{R}$ of _role names_ , and
$N_{X}$ of _concept variables_. Given a base DL L that is a fragment of
$\mathcal{SROIQ}$, such as $\mathcal{EL}$ and $\mathcal{ALC}$, we define by
$\textsf{L}\mathcal{X}$ its corresponding _extension with concept variables_ ,
in which the elements from $N_{X}$ can be used as concepts. We define, an
_$\textsf{L}\mathcal{X}$ -ontology_ as a (possibly infinite) set $\mathcal{K}$
of $\textsf{L}\mathcal{X}$-axioms.

Let ex be either an $\textsf{L}\mathcal{X}$-concept, an
$\textsf{L}\mathcal{X}$-axiom, or an $\textsf{L}\mathcal{X}$-ontology. We
denote by $\textsf{sub}(\textit{ex})$ (all) subconcepts444 _Subconcepts_ are
defined to be substrings of the expression that are valid concepts. of ex. For
$\textsf{L}\mathcal{X}$-concepts and $\textsf{L}\mathcal{X}$-axioms, we split
$\textsf{sub}(\textit{ex})$ into $\textsf{sub}^{+}(\textit{ex})$ and
$\textsf{sub}^{-}(\textit{ex})$ the set of concepts that _occur positively_ ,
respectively _negatively_ in ex555A concept occurs positively (negatively) in
an axiom, if it occurs on the right side of the axiom under even (odd) number
of nested negations or on the left side under odd (even) number of nested
negations. (i.e.
$\textsf{sub}(\textit{ex})=\textsf{sub}^{+}(\textit{ex})\cup\textsf{sub}^{-}(\textit{ex})$).
We denote by $\textsf{vars}(\textit{ex})=\textsf{sub}(\textit{ex})\cap N_{X}$
the set of _concept variables occurring in ex_. We say that ex is _ground_ if
$\textsf{vars}(\textit{ex})=\emptyset$.

A _(concept variable) substitution_ is a mapping
$\theta=[X_{1}/C_{1},\dots,X_{n}/C_{n}]$ that assigns concepts $C_{i}$ to
concept variables $X_{i}$ ($1\leq i\leq n$). We say that $\theta$ is _ground_
if all $C_{i}$ are ground $(1\leq i\leq n)$. We denote by
$\theta(\textit{ex})$ the result of _applying the substitution_ to ex, defined
in the usual way.

From now on we assume that DL concepts, axioms, and ontologies may contain
concept variables. When this is not the case, we explicitly say that these
concepts, axioms, or ontologies are _ground_ or _classical_.

######  Example 1.

Consider the following two (non-ground) axioms:

$\displaystyle\alpha=\exists r.X\sqcap\exists s.X$
$\displaystyle\sqsubseteq\exists t.X,$ (1) $\displaystyle\beta=\exists
r.X\sqcap\exists s.Y$ $\displaystyle\sqsubseteq\exists t.(X\sqcup Y).$ (2)

Axiom $\alpha$ belongs to $\mathcal{ELX}$ whereas axiom $\beta$ belongs to
$\mathcal{ALCX}$ due to the use of concept disjunction $\sqcup$. Further,
$\textsf{sub}^{+}(\alpha)=\\{\exists t.X,X\\}$,
$\textsf{sub}^{-}(\beta)=\\{\exists r.X\sqcap\exists s.Y,\exists r.X,\exists
s.Y,X,Y\\}$, and $\textsf{vars}(\beta)=\\{X,Y\\}$. Finally, for a (non-ground)
substitution $\theta=[X/X\sqcup Y]$, we have:

$\displaystyle\theta(\alpha)=\exists r.(X\sqcup Y)\sqcup\exists s(X\sqcup
Y)\sqsubseteq\exists t.(X\sqcup Y).$ (3)

Intuitively, axioms $\alpha$ and $\beta$ can be thought as _axiom schemata_
representing all axioms obtained by replacing the concept variables $X$ and
$Y$ with ordinary (ground) concepts. However, the choice of such ground
concepts is not always obvious. Should variables be replaced by just atomic
concepts? Or only by concepts appearing in the given ontology? Or by any
concepts that can be constructed in a particular DL? Clearly, each of these
choices may result in different logical consequences and algorithmic
properties of the resulting schema languages. To handle all such choices, we
provide a general (parameterized) definition of schema semantics.

######  Definition 2 (Schema Semantics).

Let $\mathcal{K}$ be an $\textsf{L}\mathcal{X}$-ontology for some DL L, and
$H$ a (possibly infinite) set of L-concepts called a _concept base_. For an
$\textsf{L}\mathcal{X}$-axiom $\alpha$, and $\textsf{L}\mathcal{X}$-ontology
$\mathcal{K}$, define by $\alpha_{\downarrow H}=\\{\alpha[X_{1}/C_{1},\dots
X_{n}/C_{n}]\mid X_{i}\in\textsf{vars}(\alpha)\>\&\>C_{i}\in H\\}$ and
$\mathcal{K}_{\downarrow H}=\bigcup_{\alpha\in\mathcal{K}}\alpha_{\downarrow
H}$ the set of _$H$ -ground instances_ of $\alpha$ and $\mathcal{K}$,
respectively.

We write $\mathcal{K}\models^{\ast}_{H}\alpha$ if $\mathcal{K}_{\downarrow
H}\models\alpha_{\downarrow H}$ and say that $\alpha$ is a logical consequence
of $\mathcal{K}$ under the _schema semantics_ (for a concept base $H$).
Finally, we write $\alpha_{\downarrow\textsf{L}}$,
$\mathcal{K}_{\downarrow\textsf{L}}$ and
$\mathcal{K}\models^{\ast}_{\textsf{L}}\alpha$ instead of $\alpha_{\downarrow
H}$, $\mathcal{K}_{\downarrow H}$ and $\mathcal{K}\models^{\ast}_{H}\alpha$,
respectively, if $H$ is the set of _all_ L-concepts.

Clearly, if the concept base $H$ is _finite_ , entailment under the schema
semantics for $H$ can be reduced to the standard DL entailment.

######  Example 2 (Example 1 Continued).

Notice that $\\{\beta\\}\models^{\ast}_{H}\alpha$ for any concept base $H$.
Indeed, take any $\alpha^{\prime}=\theta(\alpha)=\exists r.C\sqcap\exists
s.C\sqsubseteq\exists t.C\in\alpha_{\downarrow H}$. Then $\beta_{\downarrow
H}\owns\beta[X/C,Y/C]=\exists r.C\sqcap\exists s.C\sqsubseteq\exists
t.(C\sqcup C)\models\alpha^{\prime}$. Also, notice that if $H$ is closed under
concept disjunctions (i.e., $C\in H$ and $D\in H$ imply $C\sqcup D\in H$) then
$\\{\alpha\\}\models^{\ast}_{H}\beta$. Indeed, take any
$\beta^{\prime}=\theta(\beta)=\exists r.C\sqcap\exists s.D\sqsubseteq\exists
t.(C\sqcup D)\in\beta_{\downarrow H}$ for $\theta=[X/C,Y/D]$. Since $H$ is
closed under disjunction, we have $\alpha_{\downarrow H}\owns\alpha[X/C\sqcup
D]=\exists r.(C\sqcup D)\sqcap\exists s.(C\sqcup D)\sqsubseteq\exists
t.(C\sqcup D)\models\beta^{\prime}$. Consequently,
$\\{\alpha\\}\models^{\ast}_{\mathcal{ALC}}\beta$. However, it can be shown
that $\\{\alpha\\}\not\models^{\ast}_{\mathcal{EL}}\beta$. To prove this,
consider the $\mathcal{EL}$ ontology:

$\mathcal{K}=\\{~{}A\sqsubseteq\exists r.B\sqcap\exists s.C,\quad\exists
t.B\sqsubseteq D,\quad\exists t.C\sqsubseteq D~{}\\}$ (4)

It is easy to see that
$\mathcal{K}\cup\beta_{\downarrow\mathcal{EL}}\supseteq\mathcal{K}\cup\\{\beta^{\prime}\\}\models
A\sqsubseteq D$ for $\beta^{\prime}=\beta[X/B,Y/C]=\exists r.B\sqcap\exists
s.C\sqsubseteq\exists t(B\sqcup C)$. Hence
$\mathcal{K}\cup\\{\beta\\}\models^{\ast}_{\mathcal{EL}}A\sqsubseteq D$. We
show that
$\mathcal{K}\cup\\{\alpha\\}\not\models^{\ast}_{\mathcal{EL}}A\sqsubseteq D$,
which, in particular, implies that
$\\{\alpha\\}\not\models^{\ast}_{\mathcal{EL}}\beta$, for otherwise
$\mathcal{K}\cup\\{\alpha\\}\models^{\ast}_{\mathcal{EL}}\mathcal{K}\cup\\{\beta\\}\models^{\ast}_{\mathcal{EL}}A\sqsubseteq
D$.

To prove that
$\mathcal{K}\cup\\{\alpha\\}\not\models^{\ast}_{\mathcal{EL}}A\sqsubseteq D$,
consider the interpretation
$\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ defined by:
$\Delta^{\mathcal{I}}=\\{a,b,c\\}$, $A^{\mathcal{I}}=\\{a\\}$,
$B^{\mathcal{I}}=\\{b\\}$, $C^{\mathcal{I}}=\\{c\\}$,
$r^{\mathcal{I}}=\\{\langle a,b\rangle\\}$, $s^{\mathcal{I}}=\\{\langle
a,c\rangle\\}$, $t^{\mathcal{I}}=\\{\langle a,a\rangle\\}$, and
$E^{\mathcal{I}}=h^{\mathcal{I}}=\emptyset$ for all remaining $E\in N_{C}$ and
$h\in N_{R}$. Clearly, $\mathcal{I}\models\mathcal{K}$ and
$\mathcal{I}\not\models A\sqsubseteq D$. It remains to prove that
$\mathcal{I}\models\alpha_{\downarrow\mathcal{EL}}$. Take any
$\alpha[X/F]=\exists r.F\sqcap\exists s.F\in\exists
t.F\in\alpha_{\downarrow\mathcal{EL}}$ and any $d\in(\exists r.F\sqcap\exists
s.F)^{\mathcal{I}}$. Then $d=a$ and $\\{b,c\\}\subseteq F^{\mathcal{I}}$ by
definition of $r^{\mathcal{I}}$ and $s^{\mathcal{I}}$. But then $F=\top$ since
$|\\!|F^{\mathcal{I}}|\\!|\leq 1$ for all other $\mathcal{EL}$ concepts $F$.
Then $d=a\in(\exists t.\top)^{\mathcal{I}}=(\exists t.F)^{\mathcal{I}}$ as
required.

Combining the above observations, we obtain:
$\mathcal{K}\cup\\{\alpha\\}\models^{\ast}_{\mathcal{ALC}}\mathcal{K}\cup\\{\beta\\}\models^{\ast}_{\mathcal{EL}}\mathcal{K}\cup\\{\beta\\}\models^{\ast}_{\mathcal{EL}}A\sqsubseteq
D$, however,
$\mathcal{K}\cup\\{\alpha\\}\not\models^{\ast}_{\mathcal{EL}}A\sqsubseteq D$.

Example 2 shows that, for schema semantics, an ontology formulated in one DL
may have different conclusions, even in the same DL, when the concept base is
extended to a larger language. This goes against the usual understanding of
logic, as this means that the consequences of an ontology are not determined
by the ontology alone. To mitigate this problem, we consider the second-order
semantics that is independent of a concept base.

######  Definition 3 (Second-Order Semantics).

Let $\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ be an
interpretation. A _valuation_ for $\mathcal{I}$ (also called a variable
assignment) is a mapping $\eta$ that assigns to every variable $X\in N_{X}$ a
subset $\eta(X)\subseteq\Delta^{\mathcal{I}}$. The _interpretation of
concepts_ $C^{\mathcal{I},\eta}$ and _satisfaction of axioms_
$\mathcal{I}\models^{2}_{\eta}\alpha$ _under $\mathcal{I}$ and $\eta$_ is
defined in the same way as for the standard DL semantics by treating concept
variables $X$ as ordinary concept names interpreted by $\eta(X)$. We write
$\mathcal{I}\models^{2}\alpha$ if $\mathcal{I}\models^{2}_{\eta}\alpha$ for
every _valuation_ $\eta$. Finally, for an ontology $\mathcal{K}$, we write
$\mathcal{I}\models^{2}\mathcal{K}$ if $\mathcal{I}\models^{2}\beta$ for every
$\beta\in\mathcal{K}$, and we write $\mathcal{K}\models^{2}\alpha$ if
$\mathcal{I}\models^{2}\mathcal{K}$ implies $\mathcal{I}\models^{2}\alpha$.

Alternatively to the model-theoretic definition (Definition 3) it is possible
to define the second-order semantics by a translation to SOL. This translation
is simply the normal translation to FOL, treating concept variables as second-
order unary predicates and then universally quantifying over these predicates.
For example, $C\sqsubseteq\exists r.X\sqcap Y$ translates to $\forall
X.\forall Y.[\forall x.(C(x)\rightarrow\exists y.(r(x,y)\land X(y))\land
Y(x))]$.

As discussed in Section 1, second order semantics is stronger than schema
semantics. Let us consider some examples for the DL $\mathcal{EL}$, which have
more second order entailments than schema semantics for which all
$\mathcal{EL}$ concepts are included in the concept base. These examples will
help us to determine the restrictions for the use of concept variables, under
which both semantics coincide.

First, we give a minor modification of the example with axiom
$\top\sqsubseteq\exists r.X$ discussed in Section 1, which does not result in
an inconsistent ontology under the second-order semantics.

######  Example 3.

Consider the ontology $\mathcal{K}=\\{A\sqsubseteq\exists r.X\\}$. It is easy
to see that $\mathcal{K}\models^{2}\exists r.A\sqsubseteq A$. Indeed, assume
that $\mathcal{I}\models^{2}\mathcal{K}$, and take any valuation $\eta$ such
that $\eta(X)=\emptyset$. Then
$A^{\mathcal{I}}=A^{\mathcal{I},\eta}\subseteq(\exists
r.X)^{\mathcal{I},\eta}=\emptyset$. Hence $(\exists
r.A)^{\mathcal{I}}=\emptyset\subseteq A^{\mathcal{I}}$. At the same time
$\mathcal{K}\not\models^{\ast}_{\mathcal{EL}}\exists r.A\sqsubseteq A$.
Indeed, consider the interpretation
$\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ with
$\Delta^{\mathcal{I}}=\\{a,b\\}$, $A^{\mathcal{I}}=\\{a\\}$,
$B^{\mathcal{I}}=\\{a,b\\}$ for every $B\in N_{C}\setminus\\{A\\}$, and
$r^{\mathcal{I}}=\\{\langle a,a\rangle,\langle b,a\rangle\\}$ for every $r\in
N_{R}$. By structural induction, it is easy to show that $a\in
C^{\mathcal{I}}$ for every $\mathcal{EL}$ concept $C$, hence
$\mathcal{I}\models A\sqsubseteq\exists r.C$. Therefore,
$\mathcal{I}\models^{\ast}_{\mathcal{EL}}\mathcal{K}$. However, since
$(\exists r.A)^{\mathcal{I}}=\\{a,b\\}\not\subseteq\\{a\\}=A^{\mathcal{I}}$,
we obtain $\mathcal{K}\not\models^{\ast}_{\mathcal{EL}}\exists r.A\sqsubseteq
A$.

Example 3 can be generalized to many other $\mathcal{ELX}$ axioms
$C\sqsubseteq D$ for which there exists a concept variable $X$ appearing in
$D$ but not in $C$. In this case, $\mathcal{I}\models^{2}C\sqsubseteq D$
implies that $C^{\mathcal{I},\eta}=\emptyset$ for every valuation $\eta$
because for the extension $\eta^{\prime}$ of $\eta$ with
$\eta^{\prime}(X)=\emptyset$, we obtain
$C^{\mathcal{I},\eta}=C^{\mathcal{I},\eta^{\prime}}\subseteq
D^{\mathcal{I},\eta^{\prime}}=\emptyset$.

arxiv

######  Lemma 1.

Let $\mathcal{I}$ be an interpretation, $D$ a $\mathcal{ELX}$ concept
containing a concept variable $X$ and $\eta$ a valuation such that
$\eta(X)=\emptyset$. Then $D^{\mathcal{I},\eta}=\emptyset$.

###### Proof.

The proof is by structural induction over $D$. Note that the cases $D=\top$,
$D=A\in N_{C}$, and $D=Y\in N_{X}\setminus\\{X\\}$ are not possible since $D$
must contain $X$.

  * •

If $D=X$ then $D^{\mathcal{I},\eta}=\eta(X)=\emptyset$.

  * •

If $D=\exists r.E$ then $E$ contains $X$. By induction hypothesis,
$E^{\mathcal{I},\eta}=\emptyset$. Hence $D^{\mathcal{I},\eta}=\emptyset$.

  * •

If $D=E_{1}\sqcap E_{2}$ then $E_{1}$ or $E_{2}$ contain $X$. By induction
hypothesis, $E_{1}^{\mathcal{I},\eta}=\emptyset$ or
$E_{2}^{\mathcal{I},\eta}=\emptyset$. Hence
$D^{\mathcal{I},\eta}=E_{1}^{\mathcal{I},\eta}\cap
E_{2}^{\mathcal{I},\eta}=\emptyset$. ∎

Now, take any $\mathcal{I}\models^{2}C\sqsubseteq D$. Then
$C^{\mathcal{I},\eta}=\emptyset$ for every valuation $\eta$. Then
$\theta(C)^{\mathcal{I}}=\emptyset$ for every concept variable substitution
$\theta$. Then for every $\mathcal{EL}$ concept $E$ such that
$\theta(C)\in\textsf{sub}(E)$ we have $E^{\mathcal{I}}=\emptyset$ as well.
Thus $\\{C\sqsubseteq D\\}\models^{2}E\sqsubseteq F$ for every $F$. If the
schema semantics preserves all these entailments then, in particular, all such
concepts $E$ (containing instances of $C$) must be equivalent. This can happen
only in some trivial cases, e.g., when the $\mathcal{K}$ contains axiom of the
form $X\sqsubseteq Y$, which implies that all concepts are equivalent. To
ensure that the semantics coincide in non-trivial cases, it is, therefore,
make sense to require that all variables that are present on the right side of
a concept inclusion axioms are also present on the left side. Axioms that
fulfill this requirement we called _range restricted_ axioms.

Example 2 presents another situation when schema semantics gives fewer
consequences than the second-order semantics. As has been shown in this
example, for an $\mathcal{ELX}$ axiom $\alpha$ (1) and an $\mathcal{EL}$
ontology $\mathcal{K}$ from (4), we have
$\mathcal{K}\cup\\{\alpha\\}\not\models^{\ast}_{\mathcal{EL}}A\sqsubseteq D$,
however, since $\\{\alpha\\}\models^{\ast}_{\mathcal{ALC}}\beta$ (2) and
$\mathcal{K}\cup\\{\beta\\}\models^{\ast}_{\mathcal{EL}}A\sqsubseteq D$, we
have $\mathcal{K}\cup\\{\alpha\\}\models^{2}A\sqsubseteq D$.

The problem with $\alpha$ in this example is that the variable $X$ occurs
twice on the left side of the axiom, which makes this axiom equivalent to
$\beta$ under the second-order semantics, and, consequently, being able to
express an axiom with a concept disjunction $\exists r.C\sqcap\exists
s.D\sqsubseteq\exists t.(C\sqcup D)$, which otherwise could not be expressed
by ordinary $\mathcal{EL}$ axioms, i.e., under the schema semantics. To
prevent such a case for our fragment of $\mathcal{ELX}$, it therefore, makes
sense to prohibit the occurrence of the same variable twice on the left side
of an axiom. Concepts in which each variable occurs at most once, we call
_linear_.

To motivate our last restriction, consider the next example.

######  Example 4.

Consider the $\mathcal{ELX}$ ontology $\mathcal{K}=\\{\exists
r.X\sqsubseteq\exists s.(X\sqcap A)\\}$. It is easy to see that
$\mathcal{K}\models^{2}\exists r.\top\sqsubseteq\exists r.A$. Indeed, take any
$\mathcal{I}\models^{2}\mathcal{K}$ and $d\in(\exists r.\top)^{\mathcal{I}}$.
Then there exists $d^{\prime}\in\Delta^{\mathcal{I}}$ such that $\langle
d,d^{\prime}\rangle\in r^{\mathcal{I}}$. Take any valuation $\eta$ with
$\eta(X)=\\{d^{\prime}\\}$. Since $\langle d,d^{\prime}\rangle\in
r^{\mathcal{I}}$, we have $d\in(\exists r.X)^{\mathcal{I},\eta}$. Since
$\mathcal{I}\models^{2}_{\eta}\mathcal{K}$, we have $d\in(\exists s.(X\sqcap
A))^{\mathcal{I},\eta}$. In particular, $\emptyset\neq(X\sqcap
A)^{\mathcal{I},\eta}=\\{d^{\prime}\\}\cap A^{\mathcal{I}}$. Hence
$d^{\prime}\in A^{\mathcal{I}}$. Consequently, $d\in(\exists
r.A)^{\mathcal{I}}$.

On the other hand, $\mathcal{K}\not\models^{\ast}_{\mathcal{EL}}\exists
r.\top\sqsubseteq\exists r.A$, as evidenced by the counter-model
$\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ with
$\Delta^{\mathcal{I}}=\\{a,b\\}$, $A^{\mathcal{I}}=\\{a\\}$,
$r^{\mathcal{I}}=\\{\langle a,b\rangle\\}$, $s^{\mathcal{I}}=\\{\langle
a,a\rangle\\}$, and $E^{\mathcal{I}}=\emptyset$, $h^{\mathcal{I}}=\emptyset$
for any remaining $E\in N_{C}$ and $h\in N_{R}$. To show that
$\mathcal{I}\models^{\ast}_{\mathcal{EL}}\mathcal{K}$, we prove that
$\mathcal{I}\models\exists r.C\sqsubseteq\exists s.(C\sqsubseteq A)$ for every
$\mathcal{EL}$ concept $C$. For this, take any $d\in(\exists
r.C)^{\mathcal{I}}$. By definition of $r^{\mathcal{I}}$, $d=a$ and $b\in
C^{\mathcal{I}}$. Then $C$ can be only a conjunction of concept $\top$. Hence
$a\in C$. Hence $d=a\in(\exists s.C)^{\mathcal{I}}$. Thus
$\mathcal{I}\models\mathcal{K}$. Since, $a\in(\exists r.\top)^{\mathcal{I}}$
but $(\exists r.A)^{\mathcal{I}}=\emptyset$, we proved that
$\mathcal{K}\not\models^{\ast}_{\mathcal{EL}}\exists r.\top\sqsubseteq\exists
r.A$.

Note that under the second order semantics, the axiom $\exists
r.X\sqsubseteq\exists s.(X\sqcap A)$ in $\mathcal{K}$ from Example 4 implies
two properties: (1) that $r$ is a _subrole_ of $s$ ($r\sqsubseteq s$), which
is equivalent to axiom $\exists r.X\sqsubseteq\exists s.X$, and (2) that $A$
is a _range_ of the role $r$ ($ran(r)\sqsubseteq A$), which is due to the fact
that for any element $d^{\prime}$ such that $\langle d,d^{\prime}\rangle\in
r^{\mathcal{I}}$ this axiom holds for $X=\\{d^{\prime}\\}$. As was shown in
the example, the schema semantics cannot capture the second kind of
properties. In fact, an extension of $\mathcal{EL}$ with both (complex) role
inclusions and range restrictions becomes undecidable [20]), which could
explain why the schema semantics cannot characterize consequences in this
extension. To prevent situations like in Example 4, we require that variables
in the right side of axioms appear only directly under existential
restrictions. We generalize a related notion of _safe nominals_ [21] to define
this restriction:

######  Definition 4 (Safe Concept).

A $\mathcal{ELX}$ concept $C$ is called _safe_ (for concept variables), if
variables only occur in the form of $\exists r.X$, i.e. safe concepts are
defined by the grammar:

$C_{s}^{(i)}=A\mid\top\mid\exists r.X\mid\exists r.C_{s}\mid C^{1}_{s}\sqcap
C^{2}_{s}$

##  3 When Semantics Coincide

In this section we prove that the restrictions on the use of concept variables
discussed in Section 2 are sufficient to guarantee that the logical
consequences under the schema semantics and second-order semantics coincide.
Towards this goal, we define a fragment $\mathcal{ELX}_{F1}$ of
$\mathcal{ELX}$ that satisfies these restrictions:

######  Definition 5 ($\mathcal{ELX}_{F1}$).

A $\mathcal{ELX}$ axiom $\beta=C\sqsubseteq D$ is in the fragment
$\mathcal{ELX}_{F1}$, if

  * •

$\beta$ is range restricted, i.e. $\textsf{vars}(D)\subseteq\textsf{vars}(C)$,

  * •

$C$ is linear, i.e. $C$ it does not contain a variable twice, and

  * •

$D$ is safe (cf. Definition 4).

An interesting consequence of the first two restrictions in Definition 5, is
the so-called _singleton property_ for valuations. Intuitively, for checking
entailment over the second-order semantics, it is sufficient to consider only
valuations that assign concept variables to singleton subsets of the domain.

######  Definition 6 (Singleton Valuation).

A valuation $\eta$ is a _singleton valuation_ if $\forall
X:|\\!|\eta(X)|\\!|=1$.

######  Lemma 2.

Let $\mathcal{I}$ be an interpretation, $C$ a linear $\mathcal{ELX}$ concept,
$\eta$ a valuation, and $a\in C^{\mathcal{I},\eta}$. Then there is a singleton
valuation $\eta^{\prime}$ such that $\eta^{\prime}(X)\subseteq\eta(X)$ for
every $X\in\textsf{vars}(C)$ and $a\in C^{\mathcal{I},\eta^{\prime}}$.

arxiv

###### Proof.

Proof by induction over the structure of $C$:

  * •

If $\textsf{vars}(C)=\emptyset$ then every singleton valuation $\eta^{\prime}$
works since $a\in C^{\mathcal{I},\eta^{\prime}}=C^{\mathcal{I},\eta}$.

  * •

If $C=X$ then $a\in X^{\mathcal{I},\eta}=\eta(X)$ let
$\eta^{\prime}(X)=\\{a\\}$ then $|\\!|\eta^{\prime}(X)|\\!|=1$,
$\eta^{\prime}(X)\subseteq\eta(X)$ and
$a\in\eta^{\prime}(X)=X^{\mathcal{I},\eta^{\prime}}$.

  * •

If $C=\exists r.E$ then $a\in(\exists r.E)^{\mathcal{I},\eta}$ and there
exists $b\in\Delta^{\mathcal{I}}$ such that $\langle a,b\rangle\in
r^{\mathcal{I}}$ and $b\in E^{\mathcal{I},\eta}$. By induction hypothesis,
there exists a singleton $\eta^{\prime}$ such that
$\eta^{\prime}(X)\subseteq\eta(X)$ for every $X\in\textsf{vars}(E)$ such that
$b\in E^{\mathcal{I},\eta^{\prime}}$. Then $\textsf{vars}(C)=\textsf{vars}(E)$
and $a\in(\exists r.E)^{\mathcal{I},\eta^{\prime}}$.

  * •

If $C=E_{1}\sqcap E_{2}$ then $a\in(E_{1}\sqcap
E_{2})^{\mathcal{I},\eta}=E_{1}^{\mathcal{I},\eta}\cap
E_{2}^{\mathcal{I},\eta}$. By induction hypothesis for $a\in
E_{1}^{\mathcal{I},\eta}$, there exists a singleton $\eta_{1}^{\prime}$ such
that $\eta_{1}^{\prime}(X)\subseteq\eta(X)$ for $X\in\textsf{vars}(E_{1})$ and
$a\in E_{1}^{\mathcal{I},\eta_{1}^{\prime}}$. Likewise, for $a\in
E_{2}^{\mathcal{I},\eta}$, there exists a singleton $\eta_{2}^{\prime}$ such
that $\eta_{2}^{\prime}(X)\subseteq\eta(X)$ for $X\in\textsf{vars}(E_{2})$ and
$a\in E_{2}^{\mathcal{I},\eta_{2}^{\prime}}$. Define
$\eta^{\prime}(X):=\eta_{1}^{\prime}(X)$ for $X\in\textsf{vars}(E_{1})$ and
$\eta^{\prime}(X):=\eta_{2}^{\prime}(X)$ for $X\notin\textsf{vars}(E_{1})$.
Obviously, $\eta^{\prime}$ is singleton, $\eta^{\prime}(X)\subseteq\eta(X)$
for $X\in\textsf{vars}(C)=\textsf{vars}(E_{1})\cup\textsf{vars}(E_{2})$, and
$E_{1}^{\mathcal{I},\eta^{\prime}}=E_{1}^{\mathcal{I},\eta_{1}^{\prime}}$.
Since $C$ is linear, $\textsf{vars}(E_{1})\cap\textsf{vars}(E_{2})=\emptyset$,
hence $\eta^{\prime}(X)=\eta_{2}^{\prime}(X)$ for $X\in\textsf{vars}(E_{2})$.
Hence
$E_{2}^{\mathcal{I},\eta^{\prime}}=E_{2}^{\mathcal{I},\eta_{2}^{\prime}}$.
Finally, since $a\in
E_{1}^{\mathcal{I},\eta_{1}^{\prime}}=E_{1}^{\mathcal{I},\eta^{\prime}}$ and
$a\in
E_{2}^{\mathcal{I},\eta_{2}^{\prime}}=E_{2}^{\mathcal{I},\eta^{\prime}}$, we
obtain $a\in C^{\mathcal{I},\eta^{\prime}}$ as required. ∎

######  Lemma 3.

Let $\mathcal{I}$ be an interpretation, $D$ an $\mathcal{ELX}$ concept, and
$\eta^{\prime}$, $\eta$ valuations such that
$\eta^{\prime}(X)\subseteq\eta(X)$ for every $X\in\textsf{vars}(D)$. Then
$D^{\mathcal{I},\eta^{\prime}}\subseteq D^{\mathcal{I},\eta}$.

arxiv

###### Proof.

Proof by induction over the structure of $D$:

  * •

If $\textsf{vars}(D)=\emptyset$, then, trivially,
$D^{\mathcal{I},\eta^{\prime}}=D^{\mathcal{I},\eta}$.

  * •

If $D=X$ then
$X^{\mathcal{I},\eta^{\prime}}=\eta^{\prime}(X)\subseteq\eta(X)=X^{\mathcal{I},\eta}$.

  * •

If $D=\exists r.E$ then $E^{\mathcal{I},\eta^{\prime}}\subseteq
E^{\mathcal{I},\eta}$ by the induction hypothesis. Then for any $a\in(\exists
r.E)^{\mathcal{I},\eta^{\prime}}$ there exists $b\in
E^{\mathcal{I},\eta^{\prime}}\subseteq E^{\mathcal{I},\eta}$ such that
$\langle a,b\rangle\in r^{\mathcal{I}}$. Hence $a\in(\exists
r.E)^{\mathcal{I},\eta}$.

  * •

If $C=E_{1}\sqcap E_{2}$ then $E_{1}^{\mathcal{I},\eta^{\prime}}\subseteq
E_{1}^{\mathcal{I},\eta}$ and $E_{2}^{\mathcal{I},\eta^{\prime}}\subseteq
E_{2}^{\mathcal{I},\eta}$ by the induction hypothesis. Hence $(E_{1}\sqcap
E_{2})^{\mathcal{I},\eta^{\prime}}=E_{1}^{\mathcal{I},\eta^{\prime}}\cap
E_{2}^{\mathcal{I},\eta^{\prime}}\subseteq E_{1}^{\mathcal{I},\eta}\cap
E_{2}^{\mathcal{I},\eta}=(E_{1}\sqcap E_{2})^{\mathcal{I},\eta}$. ∎

By combining the above two lemmata, we obtain the required singleton property:

######  Theorem 1 (Singleton Property).

Let $\mathcal{I}$ be an interpretation, $\beta=C\sqsubseteq D$ a range
restricted $\mathcal{ELX}$ axiom such that $C$ is linear, and
$\mathcal{I}\models^{2}_{\eta^{\prime}}\beta$ for every singleton valuation
$\eta^{\prime}$. Then $\mathcal{I}\models^{2}\beta$.

arxiv

###### Proof.

Take any valuation $\eta$. We need to prove that
$\mathcal{I}\models^{2}_{\eta}\beta$, i.e., $C^{\mathcal{I},\eta}\subseteq
D^{\mathcal{I},\eta}$. Take any $a\in C^{\mathcal{I},\eta}$. Then, by Lemma 1,
there is a singleton $\eta^{\prime}$ with $\eta^{\prime}(X)\subseteq\eta(X)$
for every $X\in\textsf{vars}(C)$ such that $a\in
C^{\mathcal{I},\eta^{\prime}}$. Then
$\mathcal{I}\models^{2}_{\eta^{\prime}}\beta$ by the condition of the theorem,
so $a\in C^{\mathcal{I},\eta^{\prime}}\subseteq
D^{\mathcal{I},\eta^{\prime}}$. Since $\beta$ is range restricted, we have
$\eta^{\prime}(X)\subseteq\eta(X)$ for every
$X\in\textsf{vars}(D)\subseteq\textsf{vars}(C)$. Then $a\in
D^{\mathcal{I},\eta^{\prime}}\subseteq D^{\mathcal{I},\eta}$ by Lemma 3. Since
$a$ was chosen arbitrarily, this proves that
$\mathcal{I}\models^{2}_{\eta}\beta$. ∎

Our next goal is to prove that if $\mathcal{K}\models^{2}\alpha$ for some
$\mathcal{ELX}_{F1}$ ontology $\mathcal{K}$ and a (ground) $\mathcal{EL}$
axiom $\alpha$, then $\mathcal{K}\models^{\ast}_{H}\alpha$ for some concept
base $H$ consisting of (ground) $\mathcal{EL}$ concepts, i.e.,
$\mathcal{K}_{\downarrow H}\models\alpha$ (cf. Definition 2). Since
$\mathcal{K}_{\downarrow H}$ is an ordinary $\mathcal{EL}$ ontology, we can
use the well known characterization of $\mathcal{EL}$ entailment using so-
called $\mathcal{EL}$ _canonical models_ (also called _completion graphs_
[2]). Usually canonical models are defined using consequences of the ontology
derived by certain inference rules (see, e.g., [22]), however the following
simplified definition is sufficient for our purpose. To avoid confusion with
$\mathcal{ELX}$ ontologies, we denote $\mathcal{EL}$ ontologies by
$\mathcal{G}$.

######  Definition 7 (Canonical Interpretation).

Let $H$ be a nonempty _concept base_ and $\mathcal{G}$ an $\mathcal{EL}$
ontology. The _canonical interpretation_ (w.r.t. $\mathcal{G}$ and $H$) is an
interpretation
$\mathcal{I}=\mathcal{I}(\mathcal{G},H)=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$
defined by: $\Delta^{\mathcal{I}}=\\{x_{C}\mid C\in H\\}$,
$A^{\mathcal{I}}=\\{x_{C}\mid\mathcal{G}\models C\sqsubseteq A\\}$ for $A\in
N_{C}$, and $r^{\mathcal{I}}=\\{\langle
x_{C},x_{D}\rangle\in\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}\mid\mathcal{G}\models
C\sqsubseteq\exists r.D\\}$ for $r\in N_{R}$.

If we include all $\mathcal{EL}$ concepts into the concept base $H$, it can be
shown that the canonical interpretation $\mathcal{I}$ is a model of
$\mathcal{G}$ that satisfies exactly $\mathcal{EL}$ axioms entailed by
$\mathcal{G}$: $\mathcal{I}\models\alpha$ iff $\mathcal{G}\models\alpha$.
However, to ensure the latter property for a _fixed_ $\alpha$, it is
sufficient to use a smaller concept base $H$ that contains only certain sub-
concepts of $\mathcal{G}$ and $\alpha$. It turns out that if $H$ satisfies
certain conditions for $\mathcal{G}=\mathcal{K}_{\downarrow H}$ and $\alpha$
then $\mathcal{K}\models^{2}\alpha$ implies $\mathcal{I}\models\alpha$, which
implies $\mathcal{G}\models\alpha$. To prove that $\mathcal{I}\models\alpha$,
we show that $\mathcal{I}\models^{2}\mathcal{K}$, for which we use the
singleton valuation property from Theorem 1. There is a nice connection
between singleton valuations in $\mathcal{I}$ and substitutions of concept
variables with concepts from $H$, which we are going to exploit.

######  Definition 8 (Canonical Substitution).

We say that a concept variable substitution $\theta$ is _canonical_ for a
concept base $H$, if $\theta(X)\in H$ for every $X\in N_{X}$. Given a
canonical interpretation $\mathcal{I}$ (for $\mathcal{G}$ and $H$) and a
singleton valuation $\eta$ for $\mathcal{I}$, the _canonical substitution
determined_ by $\eta$ is the substitution $\theta=\theta_{\eta}$ defined by
$\theta(X)=C$ iff $\eta(X)=\\{x_{C}\\}\subseteq\Delta^{\mathcal{I}}$.

The connection to canonical substitutions in Definition 8 helps us to
characterize interpretations of (complex) $\mathcal{ELX}$ concepts under
canonical models and singleton valuations.

######  Lemma 4.

Let $\mathcal{I}$ be the canonical interpretation w.r.t. some $\mathcal{EL}$
ontology $\mathcal{G}$ and a concept base $H$, $F$ an $\mathcal{ELX}$ concept,
$\eta$ a singleton valuation, and $\theta=\theta_{\eta}$ the corresponding
canonical substitution. Then:

$F^{\mathcal{I},\eta}\subseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F)\\}.$ (5)

In addition, if $F$ is a safe concpet (see Definition 4) and $\theta(D)\in H$
for every $\exists r.D\in\textsf{sub}(F)$ then

$F^{\mathcal{I},\eta}\supseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F)\\}.$ (6)

arxiv

###### Proof.

Proof by induction over the definition of (safe) $\mathcal{EL}$ concept $F$:

  * •

$F=\top$. Then $\theta(F)=\top$ and
$\top^{\mathcal{I},\eta}=\top^{\mathcal{I}}=\Delta^{\mathcal{I}}=\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\top\\}$.

  * •

$F=A\in N_{C}$. Then $\theta(F)=A$ and
$A^{\mathcal{I},\eta}=A^{\mathcal{I}}=\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq A\\}$ by definition of $A^{\mathcal{I}}$.

  * •

$F=X\in N_{X}$ and $\eta(X)=\\{x_{C}\\}$. Then $\theta(F)=C$ and
$F^{\mathcal{I},\eta}=\eta(X)=\\{x_{C}\\}\subseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq C\\}$. Since $F=X$ is not safe, the converse direction does not
apply.

  * •

$F=\exists r.X$ and $\eta(X)=\\{x_{C}\\}$. Then $\theta(F)=\exists r.C$ and
$F^{\mathcal{I},\eta}=\\{x_{D}\mid\langle x_{D},x_{C}\rangle\in
r^{\mathcal{I}}\\}=\\{x_{D}\mid\mathcal{G}\models D\sqsubseteq\exists r.C\\}$
by definition of $r^{\mathcal{I}}$.

  * •

$F=\exists s.G$. Then $\theta(F)=\exists s.\theta(G)$ and
$F^{\mathcal{I},\eta}=\\{x_{D}\mid\langle x_{D},x_{C}\rangle\in
s^{\mathcal{I}}\>\&\>x_{C}\in
G^{\mathcal{I},\eta}\\}\subseteq\\{x_{D}\mid\mathcal{G}\models
D\sqsubseteq\exists s.C\>\&\>\mathcal{G}\models
C\sqsubseteq\theta(G)\\}\subseteq\\{x_{D}\mid\mathcal{G}\models
D\sqsubseteq\exists s.\theta(G)\\}$ by definition of $s^{\mathcal{I}}$,
induction hypothesis for $G$, and basic entailment properties.

If $F$ is safe and $\theta(D)\in H$ for every $\exists
r.D\in\textsf{sub}(\theta(F))$ then either $G=X$ (the previous case) or $G$ is
safe, in which case, by induction hypothesis,
$G^{\mathcal{I},\eta}\supseteq\\{x_{C}\mid\mathcal{G}\models
C\sqsubseteq\theta(G)\\}$. Since $\theta(G)\in H$ and
$\mathcal{G}\models\theta(G)\sqsubseteq\theta(G)$, this implies that
$x_{\theta(G)}\in G^{\mathcal{I},\eta}$. Then
$F^{\mathcal{I},\eta}=\\{x_{D}\mid\langle x_{D},x_{C}\rangle\in
s^{\mathcal{I}}\>\&\>x_{C}\in
G^{\mathcal{I},\eta}\\}\supseteq\\{x_{D}\mid\langle
x_{D},x_{\theta(G)}\rangle\in
s^{\mathcal{I}}\\}=\\{x_{D}\mid\mathcal{G}\models D\sqsubseteq\exists
s.\theta(G)\\}=\\{x_{D}\mid\mathcal{G}\models D\sqsubseteq\theta(F)\\}$.

  * •

$F=F_{1}\sqcap F_{2}$. Then $\theta(F)=\theta(F_{1})\sqcap\theta(F_{2})$ and
$F^{\mathcal{I},\eta}=F_{1}^{\mathcal{I},\eta}\cap
F_{2}^{\mathcal{I},\eta}\subseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F_{1})\\}\cap\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F_{2})\\}=\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F_{1})\sqcap\theta(F_{2})\\}$ by induction hypothesis and
basic entailment properties.

If $F$ is safe and $\theta(D)\in H$ for every $\exists
r.D\in\textsf{sub}(\theta(F))$ then so are $F_{1}$ and $F_{2}$, thus
$F^{\mathcal{I},\eta}=F_{1}^{\mathcal{I},\eta}\cap
F_{2}^{\mathcal{I},\eta}\supseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F_{1})\\}\cap\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F_{2})\\}=\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F_{1})\sqcap\theta(F_{2})\\}$ by induction hypothesis. ∎

The restriction to safe concepts in Lemma 4 is necessary, as the following
example shows:

######  Example 5.

Consider $H=\\{A,B\\}\subseteq N_{C}$ and $\mathcal{G}=\\{A\sqsubseteq B\\}$.
Then the canonical interpretation $\mathcal{I}$ for $\mathcal{G}$ and $H$ has
domain $\Delta^{\mathcal{I}}=\\{x_{A},x_{B}\\}$ and assigns
$A^{\mathcal{I}}=\\{x_{A},x_{B}\\}$, $B^{\mathcal{I}}=\\{x_{B}\\}$. Now take
$F=X\in N_{X}$ and define a singleton $\eta(X)=\\{x_{B}\\}$. Then the
corresponding canonical substitution $\theta(X)=B$. As can be seen,
$F^{\mathcal{I},\eta}=\eta(X)=\\{x_{B}\\}\subsetneq\\{x_{A},x_{B}\\}=\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq B\\}$.

We are now ready to harvest the fruits of our characterization of canonical
interpretations. We first show that, the canonical interpretation cannot
entail more axioms than the ontology $\mathcal{G}$ for which it is constructed
if the concept base $H$ contains relevant concepts from these axioms.

######  Corollary 1.

Let $\mathcal{I}$ be the canonical interpretation w.r.t. $\mathcal{G}$ and
$H$, and $\alpha=F\sqsubseteq G$ an $\mathcal{EL}$ axiom such that $F\in H$
and $D\in H$ for every $\exists r.D\in\textsf{sub}(F)$. Then
$\mathcal{I}\models\alpha$ implies $\mathcal{G}\models\alpha$.

###### Proof.

By Lemma 4,
$G^{\mathcal{I}}\subseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq G\\}$ and
$F^{\mathcal{I}}\supseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq F\\}$ Since $\mathcal{G}\models F\sqsubseteq F$ and $F\in H$, we
have $x_{F}\in F^{\mathcal{I}}$. Since $\mathcal{I}\models F\sqsubseteq G$, we
have $x_{F}\in
G^{\mathcal{I}}\subseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq G\\}$. Hence $\mathcal{G}\models F\sqsubseteq G$. ∎

Next, we determine what to put into $H$ and $\mathcal{G}$ so that the
canonical interpretation $\mathcal{I}=\mathcal{I}(G,H)$ satisfies a given
$\mathcal{ELX}$ axiom $\beta$ (to eventually ensure that
$\mathcal{I}\models\mathcal{K}$).

######  Corollary 2.

Let $\mathcal{I}$ be the canonical interpretation w.r.t. $\mathcal{G}$ and
$H$, and $\beta=F\sqsubseteq G$ an $\mathcal{ELX}_{F1}$ axiom such that 1)
$\beta_{\downarrow H}\in\mathcal{G}$ and 2) $D_{\downarrow H}\subseteq H$ for
every $\exists r.D\in\textsf{sub}(G)$. Then $\mathcal{I}\models^{2}\beta$.

arxiv

###### Proof.

Since $\beta$ is an $\mathcal{ELX}_{F1}$ axiom, $\beta$ is range restricted
and $F$ is linear. Therefore, by Theorem 1, $\mathcal{I}\models^{2}\beta$ iff
$F^{\mathcal{I},\eta}\subseteq G^{\mathcal{I},\eta}$ for every singleton
valuation $\eta$. Now, let $\eta$ be any such singleton valuation and $\theta$
be the corresponding canonical substitution. Then by Lemma 4,
$F^{\mathcal{I},\eta}\subseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F)\\}$. Since $\beta$ is an $\mathcal{ELX}_{F1}$ axiom, $G$
is a safe concept. Furthermore, $\theta(D)\in D_{\downarrow H}\subseteq H$ for
every $\exists r.D\in\textsf{sub}(G)$ by Condition 2). Therefore, by Lemma 4,
$G^{\mathcal{I},\eta}\supseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(G)\\}$. Finally, by Condition 1)
$\theta(\beta)=\theta(F)\sqsubseteq\theta(G)\in\mathcal{G}$, therefore
$F^{\mathcal{I},\eta}\subseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(F)\\}\subseteq\\{x_{D}\in\Delta^{\mathcal{I}}\mid\mathcal{G}\models
D\sqsubseteq\theta(G)\\}\subseteq G^{\mathcal{I},\eta}$. ∎

By combining Corollary 1 and Corollary 2, for the given $\mathcal{ELX}_{F1}$
ontology $\mathcal{K}$ and an $\mathcal{EL}$ axiom $\alpha$, we can define the
_smallest_ concept base $H$ such that the canonical interpretation
$\mathcal{I}$ w.r.t. $\mathcal{G}=\mathcal{K}_{\downarrow H}$ and $H$
satisfies all axioms $\beta\in\mathcal{K}$ under the second-order semantics
and entails $\alpha$ only if $\mathcal{G}\models\alpha$ and thus only if
$\mathcal{K}\models^{\ast}\alpha$. Note that Condition 2) in Corollary 2 is
recursive over $H$. Therefore, the required $H$ is defined as a fixed point
limit for this condition.

######  Definition 9 (Expansion & Expansion Base).

Let $\mathcal{K}$ be a $\mathcal{ELX}$ ontology and $\alpha=F\sqsubseteq E$ an
$\mathcal{EL}$ axiom. Let $H^{0}=\\{F\\}\cup\\{D\mid\exists
r.D\in\textsf{sub}(F)\\}$, and $H^{i+1}=H^{i}\cup\bigcup_{\exists
r.D\in\textsf{sub}^{+}(\mathcal{K})}D_{\downarrow H^{i}}$ for $i\geq 0$. We
call $H^{\infty}=\bigcup_{i\geq 0}H^{i}$ the _expansion base_ and
$\mathcal{G}=\mathcal{K}_{\downarrow H^{\infty}}$ the _expansion_ for
$\mathcal{K}$ w.r.t $\alpha$.

We show that the expansion base $H^{\infty}$ is indeed a fixed point of the
required condition:

######  Lemma 5.

Let $H^{\infty}$ be the expansion base for $\mathcal{K}$ w.r.t. $\alpha$. Then
$D_{\downarrow H^{\infty}}\subseteq H^{\infty}$ for every $\exists
r.D\in\textsf{sub}^{+}(\mathcal{K})$.

arxiv

###### Proof.

Take any $D$ with $\exists r.D\in\textsf{sub}^{+}(\mathcal{K})$ and
$D^{\prime}\in D_{\downarrow H^{\infty}}$. Then
$D^{\prime}=D[X_{1}/C_{1},\dots,X_{n}/C_{n}]$ for
$\\{X_{1},\dots,X_{n}\\}=\textsf{vars}(D)$ and
$\\{C_{1},\dots,C_{n}\\}\subseteq H^{\infty}=\bigcup_{i\geq 0}H^{i}$. Since
$H^{i}\subseteq H^{i+1}$ for every $i\geq 0$, then
$\\{C_{1},\dots,C_{n}\\}\subseteq H^{i}$ for some $i\geq 0$. Then
$D^{\prime}\in D_{\downarrow H^{i}}\subseteq H^{i+1}\subseteq H^{\infty}$. ∎

By combining Corollary 1, Corollary 2 and Lemma 5, we now prove the following
result:

######  Theorem 2.

Let $\mathcal{K}$ be an $\mathcal{ELX}_{F1}$ ontology, $\alpha$ an
$\mathcal{EL}$ axiom, and $\mathcal{K}^{\infty}$ the expansion of
$\mathcal{K}$ w.r.t. $\alpha$. Then $\mathcal{K}\models^{2}\alpha$ implies
$\mathcal{K}^{\infty}\models\alpha$.

arxiv

###### Proof.

Let $H^{\infty}$ be the expansion base for $\mathcal{K}$ and $\alpha$, and
$\mathcal{I}$ the canonical interpretation for $\mathcal{K}^{\infty}$ and
$H^{\infty}$. By Lemma 5, conditions 1) and 2) of Corollary 2 are satisfied
for $H=H^{\infty}$, $\mathcal{G}=\mathcal{K}^{\infty}$ and every
$\beta\in\mathcal{K}$. This implies $\mathcal{I}\models^{2}\mathcal{K}$. Then
$\mathcal{K}\models^{2}\alpha$ implies $\mathcal{I}\models\alpha$.
Furthermore, by Definition 9, the conditions of Corollary 1 are satisfied for
$H=H^{\infty}\supseteq H^{0}$, $\mathcal{G}=\mathcal{K}^{\infty}$ and
$\alpha$. Hence, $\mathcal{I}\models\alpha$ implies
$\mathcal{G}=\mathcal{K}^{\infty}\models\alpha$, as required. ∎

An immediate consequence of Theorem 2 is that the schema semantics coincides
with second-order semantics for $\mathcal{ELX}_{F1}$ ontologies.

######  Theorem 3.

Let $\mathcal{K}$ be a $\mathcal{ELX}_{F1}$ ontology and $\alpha$ an
$\mathcal{EL}$ axiom. Then
$\mathcal{K}\models^{2}\alpha\Leftrightarrow\mathcal{K}\models^{\ast}_{\mathcal{EL}}\alpha$.

arxiv

###### Proof.

$(\Rightarrow)$: By Theorem 2, $\mathcal{K}\models^{2}\alpha$ implies
$\mathcal{K}^{\infty}\models\alpha$. Then
$\mathcal{K}\models^{\ast}_{H^{\infty}}\alpha$, and so,
$\mathcal{K}\models^{\ast}_{\mathcal{EL}}\alpha$.

$(\Leftarrow)$: By Definition 2,
$\mathcal{K}\models^{\ast}_{\mathcal{EL}}\alpha$ means that
$\mathcal{K}_{\downarrow H}\models\alpha$ where $H$ is the set of all
$\mathcal{EL}$ concepts. In order to prove that
$\mathcal{K}\models^{2}\alpha$, take any $\mathcal{I}\models^{2}\mathcal{K}$.
We prove that $\mathcal{I}\models\alpha$. We first show that
$\mathcal{I}\models\mathcal{K}_{\downarrow H}$. Indeed, take any
$\beta^{\prime}\in\mathcal{K}_{\downarrow H}$. Then
$\beta^{\prime}=\theta(\beta)$ for some substitution $\theta$ of concept
variables to concepts from $H$. Define a valuation $\eta$ by
$\eta(X)=\theta(X)^{\mathcal{I}}$. By induction on the structure of
$\mathcal{EL}$ concepts $D$ it is easy to show that
$D^{\mathcal{I},\eta}=\theta(D)^{\mathcal{I}}$. Then
$\mathcal{I}\models\beta^{\prime}$ follows from
$\mathcal{I}\models^{2}_{\eta}\beta\in\mathcal{K}$ since
$\mathcal{I}\models^{2}\mathcal{K}$. This proves
$\mathcal{I}\models\mathcal{K}_{\downarrow H}$. Since $\mathcal{K}_{\downarrow
H}\models\alpha$, we obtain $\mathcal{I}\models\alpha$ as required. ∎

##  4 Decidability

Because the schema semantics and the second-order semantics coincide for
$\mathcal{ELX}_{F1}$, we immediately obtain semi-decidability of the
entailment for the latter. In general, entailment in $\mathcal{ELX}_{F1}$ ist
still _undecidable_ because $\mathcal{ELX}_{F1}$ can express (unrestricted)
role-value-maps:

######  Definition 10 (Role-Value-Maps).

A _role-value-map_ [23] is an axiom of the form $r_{1}\circ\dots\circ
r_{m}\sqsubseteq s_{1}\circ\dots\circ s_{n}$ with $m,n\geq 1$, $r_{i},s_{j}\in
N_{R}$ ($1\leq i\leq m$, $1\leq j\leq n$). The _interpretation of role-value-
maps_ is defined by: $\mathcal{I}\models r_{1}\circ\dots\circ r_{m}\sqsubseteq
s_{1}\circ\dots\circ s_{n}\text{ iff }r_{1}^{\mathcal{I}}\circ\dots\circ
r_{m}^{\mathcal{I}}\subseteq s_{1}^{\mathcal{I}}\circ\dots\circ
s_{n}^{\mathcal{I}}$, where $\circ$ is the usual composition of binary
relations.

######  Lemma 6.

For every interpretation $\mathcal{I}$ it holds $\mathcal{I}\models^{2}\exists
r_{1}.\exists r_{2}.\dots\exists r_{m}.X\sqsubseteq\exists s_{1}.\exists
s_{2}.\dots\exists s_{n}.X$ iff $r_{1}^{\mathcal{I}}\circ\dots\circ
r_{m}^{\mathcal{I}}\subseteq s_{1}^{\mathcal{I}}\circ\dots\circ
s_{n}^{\mathcal{I}}$.

arxiv

###### Proof.

  * $\Rightarrow$:

Assume that

$\mathcal{I}\models^{2}\exists r_{1}.\exists r_{2}.\dots\exists
r_{m}.X\sqsubseteq\exists s_{1}.\exists s_{2}.\dots\exists s_{n}.X$

Then we need to show that

$\displaystyle\begin{aligned} \mathllap{\forall x,z\in\Delta^{\mathcal{I}}:\
}(\exists y_{1},\dots,y_{m-1}\in\Delta^{\mathcal{I}}:&\langle
x,y_{1}\rangle\in r_{1}^{\mathcal{I}},\langle y_{1},y_{2}\rangle\in
r_{2}^{\mathcal{I}},\dots,\\\ &\langle y_{m-1},z\rangle\in
r_{m}^{\mathcal{I}})\end{aligned}$ $\displaystyle\begin{aligned}
\mathllap{\Rightarrow\ }(\exists
y_{1},\dots,y_{n-1}\in\Delta^{\mathcal{I}}:&\langle x,y_{1}\rangle\in
s_{1}^{\mathcal{I}},\langle y_{1},y_{2}\rangle\in
s_{2}^{\mathcal{I}},\dots,\\\ &\langle y_{n-1},z\rangle\in
s_{n}^{\mathcal{I}})\end{aligned}$

Take any $x,z\in\Delta^{\mathcal{I}}$ such that

$\exists y_{1},\dots,y_{m-1}\in\Delta^{\mathcal{I}}:\langle x,y_{1}\rangle\in
r_{1}^{\mathcal{I}},\langle y_{1},y_{2}\rangle\in
r_{2}^{\mathcal{I}},\dots,\langle y_{m-1},z\rangle\in r_{m}^{\mathcal{I}}$

Let $\eta$ be a valuation such that $\eta(X)=\\{z\\}$. Then $x\in(\exists
r_{1}.\exists r_{2}.\dots\exists r_{m}.X)^{\mathcal{I},\eta}$ and it follows
that $x\in(\exists s_{1}.\exists s_{2}.\dots\exists
s_{n}.X)^{\mathcal{I},\eta}$. Then

$\exists y_{1},\dots,y_{n-1}\in\Delta^{\mathcal{I}}:\langle x,y_{1}\rangle\in
s_{1}^{\mathcal{I}},\langle y_{1},y_{2}\rangle\in
s_{2}^{\mathcal{I}},\dots,\langle y_{n-1},z\rangle\in s_{n}^{\mathcal{I}}$

  * $\Leftarrow$:

Assume that

$\displaystyle\begin{aligned} \mathllap{\forall x,z\in\Delta^{\mathcal{I}}:\
}(\exists y_{1},\dots,y_{m-1}\in\Delta^{\mathcal{I}}:&\langle
x,y_{1}\rangle\in r_{1}^{\mathcal{I}},\langle y_{1},y_{2}\rangle\in
r_{2}^{\mathcal{I}},\dots,\\\ &\langle y_{m-1},z\rangle\in
r_{m}^{\mathcal{I}})\end{aligned}$ $\displaystyle\begin{aligned}
\mathllap{\Rightarrow\ }(\exists
y_{1},\dots,y_{n-1}\in\Delta^{\mathcal{I}}:&\langle x,y_{1}\rangle\in
s_{1}^{\mathcal{I}},\langle y_{1},y_{2}\rangle\in
s_{2}^{\mathcal{I}},\dots,\\\ &\langle y_{n-1},z\rangle\in
s_{n}^{\mathcal{I}})\end{aligned}$

We need to show that

$\mathcal{I}\models^{2}\exists r_{1}.\exists r_{2}.\dots\exists
r_{m}.X\sqsubseteq\exists s_{1}.\exists s_{2}.\dots\exists s_{n}.X$

Take any $x$ and $\eta$ then if $x\in(\exists r_{1}.\exists r_{2}.\dots\exists
r_{m}.X)^{\mathcal{I},\eta}$ then

$\displaystyle\exists y_{1},\dots,y_{m-1},z\in\Delta^{\mathcal{I}}:$
$\displaystyle\langle x,y_{1}\rangle\in r_{1}^{\mathcal{I}},\langle
y_{1},y_{2}\rangle\in r_{2}^{\mathcal{I}},\dots,$ $\displaystyle\langle
y_{m-1},z\rangle\in r_{m}^{\mathcal{I}},z\in\eta(X)$

Then from the role-value-map axiom it follows that

$\exists y_{1},\dots,y_{n-1}\in\Delta^{\mathcal{I}}:\langle x,y_{1}\rangle\in
s_{1}^{\mathcal{I}},\langle y_{1},y_{2}\rangle\in
s_{2}^{\mathcal{I}},\dots,\langle y_{n-1},z\rangle\in s_{n}^{\mathcal{I}}$

Then $x\in(\exists s_{1}.\exists s_{2}.\dots\exists
s_{n}.X)^{\mathcal{I},\eta}$. As $x$ and $\eta$ were chosen arbitrarily, this
proves the proposition. ∎

######  Theorem 4.

Axiom entailment in $\mathcal{ELX}_{F1}$ is undecidable.

###### Proof.

Follows directly from Lemma 6 and the fact that axiom entailment is
undecidable in $\mathcal{EL}$ extended with role-value-maps [23]. ∎

The reason for this undecidiblity, is deep nesting of concept variables on the
right side of axioms under existential restrictions. Such nested variables
result in infinite expansion base $H^{\infty}$ as the following example shows:

######  Example 6.

Consider the $\mathcal{ELX}_{F1}$ ontology $\mathcal{K}=\\{X\sqsubseteq\exists
r.\exists r.X\\}$ and $\alpha=A\sqsubseteq B$. Then according to Definition 9,
we have $H^{1}=\\{A\\}$, $\mathcal{K}^{1}=\\{A\sqsubseteq\exists r.\exists
r.A\\}$, $H^{2}=\\{A,\exists r.A\\}$, $\mathcal{K}^{2}=\\{A\sqsubseteq\exists
r.\exists r.A,\exists r.A\sqsubseteq\exists r.\exists r.\exists r.A\\}$,
$H^{3}=\\{A,\exists r.A,\exists r.\exists r.A\\}$, etc.

If we restrict $\mathcal{ELX}_{F1}$ so that variables on the right side do not
appear under nested existential restrictions, we can show that the expansion
$\mathcal{K}^{\infty}$ of the ontology is, in fact, polynomial in the size of
$\mathcal{K}$, which gives us polynomial decidability of the (schema and
second-order) entailment.

######  Definition 11 ($\mathcal{ELX}_{F2}$).

An $\mathcal{ELX}_{F2}$ axiom is an $\mathcal{ELX}_{F1}$ axiom $\alpha$ such
that for every $\exists r.D\in\textsf{sub}^{+}(\alpha)$, either $D=X\in N_{X}$
or $\textsf{vars}(D)=\emptyset$.

######  Lemma 7.

Let $\mathcal{K}$ be an $\mathcal{ELX}_{F2}$ ontology, $\alpha$ an
$\mathcal{EL}$ axiom and $H^{\infty}$ the expansion base for $\mathcal{K}$ and
$\alpha$. Then $H^{\infty}=H^{0}\cup\\{D\mid\exists
r.D\in\textsf{sub}^{+}(\mathcal{K})\>\&\>\textsf{vars}(D)=\emptyset\\}$.

arxiv

###### Proof.

By Definition 9, $H^{i+1}=H^{i}\cup\bigcup_{\exists
r.D\in\textsf{sub}^{+}(\mathcal{K})}D_{\downarrow H^{i}}$ for $i\geq 0$. By
Definition 11, $\exists r.D\in\textsf{sub}^{+}(\mathcal{K})$ implies $D=X\in
N_{X}$ or $\textsf{vars}(D)=\emptyset$. If $D=X$ then $D_{\downarrow
H^{i}}=X_{\downarrow H^{i}}=H^{i}$. If $\textsf{vars}(D)=\emptyset$ then
$D_{\downarrow H^{i}}=\\{D\\}$. Then $H^{i+1}=H^{i}\cup\\{D\mid\exists
r.D\in\textsf{sub}^{+}(\mathcal{K})\>\&\>\textsf{vars}(D)=\emptyset\\}$. Hence
$H^{\infty}=\bigcup_{i\geq 0}H^{i}\subseteq H^{0}\cup\\{D\mid\exists
r.D\in\textsf{sub}^{+}(\mathcal{K})\>\&\>\textsf{vars}(D)=\emptyset\\}$. ∎

Since the elements of $H^{\infty}$ are subsets of (ground) concepts appearing
in $\mathcal{K}$ and $\alpha$, we obtain:

######  Theorem 5.

Let $\mathcal{K}$ be a $\mathcal{ELX}_{F2}$ ontology and $\alpha$ an
$\mathcal{EL}$ axiom. Then the entailment $\mathcal{K}\models^{2}\alpha$ is
decidable in polynomial time in the size of $\mathcal{K}$ and $\alpha$.

arxiv

###### Proof.

By Lemma 7, $H^{\infty}=H^{0}\cup\\{D\mid\exists
r.D\in\textsf{sub}^{+}(\mathcal{K})\>\&\>\textsf{vars}(D)=\emptyset\\}\subseteq\textsf{sub}^{-}(\alpha)\cup\textsf{sub}^{+}(\mathcal{K})$.
Hence $|\\!|H^{\infty}|\\!|\leq|\\!|\mathcal{K}|\\!|+|\\!|\alpha|\\!|$. Since
$\mathcal{K}^{\infty}=\mathcal{K}_{\downarrow H^{\infty}}$,
$|\\!|\mathcal{K}^{\infty}|\\!|\leq|\\!|\mathcal{K}|\\!|\cdot|\\!|H^{\infty}|\\!|^{V}$
where $V$ is the maximal number of concept variables in axioms of
$\mathcal{K}$. It can be shown that, w.l.o.g., $V\leq 1$ for
$\mathcal{ELX}_{F2}$ ontologies. Hence,
$|\\!|\mathcal{K}^{\infty}|\\!|\leq|\\!|\mathcal{K}|\\!|\cdot(|\\!|\mathcal{K}|\\!|+|\\!|\alpha|\\!|)$.

By Theorem 2, $\mathcal{K}\models^{2}\alpha$ implies
$\mathcal{K}^{\infty}\models\alpha$. Conversely,
$\mathcal{K}^{\infty}\models\alpha$ implies
$\mathcal{K}\models^{\ast}_{\mathcal{EL}}\alpha$, which implies
$\mathcal{K}\models^{2}\alpha$ by Theorem 3. Hence, entailment
$\mathcal{K}\models^{2}\alpha$ can be reduced to the classical $\mathcal{EL}$
entailment in polynomial time. Since the latter is polynomially decidable [2],
this implies that the entailment $\mathcal{K}\models^{2}\alpha$ is also
decidable in polynomial time. ∎

##  5 Conclusions and Outlook

In this paper, we left behind the usual restriction of DLs to fragments of FOL
and introduced concept variables directly into DLs. These concept variables
can be understood as simple placeholders for concrete concepts, giving us
axiom schemas. This results in a semantics that replaces variables by a
specific set of concepts and in this way reduces reasoning to the classical
case. Or they can be understood more strongly, as universally quantified
concepts, similar to predicates in SOL. This gives us a semantics that
interprets variables as arbitrary subsets of the interpretation domain and
results in the DL being a fragment of SOL.

We applied this extension to $\mathcal{EL}$ and analyzed the difference in
entailed conclusions by the two semantics. We defined a fragment for which the
conclusions coincide, given us semi-decidability also for second-order
semantics. We also showed that for a slight limitation of this fragment,
second-order semantics (and schema semantics) even become decidable.

In this decidable fragment $\mathcal{ELX}_{F2}$, we can express a range of
features that usually require special constructors in classical
$\mathcal{EL}$: We can express role chain axioms that reduce a chain of roles
to a connection via one role. What would normally be expressed as
$r_{1}\circ\dots\circ r_{n}\sqsubseteq s$ (i.e. role-value-maps where the
right side is a single role, cf. Definition 10), we can express as $\exists
r_{1}.\exists r_{2}.\dots\exists r_{n}.X\sqsubseteq\exists s.X$. For example
$\textsf{father}\circ\textsf{father}\sqsubseteq\textsf{grandfather}$ is
equivalent to
$\exists\textsf{father}.\exists\textsf{father}.X\sqsubseteq\exists\textsf{grandfather}.X$.
We can also express self restrictions on the right side of axioms, i.e.
classical axioms of the form $C\sqsubseteq\exists r.\mathrm{Self}$, meaning
$\forall x:(x\in C^{\mathcal{I}})\Rightarrow(\langle x,x\rangle\in
r^{\mathcal{I}})$ (cf. e.g. [24]). We express this as $C\sqcap
X\sqsubseteq\exists r.X$. For example
$\textsf{GreatApes}\sqsubseteq\exists\textsf{recognize}.\mathrm{Self}$ is
equivalent to $\textsf{GreatApes}\sqcap
X\sqsubseteq\exists\textsf{recognize}.X$. We can express positive occurrences
of (local) _role-value-map concepts_ , i.e., concepts of the form $r\subseteq
s$ interpreted as $\\{x\mid\forall y:\langle x,y\rangle\in
r^{\mathcal{I}}\Rightarrow\langle x,y\rangle\in s^{\mathcal{I}}\\}$ (cf. e.g.
[25]). E.g., we express $C\sqsubseteq(r\subseteq s)$ as $C\sqcap\exists
r.X\sqsubseteq\exists s.X$. For example
$\textsf{Male}\sqsubseteq(\textsf{isParentOf}\subseteq\textsf{isFatherOf})$ is
equivalent to
$\textsf{Male}\sqcap\exists\textsf{isParentOf}.X\sqsubseteq\exists\textsf{isFatherOf}.X$.
Finally, we can express restrictions that generalize _all_ of these
constructs, for example, axioms of the form:

$C_{0}\sqcap\exists r_{1}.(C_{1}\sqcap\exists r_{2}.(C_{2}\dots\sqcap\exists
r_{n}.(C_{n}\sqcap X)\dots))\sqsubseteq\exists s.X,\quad(n\geq 0)$ (7)

Note that (7) can be expressed with self-restrictions over fresh roles:
$C_{i}\sqsubseteq\exists h_{i}.\text{Self}$ $(0\leq i\leq n)$ and role chain
axiom: $h_{0}\circ r_{1}\circ h_{2}\circ r_{2}\cdots r_{n}\sqsubseteq s$.
Thus, it is not clear whether our decidable fragment has more expressive power
than known polynomial extensions of $\mathcal{EL}$ [20, 24].

It is possible to generalize Theorem 3 and Theorem 5 to entailments of
arbitrary $\mathcal{ELX}$ axioms $\alpha$ because such entailments can be
always reduced to entailment of $\mathcal{EL}$ axioms by simply replacing all
concept variables in $\alpha$ with new atomic concepts, not occurring in
$\mathcal{K}$ or $\alpha$. Intuitively, to prove that every (second order or
schema) model of the ontology satisfies $\alpha$ under each valuation $\eta$
or substitution $\theta$, we can extend this model by interpreting the new
atomic concepts according to the value of $\eta(X)$ or $\theta(X)$ on the
variables $X$ which they replace. This still remains a model of the ontology
since it does not contain these new concepts.

Summarizing, the results in this paper show that an extension of DLs to being
fragments of SOL, instead of FOL, is possible (while remaining decidable for
reasonable restrictions) and does allow expressing facts in a new way without
the use of special constructors. This enlightens the relationship between FOL,
SOL and DLs and opens the way for further extensions of DLs outside FOL.

## References

  * Schmidt-Schauß [1989] M. Schmidt-Schauß,  Subsumption in KL-ONE is undecidable,  in: R. J. Brachman, H. J. Levesque, R. Reiter (Eds.), Proceedings of the 1st International Conference on Principles of Knowledge Representation and Reasoning (KR’89). Toronto, Canada, May 15-18 1989, Morgan Kaufmann, 1989, pp. 421–431.
  * Baader et al. [2005] F. Baader, S. Brandt, C. Lutz, Pushing the EL Envelope, LTCS-Report LTCS-05-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. doi:https://doi.org/10.25368/2022.144, see http://lat.inf.tu-dresden.de/research/reports.html.
  * Calvanese et al. [2007] D. Calvanese, G. D. Giacomo, D. Lembo, M. Lenzerini, R. Rosati,  Tractable reasoning and efficient query answering in description logics: The DL-Lite family,  J. of Automated Reasoning 39 (2007) 385–429.
  * Horrocks et al. [2006] I. Horrocks, O. Kutz, U. Sattler,  The even more irresistible SROIQ,  in: P. Doherty, J. Mylopoulos, C. A. Welty (Eds.), Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning, Lake District of the United Kingdom, June 2-5, 2006, AAAI Press, 2006, pp. 57–67. URL: http://www.aaai.org/Library/KR/2006/kr06-009.php.
  * Motik et al. [2009] B. Motik, P. F. Patel-Schneider, B. Cuenca Grau (Eds.), OWL 2 Web Ontology Language: Direct Semantics, W3C Recommendation, 27 October 2009. Available at http://www.w3.org/TR/owl2-direct-semantics/.
  * Blackburn et al. [2001] P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884. doi:10.1017/CBO9781107050884.
  * Carral et al. [2023] D. Carral, J. Zalewski, P. Hitzler,  An efficient algorithm for reasoning over OWL EL ontologies with nominal schemas,  J. Log. Comput. 33 (2023) 136–162. URL: https://doi.org/10.1093/logcom/exac032. doi:10.1093/logcom/exac032.
  * Krötzsch et al. [2011] M. Krötzsch, F. Maier, A. Krisnadhi, P. Hitzler,  A better uncle for OWL: nominal schemas for integrating rules and ontologies,  in: S. Srinivasan, K. Ramamritham, A. Kumar, M. P. Ravindra, E. Bertino, R. Kumar (Eds.), Proceedings of the 20th International Conference on World Wide Web, WWW 2011, Hyderabad, India, March 28 - April 1, 2011, ACM, 2011, pp. 645–654. URL: https://doi.org/10.1145/1963405.1963496. doi:10.1145/1963405.1963496.
  * Carral et al. [2013] D. Carral, C. Wang, P. Hitzler,  Towards an efficient algorithm to reason over description logics extended with nominal schemas,  in: Web Reasoning and Rule Systems: 7th International Conference, RR 2013, Mannheim, Germany, July 27-29, 2013. Proceedings 7, Springer, 2013, pp. 65–79.
  * He et al. [2015] Y. He, J. Zheng, Y. Lin,  Ontorat: Automatic generation and editing of ontology terms,  in: F. M. Couto, J. Hastings (Eds.), Proceedings of the International Conference on Biomedical Ontology, ICBO 2015, Lisbon, Portugal, July 27-30, 2015, volume 1515 of CEUR Workshop Proceedings, CEUR-WS.org, 2015. URL: https://ceur-ws.org/Vol-1515/demo2.pdf.
  * Skjæveland et al. [2018] M. G. Skjæveland, D. P. Lupp, L. H. Karlsen, H. Forssell,  Practical ontology pattern instantiation, discovery, and maintenance with reasonable ontology templates,  in: D. Vrandecic, K. Bontcheva, M. C. Suárez-Figueroa, V. Presutti, I. Celino, M. Sabou, L. Kaffee, E. Simperl (Eds.), The Semantic Web - ISWC 2018 - 17th International Semantic Web Conference, Monterey, CA, USA, October 8-12, 2018, Proceedings, Part I, volume 11136 of Lecture Notes in Computer Science, Springer, 2018, pp. 477–494. URL: https://doi.org/10.1007/978-3-030-00671-6_28. doi:10.1007/978-3-030-00671-6_28.
  * Kindermann et al. [2018] C. Kindermann, D. P. Lupp, U. Sattler, E. Thorstensen,  Generating ontologies from templates: A rule-based approach for capturing regularity,  in: M. Ortiz, T. Schneider (Eds.), Proceedings of the 31st International Workshop on Description Logics co-located with 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018), Tempe, Arizona, US, October 27th - to - 29th, 2018, volume 2211 of CEUR Workshop Proceedings, CEUR-WS.org, 2018. URL: https://ceur-ws.org/Vol-2211/paper-22.pdf.
  * Krieg-Brückner et al. [2019] B. Krieg-Brückner, T. Mossakowski, F. Neuhaus,  Generic ontology design patterns at work,  in: A. Barton, S. Seppälä, D. Porello (Eds.), Proceedings of the Joint Ontology Workshops 2019 Episode V: The Styrian Autumn of Ontology, Graz, Austria, September 23-25, 2019, volume 2518 of CEUR Workshop Proceedings, CEUR-WS.org, 2019\. URL: https://ceur-ws.org/Vol-2518/paper-BOG2.pdf.
  * Kindermann et al. [2019] C. Kindermann, B. Parsia, U. Sattler,  Comparing approaches for capturing repetitive structures in ontology design patterns,  in: K. Janowicz, A. A. Krisnadhi, M. Poveda-Villalón, K. Hammar, C. Shimizu (Eds.), Proceedings of the 10th Workshop on Ontology Design and Patterns (WOP 2019) co-located with 18th International Semantic Web Conference (ISWC 2019), Auckland, New Zealand, October 27, 2019, volume 2459 of CEUR Workshop Proceedings, CEUR-WS.org, 2019, pp. 17–31. URL: https://ceur-ws.org/Vol-2459/paper2.pdf.
  * Skjæveland et al. [2017] M. G. Skjæveland, H. Forssell, J. W. Klüwer, D. P. Lupp, E. Thorstensen, A. Waaler,  Reasonable ontology templates: APIs for OWL,  in: N. Nikitina, D. Song, A. Fokoue, P. Haase (Eds.), Proceedings of the ISWC 2017 Posters & Demonstrations and Industry Tracks co-located with 16th International Semantic Web Conference (ISWC 2017), Vienna, Austria, October 23rd - to - 25th, 2017, volume 1963 of CEUR Workshop Proceedings, CEUR-WS.org, 2017\. URL: https://ceur-ws.org/Vol-1963/paper597.pdf.
  * Borgida et al. [2012] A. Borgida, J. Horkoff, J. Mylopoulos, R. Rosati,  Experiences in mapping the business intelligence model to description logics, and the case for parametric concepts,  in: Y. Kazakov, D. Lembo, F. Wolter (Eds.), Proceedings of the 2012 International Workshop on Description Logics, DL-2012, Rome, Italy, June 7-10, 2012, volume 846 of CEUR Workshop Proceedings, CEUR-WS.org, 2012\. URL: https://ceur-ws.org/Vol-846/paper_48.pdf.
  * Colucci et al. [2010] S. Colucci, T. D. Noia, E. D. Sciascio, F. M. Donini, A. Ragone,  Second-order description logics: Semantics, motivation, and a calculus,  in: V. Haarslev, D. Toman, G. E. Weddell (Eds.), Proceedings of the 23rd International Workshop on Description Logics (DL 2010), Waterloo, Ontario, Canada, May 4-7, 2010, volume 573 of CEUR Workshop Proceedings, CEUR-WS.org, 2010. URL: https://ceur-ws.org/Vol-573/paper_41.pdf.
  * Fitting [2007] M. Fitting,  Modal proof theory,  in: P. Blackburn, J. F. A. K. van Benthem, F. Wolter (Eds.), Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, North-Holland, 2007, pp. 85–138. URL: https://doi.org/10.1016/s1570-2464(07)80005-x. doi:10.1016/s1570-2464(07)80005-x.
  * Goldblatt [1975] R. Goldblatt,  First-order definability in modal logic,  J. Symb. Log. 40 (1975) 35–40. URL: https://doi.org/10.2307/2272267. doi:10.2307/2272267.
  * Baader et al. [2008] F. Baader, C. Lutz, S. Brandt,  Pushing the EL envelope further,  in: K. Clark, P. F. Patel-Schneider (Eds.), Proceedings of the Fourth OWLED Workshop on OWL: Experiences and Directions, Washington, DC, USA, 1-2 April 2008, volume 496 of CEUR Workshop Proceedings, CEUR-WS.org, 2008. URL: https://ceur-ws.org/Vol-496/owled2008dc_paper_3.pdf.
  * Kazakov et al. [2012] Y. Kazakov, M. Kroetzsch, F. Simancik,  Practical reasoning with nominals in the EL family of description logics,  in: G. Brewka, T. Eiter, S. A. McIlraith (Eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, KR 2012, Rome, Italy, June 10-14, 2012, AAAI Press, 2012. URL: http://www.aaai.org/ocs/index.php/KR/KR12/paper/view/4540.
  * Kazakov et al. [2014] Y. Kazakov, M. Krötzsch, F. Simancik,  The incredible ELK - from polynomial procedures to efficient reasoning with EL ontologies,  J. Autom. Reason. 53 (2014) 1–61. URL: https://doi.org/10.1007/s10817-013-9296-3. doi:10.1007/s10817-013-9296-3.
  * Baader [2003] F. Baader,  Restricted role-value-maps in a description logic with existential restrictions and terminological cycles,  in: D. Calvanese, G. D. Giacomo, E. Franconi (Eds.), Proceedings of the 2003 International Workshop on Description Logics (DL2003), Rome, Italy September 5-7, 2003, volume 81 of CEUR Workshop Proceedings, CEUR-WS.org, 2003. URL: https://ceur-ws.org/Vol-81/baader.pdf.
  * Wang and Hitzler [2012] C. Wang, P. Hitzler,  Consequence-based procedure for description logics with self-restriction,  in: J. Li, G. Qi, D. Zhao, W. Nejdl, H. Zheng (Eds.), Semantic Web and Web Science - 6th Chinese Semantic Web Symposium and 1st Chinese Web Science Conference, CSWS 2012, Shenzhen, China, November 28-30, 2012, Springer, 2012, pp. 169–180. URL: https://doi.org/10.1007/978-1-4614-6880-6_15. doi:10.1007/978-1-4614-6880-6_15.
  * Donini [2003] F. M. Donini,  Complexity of reasoning,  in: F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, P. F. Patel-Schneider (Eds.), The Description Logic Handbook: Theory, Implementation, and Applications, Cambridge University Press, 2003, pp. 96–136.

##  Appendix A Acronyms

Schema-S

    schema semantics
SO-S

    second-order semantics
DL

    Description Logic
PL

    Propositional Logic
FOL

    First-Order Logic
SOL

    Second-Order Logic
ODP

    Ontology Design Pattern
ML

    Modal Logic
  *[FOL]: First-Order Logic
  *[DLs]: Description Logic
  *[SOL]: Second-Order Logic
  *[DL]: Description Logic
  *[PL]: Propositional Logic
  *[MLs]: Modal Logic
  *[PLs]: Propositional Logic
  *[ML]: Modal Logic