thmtoolsLLNCS support disables automatic casing of theorem names latexfontFont
shape ‘OMS/cmsy/m/n’ in size ¡ latexfontSize substitutions with differences

11institutetext: DI ENS, ENS, CNRS, PSL University & Inria, Paris, France
22institutetext: University of Bergen, Norway 33institutetext: University of
Edinburgh, United Kingdom

#  Geometric Models for (Temporally) Attributed Description Logics

Camille Bourgaux1 Ana Ozaki2 Jeff Z. Pan3

###### Abstract

In the search for knowledge graph embeddings that could capture ontological
knowledge, geometric models of existential rules have been recently
introduced. It has been shown that convex geometric regions capture the so-
called quasi-chained rules. Attributed description logics (DL) have been
defined to bridge the gap between DL languages and knowledge graphs, whose
facts often come with various kinds of annotations that may need to be taken
into account for reasoning. In particular, temporally attributed DLs are
enriched by specific attributes whose semantics allows for some temporal
reasoning. Considering that geometric models and (temporally) attributed DLs
are promising tools designed for knowledge graphs, this paper investigates
their compatibility, focusing on the attributed version of a Horn dialect of
the DL-Lite family. We first adapt the definition of geometric models to
attributed DLs and show that every satisfiable ontology has a convex geometric
model. Our second contribution is a study of the impact of temporal
attributes. We show that a temporally attributed DL may not have a convex
geometric model in general but we can recover geometric satisfiability by
imposing some restrictions on the use of the temporal attributes.

##  1 Introduction

Knowledge graph embeddings are popular latent representations of knowledge
graphs (KG). In the search for KG embeddings that could capture ontological
knowledge (i.e., schema of KG), geometric models of existential rules have
been recently introduced [13]. Such models have several advantages. Notably,
they ensure that facts which are valid in the embedding are logically
consistent and deductively closed w.r.t. the ontology, and they can also be
used to find plausible missing ontology rules. It has been shown that convex
geometric regions capture the so-called quasi-chained rules, a fragment of
first-order Horn logic. Attributed description logics (DL) have been defined
to bridge the gap between DL ontology languages and KG, whose facts often come
with various kinds of annotations that may need to be taken into account for
reasoning. In particular, they were introduced as a formalism for dealing with
the meta-knowledge present in KG, such as temporal validity, provenance,
language, and others [16, 17, 8]. As time is of primary interest in KG,
attributed DLs have been enriched with temporal attributes, whose semantics
allows for some temporal reasoning over discrete time [22]. Considering that
geometric models and (temporally) attributed DLs are promising tools designed
for KG, this paper investigates their compatibility, focusing on the
attributed version of a Horn dialect of the DL-Lite family.

Our contributions are as follows:

  * •

We adapt the notion of geometric models for ((temporally) attributed) DLs; in
particular, we use an arbitrary linear map to combine the individual geometric
interpretations instead of restricting ourselves to vector concatenation, and
define satisfaction of concept or role inclusions directly based on geometric
inclusion relationship between the regions that interpret the concepts or
roles.

  * •

We show that every satisfiable attributed DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontology has a convex geometric model
but there are satisfiable _temporally_ attributed DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontologies without such a model.

  * •

We exhibit restrictions on the use of temporal attributes that guarantee that
temporally attributed DL-Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontologies
have a convex geometric model.

We define attributed DLs and geometric models in Section 2. Then, in Section
3, we study the relationship between satisfiability and the existence of
convex geometric models in DL-Lite${}^{\mathcal{H}}_{\mathit{horn}}$. We then
extend our analysis for temporally attributed DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$ in Section 4. In Section 5, we discuss
related works and we conclude in Section 6. Omitted proofs are given in the
appendix.

##  2 Geometric Models for Attributed Description Logics

In this section, we recall the framework of attributed DLs and define
geometric models in this context.

###  2.1 Attributed DLs

We introduce attributed DLs by defining attributed DL-Lite [8], focusing on
the DL-Lite${}^{\mathcal{H}}_{\mathit{horn}}$ dialect. The notions presented
here can be easily adapted to other attributed DLs, e.g. $\mathcal{EL}$, as in
[16, 17]. Let $\mathsf{N_{C}}$, $\mathsf{N_{R}}$, and $\mathsf{N_{I}}$ be
countably infinite and mutually disjoint sets of _concept_ , _role_ , and
_individual names_. We assume that $\mathsf{N_{I}}$ is divided into two sets,
called $\mathsf{N_{i}}$ and $\mathsf{N_{a}}$, and we refer to the elements in
$\mathsf{N_{a}}$ as _annotation names_. We consider an additional set
$\mathsf{N_{U}}$ of _set variables_ and a set $\mathsf{N_{V}}$ of _object
variables_. The set $\mathbf{S}$ of _specifiers_ contains the following
expressions:

  * •

set variables $X\in\mathsf{N_{U}}$;

  * •

_closed specifiers_ $[a_{1}\kern 0.6pt{:}\,v_{1},\dotsc,a_{n}\kern
0.6pt{:}\,v_{n}]$; and

  * •

_open specifiers_ $\lfloor a_{1}\kern 0.6pt{:}\,v_{1},\dotsc,a_{n}\kern
0.6pt{:}\,v_{n}\rfloor$,

where $a_{i}\in\mathsf{N_{a}}$ and $v_{i}$ is either an individual name in
$\mathsf{N_{a}}$, an object variable in $\mathsf{N_{V}}$, or an expression of
the form $X.a$, with $X$ a set variable in $\mathsf{N_{U}}$ and $a$ an
individual name in $\mathsf{N_{a}}$. We use $X.a$ to refer to the (finite,
possibly empty) set of all values of attribute $a$ in an annotation set $X$. A
_ground specifier_ is a closed or open specifier built only over
$\mathsf{N_{a}}$.

Syntax.  A DL-Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ _concept_ (resp.
_role_) _assertion_ is an expression $A(a)@S$ (resp. $R(a,b)@S$), with
$A\in\mathsf{N_{C}}$ (resp. $R\in\mathsf{N_{R}}$), $a,b\in\mathsf{N_{i}}$, and
$S\in\mathbf{S}$ a ground closed specifier. A DL-
Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ _role inclusion_ is an expression of
the form:

$\displaystyle{X}\,{\boldsymbol{:}}\,{S}\quad(P\sqsubseteq Q),$ (1)

where $S\in\mathbf{S}$ is a closed or open specifier, $X\in\mathsf{N_{U}}$ is
a set variable, and $P,Q$ are role expressions built according to the
following syntax:

$\displaystyle P\coloneqq R@S\mid R^{-}@S,\quad\quad Q\coloneqq P\mid\neg P$
(2)

with $S\in\mathbf{S}$, $R\in\mathsf{N_{R}}$. A DL-
Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ _concept inclusion_ is of the form:

$\displaystyle{X_{1}}\,{\boldsymbol{:}}\,{S_{1}},\ldots,{X_{n}}\,{\boldsymbol{:}}\,{S_{n}}\quad(\bigsqcap_{i=1}^{k}B_{i}\sqsubseteq
C),$ (3)

where $k,n\geq 1$, $S_{1},\dots,S_{n}\in\mathbf{S}$ are closed or open
specifiers, $X_{1},\dots,X_{n}\in\mathsf{N_{U}}$ are set variables, and
$B_{i},C$ are concept expressions built according to:

$\displaystyle B\coloneqq A@S\mid\exists P,\quad C\coloneqq B\mid\bot,$ (4)

where $P$ is as in Equation 2, $A\in\mathsf{N_{C}}$ and $S\in\mathbf{S}$. Role
expressions of the form $P$ are called _roles_ and concept expression of the
form $B$ are _basic concepts_. We further require that all object variables
are _safe_ , that is, if they occur on the right side of a concept/role
inclusion or in a specifier associated with a set variable occurring on the
right side then they must also occur on the left side of the inclusion (or in
a specifier associated with a set variable occurring on the left).

A DL-Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ _ontology_ is a set of DL-
Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ assertions, role and concept
inclusions. We say that an inclusion is _positive_ if it does not contain
negation or $\bot$. Also, we say that a DL-
Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ ontology is _ground_ if it does not
contain variables. To simplify notation, we omit the specifier
$\lfloor\rfloor$ (meaning “any annotation set”) in role or concept
expressions. In this sense, any DL-Lite${}^{\mathcal{H}}_{\mathit{horn}}$
axiom is also a DL-Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ axiom. Moreover,
we omit prefixes of the form ${X}\,{\boldsymbol{:}}\,{\lfloor\ \rfloor}$,
which state that there is no restriction on $X$.

Semantics.  An _interpretation_ $\mathcal{I}=({\Delta^{\mathcal{I}}_{{\sf
i}},\Delta^{\mathcal{I}}_{{\sf a}},\cdot^{\mathcal{I}}})$ of an attributed DL
consists of a non-empty domain $\Delta^{\mathcal{I}}_{{\sf i}}$ of
individuals, a non-empty domain $\Delta^{\mathcal{I}}_{{\sf a}}$ of
annotations, and a function $\cdot^{\mathcal{I}}$. Individual names
$a\in\mathsf{N_{i}}$ are interpreted as elements
$a^{\mathcal{I}}\in\Delta^{\mathcal{I}}_{{\sf i}}$ and individual names
$a\in\mathsf{N_{a}}$ are interpreted as elements
$a^{\mathcal{I}}\in\Delta^{\mathcal{I}}_{{\sf a}}$. To interpret annotation
sets, we use the set
$\Phi^{\mathcal{I}}\coloneqq\\{\Sigma\subseteq\Delta^{\mathcal{I}}_{{\sf
a}}\times\Delta^{\mathcal{I}}_{{\sf a}}\mid\Sigma\text{ is finite}\\}$ of all
finite binary relations over $\Delta^{\mathcal{I}}_{{\sf a}}$. Each concept
name $A\in\mathsf{N_{C}}$ is interpreted as a set
$A^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}_{{\sf
i}}\times\Phi^{\mathcal{I}}$ of elements with annotations, and each role name
$R\in\mathsf{N_{R}}$ is interpreted as a set
$R^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}_{{\sf
i}}\times\Delta^{\mathcal{I}}_{{\sf i}}\times\Phi^{\mathcal{I}}$ of pairs of
elements with annotations. Each element (pair of elements) may appear with
multiple different annotations. $\mathcal{I}$ _satisfies_ a concept assertion
$A(a)@[a_{1}\kern 0.6pt{:}\,v_{1},\dotsc,a_{n}\kern 0.6pt{:}\,v_{n}]$ if
$({a^{\mathcal{I}},\\{({a_{1}^{\mathcal{I}},v_{1}^{\mathcal{I}}}),\ldots,({a_{n}^{\mathcal{I}},v_{n}^{\mathcal{I}}})\\}})\in
A^{\mathcal{I}}$. Role assertions are interpreted analogously. Expressions
with free set or object variables are interpreted using variable assignments
$\mathcal{Z}$ mapping object variables $x\in\mathsf{N_{V}}$ to elements
$\mathcal{Z}(x)\in\Delta^{\mathcal{I}}_{{\sf a}}$ and set variables
$X\in\mathsf{N_{U}}$ to finite binary relations
$\mathcal{Z}(X)\in\Phi^{\mathcal{I}}$. For convenience, we also extend
variable assignments to individual names, setting
$\mathcal{Z}(a)=a^{\mathcal{I}}$ for every $a\in\mathsf{N_{a}}$. A specifier
$S\in\mathbf{S}$ is interpreted as a set
$S^{\mathcal{I},\mathcal{Z}}\subseteq\Phi^{\mathcal{I}}$ of matching
annotation sets. We set
$X^{\mathcal{I},\mathcal{Z}}\coloneqq\\{\mathcal{Z}(X)\\}$ for variables
$X\in\mathsf{N_{U}}$. The semantics of closed specifiers is defined as:

  * •

$[a\kern
0.6pt{:}\,v]^{\mathcal{I},\mathcal{Z}}\coloneqq\\{\\{({a^{\mathcal{I}},\mathcal{Z}(v)})\\}\\}$
where $v\in\mathsf{N_{a}}\cup\mathsf{N_{V}}$;

  * •

$[a\kern
0.6pt{:}\,X.b]^{\mathcal{I},\mathcal{Z}}\coloneqq\\{\\{({a^{\mathcal{I}},\delta})\mid({b^{\mathcal{I}},\delta})\in\mathcal{Z}(X)\\}\\}$;

  * •

$[a_{1}\kern 0.6pt{:}\,v_{1},\dotsc,a_{n}\kern
0.6pt{:}\,v_{n}]^{\mathcal{I},\mathcal{Z}}\coloneqq\\{\bigcup_{i=1}^{n}F_{i}\\}$
where $\\{F_{i}\\}=[a_{i}\kern 0.6pt{:}\,v_{i}]^{\mathcal{I},\mathcal{Z}}$ for
all $1\leq i\leq n$.

$S^{\mathcal{I},\mathcal{Z}}$ therefore is a singleton set for variables and
closed specifiers. For open specifiers, however, we define $\lfloor a_{1}\kern
0.6pt{:}\,v_{1},\dotsc,a_{n}\kern
0.6pt{:}\,v_{n}\rfloor^{\mathcal{I},\mathcal{Z}}$ to be the set:

$\\{F\subseteq\Phi^{\mathcal{I}}\mid F\supseteq G\text{ for
}\\{G\\}=[a_{1}\kern 0.6pt{:}\,v_{1},\dotsc,a_{n}\kern
0.6pt{:}\,v_{n}]^{\mathcal{I},\mathcal{Z}}\\}.$

Now given $A\in\mathsf{N_{C}}$, $R\in\mathsf{N_{R}}$, and $S\in\mathbf{S}$, we
define:

$\displaystyle(A@S)^{\mathcal{I},\mathcal{Z}}$
$\displaystyle\coloneqq\\{\delta\mid({\delta,F})\in A^{\mathcal{I}}\text{ for
some }F\in S^{\mathcal{I},\mathcal{Z}}\\},$
$\displaystyle(R@S)^{\mathcal{I},\mathcal{Z}}$
$\displaystyle\coloneqq\\{({\delta,\epsilon})\mid({\delta,\epsilon,F})\in
R^{\mathcal{I}}\text{ for some }F\in S^{\mathcal{I},\mathcal{Z}}\\}.$

Further DL expressions are defined as:
$(R^{-}@S)^{\mathcal{I},\mathcal{Z}}\coloneqq\\{(\gamma,\delta)\mid({\delta,\gamma})\in(R@S)^{\mathcal{I},\mathcal{Z}}\\}$,
$\neg P^{\mathcal{I},\mathcal{Z}}\coloneqq(\Delta^{\mathcal{I}}_{{\sf
i}}\times\Delta^{\mathcal{I}}_{{\sf i}})\setminus
P^{\mathcal{I},\mathcal{Z}}$, $\exists
P^{\mathcal{I},\mathcal{Z}}\coloneqq\\{\delta\mid\text{there is
}({\delta,\epsilon})\in P^{\mathcal{I},\mathcal{Z}}\\}$, $(B_{1}\sqcap
B_{2})^{\mathcal{I},\mathcal{Z}}\coloneqq B^{\mathcal{I},\mathcal{Z}}_{1}\cap
B^{\mathcal{I},\mathcal{Z}}_{2}$,
$\bot^{\mathcal{I},\mathcal{Z}}\coloneqq\emptyset$. $\mathcal{I}$ _satisfies_
a concept inclusion of the form (3) if, for all variable assignments
$\mathcal{Z}$ that satisfy $\mathcal{Z}(X_{i})\in
S^{\mathcal{I},\mathcal{Z}}_{i}$ for all $1\leq i\leq n$, we have
$(\bigsqcap_{i=1}^{k}B_{i})^{\mathcal{I},\mathcal{Z}}\subseteq
C^{\mathcal{I},\mathcal{Z}}$. Satisfaction of role inclusions is defined
analogously. An interpretation $\mathcal{I}$ satisfies an ontology
$\mathcal{O}$, or is a _model_ of $\mathcal{O}$, if it satisfies all of its
axioms. As usual, $\models$ denotes the induced logical entailment relation.

For ground specifiers $\\{S,T\\}\subseteq\mathbf{S}$, we write $S\Rightarrow
T$ if $T$ is an open specifier, and the set of attribute-value pairs $a:b$ in
$S$ is a superset of the set of attribute-value pairs in $T$.

###  2.2 Geometric Models

We now define the geometric interpretations of attributed relations. Let $m$
be an integer and
$f:\mathbb{R}^{m}\times\mathbb{R}^{m}\mapsto\mathbb{R}^{2\cdot m}$ be a fixed
but arbitrary linear map satisfying the following:

  1. (i)

the restriction of $f$ to $\mathbb{R}^{m}\times\\{0\\}^{m}$ is injective;

  2. (ii)

the restriction of $f$ to $\\{0\\}^{m}\times\mathbb{R}^{m}$ is injective;

  3. (iii)

$f(\mathbb{R}^{m}\times\\{0\\}^{m})\cap
f(\\{0\\}^{m}\times\mathbb{R}^{m})=\\{0^{2\cdot m}\\}$;

where $0^{m}$ denotes the vector $(0,\ldots,0)$ with $m$ zeros. Intuitively,
individuals will be interpreted as vectors from $\mathbb{R}^{m}$ and $f$ will
be used to combine two vectors to interpret pairs of individuals.

######  Definition 1 (Geometric Interpretation)

An $m$-dimensional $f$-geometric interpretation $\eta$ of
$(\mathsf{N_{C}},\mathsf{N_{R}},\mathsf{N_{i}},\mathsf{N_{a}})$ assigns

  * •

to each $A\in\mathsf{N_{C}}$ and ground $S\in\mathbf{S}$ a region
$\eta(A@S)\subseteq\mathbb{R}^{m}$,

  * •

to each $R\in\mathsf{N_{R}}$ and ground $S\in\mathbf{S}$ a region
$\eta(R@S)\subseteq\mathbb{R}^{2\cdot m}$, and

  * •

to each $a\in\mathsf{N_{i}}$ a vector $\eta(a)\in\mathbb{R}^{m}$.

Moreover, for all $\\{S,T\\}\subseteq\mathbf{S}$ and
$E\in\mathsf{N_{C}}\cup\mathsf{N_{R}}$, if $S\Rightarrow T$ then
$\eta(E@S)\subseteq\eta(E@T)$. We say that $\eta$ is _convex_ if, for every
$E\in\mathsf{N_{C}}\cup\mathsf{N_{R}}$, every ground $S\in\mathbf{S}$, every
$\boldsymbol{v}_{1},\boldsymbol{v}_{2}\in\eta(E@S)$, and every
$\lambda\in[0,1]$, if $\boldsymbol{v}_{1},\boldsymbol{v}_{2}\in\eta(E@S)$ then
$(1-\lambda)\boldsymbol{v}_{1}+\lambda\boldsymbol{v}_{2}\in\eta(E@S)$.

The interpretation of ground complex concept or role expressions is as
follows. Assume all specifiers occurring in expressions below are ground,
$R\in\mathsf{N_{R}}$, $P$ is a role, and $B,B_{i}$ are basic concepts. Then,

  * •

$\eta(R^{-}@S)\coloneqq\\{f(\delta,\delta^{\prime})\mid
f(\delta^{\prime},\delta)\in\eta(R@S)\\}$,

  * •

$\eta(\neg P)\coloneqq\mathbb{R}^{2\cdot m}\setminus\eta(P)$,

  * •

$\eta(\exists
P)\coloneqq\\{\delta\mid\exists\delta^{\prime},f(\delta,\delta^{\prime})\in\eta(P)\\}$,

  * •

$\eta(\bigsqcap_{i=1}^{n}B_{i})\coloneqq\bigcap_{i=1}^{n}\eta(B_{i})$,

  * •

$\eta(\bot)\coloneqq\emptyset$.

We may omit “of
$(\mathsf{N_{C}},\mathsf{N_{R}},\mathsf{N_{i}},\mathsf{N_{a}})$” when we speak
about $m$-dimensional $f$-geometric interpretations. The interest of geometric
interpretations is that concept and role assertions translate into membership
in geometric regions and ground concept or role inclusions translate into
geometric inclusions.

######  Definition 2 (Satisfaction of Ground Axioms)

An $m$-dimensional $f$-geometric interpretation $\eta$ satisfies

  * •

a concept assertion $A(a)@S$, denoted $\eta\models A(a)@S$, if
$\eta(a)\in\eta(A@S)$;

  * •

a role assertion $R(a,b)@S$, denoted $\eta\models R(a,b)@S$, if
$f(\eta(a),\eta(b))\in\eta(R@S)$;

  * •

a ground role inclusion $P\sqsubseteq Q$, denoted $\eta\models P\sqsubseteq
Q$, if $\eta(P)\subseteq\eta(Q)$;

  * •

a ground concept inclusion $\bigsqcap_{i=1}^{n}B_{i}\sqsubseteq C$, denoted
$\eta\models\bigsqcap_{i=1}^{n}B_{i}\sqsubseteq C$, if we have that
$\eta(\bigsqcap_{i=1}^{n}B_{i})\subseteq\eta(C)$.

We are ready for the first theorem which establishes that our more general
notion of geometric models still has the same properties of the geometric
models originally proposed [13].

###### Theorem 2.1

Let $\eta$ be an $m$-dimensional $f$-geometric interpretation. For every
linear map $f^{\prime}$ satisfying (i)-(iii), the $m$-dimensional
$f^{\prime}$-geometric interpretation $\eta^{\prime}$ defined as:

  * •

$\eta^{\prime}(a):=\eta(a)$, for all $a\in\mathsf{N_{i}}$;

  * •

$\eta^{\prime}(A@S):=\eta(A@S)$, for all $A\in\mathsf{N_{C}}$ and ground
$S\in\mathbf{S}$; and

  * •

$\eta^{\prime}(R@S):=\\{f^{\prime}(\delta,\delta^{\prime})\mid
f(\delta,\delta^{\prime})\in\eta(R@S)\\}$, for all $R\in\mathsf{N_{R}}$ and
ground $S\in\mathbf{S}$;

is such that $\eta\models\alpha$ iff $\eta^{\prime}\models\alpha$, for all
ground axioms $\alpha$.

######  Proof (Sketch)

This result follows from the fact that there is an isomorphism between the
regions in $\eta$ and $\eta^{\prime}$.

To define when a geometric interpretation is a model of a (possibly not
ground) DL-Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ ontology, we need to
define when such an interpretation satisfies non-ground concept or role
inclusions. To do so, we use a standard interpretation built from the
geometric interpretation. Given a ground specifier $S$ and an annotation name
$\star$, we define $F^{\star}_{S}=\\{(a,b)\mid a\kern 0.6pt{:}\,b\text{ occurs
in }S\\}\cup\\{(\star,\star)\mid\text{if }S\text{ is open}\\}$. Given an
$m$-dimensional $f$-geometric interpretation $\eta$, a subset $D_{\sf a}$ of
$\mathsf{N_{a}}$ and an annotation name $\star\in\mathsf{N_{a}}\setminus
D_{\sf a}$, we define an interpretation $\mathcal{I}(\eta,D^{\star}_{\sf a})$
as follows.

  * •

$\Delta^{\mathcal{I}(\eta,D^{\star}_{\sf a})}_{\sf i}=\mathbb{R}^{m}$ and, for
all $a\in\mathsf{N_{i}}$, $a^{\mathcal{I}(\eta,D^{\star}_{\sf a})}=\eta(a)$;

  * •

$\Delta^{\mathcal{I}(\eta,D^{\star}_{\sf a})}_{\sf a}=\mathsf{N_{a}}$ and for
all $a\in\mathsf{N_{a}}$, $a^{\mathcal{I}(\eta,D^{\star}_{\sf a})}=a$;

  * •

$A^{\mathcal{I}(\eta,D^{\star}_{\sf
a})}=\\{(\delta,F^{\star}_{S})\mid\delta\in\eta(A@S),S\text{ built on }D_{\sf
a}\\}$, for all $A\in\mathsf{N_{C}}$;

  * •

$R^{\mathcal{I}(\eta,D^{\star}_{\sf
a})}=\\{(\delta,\epsilon,F^{\star}_{S})\mid
f(\delta,\epsilon)\in\eta(R@S),S\text{ built on }D_{\sf a}\\}$, for all
$R\in\mathsf{N_{R}}$.

The next proposition shows that $\eta$ and $\mathcal{I}(\eta,D^{\star}_{\sf
a})$ satisfy the same ground axioms built using only annotation names from
$D_{\sf a}$. It follows in particular that $\eta$ satisfies all ground axioms
of an ontology $\mathcal{O}$ iff
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})$
does, where $\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$ is the set of
annotation names from $\mathsf{N_{a}}$ that occur in $\mathcal{O}$.

######  Theorem 2.2 ()

Let $\eta$ be an $m$-dimensional $f$-geometric interpretation. Let $\alpha$ be
a ground axiom, i.e., $\alpha$ is either a concept/role assertion or a ground
concept/role inclusion. Let $D_{\alpha}$ be the set of annotation names that
occur in $\alpha$ and let $D$ be a subset of $\mathsf{N_{a}}$ such that
$D_{\alpha}\subseteq D$. Let $\star$ be an annotation name that does not occur
in $D$. Then, the following holds: $\eta\models\alpha$ iff
$\mathcal{I}(\eta,D^{\star})\models\alpha$.

######  Proof (Sketch)

The proof relies heavily on the definition of $F^{\star}_{S}$ and the
requirement that $\eta(E@S)\subseteq\eta(E@T)$ when $S\Rightarrow T$ in
Definition 1.

We are now ready to define geometric models of DL-
Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ ontologies.

######  Definition 3 (Geometric Model)

Let $\mathcal{O}$ be a DL-Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ ontology,
and let $\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$ be the set of
annotation names from $\mathsf{N_{a}}$ that occur in $\mathcal{O}$ and $\star$
an annotation name that does not occur in $\mathcal{O}$. An $m$-dimensional
$f$-geometric interpretation $\eta$ is a model of $\mathcal{O}$ if
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})$ is
a model of $\mathcal{O}$.

##  3 Satisfiability and Convex Geometric Models

We start by recalling some definitions and results on geometric
interpretations of an ontology containing existential rules [13]. An
existential rule is an expression of the form $B_{1}\wedge\dots\wedge
B_{n}\rightarrow\exists X_{1},\dots,X_{j}.H$ where $n\geq 0$, the $B_{i}$’s
and $H$ are atoms built from sets of predicates, constants and variables, and
the $X_{i}$’s are variables. A negative constraint is a rule whose head is
$\bot$. An existential rule or negative constraint is _quasi-chained_ if for
all $1\leq i\leq n$, $|({\sf vars}(B_{1})\cup\dots\cup{\sf
vars}(B_{i-1}))\cap{\sf vars}(B_{i})|\leq 1$, where ${\sf vars}(B)$ denotes
the variables that occur in $B$. It is easy to see that a DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontology without negative role
inclusions can be translated into a quasi-chained ontology. Negative role
inclusions are not quasi-chained: their translation to rules is indeed of the
form $P_{1}(x,y)\wedge P_{2}(x,y)\rightarrow\bot$ where the body atoms share
two variables. A (standard) model $\mathcal{M}$ of an existential rules
ontology $\mathcal{K}$ is a set of facts that contains all facts from
$\mathcal{K}$ and satisfies all existential rules from $\mathcal{K}$. In this
setting, for every fact $\alpha$, $\alpha\in\mathcal{M}$ iff
$\mathcal{M}\models\alpha$.

Given a set $\mathcal{R}$ of relation names and a set $X$ of constants and
labelled nulls, a $m$-dimensional geometric interpretation $\eta$ of
$(\mathcal{R},X)$ assigns to each $k$-ary relation $R$ from $\mathcal{R}$ a
region $\eta(R)\subseteq\mathbb{R}^{k.m}$ and to each object $o$ from $X$ a
vector $\eta(o)\in\mathbb{R}^{m}$. Tuples of individuals are interpreted using
vectors concatenation, which plays the role of the linear map $f$ we use to
interpret a pair of individuals: for every $R\in\mathcal{R}$ and
$o_{1},\dots,o_{k}\in X$, $\eta\models R(o_{1},\dots,o_{k})$ if
$\eta(o_{1})\oplus\dots\oplus\eta(o_{k})\in\eta(R)$. The authors define

$\Phi(\eta)=\\{R(o_{1},\dots,o_{k})\mid R\in\mathcal{R},o_{1},\dots,o_{k}\in
X,\eta\models R(o_{1},\dots,o_{k})\\}.$

Proposition 3 in [13] states that if $\mathcal{K}$ is a quasi-chained ontology
and $\mathcal{M}$ is a finite model of $\mathcal{K}$, then $\mathcal{K}$ has a
convex geometric model $\eta$ such that $\Phi(\eta)=\mathcal{M}$. This
transfers to the DL setting as follows. Let $\mathcal{O}$ be a quasi-chained
DL ontology and $\mathcal{J}$ be a finite model of $\mathcal{O}$ such that
$\Delta^{\mathcal{J}}=\mathsf{N_{i}}$, and $a^{\mathcal{J}}=a$ for every
$a\in\mathsf{N_{i}}$ (which implies that for every concept $A$, if $\delta\in
A^{\mathcal{J}}$, then $\mathcal{J}\models A(\delta)$, and similarly for
roles). Then $\mathcal{O}$ has a convex geometric model $\eta$ such that

$\\{E(\boldsymbol{t})\mid\eta\models
E(\boldsymbol{t})\\}=\\{E(\boldsymbol{t})\mid\mathcal{J}\models
E(\boldsymbol{t})\\},$

where $E\in\mathsf{N_{C}}\cup\mathsf{N_{R}}$ and $\boldsymbol{t}$ is a tuple
with the arity of $E$. In the following, we may similarly write
$E(\boldsymbol{t})@S$ to refer to an atom of the form $A(a)@S$ or $R(a,b)@S$.

######  Theorem 3.1 ()

Let $\mathcal{O}$ be a satisfiable DL-Lite${}^{\mathcal{H},@}_{\mathit{horn}}$
ontology without negative role inclusions. $\mathcal{O}$ has a convex
geometric model.

######  Proof (Sketch)

We use grounding to translate $\mathcal{O}$ into an equisatisfiable DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontology. Since $\mathcal{O}$ does not
contain negative role inclusion, the obtained DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontology is quasi-chained. We can thus
apply the result by Gutiérrez-Basulto and Schockaert [13] to get a convex
$m$-dimensional $f$-geometric model with $f$ being vector concatenation. This
geometric model is used to construct a geometric model of $\mathcal{O}$.

##  4 Adding Time

In this section, we discuss the ability of convex geometric models to capture
temporally attributed DLs. We show that we need to restrict the expressivity
of the temporal ontology to get a convex geometric model.

We introduce temporally attributed DLs by defining temporally attributed DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$, called DL-
Lite${}^{\mathcal{H},\mathbb{T},@}_{\mathit{horn}}$, as in [22]. The
description logic DL-Lite${}^{\mathcal{H},\mathbb{T},@}_{\mathit{horn}}$ is
defined as a multi-sorted version of DL-
Lite${}^{\mathcal{H},@}_{\mathit{horn}}$, where time points and intervals are
seen as datatypes. _Time points_ are elements of $\mathsf{N_{T}}$, and _time
intervals_ are elements of $\mathsf{N^{2}_{T}}$. These sets and the set of
_(abstract) individual names_ $\mathsf{N_{I}}$ are mutually disjoint. Time
points are represented in a discrete manner by natural numbers, and we assume
that elements of $\mathsf{N_{T}}$ ($\mathsf{N^{2}_{T}}$) are (pairs of)
numbers. A pair of numbers $k,\ell$ in $\mathsf{N^{2}_{T}}$ is denoted
$[k,\ell]$.

The annotation names: ${\sf time},{\sf before},{\sf after},{\sf until},{\sf
since},{\sf during},{\sf between}\in\mathsf{N_{a}}$ are called _temporal
attributes_ and have their own semantics. Basically, ${\sf time}$ is used to
mark a point in time and ${\sf before}$ and ${\sf after}$ refer to _some_
point in the past and in the future, respectively. The temporal attributes
${\sf until}$ and ${\sf since}$ refer to _all_ points in the past and all
point in the future (e.g. ${\sf since}$ $2020$ the KR conference became an
annual event). Finally, ${\sf during}$ is an interval which represents a
period of time (it refers to all points in the interval) and ${\sf between}$
is an interval of uncertainty for when an event happened. The _value type_ of
${\sf time},{\sf before},{\sf after},{\sf until},{\sf since}$ is
$\mathsf{N_{T}}$, while the value type of ${\sf during},{\sf between}$ is
$\mathsf{N^{2}_{T}}$. We write ${\sf valtype}(a)$ to refer to the value type
of the annotation name $a$. Object variables are now taken from pairwise
disjoint sets ${\sf Var}(\mathsf{N_{a}})$, ${\sf Var}(\mathsf{N_{T}})$, and
${\sf Var}(\mathsf{N^{2}_{T}})$.

Annotation set specifiers are defined as in Section 2.1 with the difference
that for each $a_{i}\in\mathsf{N_{a}}$ and each $v_{i}$ in attribute value
pair $a_{i}:v_{i}$ we require compatibility between the value type of its
attribute, that is:

  * •

$v_{i}\in{\sf valtype}(a_{i})\cup{\sf Var}({\sf valtype}(a_{i}))$, or

  * •

$v_{i}=[v,w]$ with ${\sf valtype}(a_{i})=\mathsf{N^{2}_{T}}$ and $v,w$ in
$\mathsf{N_{T}}\cup{\sf Var}(\mathsf{N_{T}})$, or

  * •

$v_{i}=X.b$ with $X\in\mathsf{N_{U}}$, $b\in\mathsf{N_{a}}$, and ${\sf
valtype}(a_{i})={\sf valtype}(b)$.

A _time-sorted interpretation_ $\mathcal{I}=({\Delta^{\mathcal{I}}_{\sf
i},\Delta^{\mathcal{I}}_{\sf a},\cdot^{\mathcal{I}}})$ is an interpretation
with a domain $\Delta^{\mathcal{I}}_{\sf a}$ that is a disjoint union of
$\Delta^{\mathcal{I}}_{A}\cup\Delta^{\mathcal{I}}_{T}\cup\Delta^{\mathcal{I}}_{2T}$,
where $\Delta^{\mathcal{I}}_{A}$ is the _abstract domain of annotations_ ,
$\Delta^{\mathcal{I}}_{T}$ (the _temporal domain_) is a finite or infinite
interval, and
$\Delta^{\mathcal{I}}_{2T}=\Delta^{\mathcal{I}}_{T}\times\Delta^{\mathcal{I}}_{T}$.
We interpret individual names in $\mathsf{N_{i}}$ as elements in
$\Delta^{\mathcal{I}}_{\sf i}$; annotation names in $\mathsf{N_{a}}$ as
elements in $\Delta^{\mathcal{I}}_{A}$; time points $t\in\mathsf{N_{T}}$ as
$t^{\mathcal{I}}\in\Delta^{\mathcal{I}}_{T}$; and intervals
$[t,t^{\prime}]\in\mathsf{N^{2}_{T}}$ as
$[t,t^{\prime}]^{\mathcal{I}}=(t^{\mathcal{I}},t^{\prime\mathcal{I}})\in\Delta^{\mathcal{I}}_{2T}$.
A pair
$({\delta,\epsilon})\in\Delta^{\mathcal{I}}_{A}\times\Delta^{\mathcal{I}}_{\sf
a}$ is _well-typed_ , if:

  1. 1.

$\delta=a^{\mathcal{I}}$ for an attribute ‘$a$’ of value type $\mathsf{N_{T}}$
and $\epsilon\in\Delta^{\mathcal{I}}_{T}$; or

  2. 2.

$\delta=a^{\mathcal{I}}$ for an attribute ‘$a$’ of value type
$\mathsf{N^{2}_{T}}$ and $\epsilon\in\Delta^{\mathcal{I}}_{2T}$; or

  3. 3.

$\delta=a^{\mathcal{I}}$ for an attribute ‘$a$’ of value type $\mathsf{N_{a}}$
and $\epsilon\in\Delta^{\mathcal{I}}_{A}$.

Let $\Phi^{\mathcal{I}}$ be the set of all finite sets of well-typed pairs.
The function $\cdot^{\mathcal{I}}$ maps concept names $A\in\mathsf{N_{C}}$ to
$A^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}_{\sf i}\times\Phi^{\mathcal{I}}$
and role names $R\in\mathsf{N_{R}}$ to
$R^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}_{\sf
i}\times\Delta^{\mathcal{I}}_{\sf i}\times\Phi^{\mathcal{I}}$. The semantics
of terms is given by variable assignments, which for a time-sorted
interpretation $\mathcal{I}$ is defined as a function $\mathcal{Z}$ that maps

  * •

set variables $X\in\mathsf{N_{U}}$ to finite binary relations
$\mathcal{Z}(X)\in\Phi^{\mathcal{I}}$, and

  * •

object variables $x\in{\sf Var}(\mathsf{N_{I}})\cup{\sf
Var}(\mathsf{N_{T}})\cup{\sf Var}(\mathsf{N^{2}_{T}})$ to elements
$\mathcal{Z}(x)\in\Delta^{\mathcal{I}}_{I}\cup\Delta^{\mathcal{I}}_{T}\cup\Delta^{\mathcal{I}}_{2T}$
(respecting their types).

For (set or object) variables $x$, we define
$x^{\mathcal{I},\mathcal{Z}}\coloneqq\mathcal{Z}(x)$, and for abstract
individuals, time points, or time intervals $a$, we define
$a^{\mathcal{I},\mathcal{Z}}\coloneqq a^{\mathcal{I}}$. The semantics of
specifiers is as in Section 2.1 with the difference that values can also be
time points and intervals:

  * •

$[a\kern
0.6pt{:}\,v]^{\mathcal{I},\mathcal{Z}}\coloneqq\\{\\{({a^{\mathcal{I}},v^{\mathcal{I},\mathcal{Z}}})\\}\\}$,
with $v\in\mathsf{valtype}(a)\cup{\sf Var}(\mathsf{valtype}(a))$;

  * •

$[a\kern
0.6pt{:}\,[v,w]]^{\mathcal{I},\mathcal{Z}}\coloneqq\\{\\{({a^{\mathcal{I}},(v^{\mathcal{I},\mathcal{Z}},w^{\mathcal{I},\mathcal{Z}})})\\}\\}$,
with $\mathsf{valtype}(a)=\mathsf{N^{2}_{T}}$, and
$v,w\in\mathsf{N_{T}}\cup{\sf Var}(\mathsf{N_{T}})$.

We are now ready to formally define the semantics of temporal attributes.

###### Definition 4

Consider a temporal domain $\Delta^{\mathcal{I}}_{T}$ and a domain
$\Delta^{\mathcal{I}}_{{\sf i}}$ of individuals and a domain
$\Delta^{\mathcal{I}}_{{\sf a}}$ of annotations, and let
$(\mathcal{I}_{i})_{i\in\Delta^{\mathcal{I}}_{T}}$ be a sequence of (non-
temporal) interpretations with domains $\Delta^{\mathcal{I}}_{{\sf i}}$ and
$\Delta^{\mathcal{I}}_{{\sf a}}$, such that, for all $a\in\mathsf{N_{I}}$, we
have $a^{\mathcal{I}_{i}}=a^{\mathcal{I}_{j}}$ for all
$i,j\in\Delta^{\mathcal{I}}_{T}$. We define a _global interpretation_ for
$(\mathcal{I}_{i})_{i\in\Delta^{\mathcal{I}}_{T}}$ as a time-sorted
interpretation $\mathcal{I}=({\Delta^{\mathcal{I}}_{{\sf
i}},\Delta^{\mathcal{I}}_{{\sf a}},\cdot^{\mathcal{I}}})$ as follows. Let
$a^{\mathcal{I}}=a^{\mathcal{I}_{i}}$ for all $a\in\mathsf{N_{I}}$. For any
finite set $F\in\Phi^{\mathcal{I}}$, let $F_{I}\coloneqq
F\cap(\Delta^{\mathcal{I}}_{A}\times\Delta^{\mathcal{I}}_{A})$ denote its
abstract part without any temporal attributes. For any $A\in\mathsf{N_{C}}$,
$\delta\in\Delta^{\mathcal{I}}_{{\sf i}}$, and $F\in\Phi^{\mathcal{I}}$ with
$F\setminus F_{I}\neq\emptyset$, we have $({\delta,F})\in A^{\mathcal{I}}$ if
and only if $({\delta,F_{I}})\in A^{\mathcal{I}_{i}}$ for some
$i\in\Delta^{\mathcal{I}}_{T}$, and the following conditions hold for all
$({a^{\mathcal{I}},x})\in F$:

  * •

if $a={\sf time}$, then $({\delta,F_{I}})\in A^{\mathcal{I}_{x}}$,

  * •

if $a={\sf before}$, then $({\delta,F_{I}})\in A^{\mathcal{I}_{j}}$ for some
$j<x$,

  * •

if $a={\sf after}$, then $({\delta,F_{I}})\in A^{\mathcal{I}_{j}}$ for some
$j>x$,

  * •

if $a={\sf until}$, then $({\delta,F_{I}})\in A^{\mathcal{I}_{j}}$ for all
$j\leq x$,

  * •

if $a={\sf since}$, then $({\delta,F_{I}})\in A^{\mathcal{I}_{j}}$ for all
$j\geq x$,

  * •

if $a={\sf between}$, then $({\delta,F_{I}})\in A^{\mathcal{I}_{j}}$ for some
$j\in[x]$,

  * •

if $a={\sf during}$, then $({\delta,F_{I}})\in A^{\mathcal{I}_{j}}$ for all
$j\in[x]$,

where $[x]$ for an element $x\in\Delta^{\mathcal{I}}_{2T}$ denotes the finite
interval represented by the pair of numbers $x$, and
$j\in\Delta^{\mathcal{I}}_{T}$. For roles $R\in\mathsf{N_{R}}$, we define
$({\delta,\epsilon,F})\in R^{\mathcal{I}}$ analogously.

######  Definition 5 (Temporal Geometric Interpretation)

A temporal $m$-dimensional $f$-geometric interpretation with temporal domain
$\Delta_{T}$ is a sequence $(\eta_{j})_{j\in\Delta_{T}}$ of $m$-dimensional
$f$-geometric interpretations. An $m$-dimensional $f$-geometric interpretation
$\eta$ is _global_ for $(\eta_{j})_{j\in\Delta_{T}}$ and $D_{\sf
a}\subseteq\mathsf{N_{a}}$ if $\mathcal{I}(\eta,(D_{\sf
a}\cup\mathsf{N_{T}}\cup\mathsf{N^{2}_{T}})^{\star})$ is global for
$(\mathcal{I}(\eta_{j},D^{\star}_{\sf a}))_{j\in\Delta_{T}}$.

Let $\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$ denote the union of all
elements in $\mathsf{N_{a}}$, $\mathsf{N_{T}}$, and $\mathsf{N^{2}_{T}}$
occurring in $\mathcal{O}$.

######  Definition 6 (Geometric Model)

Let $\mathcal{O}$ be a DL-Lite${}^{\mathcal{H},\mathbb{T},@}_{\mathit{horn}}$
ontology. An $f$-geometric interpretation $\eta$ is an $m$-dimensional
$f$-geometric model of $\mathcal{O}$ if it is global for a sequence
$(\eta_{j})_{j\in\Delta_{T}}$ of $m$-dimensional $f$-geometric interpretations
and $\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$, plus
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})$
satisfies $\mathcal{O}$.

Example 1 shows that even if temporal specifiers are only of the form ${\sf
time}$ and ${\sf during}$, convex geometric models may not exist for
satisfiable DL-Lite${}^{\mathcal{H},\mathbb{T},@}_{\mathit{horn}}$ ontologies.

###### Example 1

Let

$\displaystyle\mathcal{O}=$ $\displaystyle\\{\exists R@[{\sf during}\kern
0.6pt{:}\,[1,2]]\sqsubseteq A,\exists R@[{\sf time}\kern 0.6pt{:}\,1]\sqcap
A\sqsubseteq\bot,$ $\displaystyle R(a,a)@[{\sf time}\kern
0.6pt{:}\,1],R(b,b)@[{\sf time}\kern 0.6pt{:}\,1],R(a,b)@[{\sf time}\kern
0.6pt{:}\,2],R(b,a)@[{\sf time}\kern 0.6pt{:}\,2]\\}$

and let $\eta$ be a convex $f$-geometric model of $\mathcal{O}$. Let
$\delta=0.5\eta(a)+0.5\eta(b)$. By the convexity of $\eta(R@[{\sf time}\kern
0.6pt{:}\,1])$ and $\eta(R@[{\sf time}\kern 0.6pt{:}\,2])$, we have that

$\displaystyle f(\delta,\delta)\in\eta(R@[{\sf time}\kern 0.6pt{:}\,1])\text{
and }f(\delta,\delta)\in\eta(R@[{\sf time}\kern 0.6pt{:}\,2]),$

so
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})\models
R(\delta,\delta)@[{\sf time}\kern 0.6pt{:}\,1]$ and
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})\models
R(\delta,\delta)@[{\sf time}\kern 0.6pt{:}\,2]$. It follows that
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})\models
R(\delta,\delta)@[{\sf during}\kern 0.6pt{:}\,[1,2]]$. Since
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})\models
R@[{\sf during}\kern 0.6pt{:}\,[1,2]]\sqsubseteq A$, we also have that
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})\models
A(\delta)$. Hence
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})\not\models\exists
R@[{\sf time}\kern 0.6pt{:}\,1]\sqcap A\sqsubseteq\bot$. This means that
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})$ is
not a model of $\mathcal{O}$. $\triangleleft$

To overcome this problem, we introduce a restriction on the specifiers allowed
on roles. We introduce _atemporal specifiers_. An atemporal specifier is a
specifier $S$ that can only be interpreted as a set
$S^{\mathcal{I},\mathcal{Z}}\subseteq\Phi^{\mathcal{I}}$ of matching
annotation sets that do not contain any temporal attribute.

To show that convex geometric models can capture some DL-
Lite${}^{\mathcal{H},\mathbb{T},@}_{\mathit{horn}}$ ontologies, we use concept
inclusions with conjunctions on the left-hand side, which can be expressed in
DL-Lite${}^{\mathcal{H}}_{\mathit{horn}}$. The following example shows that
adding conjunction in role inclusions may however lead to satisfiable
ontologies not having a convex model, even for plain DLs.

###### Example 2

Assume role conjunctions are allowed in the ontology. Let

$\begin{array}[]{l}\mathcal{O}=\\{R_{1}\sqcap R_{2}\sqsubseteq R_{3},\exists
R_{1}\sqsubseteq A,\exists R_{3}\sqcap
A\sqsubseteq\bot,R_{1}(a,a),R_{1}(b,b),R_{2}(a,b),R_{2}(b,a)\\}\end{array}$

and let $\eta$ be a convex $f$-geometric model of $\mathcal{O}$. Let
$\delta=0.5\eta(a)+0.5\eta(b)$. By the convexity of $\eta(R_{1})$ and
$\eta(R_{2})$, we have that

$\displaystyle f(\delta,\delta)\in\eta(R_{1})\text{ and
}f(\delta,\delta)\in\eta(R_{2}),\text{ hence
}f(\delta,\delta)\in\eta(R_{1}\sqcap R_{2}).$

Then since $\eta$ is a model of $R_{1}\sqcap R_{2}\sqsubseteq R_{3}$,
$f(\delta,\delta)\in\eta(R_{3})$ so $\delta\in\eta(\exists R_{3})$. Moreover,
since $\eta$ is a model of $\exists R_{1}\sqsubseteq A$, and
$\delta\in\eta(\exists R_{1})$, $\delta\in\eta(A)$. Hence
$\eta\not\models\exists R_{3}\sqcap A\sqsubseteq\bot$ so $\eta$ is not a model
of $\mathcal{O}$. $\triangleleft$

We now state the main result of this section, which states that, under certain
conditions, satisfiable DL-Lite${}^{\mathcal{H},\mathbb{T},@}_{\mathit{horn}}$
ontologies have a convex geometric model. The need of Condition (i) is already
illustrated by Example 1 whereas Condition (ii) ensures that the underlying
logic is Horn (that is, it does not have disjunctions which can be expressed
with the temporal attributes ${\sf before}$, ${\sf after}$ and ${\sf
between}$).

######  Theorem 4.1 ()

Let $\mathcal{O}$ be a satisfiable DL-
Lite${}^{\mathcal{H},\mathbb{T},@}_{\mathit{horn}}$ ontology without negative
role inclusions and such that (i) all specifiers attached to a role in
$\mathcal{O}$ are atemporal, and (ii) ${\sf before}$, ${\sf after}$ and ${\sf
between}$ do not occur in $\mathcal{O}$. Then $\mathcal{O}$ has a convex
geometric model.

##  5 Related Work

Traditionally, most KG embedding models are time-unaware. These models embed
both entities and relations in a low-dimensional latent space based on some
regularities of target KG. They can be used as approximate reasoning methods
[24, 23] for completing KG without using the schema. Typical embedding models
include the translation based models, such as TransE [7] and bilinear models,
such as ComplEx [28] and SimplE [15]. From the expressiveness perspective,
TransE and DisMult have been shown to be not fully expressive; however,
CompleEx and SimplE are fully expressive. Gutierrez-Basulto and Schockaert
[13] use geometric models to study the compatibility between TBox/ontology and
KG embeddings. They show that bilinear models (inc. ComplEx and SimplE) cannot
strictly represent relation subsumption rules. Wiharja et al. [29] show that
many well known KG embeddings based on KG completion methods are not
impressive, when schema aware correctness is considered, despite good
performance reported in silver standard based evaluations. Currently, more and
more applications are involving dynamic KG, where knowledge in practice is
time-variant and consists of sequences of observations. For example, in
recommendation systems based on KG, new items and new user actions appear in
real time. Accordingly, temporal KG embedding models incorporate time
information into their node and relation representations. We next discuss how
temporal information is taken into account in KG embeddings and how it has
been used in combination with classical DLs.

Temporal Knowledge Graph Embeddings.  Temporal KG embedding models can be seen
as extensions of static KG embedding models. A basic approach is to collapse
the dynamic graph into a static graph by aggregating the temporal observations
over time [18]. This approach, however, may lose large amounts of information.
An alternative approach is to give more weights to snapshots that are more
recent [27]. Another alternative approach to aggregating temporal observations
is to apply decomposition methods to dynamic graphs. The idea is to model a KG
as an order 4 tensor and decompose it using CP or Tucker, or other
decomposition methods to obtain entity, relation, and timestamp embeddings
[11]. In addition to aggregation based approaches, there are approaches
extending static KG embedding, such as TransE, by adding a timestamp embedding
into the score function [14, 20]. Jiang et al. [14] only use such timestamps
to maintain temporal order, while using Integer Linear Programming to encode
the temporal consistency information as constraints. Ma et al. [20] extend
several models (Tucker, RESCAL, HolE, ComplEx, DistMult) by adding a timestamp
embedding to their score functions. These models may not work well when the
number of timestamps is large. Furthermore, since they only learn embeddings
for observed timestamps, they cannot generalize to unseen timestamps. Dasgupta
et al. [10] fragments a temporally-scoped input KG into multiple static
subgraphs with each subgraph corresponding to a timestamp. There are also
approaches of applying random walk models for temporal KG. E.g., Bian et al
[6] use metapath2vec to generate random walks on both the initial KG and the
updated nodes and re-compute the embeddings for these nodes. These approaches
mainly leverage the temporal aspect of dynamic graphs to reduce the
computations. However, they may fail at capturing the evolution and the
temporal patterns of the nodes. Another natural choice for modeling temporal
KG is by extending sequence models to graph data. E.g., García-Duran [12]
extend TransE and DistMult by combining the relation and timestamp through a
character LSTM, so as to learn representations for time-augmented KG facts
that can be used in conjunction with existing scoring functions for link
prediction. Ma et al. [20] argue that temporal KG embeddings could also be
used as models for cognitive episodic memory (facts we remember and can
recollect) and for semantic memory (current facts we know) can be generated
from episodic memory by a marginalization operation.

Temporal Description Logics.  In the DL literature, there are several
approaches for representing and reasoning temporal information [19, 32, 5].
Schmiedel [26] was the first to propose an extension of the description logics
(the $\mathcal{FLENR^{-}}$ DL in this case) with an interval-based temporal
logic, with the temporal quantifier at, the existential and universal temporal
quantifiers sometime and alltime. Artale and Franconi [2, 3] considered a
class of interval-based temporal description logics by reducing the
expressivity to keep the property of decidability of the logic proposed by
Schmiedel [26]. Schild proposed $\mathcal{ALCT}$ [25], extending
$\mathcal{ALC}$ with point-based modal temporal connectives from tense logic
[9], including existential future ($\lozenge$), universal future ($\square$),
next instant ($\bigcirc$),until ($\mathcal{U}$), reflexive until (U). Wolter
and Zakharyaschev studied the $\mathcal{ALC_{M}^{-}}$ DL and showed that it is
decidable in the class of linear, discrete and unbounded temporal structures
[30]. They also showed that the $\mathcal{ALC_{M}}$ DL (extending the
$\mathcal{ALC_{M}^{-}}$ DL with global roles) is undecidable [31]. Temporal
operators can be used in a temporal ABox as well, allowing the use of next
instant ($\bigcirc\varphi$) and until ($\varphi\mathcal{U}\psi$) with ABox
assertions [4]. Ozaki et al. [21, 22] propose temporally attributed DLs, which
allows the use of absolute temporal information in both TBoxes and ABoxes.
They show that the satisfiability of ground $\mathcal{ELH^{\mathbb{T}}_{@}}$
ontologies is ExpTime-complete, and that the satisfiability of ground
$\mathcal{ELH^{\mathbb{T}}_{@}}$ ontologies without the temporal attributes
between, before and after is PTime-complete.

##  6 Conclusion

We investigate how geometric models can (or cannot) be used to capture rules
about annotated data expressed in the formalism of attributed DLs. We show
that every satisfiable attributed DL-Lite${}^{\mathcal{H}}_{\mathit{horn}}$
ontology has a convex geometric model and that this is also the case when
allowing the use of temporal attributes under some restrictions. There is
still a long way to make this result practical since we still require an
embedding technique that would construct such a model. In this direction, we
highlight the work of Abboud et al. [1], where relations are mapped to convex
regions in the format of hyper-rectangles.

Acknowledgements.  We thank Bruno Figueira Lourenço for his contribution on
the proof of Theorem 2.1. Ozaki is supported by the Norwegian Research
Council, grant number 316022.

## References

  * [1] Ralph Abboud, İsmail İlkan Ceylan, Thomas Lukasiewicz, and Tommaso Salvatori.  Boxe: A box embedding model for knowledge base completion.  In Proceedings of NeurIPS, 2020.
  * [2] A. Artale and E. Franconi.  A computational account for a description logic of time and action.  In Proceedings of KR, 1994.
  * [3] A. Artale and E. Franconi.  A temporal description logic for reasoning about actions and plans.  Journal of Artificial Intelligence Research, 9, 1998.
  * [4] Alessandro Artale, Roman Kontchakov, Carsten Lutz, Frank Wolter, and Michael Zakharyaschev.  Temporalising tractable description logics.  In Proceedings of TIME, 2007.
  * [5] Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, and Michael Zakharyaschev.  A cookbook for temporal conceptual data modelling with description logics.  ACM Trans. Comput. Log., 15(3):25:1–25:50, 2014.
  * [6] Ranran Bian, Yun Sing Koh, Gillian Dobbie, and Anna Divoli.  Network embedding and change modeling in dynamic heterogeneous networks.  In Proceedings of the of the 42nd International ACM SIGIR Conference on Research and Development in Information Retrieval, pages 861–864, 2019.
  * [7] Antoine Bordes, Nicolas Usunier, Alberto Garcia-Duran, Jason Weston, and Oksana Yakhnenko.  Translating embeddings for modeling multi-relational data.  In Advances in neural information processing systems, pages 2787–2795, 2013.
  * [8] Camille Bourgaux and Ana Ozaki.  Querying attributed DL-Lite ontologies using provenance semirings.  In Proceedings of AAAI , 2019.
  * [9] J.P. Burgess.  Basic tense logic.  In D. Gabbay and F. Guenther, editors, Handbook of Philosophical Logic, page 89–133. 1984.
  * [10] Shib Sankar Dasgupta, Swayambhu Nath Ray, and Partha Talukdar.  HyTE: Hyperplane-based temporally aware knowledge graph embedding.  In Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing, 2018.
  * [11] Cristobal Esteban, Volker Tresp, Yinchong Yang, Stephan Baier, and Denis Krompass.  Predicting the co-evolution of event and knowledge graphs.  In Proceedings of FUSION, 2016.
  * [12] Alberto García-Durán, Sebastijan Dumancic, and Mathias Niepert.  Learning sequence encoders for temporal knowledge graph completion.  In Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing, 2018.
  * [13] Víctor Gutiérrez-Basulto and Steven Schockaert.  From knowledge graph embedding to ontology embedding? an analysis of the compatibility between vector space representations and rules.  In Proceedings of KR, 2018.
  * [14] Tingsong Jiang, Tianyu Liu, Tao Ge, Lei Sha, Baobao Chang, Sujian Li, and Zhifang Sui.  Towards time-aware knowledge graph completion.  In Proceedings of COLING, 2016.
  * [15] Seyed Mehran Kazemi and David Poole.  Simple embedding for link prediction in knowledge graphs.  In Proceedings of NeurIPS, 2018.
  * [16] Markus Krötzsch, Maximilian Marx, Ana Ozaki, and Veronika Thost.  Attributed description logics: Ontologies for knowledge graphs.  In Proceedings of ISWC, 2017.
  * [17] Markus Krötzsch, Maximilian Marx, Ana Ozaki, and Veronika Thost.  Attributed description logics: Reasoning on knowledge graphs.  In Proceedings of IJCAI, 2018.
  * [18] David Liben-nowell and Jon Kleinberg.  The link-prediction problem for social networks.  J. AMERICAN SOCIETY FOR INFORMATION SCIENCE AND TECHNOLOGY, 2007\.
  * [19] Carsten Lutz, Frank Wolter, and Michael Zakharyaschev.  Temporal description logics: A survey.  In Proceedings of TIME, 2008.
  * [20] Yunpu Ma, Volker Tresp, and Erik A Daxberger.  Embedding models for episodic knowledge graphs.  Journal of Web Semantics, 59, 2018.
  * [21] Ana Ozaki, Markus Krötzsch, and Sebastian Rudolph.  Happy ever after: Temporally attributed description logics.  In Magdalena Ortiz and Thomas Schneider, editors, Proceedings of DL, 2018.
  * [22] Ana Ozaki, Markus Krötzsch, and Sebastian Rudolph.  Temporally attributed description logics.  In Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 2019.
  * [23] Jeff Z. Pan, Yuan Ren, and Yuting Zhao.  Tractable approximate deduction for OWL.  Artificial Intelligence, 235:95–155, 2016.
  * [24] Jeff Z. Pan and Edward Thomas.  Approximating OWL-DL Ontologies.  In Proceedings of AAAI, 2007.
  * [25] K.D. Schild.  Combining terminological logics with tense logic knowledge bases.  In Proceedings of EPIA, 1993.
  * [26] A. Schmiedel.  A temporal terminological logic.  In Proceedings of AAAI, 1990.
  * [27] Umang Sharan.  Temporal-relational classifiers for prediction in evolving domains.  In In Proceedings of the IEEE International Conference on Data Mining, 2008.
  * [28] Theo Trouillon, Christopher R. Dance, Eric Gaussier, Johannes Welbl, Sebastian Riedel, and Guillaume Bouchard.  Knowledge graph completion via complex tensor factorization.  J. Mach. Learn. Res., 18:130:1–130:38, 2017.
  * [29] Kemas Wiharja, Jeff Z. Pan, Martin J. Kollingbaum, and Yu Deng.  Schema Aware Iterative Knowledge Graph Completion.  Journal of Web Semantics, 2020.
  * [30] F. Wolter and M. Zakharyaschev.  Satisfiability problem in description logics with modal operators.  In Proceedings of KR, 1998.
  * [31] F. Wolter and M. Zakharyaschev.  Modal description logics: Modalizing roles.  In Fundamentae Informaticae, pages 411–438, 1999.
  * [32] Frank Wolter and Michael Zakharyaschev.  Temporalizing description logics.  Frontiers of Combining Systems, 2:379–402, 1999.

##  Appendix 0.A Proof of Theorem 3

Our definitions of geometric interpretations and models are based on the work
by Gutiérrez-Basulto and Schockaert [13]. The main difference is that in
Definition 1 we allow any kind of linear map that respects some conditions (in
particular, (i) to (iii)), instead of using vector concatenation for
representing tuples in the vector space. Here we show that our conditions for
the linear maps are harmless in the sense that all results obtained in the
mentioned work still hold with the more general conditions.

Let $f:\mathbb{R}^{m}\times\mathbb{R}^{n}\mapsto\mathbb{R}^{m+n}$ be a linear
map satisfying the following:

  1. (i)

the restriction of $f$ to $\mathbb{R}^{m}\times\\{0\\}^{n}$ is injective;

  2. (ii)

the restriction of $f$ to $\\{0\\}^{m}\times\mathbb{R}^{n}$ is injective;

  3. (iii)

$f(\mathbb{R}^{m}\times\\{0\\}^{n})\cap
f(\\{0\\}^{m}\times\mathbb{R}^{n})=\\{0^{m+n}\\}$;

where $0^{n}$ denotes the vector $(0,\ldots,0)$ with $n$ zeros.

###### Proposition 1

Any linear map satisfying (i), (ii), and (iii) is bijective.

###### Proof

Let $f$ be a linear map satisfying (i), (ii), and (iii).

###### Claim

The _kernel of $f$_ $\\{x\in\mathbb{R}^{m}\times\mathbb{R}^{n}\mid
f(x)=0^{m+n}\\}$ is equal to $\\{0^{m+n}\\}$.

Proof of the Claim. Suppose that $(x,y)$ belongs to the kernel of $f$, where
$x\in\mathbb{R}^{m}$ and $y\in\mathbb{R}^{n}$. Then, $f(x,y)=0^{m+n}$. Since
$f$ is a linear map, addition is preserved, so
$f(x,0^{n})+f(0^{m},y)=f(x,y)=0^{m+n}$. Because of (iii), we conclude that
$f(x,0^{n})=f(0^{m},y)=0^{m+n}$. By (i)-(ii), $x=0^{m}$ and $y=0^{n}$, as
required.

Suppose $f(x)=f(y)$. In other words, $0^{m+n}=f(x)-f(y)$. Since $f$ is a
linear map, $0^{m+n}=f(x)-f(y)=f(x-y)$. This means that $x-y$ is in the kernel
of $f$ and, by the Claim, $x-y=0^{m+n}$. Thus, $x=y$, which means that $f$ is
injective.

By the Claim, the dimension of the kernel of $f$ is $0$. Since the dimension
of the domain of $f$ is $m+n$, by the rank-nullity theorem, the dimension of
the image of $f$ must be $m+n$. This means that $f$ is also surjective. ∎

By Proposition 1, any linear map satisfying (i), (ii), and (iii) is bijective
and, by the next proposition, any such linear map could be used in the
formalisation as it would yield isomorphic regions. Given
$S\subseteq\mathbb{R}^{n}$, we denote by ${\sf co}(S)$ the convex hull of $S$.

###### Proposition 2

Let $f:\mathbb{R}^{m}\times\mathbb{R}^{n}\mapsto\mathbb{R}^{m+n}$ and
$g:\mathbb{R}^{m}\times\mathbb{R}^{n}\mapsto\mathbb{R}^{m+n}$ be bijective
linear maps. Let $h:=f\circ g^{-1}$. Then, for every
$S\subseteq\mathbb{R}^{m}\times\mathbb{R}^{n}$, we have

$h({\sf co}(f(S)))={\sf co}(g(S)).$

###### Proof

Let $S\subseteq\mathbb{R}^{m}\times\mathbb{R}^{n}$ and let $x\in{\sf
co}(f(S))$. Then, there are $\alpha_{1},\dots,\alpha_{k}\in[0,1]$ and
$s_{1},\ldots,s_{k}\in S$ such that

$x=\sum^{k}_{i=1}\alpha_{i}f(s_{i}),\qquad\sum^{k}_{i=1}\alpha_{i}=1.$

By definition of $h$ and its linearity, we have

$h(x)=\sum^{k}_{i=1}\alpha_{i}g(s_{i})$

therefore $h(x)\in{\sf co}(g(S))$. Conversely, if $x\in{\sf co}(g(S))$, an
analogous argument shows that $h^{-1}(x)\in f(S)$. This shows that, indeed,
$h({\sf co}(f(S)))={\sf co}(g(S))$. ∎

##  Appendix 0.B Proof of Theorem 4

See 2.2

###### Proof

We start with the case where $\alpha$ is a concept assertion.

  1. 1.

$\mathcal{I}(\eta,D^{\star})\models A(a)@S$ iff
$(a^{\mathcal{I}(\eta,D^{\star})},F)\in A^{\mathcal{I}(\eta,D^{\star})}$ for
some $F\in S^{\mathcal{I}(\eta,D^{\star})}$.

  2. 2.

$a^{\mathcal{I}(\eta,D^{\star})}=\eta(a)$.

  3. 3.

Since $S$ is closed, $S^{\mathcal{I}(\eta,D^{\star})}=\\{F^{\star}_{S}\\}$.

  4. 4.

It follows from (1), (2) and (3) that $\mathcal{I}(\eta,D^{\star})\models
A(a)@S$ iff $(\eta(a),F^{\star}_{S})\in A^{\mathcal{I}(\eta,D^{\star})}$.

  5. 5.

By definition of $\mathcal{I}(\eta,D^{\star})$, $(\eta(a),F^{\star}_{S})\in
A^{\mathcal{I}(\eta,D^{\star})}$ iff $\eta(a)\in\eta(A@S)$, i.e., $\eta\models
A(a)@S$.

The proof for the case where $\alpha$ is a role assertion is similar.

We next show the case where $\alpha$ is a concept inclusion, i.e., $\alpha$ is
either of the form $\bigsqcap_{i=1}^{n}B_{i}@S_{i}\sqsubseteq B@S$ or
$\bigsqcap_{i=1}^{n}B_{i}@S_{i}\sqsubseteq\bot$ where $B_{i}$ and $B$ are of
the form $A_{i}$ or $\exists P_{i}$.

Assume that $\mathcal{I}(\eta,D^{\star})\models\alpha$. Let
$\delta\in\mathbb{R}^{m}$ be such that
$\delta\in\eta(\bigsqcap_{i=1}^{n}B_{i}@S_{i})=\bigcap_{i=1}^{n}\eta(B_{i}@S_{i})$.
For $1\leq i\leq n$:

  1. 1.

$\delta\in\eta(B_{i}@S_{i})$ so $(\delta,F^{\star}_{S_{i}})\in
B_{i}^{\mathcal{I}(\eta,D^{\star})}$;

  2. 2.

$F^{\star}_{S_{i}}\in S_{i}^{{\mathcal{I}(\eta,D^{\star})},\mathcal{Z}}$ for
every variable assignment $\mathcal{Z}$;

  3. 3.

(1) and (2) implies that
$\delta\in(B_{i}@S_{i})^{{\mathcal{I}(\eta,D^{\star})},\mathcal{Z}}$ for every
variable assignment $\mathcal{Z}$.

It follows that
$\delta\in(\bigsqcap_{i=1}^{n}B_{i}@S_{i})^{{\mathcal{I}(\eta,D^{\star})},\mathcal{Z}}$.

  * •

Assume that $\alpha$ is of the form $\bigsqcap_{i=1}^{n}B_{i}@S_{i}\sqsubseteq
B@S$.

    1. 1.

Since $\mathcal{I}(\eta,D^{\star})\models\alpha$, then
$\delta\in(B@S)^{{\mathcal{I}(\eta,D^{\star})},\mathcal{Z}}$.

    2. 2.

Hence there exists $F\in S^{\mathcal{I},\mathcal{Z}}$ such that $(\delta,F)\in
B^{{\mathcal{I}(\eta,D^{\star})}}$.

    3. 3.

By definition of $B^{{\mathcal{I}(\eta,D^{\star})}}$, it follows that
$\delta\in\eta(B@S_{F})$ with $S_{F}$ a ground (closed or open) specifier that
contains exactly the pairs $a\kern 0.6pt{:}\,b$ such that $(a,b)$ are in $F$,
except $(\star,\star)$.

    4. 4.

By (2), $F\in S^{\mathcal{I},\mathcal{Z}}$ so the attribute-value pairs in
$S_{F}$ form a superset of those in $S$ and either $S_{F}=S$ if $S$ is closed,
or $S_{F}\Rightarrow S$ if $S$ is open. In both cases,
$\eta(B@S_{F})\subseteq\eta(B@S)$.

    5. 5.

By (3) and (4), $\delta\in\eta(B@S)$.

It follows that $\eta(\bigsqcap_{i=1}^{n}B_{i}@S_{i})\subseteq\eta(B@S)$

  * •

Assume that $\alpha$ is of the form
$\bigsqcap_{i=1}^{n}B_{i}@S_{i}\sqsubseteq\bot$. Since
$\mathcal{I}(\eta,D^{\star})\models\alpha$, then $\delta\in\emptyset$. This is
a contradiction so $\eta(\bigsqcap_{i=1}^{n}B_{i}@S_{i})$ must be empty. Hence

$\eta(\bigsqcap_{i=1}^{n}B_{i}@S_{i})\subseteq\eta(\bot).$

We conclude that $\eta\models\alpha$.

In the other direction, assume that $\eta\models\alpha$. Let
$\delta\in(\bigsqcap_{i=1}^{n}B_{i}@S_{i})^{\mathcal{I}(\eta,D^{\star})}=\bigcap_{i=1}^{n}B_{i}@S_{i}^{\mathcal{I}(\eta,D^{\star})}$.
For $1\leq i\leq n$:

  1. 1.

There exists $(\delta,F_{i})\in B_{i}^{\mathcal{I}(\eta,D^{\star})}$ such that
$F_{i}\in S_{i}^{\mathcal{I}(\eta,D^{\star}),\mathcal{Z}}$ (for any
$\mathcal{Z}$).

  2. 2.

By (1) and the definition of $\mathcal{I}(\eta,D^{\star})$,
$\delta\in\eta(B_{i}@T_{i})$ for some $T_{i}$ that contains exactly the
attribute value pairs in $F_{i}$, except $(\star,\star)$, and such that
$T_{i}$ is closed if $(\star,\star)\notin F_{i}$, and open otherwise.

  3. 3.

By (1), $F_{i}\in S_{i}^{\mathcal{I}(\eta,D^{\star}),\mathcal{Z}}$ so by
definition of $T_{i}$ in (2), it is easy to check that when $S_{i}$ is closed
$T_{i}=S_{i}$ and when $S_{i}$ is open so is $T_{i}$ and $T_{i}\Rightarrow
S_{i}$. Hence, in both cases $\eta(B_{i}@T_{i})\subseteq\eta(B_{i}@S_{i})$

By (2) and (3) $\delta\in\eta(\bigsqcap_{i=1}^{n}B_{i}@S_{i})$.

  * •

Assume that $\alpha$ is of the form $\bigsqcap_{i=1}^{n}B_{i}@S_{i}\sqsubseteq
B@S$. Since $\eta\models\alpha$, it follows that $\delta\in\eta(B@S)$. By
construction of $\mathcal{I}(\eta,D^{\star})$, it follows that
$(\delta,F_{S}^{\star})\in B^{\mathcal{I}(\eta,D^{\star})}$. Since
$F_{S}^{\star}\in S^{\mathcal{I}(\eta,D^{\star}),\mathcal{Z}}$ for any
$\mathcal{Z}$, $\delta\in(B@S)^{\mathcal{I}(\eta,D^{\star})}$. Hence

$(\bigsqcap_{i=1}^{n}B_{i}@S_{i})^{\mathcal{I}(\eta,D^{\star})}\subseteq(B@S)^{\mathcal{I}(\eta,D^{\star})}.$

  * •

Assume that $\alpha$ is of the form
$\bigsqcap_{i=1}^{n}B_{i}@S_{i}\sqsubseteq\bot$. Since $\eta\models\alpha$,
then $\delta\in\emptyset$. This is a contradiction so
$(\bigsqcap_{i=1}^{n}B_{i}@S_{i})^{\mathcal{I}(\eta,D^{\star})}$ must be
empty. Hence

$(\bigsqcap_{i=1}^{n}B_{i}@S_{i})^{\mathcal{I}(\eta,D^{\star})}\subseteq\bot^{\mathcal{I}(\eta,D^{\star})}.$

We conclude that $\mathcal{I}(\eta,D^{\star})\models\alpha$.

Finally, we show the case where $\alpha$ is a role inclusion, i.e., $\alpha$
is either of the form $P@S\sqsubseteq Q@T$ or $P@S\sqsubseteq\neg Q@T$, where
$P$ and $Q$ are of the form $R$ or $R^{-}$ for some $R\in\mathsf{N_{R}}$.

Assume that $\mathcal{I}(\eta,D^{\star})\models\alpha$. Let
$\delta_{1},\delta_{2}\in\mathbb{R}^{m}$ be such that
$f(\delta_{1},\delta_{2})\in\eta(P@S)$. By construction of
$\mathcal{I}(\eta,D^{\star})$, $(\delta_{1},\delta_{2},F^{\star}_{S})\in
P^{\mathcal{I}(\eta,D^{\star})}$. Moreover, $F^{\star}_{S}\in
S^{{\mathcal{I}(\eta,D^{\star})},\mathcal{Z}}$ for every variable assignment
$\mathcal{Z}$. Hence,
$(\delta_{1},\delta_{2})\in(P@S)^{{\mathcal{I}(\eta,D^{\star})},\mathcal{Z}}$
for every $\mathcal{Z}$.

  * •

Assume that $\alpha$ is of the form $P@S\sqsubseteq Q@T$.

    1. 1.

Since $\mathcal{I}(\eta,D^{\star})\models\alpha$,
$(\delta_{1},\delta_{2})\in(Q@T)^{{\mathcal{I}(\eta,D^{\star})},\mathcal{Z}}$.

    2. 2.

By (1), there exists $F\in T^{\mathcal{I},\mathcal{Z}}$ such that
$(\delta_{1},\delta_{2},F)\in Q^{{\mathcal{I}(\eta,D^{\star})}}$.

    3. 3.

By (2) and definition of $Q^{{\mathcal{I}(\eta,D^{\star})}}$, it follows that
$f(\delta_{1},\delta_{2})\in\eta(Q@S_{F})$ with $S_{F}$ a ground (closed or
open) specifier that contains exactly the pairs $a\kern 0.6pt{:}\,b$ such that
$(a,b)$ are in $F$, except $(\star,\star)$.

    4. 4.

By (2) $F\in T^{\mathcal{I},\mathcal{Z}}$ so the attribute-value pairs in
$S_{F}$ defined in (3) form a superset of those in $T$ and either $S_{F}=T$ if
$T$ is closed, or $S_{F}\Rightarrow T$ if $T$ is open. In both cases,
$\eta(Q@S_{F})\subseteq\eta(Q@T)$.

    5. 5.

By (3) and (4), $f(\delta_{1},\delta_{2})\in\eta(Q@T)$.

It follows that $\eta(P@S)\subseteq\eta(Q@T)$.

  * •

Assume that $\alpha$ is of the form $P@S\sqsubseteq\neg Q@T$.

    1. 1.

Since $\mathcal{I}(\eta,D^{\star})\models\alpha$,
$(\delta_{1},\delta_{2})\in(\mathbb{R}^{m}\times\mathbb{R}^{m})\setminus(Q@T)^{{\mathcal{I}(\eta,D^{\star})},\mathcal{Z}}$.

    2. 2.

By (1), for every $F\in T^{\mathcal{I},\mathcal{Z}}$,
$(\delta_{1},\delta_{2},F)\notin Q^{{\mathcal{I}(\eta,D^{\star})}}$.

    3. 3.

(2) implies that $f(\delta_{1},\delta_{2})\notin\eta(Q@T)$ (otherwise we would
have $(\delta_{1},\delta_{2},F^{\star}_{T})\in
Q^{{\mathcal{I}(\eta,D^{\star})}}$ and $F^{\star}_{T}\in
T^{\mathcal{I},\mathcal{Z}}$). Hence
$f(\delta_{1},\delta_{2})\in\mathbb{R}^{2\cdot m}\setminus\eta(Q@T)=\eta(\neg
Q@T)$.

It follows that $\eta(P@S)\subseteq\eta(\neg Q@T)$.

We conclude that $\eta\models\alpha$.

In the other direction, assume that $\eta\models\alpha$. Let
$(\delta_{1},\delta_{2})\in(P@S)^{\mathcal{I}(\eta,D^{\star})}$. There exists
$(\delta_{1},\delta_{2},F)\in P^{\mathcal{I}(\eta,D^{\star})}$ such that $F\in
S^{\mathcal{I}(\eta,D^{\star}),\mathcal{Z}}$ (for any $\mathcal{Z}$). By
construction of $\mathcal{I}(\eta,D^{\star})$, it follows that
$f(\delta_{1},\delta_{2})\in\eta(P@S^{\prime})$ for some $S^{\prime}$ that
contains exactly the attribute value pairs in $F$, except $(\star,\star)$, and
such that $S^{\prime}$ is closed if $(\star,\star)\notin F$, and open
otherwise. It is easy to check that when $S$ is closed $S^{\prime}=S$ and when
$S$ is open so is $S^{\prime}$ and $S^{\prime}\Rightarrow S$. Hence, in both
cases $\eta(P@S^{\prime})\subseteq\eta(P@S)$, so that
$f(\delta_{1},\delta_{2})\in\eta(P@S)$.

  * •

Assume that $\alpha$ is of the form $P@S\sqsubseteq Q@T$.

    1. 1.

Since $\eta\models\alpha$, $f(\delta_{1},\delta_{2})\in\eta(Q@T)$.

    2. 2.

By (1) and construction of $\mathcal{I}(\eta,D^{\star})$,
$(\delta_{1},\delta_{2},F_{T}^{\star})\in Q^{\mathcal{I}(\eta,D^{\star})}$.

    3. 3.

By (2) and since $F_{T}^{\star}\in
T^{\mathcal{I}(\eta,D^{\star}),\mathcal{Z}}$ for any $\mathcal{Z}$,
$(\delta_{1},\delta_{2})\in(Q@T)^{\mathcal{I}(\eta,D^{\star})}$.

It follows that
$(P@S)^{\mathcal{I}(\eta,D^{\star})}\subseteq(Q@T)^{\mathcal{I}(\eta,D^{\star})}$.

  * •

Assume that $\alpha$ is of the form $P@S\sqsubseteq\neg Q@T$.

    1. 1.

Since $\eta\models\alpha$, $f(\delta_{1},\delta_{2})\in\mathbb{R}^{2\cdot
m}\setminus\eta(Q@T)$.

    2. 2.

(1) implies
$(\delta_{1},\delta_{2})\notin(Q@T)^{\mathcal{I}(\eta,D^{\star})}$. Indeed,
otherwise there would exist $F\in T^{\mathcal{I}(\eta,D^{\star}),\mathcal{Z}}$
such that $(\delta_{1},\delta_{2},F)\in(Q)^{\mathcal{I}(\eta,D^{\star})}$: in
the case where $T$ is closed $F$ would be equal to $F_{T}^{\star}$ and it
would imply that $f(\delta_{1},\delta_{2})\in\eta(Q@T)$. In the case where $T$
is open, $F$ would be such that there exists $S_{F}\Rightarrow T$ such that
$f(\delta_{1},\delta_{2})\in\eta(Q@S_{F})$ and thus
$f(\delta_{1},\delta_{2})\in\eta(Q@S_{F})\subseteq\eta(Q@T)$.

    3. 3.

By (2),
$(\delta_{1},\delta_{2})\in(\mathbb{R}^{m}\times\mathbb{R}^{m})\setminus(Q@T)^{\mathcal{I}(\eta,D^{\star})}=(\neg
Q@T)^{\mathcal{I}(\eta,D^{\star})}$.

It follows that $(P@S)^{\mathcal{I}(\eta,D^{\star})}\subseteq(\neg
Q@T)^{\mathcal{I}(\eta,D^{\star})}$

We conclude that $\mathcal{I}(\eta,D^{\star})\models\alpha$.

##  Appendix 0.C Proof of Theorem 6

See 3.1

###### Proof

Let $\mathcal{O}$ be a satisfiable DL-Lite${}^{\mathcal{H},@}_{\mathit{horn}}$
ontology without negative role inclusions. We use grounding to translate
$\mathcal{O}$ into an equisatisfiable DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontology. Let $\mathcal{J}$ be an
interpretation such that $\Delta^{\mathcal{J}}_{\sf i}=\mathsf{N_{i}}$,
$\Delta^{\mathcal{J}}_{\sf a}=\mathsf{N_{a}}$ and $a^{\mathcal{J}}=a$ for all
$a\in\mathsf{N_{I}}$. Let $\mathcal{Z}$ be a variable assignment mapping
object variables $x\in\mathsf{N_{V}}$ to elements
$\mathcal{Z}(x)\in\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$ and set
variables $X\in\mathsf{N_{U}}$ to finite binary relations
$\mathcal{Z}(X)\in\Phi^{\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}}$.
Consider a concept or role inclusion $I$ of the form
${X_{1}}\,{\boldsymbol{:}}\,{S_{1}},\ldots,{X_{n}}\,{\boldsymbol{:}}\,{S_{n}}\quad(\bigsqcap_{i=1}^{k}K_{i}\sqsubseteq
L)$. A variable assignment $\mathcal{Z}$ is said to be compatible with $I$ if
$\mathcal{Z}(X_{1})\in
S_{1}^{\mathcal{J},\mathcal{Z}},\dots,\mathcal{Z}(X_{n})\in
S_{n}^{\mathcal{J},\mathcal{Z}}$. The _$\mathcal{Z}$ -instance_
$I_{\mathcal{Z}}$ of $I$ is the concept or role inclusion
$\bigsqcap_{i=1}^{k}K_{i}^{\prime}\sqsubseteq L^{\prime}$ obtained by:

  * •

replacing each $X$ with $[a\kern 0.6pt{:}\,b\mid({a,b})\in\mathcal{Z}(X)]$;

  * •

replacing each assignment $a\kern 0.6pt{:}\,X.b$ occurring in some specifier
by all assignments $a\kern 0.6pt{:}\,c$ such that $({b,c})\in\mathcal{Z}(X)$;
and,

  * •

replacing each object variable $x$ by $\mathcal{Z}(x)$.

Let $\mathcal{O}_{\sf g}$ contains

  * •

all assertions $E(\boldsymbol{t})@S$ of $\mathcal{O}$, and

  * •

all $\mathcal{Z}$-instances $I_{\mathcal{Z}}$ for all concept or role
inclusions $I$ in $\mathcal{O}$ and all compatible variable assignments
$\mathcal{Z}$ (they are a finite number since
$\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$ is finite).

The ground ontology $\mathcal{O}_{\sf g}$ can be translated into a standard
DL-Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontology ${\sf dl}(\mathcal{O}_{\sf
g})$ as follows: replace every annotated concept/role name $E@S$ (or inverse
role $R^{-}@S$) with a fresh concept/role name $E_{S}$ (or inverse role
$R_{S}^{-}$) in all the assertions and concept or role inclusions of
$\mathcal{O}_{\sf g}$, and extend the obtained DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontology ${\sf dl}(\mathcal{O}_{\sf
g})$ by all axioms $E_{S}\sqsubseteq E_{T}$ where $S$ and $T$ are ground
specifiers built over $\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$ and
$S\Rightarrow T$.

Since ${\sf dl}(\mathcal{O}_{\sf g})$ is a satisfiable DL-
Lite${}^{\mathcal{H}}_{\mathit{horn}}$ ontology, it has a finite model
$\mathcal{J}^{\prime}$, which can be chosen such that
$\Delta^{\mathcal{J}^{\prime}}=\mathsf{N_{i}}$, and
$a^{\mathcal{J}^{\prime}}=a$ for every $a\in\mathsf{N_{i}}$. Moreover, since
${\sf dl}(\mathcal{O}_{\sf g})$ does not contain negative role inclusion, it
is a quasi-chained ontology. By Proposition 3 in [13], it follows that ${\sf
dl}(\mathcal{O}_{\sf g})$ has a convex $m$-dimensional $f$-geometric model
$\eta^{\prime}$ such that $\\{E(\boldsymbol{t})\mid\eta^{\prime}\models
E(\boldsymbol{t})\\}=\\{E(\boldsymbol{t})\mid\mathcal{J}^{\prime}\models
E(\boldsymbol{t})\\}$, with $m=|\\{a\mid\mathcal{J}^{\prime}\models
E(\boldsymbol{t}),a\in\boldsymbol{t}\\}|$ and $f$ being vector concatenation.

Let $\eta$ be the interpretation of
$(\mathsf{N_{C}},\mathsf{N_{R}},\mathsf{N_{i}},\mathsf{N_{a}})$ such that
$\eta(a)=\eta^{\prime}(a)$ for every $a\in\mathsf{N_{i}}$ and for every
$E\in\mathsf{N_{C}}\cup\mathsf{N_{R}}$ and ground $S\in\mathbf{S}$, if $E_{S}$
occurs in ${\sf dl}(\mathcal{O}_{\sf g})$ then
$\eta(E@S)=\eta^{\prime}(E_{S})$, and otherwise $\eta(E@S)=\emptyset$. Since
for all $S\Rightarrow T$ where $E_{S}$ and $E_{T}$ occur in ${\sf
dl}(\mathcal{O}_{\sf g})$, $E_{S}\sqsubseteq E_{T}\in{\sf dl}(\mathcal{O}_{\sf
g})$, then $\eta^{\prime}(E_{S})\subseteq\eta^{\prime}(E_{T})$. Moreover, if
$S$ does not occur in ${\sf dl}(\mathcal{O}_{\sf g})$, then
$\eta(E@S)=\emptyset$. Thus for all $S\Rightarrow T$,
$\eta(E@S)\subseteq\eta(E@T)$. It follows that $\eta$ is a $m$-dimensional
$f$-geometric interpretation. It is clear that $\eta$ is convex since
$\eta^{\prime}$ is convex.

We show that
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})$ is
a model of $\mathcal{O}$. We have the following

  * •

$\Delta^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}_{\sf
i}=\mathbb{R}^{m}$ and, for all $a\in\mathsf{N_{i}}$,
$a^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}=\eta(a)$;

  * •

$\Delta^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}_{\sf
a}=\mathsf{N_{a}}$ and for all $a\in\mathsf{N_{a}}$,
$a^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}=a$;

  * •

$A^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}=\\{(\delta,F^{\star}_{S})\mid\delta\in\eta(A@S),S\text{
built on
}\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}\\}=\\{(\delta,F^{\star}_{S})\mid\delta\in\eta^{\prime}(A_{S}),$
$S\text{ built on }\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}\\}$, for all
$A\in\mathsf{N_{C}}$;

  * •

$R^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}=\\{(\delta,\epsilon,F^{\star}_{S})\mid
f(\delta,\epsilon)=\delta\oplus\epsilon\in\eta(R@S),S\text{ built on
}\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}\\}=\\{(\delta,\epsilon,F^{\star}_{S})\mid\delta\oplus\epsilon\in\eta^{\prime}(R_{S}),S\text{
built on }\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}\\}$, for all
$R\in\mathsf{N_{R}}$.

Let $E(\boldsymbol{t})@S$ be an assertion in $\mathcal{O}$. Since
$\mathcal{J}^{\prime}$ is a model of ${\sf dl}(\mathcal{O}_{\sf g})$, then
$\mathcal{J}^{\prime}\models E_{S}(\boldsymbol{t})$ and $\eta^{\prime}\models
E_{S}(\boldsymbol{t})$. Thus $\oplus_{t\in\boldsymbol{t}}\eta(t)\in\eta(E@S)$,
where $\oplus_{t\in\boldsymbol{t}}\eta(t)=t$ if $\boldsymbol{t}=(t)$ and
$\oplus_{t\in\boldsymbol{t}}\eta(t)=t\oplus u$ if $\boldsymbol{t}=(t,u)$. By
Theorem 2.2, it follows that
${\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}\models
E(\boldsymbol{t})@S$.

Let
$\alpha={X_{1}}\,{\boldsymbol{:}}\,{T_{1}},\ldots,{X_{n}}\,{\boldsymbol{:}}\,{T_{n}}\
(\bigsqcap_{i=1}^{k}E_{i}@S_{i}\sqsubseteq E@S)$ be a (concept or role)
inclusion in $\mathcal{O}$ (note that in case of role inclusion, $k=n=1$ and
the inclusion is positive). Let $\mathcal{Z}$ be a variable assignment mapping
object variables $x\in\mathsf{N_{V}}$ to elements
$\mathcal{Z}(x)\in\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$ and set
variables $X\in\mathsf{N_{U}}$ to finite binary relations
$\mathcal{Z}(X)\in\Phi^{\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}}$ that
satisfies $\mathcal{Z}(X_{1})\in
T_{1}^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}},\dots,\mathcal{Z}(X_{n})\in
T_{n}^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$
and let
$\boldsymbol{\delta}\in(\bigsqcap_{i=1}^{k}E_{i}@S_{i})^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$.

  1. 1.

For every $1\leq i\leq k$, $\boldsymbol{\delta}\in
E_{i}@S_{i}^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$.

  2. 2.

It follows that for every $1\leq i\leq k$, $(\boldsymbol{\delta},F_{i})\in
E_{i}^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$
for some $F_{i}\in
S_{i}^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$.

  3. 3.

By (2) and by construction of
$E_{i}^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$,
$\oplus_{\delta\in\boldsymbol{\delta}}\delta\in\eta(E_{i}@S_{F_{i}})$ where
$S_{F_{i}}$ is a (closed or open) specifier containing exactly the attribute-
value pairs that occur in $F_{i}$, except $(\star,\star)$.

  4. 4.

Let ${S_{i}}_{\mathcal{Z}}$ be the specifier obtained by grounding $S_{i}$
according to $\mathcal{Z}$. By (2), $F_{i}\in
S_{i}^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$
so if $S_{i}$ is closed $S_{F_{i}}={S_{i}}_{\mathcal{Z}}$, and otherwise,
$S_{F_{i}}\Rightarrow{S_{i}}_{\mathcal{Z}}$.

  5. 5.

By (4), ${\sf dl}(\mathcal{O}_{\sf g})$ contains by construction
${E_{i}}_{S_{F_{i}}}\sqsubseteq{E_{i}}_{{S_{i}}_{\mathcal{Z}}}$ for every
$1\leq i\leq k$ such that ${S_{i}}_{\mathcal{Z}}\neq S_{F_{i}}$, as well as
the DL translation of the $\mathcal{Z}$-instance of $\alpha$ :
$\bigsqcap_{i=1}^{k}{E_{i}}_{{S_{i}}_{\mathcal{Z}}}\sqsubseteq{E}_{{S}_{\mathcal{Z}}}\in{\sf
dl}(\mathcal{O}_{\sf g})$.

  6. 6.

By (5) and since $\eta^{\prime}$ is a geometric model of ${\sf
dl}(\mathcal{O}_{\sf g})$:

$\bigcap_{i=1}^{k}\eta^{\prime}({E_{i}}_{S_{F_{i}}})\subseteq\bigcap_{i=1}^{k}\eta^{\prime}({E_{i}}_{{S_{i}}_{\mathcal{Z}}}).$

  7. 7.

Hence
$\eta^{\prime}(\bigsqcap_{i=1}^{k}{E_{i}}_{{S_{i}}_{\mathcal{Z}}})\subseteq\eta^{\prime}({E}_{{S}_{\mathcal{Z}}})$.

  8. 8.

Thus
$\oplus_{\delta\in\boldsymbol{\delta}}\delta\in\eta(\bigsqcap_{i=1}^{k}{E_{i}}_{S_{F_{i}}})=\eta^{\prime}(\bigsqcap_{i=1}^{k}{E_{i}}_{S_{F_{i}}})$
implies that
$\oplus_{\delta\in\boldsymbol{\delta}}\delta\in\eta^{\prime}({E}_{{S}_{\mathcal{Z}}})=\eta({E}_{{S}_{\mathcal{Z}}})$.

  9. 9.

If $\alpha$ is a positive inclusion, it follows from (8) that
$(\boldsymbol{\delta},F^{\star}_{{S}_{\mathcal{Z}}})\in
E^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$.
It is then easy to see that $F^{\star}_{{S}_{\mathcal{Z}}}\in
S^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$,
since $F^{\star}_{{S}_{\mathcal{Z}}}$ is the annotation set that contains the
attribute-value pairs that occur in the grounding of $S$ w.r.t. $\mathcal{Z}$,
plus $(\star,\star)$ if $S$ is open. Hence $\boldsymbol{\delta}\in
E@S^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$.

  10. 10.

If $\alpha$ is a negative concept inclusion, with $E@S=\bot$, it follows from
(8) that $\delta\in\emptyset$, which is a contradiction. Hence
$(\bigsqcap_{i=1}^{k}E_{i}@S_{i})^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}=\emptyset$.

  11. 11.

By (9) and (10),
$(\bigsqcap_{i=1}^{k}E_{i}@S_{i})^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}\subseteq
E@S^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$,
hence
${\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}\models\alpha$.

As $\alpha$ was an arbitrary (concept or role) inclusion in $\mathcal{O}$, it
follows that
${\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}\models\mathcal{O}$,
and $\eta$ is a convex geometric model of $\mathcal{O}$.

##  Appendix 0.D Proof of Theorem 12

See 4.1

###### Proof

We first ground the ontology $\mathcal{O}$. Let $\mathcal{O}$ be a satisfiable
DL-Lite${}^{\mathcal{H},\mathbb{T},@}_{\mathit{horn}}$ ontology and let
$\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$ be the union of the sets of
annotation names, time points, and intervals, occurring in $\mathcal{O}$,
respectively. Let $\mathcal{J}$ be an interpretation of DL-
Lite${}^{\mathcal{H},\mathbb{T},@}_{\mathit{horn}}$ over the domain
$\Delta^{\mathcal{J}}=\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}\cup\\{{\sf
f}\\}\cup\\{max(\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}})+1,max(min(\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}})-1,0)\\}$,
where ${\sf f}$ is a fresh individual name, satisfying $a^{\mathcal{J}}=a$ for
all $a\in\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$. Let
$\mathcal{Z}:\mathsf{N_{V}}\to\Phi^{\mathcal{J}}_{\mathcal{O}}$ be a variable
assignment, where
$\Phi^{\mathcal{J}}_{\mathcal{O}}\coloneqq\mathcal{P_{\text{\sf{fin}}}}\left(\Delta^{\mathcal{J}}\times\Delta^{\mathcal{J}}\right)$.
Consider a concept or role inclusion $\alpha$ of the form
${X_{1}}\,{\boldsymbol{:}}\,{S_{1}},\ldots,{X_{n}}\,{\boldsymbol{:}}\,{S_{n}}\quad(\bigsqcap_{i=1}^{k}K_{i}\sqsubseteq
L)$. A variable assignment $\mathcal{Z}$ is said to be compatible with
$\alpha$ if $\mathcal{Z}(X_{1})\in
S_{1}^{\mathcal{J},\mathcal{Z}},\dots,\mathcal{Z}(X_{n})\in
S_{n}^{\mathcal{J},\mathcal{Z}}$. The _$\mathcal{Z}$ -instance_
$\alpha_{\mathcal{Z}}$ of $\alpha$ is the concept or role inclusion
$\bigsqcap_{i=1}^{k}K^{\prime}_{i}\sqsubseteq L^{\prime}$ obtained by:

  * •

replacing each $X_{i}$ with $[a\kern
0.6pt{:}\,b\mid({a,b})\in\mathcal{Z}(X_{i})]$;

  * •

replacing each assignment $a\kern 0.6pt{:}\,X.b$ occurring in some specifier
by all assignments $a\kern 0.6pt{:}\,c$ such that
$({b,c})\in\mathcal{Z}(X_{i})$; and,

  * •

replacing each object variable $x$ by $\mathcal{Z}(x)$.

Let $\mathcal{O}_{\sf g}$ be the ontology containing all
$\mathcal{Z}$-instances $\alpha_{\mathcal{Z}}$ of all concept or role
inclusions $\alpha$ in $\mathcal{O}$ and all compatible variable assignments
$\mathcal{Z}$ (they are a finite number since $\Delta^{\mathcal{J}}$ is
finite). Recall that since specifiers attached to roles are atemporal, the
specifiers attached to roles in $\mathcal{O}_{\sf g}$ do not contain any
temporal attributes.

Now, we translate $\mathcal{O}_{\sf g}$ into an DL-
Lite${}^{\mathcal{H},@}_{\mathit{horn}}$ ontology $\mathcal{O}^{\dagger}_{\sf
g}$ as follows.

First, $\mathcal{O}^{\dagger}_{\sf g}$ contains every axiom from
$\mathcal{O}_{\sf g}$ (but in DL-Lite${}^{\mathcal{H},@}_{\mathit{horn}}$
temporal attribute value pairs will be treated in the same way as the
“regular” attribute value pairs). Second, given a ground specifier $S$, we
denote by $S(a\kern 0.6pt{:}\,b)$ the result of removing all temporal
attributes from $S$ and adding the pair $a\kern 0.6pt{:}\,b$. Let $k_{\sf
min}$ and $k_{\sf max}$ be the smallest and the largest numbers occurring in
$\mathcal{O}$ (or $0$ if none occurs). Moreover, let $S_{\mathbb{T}}$ be the
set of temporal attribute-value pairs in $S$. By assumption, there are no
temporal attributes on roles. Then, for each $A@S$ with
$S_{\mathbb{T}}\neq\emptyset$, $\mathcal{O}^{\dagger}_{\sf g}$ contains the
equivalence (as usual, $\equiv$ refers to bidirectional $\sqsubseteq$ here):

$A@S\equiv\\!\bigsqcap_{(a:b)\in S_{\mathbb{T}}}\\!(A@S(a:b))^{\sharp}$ (5)

where the concept expressions $(A@S(a:b))^{\sharp}$ are defined as follows:

  * •

$(A@S({\sf
during}:v))^{\sharp}=\bigsqcap_{u\in\mathbb{N}^{v}_{\mathcal{O}}}A@S({\sf
during}:u)$

  * •

$(A@S({\sf time}:k))^{\sharp}=(A@S({\sf during}:[k,k]))^{\sharp}$

  * •

$(A@S({\sf since}:k))^{\sharp}=(A@S({\sf during}:[k,k_{\sf
max}]))^{\sharp}\sqcap A@S({\sf since}:k_{\sf max})$

  * •

$(A@S({\sf until}:k))^{\sharp}=(A@S({\sf during}:[k_{\sf
min},k]))^{\sharp}\sqcap A@S({\sf until}:k_{\sf min})$

with $k\neq k_{\sf min}$ and $k\neq k_{\sf max}$. For $k\in\\{k_{\sf
min},k_{\sf max}\\}$, we have $(A@S(a:k))^{\sharp}=A@S(a:k)$.

Finally, given attribute-value pairs $a\kern 0.6pt{:}\,b$ and $c\kern
0.6pt{:}\,d$ for temporal attributes $a$ and $b$, we say that $a\kern
0.6pt{:}\,b$ _implies_ $c\kern 0.6pt{:}\,d$ if $A(e)@[a\kern
0.6pt{:}\,b]\models A(e)@[c\kern 0.6pt{:}\,d]$ for some arbitrary
$A\in\mathsf{N_{C}}$ and $e\in\mathsf{N_{I}}$. We then extend
$\mathcal{O}^{\dagger}_{\sf g}$ with all inclusions $A@S\sqsubseteq A@T$ and
$R@S\sqsubseteq R@T$, where $A@S,A@T$ and $R@S,R@T$ occur in
$\mathcal{O}^{\dagger}_{\sf g}$, including those introduced in (6), such that
for each temporal attribute-value pair $c\kern 0.6pt{:}\,d$ in $T$ there is a
temporal attribute-value pair $a\kern 0.6pt{:}\,b$ in $S$ such that $a\kern
0.6pt{:}\,b$ implies $c\kern 0.6pt{:}\,d$ and:

  * •

$T$ is an open specifier and the set of non-temporal attribute-value pairs in
$S$ is a superset of the set of non-temporal attribute-value pairs in $T$; or

  * •

$S,T$ are closed specifiers and the set of non-temporal attribute-value pairs
in $S$ is equal to the set of non-temporal attribute-value pairs in $T$.

Whenever this happens we write $S\Rightarrow T$.

This finishes the construction of $\mathcal{O}^{\dagger}_{\sf g}$. By Theorem
3.1, $\mathcal{O}^{\dagger}_{\sf g}$ has a $m$-dimensional convex $f$-model
$\eta^{\prime}$. Let $\eta$ be defined as follows:

  * •

$\eta(a)=\eta^{\prime}(a)$ for every individual name $a$,

  * •

for every role name $R$ and atemporal specifier $S$,
$\eta(R@S)=\eta^{\prime}(R@S)$,

  * •

for every concept name $A$ and specifier $S$, $\eta(A@S)=\bigcap_{(a:b)\in
S_{\mathbb{T}}}\eta^{\prime}(A@S(a:b))^{\sharp}$ where
$\eta^{\prime}(A@S(a:b))^{\sharp}$ is defined as follows:

    * –

$\eta^{\prime}(A@S({\sf
during}:v))^{\sharp}=\bigcap_{u\in\mathbb{N}^{v}_{\mathcal{O}}}\eta^{\prime}(A@S({\sf
during}:u))$

    * –

$\eta^{\prime}(A@S({\sf time}:k))^{\sharp}=\eta^{\prime}(A@S({\sf
during}:[k,k]))^{\sharp}$

    * –

$\eta^{\prime}(A@S({\sf since}:k))^{\sharp}=\eta^{\prime}(A@S({\sf
during}:[k,k_{\sf max}]))^{\sharp}\cap\eta^{\prime}(A@S({\sf since}:k_{\sf
max}))$

    * –

$\eta^{\prime}(A@S({\sf until}:k))^{\sharp}=\eta^{\prime}(A@S({\sf
during}:[k_{\sf min},k]))^{\sharp}\cap\eta^{\prime}(A@S({\sf until}:k_{\sf
min}))$

with $k\neq k_{\sf min}$ and $k\neq k_{\sf max}$. For $k\in\\{k_{\sf
min},k_{\sf max}\\}$, we have
$\eta^{\prime}(A@S(a:k))^{\sharp}=\eta^{\prime}(A@S(a:k))$.

We have that $\eta$ is convex since the $\eta^{\prime}(R@S)$ and
$\eta^{\prime}(A@S(a:b))$ are convex, and intersections of convex regions are
convex.

Let $(\eta_{j})_{j\in\Delta_{T}}$ be such that

  * •

$\eta_{j}(a)=\eta(a)=\eta^{\prime}(a)$ for every individual name $a$ and time
point $j$,

  * •

for every concept name $A$, specifier $S$ without temporal attribute, and time
point $k_{\sf min}\leq j\leq k_{\sf max}$,
$\eta_{j}(A@S)=\eta^{\prime}(A@S({\sf during}:v))$ with $j\in v$. For
$j>k_{\sf max}$, we have $\eta_{j}(A@S)=\eta^{\prime}(A@S({\sf during}:[k_{\sf
max},k_{\sf max}+1]))$ and, for $j<k_{\sf min}$, we have
$\eta_{j}(A@S)=\eta^{\prime}(A@S({\sf during}:[k_{\sf min}-1,k_{\sf min}]))$.

We show that $\eta$ is global for $(\eta_{j})_{j\in\Delta_{T}}$ and
$\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$, i.e.,
$\mathcal{I}(\eta,\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}})$ is global
for
$\mathcal{I}(\eta_{j},\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}\setminus(\mathsf{N_{T}}\cup\mathsf{N^{2}_{T}}))_{j\in\Delta_{T}}$:
let $A\in\mathsf{N_{C}}$, $\delta\in\mathbb{R}^{m}$ and $F$ be a finite binary
relation over $\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$. We have
$(\delta,F)\in
A^{\mathcal{I}(\eta,\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}})}$ iff
$\delta\in\eta(A@S)$ for a specifier $S$ that contains exactly the same
attribute-value pairs as $F$, except $(\star,\star)$. This is the case exactly
when for all $(a,x)\in F$:

  * •

if $a={\sf time}$, then $\delta\in\eta^{\prime}(A@S({\sf during}:[x,x]))$;

  * •

if $a={\sf until}$, then $\delta\in\eta^{\prime}(A@S({\sf during}:[j,j]))$ for
every $j\leq min(x,k)$;

  * •

if $a={\sf since}$, then $\delta\in\eta^{\prime}(A@S({\sf during}:[j,j]))$ for
every $x\leq j\leq k_{\sf max}$;

  * •

if $a={\sf during}$, then $\delta\in\eta^{\prime}(A@S({\sf during}:[j,j]))$
for every $j\in x$ and $j\leq k_{\sf max}$.

Let $R\in\mathsf{N_{R}}$, $(\delta_{1},\delta_{2})\in\mathbb{R}^{2m}$ and $F$
be a finite binary relation over
$\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}$. We have
$(\delta_{1},\delta_{2},F)\in
R^{\mathcal{I}(\eta,\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}})}$ iff
$f(\delta_{1},\delta_{2})\in\eta(R@S)$ for a specifier $S$ that contains
exactly the same attribute-value pairs as $F$, except $(\star,\star)$. By
assumption, $S$ is atemporal so $F$ is built over
$\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}\setminus(\mathsf{N_{T}}\cup\mathsf{N^{2}_{T}})$
and $(\delta_{1},\delta_{2},F)\in
R^{\mathcal{I}(\eta_{j},\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}})}$ for
every $j$. Hence we have shown that
$\mathcal{I}(\eta,\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}})$ is global
for
$(\mathcal{I}(\eta_{j},\mathsf{\mathsf{N}_{\mathnormal{\mathcal{O}}}}\setminus(\mathsf{N_{T}}\cup\mathsf{N^{2}_{T}})))_{j\in\Delta_{T}}$.

Finally, we show below that
$\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})$
satisfies $\mathcal{O}$. We write the argument for assertions and concept
inclusions and omit for role inclusions because it is similar to the one for
concept inclusions, but simpler since role inclusions do not have temporal
attributes.

$\bullet$ Let $A(t)@S$ be a concept assertion in $\mathcal{O}$. Since
$\mathcal{J}\models A(t)@S$ and interprets every individual name by itself,
then $(t,F_{S})\in A^{\mathcal{J}}$ (since $S$ is a closed specifier). Since
$\mathcal{J}$ is global for $(\mathcal{J}_{j})_{j\in\Delta_{T}}$, it follows
that for every $a:x\in S$,

  * •

if $a={\sf time}$, then $\eta^{\prime}(t)\in\eta^{\prime}(A@S({\sf
during}:[x,x]))$ because $A@S\sqsubseteq A@S({\sf
during}:[x,x])\in\mathcal{O}^{\dagger}_{\sf g}$ and $\eta^{\prime}$ is an
$m$-dimensional convex $f$-model of $\mathcal{O}^{\dagger}_{\sf g}$;

  * •

if $a={\sf until}$, then, for every $k_{\sf min}\leq j\leq x$,
$\eta^{\prime}(t)\in\eta^{\prime}(A@S({\sf during}:[j,j]))$ and
$\eta^{\prime}(t)\in\eta^{\prime}(A@S({\sf until}:k_{\sf min}))$ because
$A@S\sqsubseteq A@S({\sf during}:[j,j])\in\mathcal{O}^{\dagger}_{\sf g}$, for
every $k_{\sf min}\leq j\leq x$, $A@S\sqsubseteq A@S({\sf until}:k_{\sf
min})\in\mathcal{O}^{\dagger}_{\sf g}$, and $\eta^{\prime}$ is an
$m$-dimensional convex $f$-model of $\mathcal{O}^{\dagger}_{\sf g}$;

  * •

if $a={\sf since}$, then, for every $x\leq j\leq k_{\sf max}$,
$\eta^{\prime}(t)\in\eta^{\prime}(A@S({\sf during}:[j,j]))$ and
$\eta^{\prime}(t)\in\eta^{\prime}(A@S({\sf since}:k_{\sf max}))$ because
$A@S\sqsubseteq A@S({\sf during}:[j,j])\in\mathcal{O}^{\dagger}_{\sf g}$, for
every $x\leq j\leq k_{\sf max}$, $A@S\sqsubseteq A@S({\sf since}:k_{\sf
max})\in\mathcal{O}^{\dagger}_{\sf g}$, and $\eta^{\prime}$ is an
$m$-dimensional convex $f$-model of $\mathcal{O}^{\dagger}_{\sf g}$;

  * •

if $a={\sf during}$, then for every $j\in x$,
$\eta^{\prime}(t)\in\eta^{\prime}(A@S({\sf during}:[j,j]))$ because
$A@S\sqsubseteq A@S({\sf during}:[j,j])\in\mathcal{O}^{\dagger}_{\sf g}$.

Since $\eta(A@S)=\bigcap_{(a:b)\in
S_{\mathbb{T}}}\eta^{\prime}(A@S(a:b))^{\sharp}$, it follows that
$\eta(t)=\eta^{\prime}(t)$ belongs to $\eta(A@S)$, i.e., $\eta\models A(t)@S$.

$\bullet$ Let $R(t_{1},t_{2})@S$ be a role assertion in $\mathcal{O}$. Since
$\mathcal{J}\models R(t_{1},t_{2})@S$ and interprets every individual name by
itself, then $(t_{1},t_{2},F_{S})\in R^{\mathcal{J}}$ (since $S$ is a closed
specifier). Since $\mathcal{J}$ is global for
$(\mathcal{J}_{j})_{j\in\Delta_{T}}$, and by construction of
$\mathcal{O}^{\dagger}_{\sf g}$, it follows that
$R(t_{1},t_{2})@S\in\mathcal{O}^{\dagger}_{\sf g}$. It follows that
$f(\eta(t_{1}),\eta(t_{2}))=f(\eta^{\prime}(t_{1}),\eta^{\prime}(t_{2}))\in\mathbb{R}^{2m}$
belongs to $\eta(R@S)=\eta^{\prime}(R@S)$, i.e., $\eta\models
R(t_{1},t_{2})@S$.

$\bullet$ Let
$I={X_{1}}\,{\boldsymbol{:}}\,{S_{1}},\ldots,{X_{n}}\,{\boldsymbol{:}}\,{S_{n}}\quad(\bigsqcap_{i=1}^{n}B_{i}@T_{i}\sqsubseteq
B@S)$ be a concept inclusion in $\mathcal{O}$. Let $\mathcal{Z}$ be a variable
assignment mapping object variables $x\in\mathsf{N_{V}}$ to elements
$\mathcal{Z}(x)\in\mathsf{N_{a}}\cup\mathsf{N_{T}}\cup\mathsf{N^{2}_{T}}$ and
set variables $X\in\mathsf{N_{U}}$ to finite binary relations $\mathcal{Z}(X)$
over $\mathsf{N_{a}}\cup\mathsf{N_{T}}\cup\mathsf{N^{2}_{T}}$ that satisfy
$\mathcal{Z}(X_{1})\in
S_{1}^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}},\dots,\mathcal{Z}(X_{n})\in
S_{n}^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$
and let
$\delta\in(\bigsqcap_{i=1}^{k}B_{i}@T_{i})^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$.
For every $1\leq i\leq k$, we have $(\delta,F_{i})\in
B_{i}^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$
for some $F_{i}\in
T_{i}^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$.
It follows from the construction of
$B_{i}^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$
that $\delta\in\eta(B_{i}@S_{F_{i}})$ where $S_{F_{i}}$ is a (closed or open)
specifier containing exactly the attribute-value pairs that occur in $F_{i}$
except $(\star,\star)$. By construction, if $B_{i}=A_{i}\in\mathsf{N_{C}}$,
then $\eta(B_{i}@S_{F_{i}})=\bigcap_{(a:b)\in
S_{F_{i},\mathbb{T}}}\eta^{\prime}(A_{i}@S_{F_{i}}(a:b))^{\sharp}$. Otherwise,
if $B_{i}=\exists P_{i}$, then $\eta(B_{i}@S_{F_{i}})=\eta^{\prime}(\exists
P_{i}@S_{F_{i}})$. Moreover, since $F_{i}\in
T_{i}^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$,
then if $T_{i}$ is closed $S_{F_{i}}={T_{i}}_{\mathcal{Z}}$, and otherwise,
$S_{F_{i}}\Rightarrow{T_{i}}_{\mathcal{Z}}$, where ${T_{i}}_{\mathcal{Z}}$ is
the specifier obtained by grounding $T_{i}$ according to $\mathcal{Z}$. In the
case $B_{i}=A_{i}$, this implies that for every $j$,
$\eta^{\prime}(A_{i}@S_{F_{i}}({\sf
during}:[j,j]))\subseteq\eta^{\prime}(A_{i}@{T_{i}}({\sf
during}:[j,j])_{\mathcal{Z}})$ by the semantics of geometric interpretations.
It follows that
$\eta(B_{i}@S_{F_{i}})\subseteq\bigcap_{(a:b)\in{T_{i}}_{\mathcal{Z},\mathbb{T}}}\eta^{\prime}(A_{i}@{T_{i}}_{\mathcal{Z}}(a:b))^{\sharp}$.
In the case $B_{i}=\exists P_{i}$, this implies that
$\eta^{\prime}(P_{i}@S_{F_{i}})\subseteq\eta^{\prime}(P_{i}@{T_{i}}_{\mathcal{Z}})$,
so $\delta\in\eta(\exists P_{i}@S_{F_{i}})=\eta^{\prime}(\exists
P_{i}@S_{F_{i}})\subseteq\eta^{\prime}(\exists P_{i}@{T_{i}}_{\mathcal{Z}})$.

Since $\eta^{\prime}$ is a model of $\mathcal{O}^{\dagger}_{\sf g}$ which
contains a $\mathcal{Z}$-instance
$\bigsqcap_{i=1}^{n}B_{i}@T_{i\mathcal{Z}}\sqsubseteq B@S_{\mathcal{Z}}$ of
the concept inclusion $I$ and equivalences

$B_{(i)}@S_{\mathcal{Z}}\equiv\\!\bigsqcap_{(a:b)\in
S_{\mathcal{Z}\mathbb{T}}}\\!(B_{(i)}@S_{\mathcal{Z}}(a:b))^{\sharp}$ (6)

for each $B_{(i)}$. This implies that
$\delta\in\eta^{\prime}(B@{S_{\mathcal{Z}}({\sf during}:[j,j])})$ for every
$j$ such that $S_{\mathcal{Z}}\Rightarrow S_{\mathcal{Z}}({\sf
during}:[j,j])$. By construction of $\eta(B@{S}_{\mathcal{Z}})$, it follows
that $\delta\in\eta(B@{S}_{\mathcal{Z}})$. It follows that
$(\delta,F^{\star}_{{S}_{\mathcal{Z}}})\in
B^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$.
We can see that $F^{\star}_{{S}_{\mathcal{Z}}}\in
S^{{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})},\mathcal{Z}}$,
since $F^{\star}_{{S}_{\mathcal{Z}}}$ is the annotation set that contains the
attribute-value pairs that occur in the grounding of $S$ w.r.t. $\mathcal{Z}$,
plus $(\star,\star)$ if the specifier is open. So
$\delta\in(B@{S})^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}}),\mathcal{Z}}$.
This means that $\eta$ satisfies $I$.

$\bullet$ The argument for $I$ of the form
${X_{1}}\,{\boldsymbol{:}}\,{S_{1}},\ldots,{X_{n}}\,{\boldsymbol{:}}\,{S_{n}}\quad(\bigsqcap_{i=1}^{n}B_{i}@T_{i}\sqsubseteq\bot)$
is in the same lines but we have to argue that if there is a variable
assignment $\mathcal{Z}$ such that
$(\bigsqcap_{i=1}^{n}B_{i}@T_{i\mathcal{Z}})^{\mathcal{I}(\eta,\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$
is not the empty set then there is also a variable assignment
$\mathcal{Z}^{\prime}$ such that
$(\bigsqcap_{i=1}^{n}B_{i}@T_{i\mathcal{Z}^{\prime}})^{\mathcal{I}(\eta^{\prime},\mathsf{\mathsf{N}^{\star}_{\mathnormal{\mathcal{O}}}})}$
is not the empty set which contradicts the assumption that $\eta^{\prime}$ is
a convex $m$-dimensional model of $\mathcal{O}^{\dagger}_{\sf g}$.