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

[ orcid=0000-0002-3852-9351<EMAIL_ADDRESS>url=http://www.inf.unibz.it/ artale/, ]

[ orcid=0000-0001-8512-1933<EMAIL_ADDRESS>url=https://sites.google.com/view/andreamazzullo/, ]

# Non-Rigid Designators in Epistemic and Temporal Free Description Logics
(Extended Version)

Alessandro Artale  Free University of Bozen-Bolzano  Andrea Mazzullo
University of Trento

(2023)

###### Abstract

Definite descriptions, such as ‘the smallest planet in the Solar System’, have
been recently recognised as semantically transparent devices for object
identification in knowledge representation formalisms. Along with individual
names, they have been introduced also in the context of description logic
languages, enriching the expressivity of standard nominal constructors.
Moreover, in the first-order modal logic literature, definite descriptions
have been widely investigated for their _non-rigid_ behaviour, which allows
them to denote different objects at different states. In this direction, we
introduce _epistemic_ and _temporal_ extensions of standard description
logics, with nominals and the universal role, additionally equipped with
definite descriptions constructors. Regarding names and descriptions, in these
languages we allow for: possible _lack of denotation_ , ensured by _partial_
models, coming from free logic semantics as a generalisation of the classical
ones; and _non-rigid designation_ features, obtained by assigning to terms
distinct values across states, as opposed to the standard rigidity condition
on individual expressions. In the absence of the rigid designator assumption,
we show that the satisfiability problem for epistemic free description logics
is NExpTime-complete, while satisfiability for temporal free description
logics over linear time structures is undecidable.

###### keywords:

Epistemic and temporal description logics, Definite descriptions, Non-rigid
designators

##  1 Introduction

_Definite descriptions_ , like ‘the smallest planet in the Solar System’, are
expressions having form ‘the $x$ such that $\varphi$’. Together with
_individual names_ , such as ‘Mercury’, they are used as _referring
expressions_ to identify objects in a given domain [1, 2, 3]. Definite
description and individual names can also _fail to denote_ any object at all,
as in the cases of the definite description ‘the planet between Mercury and
the Sun’ or the individual name ‘Vulcan’. Formal accounts that address these
aspects and still admit definite descriptions as genuine terms of the
language, on a par with individual names, are usually based on so-called _free
logics_ [4, 5, 6, 7]. These are in contrast with classical logic approaches,
in which individual names are assumed to always designate, and where definite
descriptions are paraphrased in terms of sentences expressing existence and
uniqueness conditions (an approach dating back to Russell [8]). Recently,
definite descriptions have been introduced into description logic (DL)
formalisms [9, 10, 11], by enriching standard languages with nominals like
$\smash{\mathcal{ALCO}}$ and $\smash{\mathcal{ELO}}$. In particular, the DLs
$\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}$ and
$\smash{\mathcal{ELO}_{\\!u}^{\smash{\iota}}}$ from [10, 11], which include
the universal role and are based on a free logic semantics allowing for non-
denoting terms, have been shown to have, respectively, ExpTime-complete
ontology satisfiability and PTime-complete subsumption checking problem, hence
matching the complexities of the classical DL counterparts.

In addition, expressions referring to the same object cannot always be
mutually substituted in a sentence while preserving the truth value. For
instance, even if everybody is aware that Mercury is very close to the Sun,
not everyone thereby knows that also the smallest planet in the Solar System
is very close to the Sun, despite the fact that ‘the smallest planet in the
Solar System’ and ‘Mercury’ denote the same object. Indeed, _modal_ settings,
like the temporal or the epistemic ones, are _referentially opaque_ contexts,
where the _intension_ (i.e., the meaning) of a term might not coincide with
its _extension_ (that is, its referent) [12]. In these cases, referring
expressions can behave as _non-rigid designators_ , meaning that they can
denote different individuals across different states (epistemic alternatives,
instants of time, etc.).

For example, in an epistemic scenario, ‘the smallest planet’ can be conceived
as denoting another astronomical object, by someone unaware of its actual
reference to Mercury. Similarly, on a temporal scale, ‘the smallest planet’
refers to Mercury nowadays, but denoted Pluto less than twenty years ago [13].
Due to this problematic interplay between designation and modalities, non-
rigid descriptions and names have been widely investigated in first-order
modal and temporal logics [14, 15, 16, 17, 13, 18, 19, 20], as _individual
concepts_ or _flexible terms_ capable of taking different values across
states. However, despite the wide body of research both on temporal [21, 22,
23] and epistemic [24, 25, 26] extensions, non-rigid designators have
received, to the best of our knowledge, little attention in modal DLs. In an
epistemic DL context, non-rigid individual names appear in [27], under an
approach that involves abstract individual names interpreted on an infinite
common domain, but without definite descriptions.

In this paper, we extend the free DLs proposed for the non-modal case in [10,
11], by: (i) adding _epistemic modalities_ , such as $\Box$ (_box_ , read as
‘it is known that’), or _temporal_ ones, like $\mathbin{\mathcal{U}}$
(_until_)applicable both to formulas and concepts of the language; (ii)
introducing nominals built from _definite descriptions_ of the form $\iota C$
(read as ‘the object that is $C$’), where $C$ is a concept, alongside the
standard ones based on _individual names_ ; (iii) dropping the _rigid
designator assumption_ , hence allowing terms to behave as flexible individual
concepts across states. We study the complexity of formula satisfiability,
showing that, without the rigid designator assumption, this problem for
epistemic free DLs is NExpTime-complete (same as the logic
$\mathbf{S5}\times\mathbf{S5}$ [28, Theorem 5.26]), whereas it becomes
undecidable for temporal free DLs interpreted on linear time structures (while
it is decidable without definite descriptions and with the RDA [28, Theorem
14.12]).

Section 2 provides the necessary background on the epistemic and temporal free
DLs introduced in this paper. In Section 3, we motivate with examples the
syntactical and semantical choices for these languages. Section 4 studies the
complexity of formula satisfiability in epistemic free DLs, while Section 5
focuses on the undecidability of temporal free DLs over time flows consisting
of finite or infinite traces. Finally, Section 6 concludes the paper,
discussing open problems and future research directions.

##  2 Epistemic and Temporal Free Description Logics

In this section, we introduce the syntax of
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
and $\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$,
respectively a modal and a temporal extension of the free DL
$\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}$ language [10, 11], as well as
their semantics based on epistemic and temporal frames, respectively.

###  2.1 Epistemic free description logics

The
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
language is a modalised extension of the free DL
$\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}$ language. Let ${\sf N_{C}}$,
${\sf N_{R}}$ and ${\sf N_{I}}$ be countably infinite and pairwise disjoint
sets of _concept names_ , _role names_ , and _individual names_ ,
respectively. The
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
_terms_ and _concepts_ are defined as:

$\displaystyle\tau::=a\mid\smash{\iota}C,\qquad C::=A\mid\\{\tau\\}\mid\lnot
C\mid C\sqcap C\mid\exists r.C\mid\exists u.C\mid\Diamond C$

where $a\in{\sf N_{I}}$, $A\in{\sf N_{C}}$, $r\in{\sf N_{R}}$, and $u$ is the
_universal role_. A term of the form $\smash{\iota}C$ is called a _definite
description_ , with the concept $C$ being the _body of $\smash{\iota}C$_, and
a concept $\\{\tau\\}$ is called a _(term) nominal_. All the usual syntactic
abbreviations are assumed: $\bot=A\sqcap\lnot A$, $\top=\lnot\bot$, $C\sqcup
D=\lnot(\lnot C\sqcap\lnot D)$, $C\Rightarrow D=\lnot C\sqcup D$, $\forall
s.C=\lnot\exists s.\lnot C$, with $s\in{\sf N_{R}}\cup\\{u\\}$, and $\Box
C=\lnot\Diamond\lnot C$. We will consider also the _reflexive diamond_
operator, $\Diamond^{+}C=C\sqcup\Diamond C$, and the _reflexive box_ operator,
$\Box^{+}C=C\sqcap\Box C$.

An
_$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
axiom_, denoted as $\alpha$, is either a _concept inclusion_ (_CI_) of the
form $C\sqsubseteq D$, or an
_$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
assertion_ of the form $C(\tau)$ or $r(\tau_{1},\tau_{2})$, where $C,D$ are
concepts, $r\in{\sf N_{R}}$, and $\tau,\tau_{1},\tau_{2}$ are terms. An
_$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
formula_ is an expression of the following form:

$\varphi::=(\alpha)\mid\neg\varphi\mid\varphi\land\varphi\mid\Diamond\varphi$

Given a _frame_ $\mathfrak{F}=(W,\lhd)$, with $W$ being a non-empty set of
_worlds_ (or _states_) and $\lhd\subseteq W\times W$ being a binary
_accessibility relation_ on $W$, a _partial modal interpretation_ based on
$\mathfrak{F}$ is a triple $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$,
where: $\mathfrak{F}$ is the frame of $\mathfrak{M}$; $\Delta$ is a non-empty
set, called the _domain_ of $\mathfrak{M}$ (we adopt the so-called _constant
domain assumption_ [28]); and $\mathcal{I}$ is a function associating with
every $w\in W$ a _partial interpretation_
$\mathcal{I}_{w}=(\Delta,\cdot^{\mathcal{I}_{w}})$ that maps every $A\in{\sf
N_{C}}$ to a subset of $\Delta$, every $r\in{\sf N_{R}}$ to a subset of
$\Delta\times\Delta$, the universal role $u$ to the set $\Delta\times\Delta$
itself, and every $a$ in a _subset_ of ${\sf N_{I}}$ to an element in
$\Delta$. In other words, every $\cdot^{\mathcal{I}_{w}}$ is a total function
on ${\sf N_{C}}\cup{\sf N_{R}}$ and a _partia_ l function on ${\sf N_{I}}$. We
say that $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$ is a _total modal
interpretation_ if every $\mathcal{I}_{w}$, with $w\in W$, is a _total_
interpretation, meaning that $\cdot^{\mathcal{I}_{w}}$ is defined as above,
except that it maps _every_ $a\in{\sf N_{I}}$ to an element of $\Delta$.

######  Definition 1.

Given $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$, with
$\mathfrak{F}=(W,\lhd)$, we say that $\mathfrak{M}$ satisfies the _rigid
designator assumption_ (_RDA_) if, for every individual name $a\in{\sf N_{I}}$
and every $w,v\in W$, the following condition holds: if $a^{\mathcal{I}_{w}}$
is defined, then $a^{\mathcal{I}_{w}}=a^{\mathcal{I}_{v}}$, i.e., $a$ is a
_rigid designator_. An individual name $a\in{\sf N_{I}}$ is said to _denote in
$\mathcal{I}_{w}$_ if $a^{\mathcal{I}_{w}}$ is defined, and we say that it
_denotes in $\mathfrak{M}$_ if $a$ denotes in $\mathcal{I}_{w}$, for some
$w\in W$. Moreover, $a$ is called a _ghost in_ $\mathfrak{M}$ if, for every
$w\in W$, $a$ does not denote in $\mathcal{I}_{w}$.

######  Remark 1.

Dropping the RDA is the most general assumption, since rigid designators can
be enforced by the CI $\Diamond^{+}\\{a\\}\sqsubseteq\Box^{+}\\{a\\}$.
Moreover, partial interpretations are a generalisation of the classical ones:
an individual can be forced to denote at some state (i.e., not being a ghost)
with the CI $\top\sqsubseteq\Diamond^{+}\exists u.\\{a\\}$, and to denote at
all states with the formula $\Box^{+}(\top\sqsubseteq\exists u.\\{a\\})$. Note
that a ghost individual is vacuously rigid.

Given $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$, with
$\mathfrak{F}=(W,\lhd)$, and a world $w\in W$, we define the _value_
$\tau^{\mathcal{I}_{w}}$ of a term $\tau$ in $w$ as $a^{\mathcal{I}_{w}}$, if
$\tau=a$, and as follows, for $\tau=\smash{\iota}C$:

$\displaystyle(\smash{\iota}C)^{\mathcal{I}_{w}}=\begin{cases}d,&\text{if}\
C^{\mathcal{I}_{w}}=\\{d\\},\ \text{for some}\ d\in\Delta;\\\
\text{undefined},&\text{otherwise}.\end{cases}$

As for the _extension_ of a concept $C$ in $w$, $C^{\mathcal{I}_{w}}$ is as
usual with the following additions:

$\displaystyle(\Diamond C)^{\mathcal{I}_{w}}$
$\displaystyle=\\{d\in\Delta\mid\exists v\in W,w\lhd v\colon d\in
C^{\mathcal{I}_{v}}\\},\quad\\{\tau\\}^{\mathcal{I}_{w}}$
$\displaystyle=\begin{cases}\\{\tau^{\mathcal{I}_{w}}\\},&\text{if $\tau$
denotes in $\mathcal{I}_{w}$},\\\ \,\emptyset,&\text{otherwise,}\end{cases}$

where a term $\tau$ is said to _denote_ in $\mathcal{I}_{w}$ if
$\tau^{\mathcal{I}_{w}}$ is defined. A concept $C$ is _satisfied at $w$ of
$\mathfrak{M}$_ if $C^{\mathcal{I}_{w}}\neq\emptyset$. An
_$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
formula $\varphi$ is satisfied at $w$ of $\mathfrak{M}$_, written
$\mathfrak{M},w\models\varphi$, when:

$\displaystyle\mathfrak{M},w\models C\sqsubseteq D$ $\displaystyle\text{ \,
iff \, }C^{\mathcal{I}_{w}}\subseteq D^{\mathcal{I}_{w}},$
$\displaystyle\mathfrak{M},w\models C(\tau)$ $\displaystyle\text{ \, iff \,
}\tau~{}\text{denotes
in}~{}{\mathcal{I}_{w}}~{}\text{and}~{}\tau^{\mathcal{I}_{w}}\in
C^{\mathcal{I}_{w}},$ $\displaystyle\mathfrak{M},w\models
r(\tau_{1},\tau_{2})$ $\displaystyle\text{ \, iff \,
}\tau_{1},\tau_{2}~{}\text{denotes
in}~{}{\mathcal{I}_{w}}~{}\text{and}~{}(\tau_{1}^{\mathcal{I}_{w}},\tau_{2}^{\mathcal{I}_{w}})\in
r^{\mathcal{I}_{w}},$ $\displaystyle\mathfrak{M},w\models\Diamond\psi$
$\displaystyle\text{ \, iff \, }\exists v\in W,w\lhd
v\colon\mathfrak{M},v\models\psi,$

together with the usual interpretation of Boolean operators. An
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
formula $\varphi$ is _satisfied in $\mathfrak{M}$_ if there exists a world $w$
in $\mathfrak{M}$ such that $\mathfrak{M},w\models\varphi$, and it is
_partial_ (_total_) _satisfiable_ if there is a partial (total) modal
interpretation $\mathfrak{M}$ such that $\varphi$ is satisfied in
$\mathfrak{M}$.

###  2.2 Temporal free description logics

For the temporal DL language
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$, we
build $\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
_terms_ , _concepts_ , and _formulas_ similarly to the
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
case, by using the temporal operator _until_ , $\mathbin{\mathcal{U}}$, for
the construction of concepts, $C\mathbin{\mathcal{U}}D$, and formulas,
$\varphi\mathbin{\mathcal{U}}\psi$.

We call _flow of time_ a frame $\mathfrak{F}=(T,<)$, where $T$ is a non-empty
set of _instants_ and $<\ \subseteq T\times T$ is a strict linear order on
$T$. A _partial temporal interpretation_ , or _partial trace_ , based on a
flow of time $\mathfrak{F}$, is a triple
$\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$, defined as in the modal
case. We similarly define the notion of _total trace_. If $\mathfrak{M}$ is
based on the flow of time $(\mathbb{N},<)$, where $<$ is the natural strict
linear order on $\mathbb{N}$, we call it an _infinite trace_ , and we often
denote it (with an abuse of notation) by
$\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in\mathbb{N}})$; whereas, if it is
based on $(\\{0,\ldots,n\\},<)$, with $n\in\mathbb{N}$, it is called a _finite
trace_ , and it is simply denoted by
$\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in T})$, with $T=[0,n]$. Given a
partial trace $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$, with
$\mathfrak{F}=(T,<)$ and $t\in T$ (that we call an _instant of
$\mathfrak{M}$_), the _value_ of an
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ term
$\tau$ at $t$, and the _extension_ of an
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ concept
$C$ at $t$, are defined as for the modal case, by replacing the semantics of
the $\Diamond$ modal operator with the following one for the
$\mathbin{\mathcal{U}}$ temporal operator:

$\displaystyle(C\mathbin{\mathcal{U}}D)^{\mathcal{I}_{t}}=\\{d\in\Delta\mid\text{there
is}\ u\in T,t<u\colon d\in D^{\mathcal{I}_{u}}\ \text{and, for all}\
v\in(t,u),d\in C^{\mathcal{I}_{v}}\\}.$

Similarly, the _satisfaction_ of a
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ formula
$\varphi$ at $t$ of $\mathfrak{M}$ is defined as for the modal case, with the
following semantics of $\mathbin{\mathcal{U}}$ replacing the one for the
$\Diamond$ operator:

$\displaystyle\mathfrak{M},t\models\varphi\mathbin{\mathcal{U}}\psi\
\text{iff}\ \text{there is}\ u\in T,t<u\colon\mathfrak{M},u\models\psi\
\text{and, for all $v\in(t,u)$,}\ \mathfrak{M},v\models\varphi.$

As usual, we use the until operator to define the other temporal operators, as
follows. For concepts: _(strong) next_ operator,
${\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}C=\bot\mathbin{\mathcal{U}}C$;
_diamond_ operator, $\Diamond C=\top\mathbin{\mathcal{U}}C$; and _box_
operator, $\Box C=\lnot\Diamond\lnot C$; _reflexive diamond_ operator,
$\Diamond^{+}C=C\sqcup\Diamond C$; _reflexive box_ operator,
$\Box^{+}C=C\sqcap\Box C$. Similar abbreviations are used for formulas.

We say that a
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ formula
$\varphi$ (respectively, a concept $C$) is _satisfiable on partial (total)
traces_ , if $\varphi$ (respectively, $C$) is satisfied at time $0$ in some
partial (total) trace $\mathfrak{M}$.

######  Remark 2.

Assertions are syntactic sugar, since $C(\tau)$ and $r(\tau_{1},\tau_{2})$ are
captured by the following CIs, respectively: $\top\sqsubseteq\exists
u.\\{\tau\\},\\{\tau\\}\sqsubseteq C$; and $\top\sqsubseteq\exists
u.\\{\tau_{1}\\},\\{\tau_{1}\\}\sqsubseteq\exists r.\\{\tau_{2}\\}$. To avoid
ambiguities, we use parentheses when applying Boolean or modal operators to
assertions. Thus, for instance, the formulas $\lnot(C(\tau))$ and
$\Diamond(C(\tau))$ abbreviate, respectively, $\lnot(\top\sqsubseteq\exists
u.\\{\tau\\}\land\\{\tau\\}\sqsubseteq C)$ and
$\Diamond(\top\sqsubseteq\exists u.\\{\tau\\}\land\\{\tau\\}\sqsubseteq C)$,
whereas the assertions $\lnot C(\tau)$ and $\Diamond C(\tau)$ stand,
respectively, for $\top\sqsubseteq\exists
u.\\{\tau\\}\land\\{\tau\\}\sqsubseteq\lnot C$ and $\top\sqsubseteq\exists
u.\\{\tau\\}\land\\{\tau\\}\sqsubseteq\Diamond C$. Finally, as already
observed for $\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}$ [11], we point
out that formulas are just syntactic sugar in
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$,
since a CI $C\sqsubseteq D$ can be internalised [29, 30] as a concept of the
form $\forall u.(C\Rightarrow D)$.

######  Remark 3.

We point out a counter-intuitive behaviour of formulas without the RDA
assumption. Let us consider the following: $(\\{a\\}\sqsubseteq\Box
C)\land\Diamond(\\{a\\}\sqsubseteq\lnot C)$. This formula, while unsatisfiable
if the RDA is assumed, is satisfiable without the RDA, since it is satisfied
in a modal interpretation that interprets the individual name $a$ differently
in different states.

###  2.3 Formula satisfiability problems and reductions

Given a class of frames $\mathcal{C}$, the _partial_ (_total_)
_$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
formula satisfiability problem over $\mathcal{C}$_ (_with_ or _without the
RDA_ , respectively) is the problem of deciding, given an
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
formula $\varphi$, whether there exists a partial (total) modal interpretation
(with or without the RDA, respectively) based on a frame in $\mathcal{C}$ that
satisfies $\varphi$. Similarly, for a class of flows of time $\mathcal{C}$,
the _partial_ (_total_)
_$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
formula satisfiability problem over $\mathcal{C}$_ (_with_ or _without the
RDA_ , respectively) is the problem of deciding, given an
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ formula
$\varphi$, whether there exists a partial (total) trace (with or without the
RDA, respectively) based on a flow of time in $\mathcal{C}$ that satisfies
$\varphi$.

The _partial_ (_total_)
_$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ formula
satisfiability problem_ (_with_ or _without the RDA_ , respectively) is the
partial (total)
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
formula satisfiability problem (with or without the RDA, respectively) over
the class of _epistemic frames_ $(W,\sim)$ such that $\sim$ is an _equivalence
relation_ on $W$.

The _partial_ (_total_)
_$\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ formula
satisfiability problem_ (_with_ or _without the RDA_ , respectively) is the
partial (total)
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ formula
satisfiability problem (with or without the RDA, respectively) over
$\\{(\mathbb{N},<)\\}$. The _partial_ (_total_)
_$\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
formula satisfiability problem_ (_with_ or _without the RDA_ , respectively)
is the partial (total)
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ formula
satisfiability problem (with or without the RDA, respectively) over the class
of finite strict linear orders of the form $(\\{0,\ldots,n\\},<)$, where
$n\in\mathbb{N}$.

We first illustrate a polynomial-time reduction of formula satisfiability on
total modal or temporal interpretations without the RDA, to the same problem
over partial ones.

######  Lemma 1.

Total
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
and $\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
formula satisfiability without the RDA are polynomial-time reducible to,
respectively, partial
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
and $\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
formula satisfiability without the RDA.

###### Proof.

We adapt, to the
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
and $\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
cases, the reduction of $\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}$
ontology satisfiability and entailment from total to partial interpretation,
given in [11]. In particular, given a
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
or $\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
formula $\varphi$, we define $\varphi^{\prime}$ as the conjunction of
$\varphi$ with formulas of the form

$\Box^{+}(\top\sqsubseteq\exists u.\\{a\\}),$ ($\ast$)

for every individual name $a$ occurring in $\varphi$. It can be seen that
$\varphi$ is satisfiable on _total_ modal or temporal interpretations without
the RDA iff $\varphi^{\prime}$ is satisfiable on _partial_ modal or temporal
interpretations without the RDA, respectively. Observe that, despite the fact
that each individual name $a$ occurring in $\varphi$ is forced by ($\ast$ ‣
2.3) to denote at every world or instant of any model of $\varphi^{\prime}$,
its interpretation is allowed to vary across states, due to the lack of the
RDA. ∎

In addition, we show how to remove, in polynomial time, definite descriptions
of the form $\iota C$, hence reducing the original problem to the formula
satisfiability problem in
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}}}}$.

######  Lemma 2.

Partial
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
and $\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
formula satisfiability without the RDA are polynomial-time reducible to,
respectively, partial
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}}}}$ and
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}}}$ formula satisfiability
without the RDA.

###### Proof.

Similar to the proof of [11, Lemma 1], which shows that
$\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}$ formula satisfiability problem
on partial interpretations is polynomial-time reducible to the
$\smash{\mathcal{ALCO}_{\\!u}}$ formula satisfiability problem on partial
interpretations. ∎

Finally, given a formula $\varphi$ in
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}}}}$ or
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}}}$, checking for its
satisfiability reduces to check concept satisfiability in
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}}}}$ or
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}}}$, respectively.

######  Lemma 3.

Partial $\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}}}}$ and
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}}}$ formula satisfiability
are linear-time reducible to, respectively, partial
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}}}}$ and
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}}}$ concept satisfiability.

###### Proof.

This is an adaptation to the modal and temporal case of the so-called
_internalisation_ property [29, Chapter 5] of those DLs equipped with the
universal role, allowing us to internalise a CI of the form $C\sqsubseteq D$
as a concept of the form $\forall u.(\lnot C\sqcup D)$. ∎

##  3 Motivations and examples

In the following, we provide some motivating examples to illustrate the novel
features of the modal and temporal free DL languages introduced in the
previous section.

#### Epistemic scenario.

We discuss here the main features of the language
$\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}}$
interpreted on partial modal interpretations without the RDA and based on
frames equipped with an equivalence relation, to provide motivating examples
in an epistemic setting. Thus, in the following, we will refer to such
interpretations as _epistemic contexts_ , and the worlds of the epistemic
context will be called _states_.

Let us consider the following individual names: $\mathsf{clark}$ standing for
the ‘Clark Kent’, $\mathsf{superman}$ standing for ‘Superman’, and
$\mathsf{lois}$ standing for ‘Lois Lane’. In a given state of an epistemic
context, $\mathsf{clark}$ and $\mathsf{superman}$ can denote the same element
of the domain. However, since the epistemic context does not satisfy the RDA,
these individual names can also refer to different individuals at different
states. Moreover, the term
$\smash{\iota}(\mathsf{Journalist}\sqcap\exists\mathsf{worksWith}.\\{\mathsf{lois}\\})$
can be used to refer to the journalist that works with Lois Lane, which can be
understood as an alternative way to describe Clark Kent.

The concept $\Box\\{\mathsf{superman}\\}$ captures those individuals that are
_known to be_ Superman, whereas $\Diamond\\{\mathsf{superman}\\}$ would be the
set of individuals _suspectable of being_ (i.e., for which it is not known
that they are not) Superman. The following CI can be used to express that
Clark Kent is known to be Clark Kent:
$\\{\mathsf{clark}\\}\sqsubseteq\Box\\{\mathsf{clark}\\}$, whereas we can use
$\\{\mathsf{clark}\\}\sqsubseteq\lnot\Box\\{\mathsf{superman}\\}$ to express
that Clark Kent is not known to be Superman. Moreover, the following CIs
assert that Lois Lane is known to be Lois Lane, i.e.,
$\\{\mathsf{lois}\\}\sqsubseteq\Box\\{\mathsf{lois}\\}$, and she is also known
to love Superman, i.e.,
$\\{\mathsf{lois}\\}\sqsubseteq\Box\exists\mathsf{loves}.\\{\mathsf{superman}\\}$,
but (unfortunately for Clark Kent) not the journalist that works with her,
i.e.,
$\\{\mathsf{lois}\\}\sqsubseteq\lnot\Box\exists\mathsf{loves}.\\{\smash{\iota}(\mathsf{Journalist}\sqcap\exists\mathsf{worksWith}.\\{\mathsf{lois}\\}\\}$.

#### Temporal scenario.

In the following, we exemplify and discuss the main features of the language
$\smash{\smash{\mathcal{TL}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
interpreted on partial traces without the RDA.

Let us consider the individual name $\mathsf{dl}$ which can serve as a
“variable”-name, that might change its value (and even remain uninterpreted)
at different instants, so to denote, e.g., the Description Logic (DL)
workshops that take place over the years. Instead, the individual name
$\mathsf{dl22}$ can be used as an individual name with a fixed referent across
time, denoting the DL workshop that takes place in 2022 only. Finally, the
definite description $\smash{\iota}\exists\mathsf{isGCof}.\\{\mathsf{dl}\\}$
is able to refer non-rigidly to the General Chair of the DL workshop.

The concept $\Diamond^{+}\\{\mathsf{dl}\\}$ can be used to refer to those
objects that will eventually be the DL workshop. When interpreted on total
traces with the RDA, the extension of this concept would contain exactly one
object, i.e., the (rigid) referent of the individual name $\mathsf{dl}$. On
the other hand, on partial traces without the RDA, its extension might contain
also zero, or more than one, objects, namely, those individuals that are the
values of $\mathsf{dl}$ at different time points. In addition, the concept
$\Diamond^{+}\\{\smash{\iota}\exists\mathsf{isGCof}.\\{\mathsf{dl}\\}\\}$ can
be used to represent those individuals that will eventually be the General
Chair of the various DL workshops. The concept
$\Diamond^{+}\exists\mathsf{hasPCM}.\Diamond^{+}\\{\smash{\iota}\exists\mathsf{isGCof}.\\{\mathsf{dl}\\}\\}$
captures those objects that will eventually have as PC Members some
individuals that, at some point in the future, will be the General Chair of
the DL workshop.

Let $\mathsf{proc\mbox{-}dl22}$ stands for the proceedings of the DL22
workshop. To enforce the proceedings of the DL22 to behave as a rigid
designator, we can enforce the following CI,
$\Diamond^{+}\\{\mathsf{proc\mbox{-}dl22}\\}\sqsubseteq\Box^{+}\\{\mathsf{proc\mbox{-}dl22}\\}$.
On the other hand, we can require $\mathsf{dl}$ to be a _flexible_ designator
by enforcing the following CI, $\top\sqsubseteq\exists
u.(\Diamond^{+}\\{\mathsf{dl}\\}\sqcap\Diamond^{+}\lnot\\{\mathsf{dl}\\})$.
Finally, we can enforce $\mathsf{dl22}$ to be an _instantaneous_ designator by
using the following CIs, $\top\sqsubseteq\Diamond^{+}\exists
u.\\{\mathsf{dl22}\\}$,
$\Diamond^{+}(\\{\mathsf{dl22}\\}\sqcap\Diamond\\{\mathsf{dl22}\\})\sqsubseteq\bot$,
meaning that $\mathsf{dl22}$ is not gost and that no objects can be the
denotation of the individual name $\mathsf{dl22}$ at two distinct instants.
Notice that gost individuals are assumed to be (vacuously) rigid, while
flexible and instantaneous individuals should denote.

To state that the (current) General Chair of DL will be one of next year’s PC
Members of DL we can use the assertion,
$({\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}\exists{\sf
isPCMof}.\\{{\sf dl}\\})(\\{\smash{\iota}\exists{\sf isGCof}.\\{{\sf
dl}\\}\\})$. On the other hand, to say that, next year, the (future) General
Chair of DL will be one of the PC Members of DL, the following formula should
be used instead,
${\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}(\top\sqsubseteq\exists
u.\\{\smash{\iota}\exists{\sf isGCof}.\\{{\sf
dl}\\}\\}\land\\{\smash{\iota}\exists{\sf isGCof}.\\{{\sf
dl}\\}\\}\sqsubseteq\exists{\sf isPCMof}.\\{{\sf dl}\\})$. Moreover, one can
express that, at some point, DL22 will be the DL workshop, by writing the
following assertion, $\Diamond^{+}(\\{\mathsf{dl}\\}(\\{\mathsf{dl22}\\}))$.
Finally, the formula $\Box^{+}(\\{\smash{\iota}\exists{\sf isGCof}.\\{{\sf
dl}\\}\\}\sqsubseteq\exists{\sf
isPCMof}.{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}\\{{\sf
dl}\\})$ asserts that it will always be the case that the General Chair of DL
is going to be a DL’s PC Member on the subsequent year.

##  4 Reasoning in epistemic free description logics

In this section, we show that the formula satisfiability problem for the
epistemic free DL
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ is decidable and
NExpTime-complete. After reducing, thanks to Lemmas 2 and 3, satisfiability of
a formula $\varphi$ in
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ to the
satisfiability of a concept $C_{\varphi}$ in
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$, we can show how to decide the
satisfiability of the latter by adapting the technique of _quasimodels_ [28]
to the case where individual names can be left uninterpreted and do not
respect the RDA.

Given an $\smash{\smash{\mathcal{ML}}_{\smash{\mathcal{ALCO}_{\\!u}}}}$
concept $C_{\varphi}$, let $\mathsf{con}(C_{\varphi})$ be the closure under
single negation of the set of concepts occurring in $C_{\varphi}$. A _type_
for $C_{\varphi}$ is a subset ${\boldsymbol{t}}$ of
$\mathsf{con}(C_{\varphi})$ such that:

  1. C1

$\neg C\in{\boldsymbol{t}}$ iff $C\not\in{\boldsymbol{t}}$, for all $\neg
C\in\mathsf{con}(C_{\varphi})$;

  2. C2

$C\sqcap D\in{\boldsymbol{t}}$ iff $C,D\in{\boldsymbol{t}}$, for all $C\sqcap
D\in\mathsf{con}(C_{\varphi})$.

Note that there are at most exponentially many types, i.e., there are
$2^{|\mathsf{con}(C_{\varphi})|}$ types for $C_{\varphi}$.

A _quasistate for $C_{\varphi}$_ is a non-empty set $\boldsymbol{T}$ of types
for $C_{\varphi}$ satisfying the following conditions:

  1. Q1

for every $\\{a\\}\in\mathsf{con}(C_{\varphi})$, there exists at most one
${\boldsymbol{t}}\in\boldsymbol{T}$ such that $\\{a\\}\in{\boldsymbol{t}}$;

  2. Q2

for every ${\boldsymbol{t}}\in\boldsymbol{T}$ and every $\exists
r.C\in{\boldsymbol{t}}$, there exists
${\boldsymbol{t}}^{\prime}\in\boldsymbol{T}$ such that $\\{\lnot
D\mid\lnot\exists
r.D\in{\boldsymbol{t}}\\}\cup\\{C\\}\subseteq{\boldsymbol{t}}^{\prime}$;

  3. Q3

for every ${\boldsymbol{t}}\in\boldsymbol{T}$, $\exists
u.C\in{\boldsymbol{t}}$ iff there exists
${\boldsymbol{t}}^{\prime}\in\boldsymbol{T}$ such that
$C\in{\boldsymbol{t}}^{\prime}$.

A _basic structure for $C_{\varphi}$_ is a pair $(W,\boldsymbol{q})$, where
$W$ is a non-empty set, and $\boldsymbol{q}$ is a function associating with
every $w\in W$ a quasistate $\boldsymbol{q}(w)$ for $C_{\varphi}$, satisfying
the following condition:

  1. B1

there exists a world $w^{\prime}\in W$ and a type
${\boldsymbol{t}}\in\boldsymbol{q}(w^{\prime})$ such that
$C_{\varphi}\in{\boldsymbol{t}}$.

A _run through $(W,\boldsymbol{q})$_ is a function $\rho$ mapping each world
$w\in W$ into a type $\rho(w)\in\boldsymbol{q}(w)$ and satisfying the
following condition for every $\Diamond C\in\mathsf{con}(\varphi)$:

  1. R1

$\Diamond C\in\rho(w)$ iff there exists $v\in W$ such that $C\in\rho(v)$.

An _$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$ quasimodel for
$C_{\varphi}$_ is a triple $\mathfrak{Q}=(W,\boldsymbol{q},\mathfrak{R})$,
where $(W,\boldsymbol{q})$ is a basic structure for $C_{\varphi}$, and
$\mathfrak{R}$ is a set of runs through $(W,\boldsymbol{q})$ such that the
following condition holds:

  1. M1

for every $w\in W$ and every ${\boldsymbol{t}}\in\boldsymbol{q}(w)$, there
exists $\rho\in\mathfrak{R}$ with $\rho(w)={\boldsymbol{t}}$;

  2. M2

for every $w\in W$ and for every ${\boldsymbol{t}}\in\boldsymbol{q}(w),\text{
with }\\{a\\}\in{\boldsymbol{t}}$, there exists exactly one
$\rho\in\mathfrak{R}$ such that $\\{a\\}\in\rho(w)$.

We are now able to show how a quasimodel is related to the notion of
satisfiability.

######  Proposition 1.

A concept $C_{\varphi}$ is partial
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$ satisfiable without the RDA iff
there exists an $\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$ quasimodel for
$C_{\varphi}$.

###### Proof.

$(\Rightarrow)$ Let $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$, with
$\mathfrak{F}=(W,\sim)$, be a partial modal interpretation satisfying
$C_{\varphi}$. Without loss of generality [28], we can assume that $\sim\
=W\times W$. Consider
${\boldsymbol{t}}^{\mathcal{I}_{w}}(d)=\\{C\in\mathsf{con}(C_{\varphi})\mid
d\in C^{\mathcal{I}_{w}}\\}$, for every $d\in\Delta$ and $w\in W$. Clearly,
${\boldsymbol{t}}^{\mathcal{I}_{w}}(d)$ is a concept type for $C_{\varphi}$
since it clearly satisfies C1-C2. We now define a triple
$\mathfrak{Q}=(W,\boldsymbol{q},\mathfrak{R})$, where:

  * •

$\boldsymbol{q}$ is a function from $W$ to the set of quasistates for
$C_{\varphi}$ such that
$\boldsymbol{q}(w)=\\{{\boldsymbol{t}}^{\mathcal{I}_{w}}(d)\mid
d\in\Delta\\}$, for every $w\in W$;

  * •

$\mathfrak{R}$ is the set of functions $\rho_{d}$ from $W$ to the set of types
for $C_{\varphi}$ such that
$\rho_{d}(w)={\boldsymbol{t}}^{\mathcal{I}_{w}}(d)$, for every $d\in\Delta$
and for every $w\in W$.

It is easy to show that $\mathfrak{Q}$ is a quasimodel for $C_{\varphi}$.
Indeed, $\boldsymbol{q}$ is well-defined, as $\boldsymbol{q}(w)$ is a set of
types for $C_{\varphi}$ satisfying Q1-Q3, for every $w\in W$. Moreover,
$(W,\boldsymbol{q})$ is a basic structure for $C_{\varphi}$ since
$\mathfrak{M}$ is satisfying $C_{\varphi}$, i.e., $\mathfrak{M},w\models
C_{\varphi}(d)$, for some $w\in W$ and $d\in\Delta$, and thus
$(W,\boldsymbol{q})$ satisfies B1. The set of runs, $\mathfrak{R}$, by
construction, satisfies R1. Finally, by definition of $\boldsymbol{q}(w)$ and
of $\rho$, $\mathfrak{Q}$ satisfies M1, and, since for every $w\in W$, if
$\\{a\\}\in{\boldsymbol{t}}$, then there should be exactly one $d\in\Delta$
such that $d=\\{a\\}^{\mathcal{I}_{w}}$, thus $\mathfrak{Q}$ satisfies M2.

$(\Leftarrow)$ Suppose there is a quasimodel
$\mathfrak{Q}=(W,\boldsymbol{q},\mathfrak{R})$ for $C_{\varphi}$. Define a
partial modal interpretation $\mathfrak{M}=(\mathfrak{F},\Delta,\mathcal{I})$,
with $\mathfrak{F}=(W,W\times W)$, $\Delta=\mathfrak{R}$, and, for any
$A\in{\sf N_{C}}$, $r\in{\sf N_{R}}$ and $a\in{\sf N_{I}}$ the following
holds:

  * •

$A^{\mathcal{I}_{w}}=\\{\rho\in\Delta\mid A\in\rho(w)\\}$;

  * •

$r^{\mathcal{I}_{w}}=\\{(\rho,\rho^{\prime})\in\Delta\times\Delta\mid\\{\lnot
C\mid\lnot\exists r.C\in\rho(w)\\}\subseteq\rho^{\prime}(w)\\}$;

  * •

$u^{\mathcal{I}_{w}}=\Delta\times\Delta$;

  * •

$a^{\mathcal{I}_{w}}=\rho$, for the (unique, if any) $\rho\in\mathfrak{R}$
such that $\\{a\\}\in\rho(w)$ (undefined, otherwise).

Observe that $\Delta$ is well-defined since $W$ is a non-empty set and
$\boldsymbol{q}(w)\neq\emptyset$, for all $w\in W$. Thus, by M1,
$\mathfrak{R}\neq\emptyset$. Also, by Q1 and M2, $a^{\mathcal{I}_{w}}$ is
well-defined. We now require the following claim.

######  Claim 1.

For every $C\in\mathsf{con}(C_{\varphi})$, $w\in W$ and $\rho\in\Delta$,
$\rho\in C^{\mathcal{I}_{w}}$ iff $C\in\rho(w)$.

###### Proof.

The proof is by induction on $C$. The base cases, $C=A$ and $C=\\{a\\}$,
follow immediately from the definition of $\mathfrak{M}$. We then consider the
inductive cases.
Let $C=\lnot D$. $\lnot D\in\rho(w)$ iff, by C1, $D\not\in\rho(w)$. By
induction, $D\not\in\rho(w)$ iff $\rho\not\in D^{\mathcal{I}_{w}}$ iff
$\rho\in(\lnot D)^{\mathcal{I}_{w}}$.
Let $C=D\sqcap E$. Similar to the previous case, now by using C2.
Let $C=\exists u.D$. $\rho\in(\exists u.D)^{\mathcal{I}_{w}}$ iff there exists
$\rho^{\prime}\in D^{\mathcal{I}_{w}}$. By inductive hypothesis,
$\rho^{\prime}\in D^{\mathcal{I}_{w}}$ iff $D\in\rho^{\prime}(w)$. By Q3, the
previous step holds iff $\exists u.D\in\rho(w)$.
Let $C=\exists r.D$. $(\Rightarrow)$ Suppose that $\rho\in(\exists
r.D)^{\mathcal{I}_{w}}$. Then, there exists $\rho^{\prime}\in\Delta$ such that
$(\rho,\rho^{\prime})\in r^{\mathcal{I}_{w}}$ and $\rho^{\prime}\in
D^{\mathcal{I}_{w}}$. By inductive hypothesis, $\rho^{\prime}\in
D^{\mathcal{I}_{w}}$ iff $D\in\rho^{\prime}(w)$. By contradiction, assume that
$\exists r.D\not\in\rho(w)$, then, by C1, $\lnot\exists r.D\in\rho(w)$. By
definition of $r^{\mathcal{I}_{w}}$, since $(\rho,\rho^{\prime})\in
r^{\mathcal{I}_{w}}$, then, $\lnot D\in\rho^{\prime}(w)$, thus contadicting,
by C1, that $D\in\rho^{\prime}(w)$. $(\Leftarrow)$ Conversely, suppose that
$\exists r.D\in\rho(w)$. By Q2 and M1, there exists a $\rho^{\prime}\in\Delta$
such that $\\{\lnot E\mid\lnot\exists
r.E\in\rho(w)\\}\cup\\{D\\}\subseteq\rho^{\prime}(w)$. By inductive hypothesis
and the definition of $r^{\mathcal{I}_{w}}$, $\rho^{\prime}\in
D^{\mathcal{I}_{w}}$ and $(\rho,\rho^{\prime})\in r^{\mathcal{I}_{w}}$. Thus,
$\rho\in(\exists r.D)^{\mathcal{I}_{w}}$.
Let $C=\Diamond D$. $\rho\in(\Diamond D)^{\mathcal{I}_{w}}$ iff there exists
$v\in W$ s.t. $\rho\in D^{\mathcal{I}_{v}}$. By inductive hypothesis, $\rho\in
D^{\mathcal{I}_{v}}$ iff $D\in\rho(v)$ iff, by R1, $\Diamond D\in\rho(w)$. ∎

Now we can easily finish the proof of the proposition by observing that, by
B1, there exists a world $w^{\prime}\in W$ and a type
${\boldsymbol{t}}\in\boldsymbol{q}(w^{\prime})$ such that
$C_{\varphi}\in{\boldsymbol{t}}$. Thus, by M1, there exists
$\rho\in\mathfrak{R}$ with $\rho(w^{\prime})={\boldsymbol{t}}$ and, by the
above claim, $\rho\in C_{\varphi}^{\mathcal{I}_{w^{\prime}}}$. ∎

We now show that if there exists a quasimodel it exists one of exponential
size.

######  Theorem 1.

There exists an $\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$ quasimodel for
$C_{\varphi}$ iff there exists an
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$ quasimodel for $C_{\varphi}$ of
exponential size in the length of $C_{\varphi}$.

###### Proof.

The $(\Rightarrow)$ direction is straightforward. For the $(\Leftarrow)$
direction, we adapt the proof of [28, Theorem 5.25] where the notion of _twin_
is substituted by a new notion of _w-copies_. Intuitively, the notion of
_twin_ does not work here due to the absence of the RDA. Indeed, the following
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$ concept:

$\exists u.(C\sqcap\Diamond\\{a\\})\sqcap\exists u.(\lnot
C\sqcap\Diamond\\{a\\})$

is satisfiable only without the RDA thanks to the possibility to interpret the
nominal concept $\\{a\\}$ as two different domain individuals at two different
worlds. Let’s now show the construction of the exponentially bounded
quasimodel based on the notion of _w-copies_. Suppose that
$\mathfrak{Q}=(W,\boldsymbol{q},\mathfrak{R})$ is a quasimodel for
$C_{\varphi}$. Now, we construct from $\mathfrak{Q}$ a quasimodel
$\mathfrak{Q}^{\prime}=(W_{1}\cup
W_{2},\boldsymbol{q}^{\prime},\mathfrak{R}^{\prime})$, where
$\boldsymbol{q}^{\prime}$ is the restriction of $\boldsymbol{q}$ to $W_{1}\cup
W_{2}$. We start with the construction of $W_{1}$ and a set of runs
$\mathfrak{G}$. First, we add to $W_{1}$ a world $w_{\varphi}\in W$ such that
$C_{\varphi}\in{\boldsymbol{t}}$, for some
${\boldsymbol{t}}\in\boldsymbol{q}(w_{\varphi})$. Such a world exists due to
B1. We then associate with every
${\boldsymbol{t}}\in\boldsymbol{q}(w_{\varphi})$ a run
$\rho_{{\boldsymbol{t}}}$ such that
$\rho_{{\boldsymbol{t}}}(w_{\varphi})={\boldsymbol{t}}$. These runs exist due
to M1. For each ${\boldsymbol{t}}\in\boldsymbol{q}(w_{\varphi})$ and for each
$\Diamond C\in{\boldsymbol{t}}$, select a world $w\in W$ such that
$C\in\rho_{{\boldsymbol{t}}}(w)$ (such a $w$ exists by R1), and add $w$ to
$W_{1}$. Thus, the resulting $W_{1}\subseteq W$ contains at most
$2^{|\mathsf{con}(C_{\varphi})|}\cdot{|\mathsf{con}(C_{\varphi})|}$ worlds.
Denote by $\rho^{\prime}_{{\boldsymbol{t}}}$ the restriction of
$\rho_{{\boldsymbol{t}}}$ to $W_{1}$, for every
${\boldsymbol{t}}\in\boldsymbol{q}(w_{\varphi})$. By construction, for every
${\boldsymbol{t}}\in\boldsymbol{q}(w_{\varphi})$,
$\rho^{\prime}_{{\boldsymbol{t}}}$ is a run through
$(W_{1},\boldsymbol{q}^{\prime})$. We thus set
$\mathfrak{G}=\\{\rho^{\prime}_{{\boldsymbol{t}}}\mid{\boldsymbol{t}}\in\boldsymbol{q}(w_{\varphi})\\}$,
and add all runs in $\mathfrak{G}$ to $\mathfrak{R}^{\prime}$. We now proceed
to the construction of $W_{2}$ and $\mathfrak{R}^{\prime}$ by using _w-copies_
of worlds in $W_{1}$, and by either introducing new runs or extending runs in
$\mathfrak{G}$ to worlds in $W_{2}$. This new construction is needed to
satisfy property M1 of quasimodels. Indeed, $\mathfrak{G}$ may not contain
runs coming through all types in $(W_{1},\boldsymbol{q}^{\prime})$. For every
$w\in W_{1}$, let ${\boldsymbol{t}}\in\boldsymbol{q}^{\prime}(w)$ such that
there is no $\rho\in\mathfrak{G}$ with ${\boldsymbol{t}}\in\rho(w)$. Then,
there exists $t^{\prime}\in\boldsymbol{q}^{\prime}(w)$, a run
$\rho\in\mathfrak{G}$, and a run $\rho_{{\boldsymbol{t}},w}\in\mathfrak{R}$
such that:

  1. T1

$\rho(w)={\boldsymbol{t}}^{\prime}$ and
$\rho_{{\boldsymbol{t}},w}(w)={\boldsymbol{t}}$;

  2. T2

$\rho(w_{\varphi})=\rho_{{\boldsymbol{t}},w}(w_{\varphi})$;

  3. T3

for any $\Diamond C\in{\boldsymbol{t}}$, $\Diamond
C\in{\boldsymbol{t}}^{\prime}$;

  4. T4

if $\Diamond C,\lnot C\in{\boldsymbol{t}}$, then, $\Box
C\not\in{\boldsymbol{t}}^{\prime}$.

The above properties are guaranteed by
$\mathfrak{Q}=(W,\boldsymbol{q},\mathfrak{R})$ being a quasimodel for
$C_{\varphi}$. We thus add $\rho_{{\boldsymbol{t}},w}$ to
$\mathfrak{R}^{\prime}$ and construct $W_{2}$ using _w-copies_ of quasistates
in $W_{1}$ in such a way that: for every $w_{2}\in W_{2}$ there is a unique
$w_{1}\in W_{1}$ such that $w_{2}$ is a _w-copy_ of $w_{1}$, and
$\boldsymbol{q}^{\prime}(w_{2})=\boldsymbol{q}^{\prime}(w_{1})$. Such _w-
copies_ are added to satisfy sub-concepts of the form $\Diamond C$ possibly
present in ${\boldsymbol{t}}$. We distinguish the following two cases:

  * •

Let $\Diamond\\{a\\},\lnot\\{a\\}\in{\boldsymbol{t}}$. Then, let $w_{a}\in
W_{1}$ such that $\\{a\\}\in\rho(w_{a})$ (wich exists by T3 and by
construction of $W_{1}$), add a fresh new _w-copy_ of $w_{a}$, say
$w^{\prime}_{a}$, to $W_{2}$ and extend the two runs, $\rho$ and
$\rho_{{\boldsymbol{t}},w}$, in the following way:

$\displaystyle\rho_{{\boldsymbol{t}},w}(w^{\prime}_{a})=\rho(w_{a});\quad\quad\rho(w^{\prime}_{a})=\rho_{{\boldsymbol{t}},w}(w_{a}).$

For all other runs in $r\in\mathfrak{R}^{\prime}$ their type is
$w^{\prime}_{a}$ is the same as the one in $w_{a}$, i.e.,
$r(w^{\prime}_{a})=r(w_{a})$.

  * •

Let $\Diamond C,\lnot C\in{\boldsymbol{t}}$. Then, let $w_{c}\in W_{1}$ such
that $C\in\rho(w_{a})$ (wich exists by T3 and by construction of $W_{1}$) and
$C\not\in\rho_{{\boldsymbol{t}},w}(w_{c})$ (for otherwise we don’t need to
introduce a new _w-copy_). Then, add a fresh new _w-copy_ of $w_{c}$, say
$w^{\prime}_{c}$, to $W_{2}$ and extend the two runs, $\rho$ and
$\rho_{{\boldsymbol{t}},w}$, in the following way:

$\displaystyle\rho_{{\boldsymbol{t}},w}(w^{\prime}_{c})=\rho(w_{c});\quad\quad\rho(w^{\prime}_{c})=\rho_{{\boldsymbol{t}},w}(w_{c}).$

For all other runs in $r\in\mathfrak{R}^{\prime}$ their type is
$w^{\prime}_{c}$ is the same as the one in $w_{c}$, i.e.,
$r(w^{\prime}_{c})=r(w_{c})$.

It is easy to show that all elements in $\mathfrak{R}^{\prime}$ are indeed
runs mainly due to T4 and the way _w-copies_ are added in $W_{2}$. At the same
time, we notice that $\mathfrak{Q}^{\prime}$ respects M1 and, in particular,
M2 due to the way we extend runs. As for the size of the set of worlds in
$\mathfrak{Q}^{\prime}$, we have that $|W_{1}\cup W_{2}|$ contains at most
$2^{2|\mathsf{con}(C_{\varphi})|}\cdot{|\mathsf{con}(C_{\varphi})|^{2}}$
worlds. ∎

By the previous theorem, we obtain decidability of the
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$ formula satisfiability problem
in NExpTime. Indeed, to check whether an
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$ formula $\varphi$ is
satisfiable, one can guess a triple
$\mathfrak{Q}=(W,\boldsymbol{q},\mathfrak{R})$ of size exponential in the
length of $\varphi$, and then check whether $\mathfrak{Q}$ is an
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}}}$ quasimodel for $\varphi$. Given
that already $\mathbf{S5}_{\mathcal{ALC}}$ formula satisfiability (without
nominals and universal role) is known to be NExpTime-hard [28, Theorem14.14],
we obtain a matching lower bound. By Lemma 2, we also get the following
result.

######  Theorem 2.

Partial $\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ formula
satisfiability without the RDA is NExpTime-complete.

##  5 Reasoning in temporal free description logics

In the following, we show that temporal DLs without RDA are undecidable,
differently from the case with RDA which has been shown to be decidable in the
absence of definite descriptions [28, Theorem 14.12]. We start considering the
DL $\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}}}$, obtained
from
$\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
by dropping definite descriptions. We show that, without the RDA for
individual names, the formula satisfiability problem is undecidable. This
result holds already for _total_ interpretations (hence also for the _partial_
case). The undecidability is due to the interaction between temporal
operators, the universal role, and nominals interpreted non-rigidly over time.
The main proof, that adapts an analogous one due to Degtyarev et al. [31],
goes by a reduction of the halting problem for Minsky machines to total
$\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}}}$ formula
satisfiability without the RDA.

######  Theorem 3.

$\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}}}$ formula
satisfiability without the RDA is undecidable.

###### Proof.

We consider the simpler case of a total interpretation. The result is obtained
by a reduction of the (undecidable) halting problem for (two-counter) Minsky
machines starting with $0$ as initial counters values [31, 32], that can be
encoded in $\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}}}$
without the RDA.

A _(two-counter) Minsky machine_ is a pair $M=(Q,P)$, where
$Q=\\{q_{0},\ldots,q_{L}\\}$ is a set of _states_ and
$P=(I_{0},\ldots,I_{L-1})$ is a sequence of _instructions_. We assume $q_{0}$
to be the _initial state_ , and $q_{L}$ to be the _halting state_. Moreover,
the instruction $I_{i}$ is executed at state $q_{i}$, for $0\leq i<L$. Each
instruction $I$ can have one of the following forms, where
$r\in\\{r_{1},r_{2}\\}$ is a _register_ , that stores non-negative integers as
values, and $q,q^{\prime}$ are states:

  1. 1.

$I=+(r,q)$ – add $1$ to the value of register $r$ and go to state $q$;

  2. 2.

$I=-(r,q,q^{\prime})$ – if the value of register $r$ is (strictly) greater
than $0$, subtract $1$ to the value of $r$ and go to state $q$; otherwise, go
to state $q^{\prime}$.

Given a Minsky machine $M$, a _configuration of $M$_ is a triple
$(q,v_{r_{1}},v_{r_{2}})$, where $q$ is a state of $M$ and
$v_{r_{1}},v_{r_{2}}\in\mathbb{N}$ are the _values_ of registers
$r_{1},r_{2}$, respectively. In the following, we set
$\overline{r_{k}}=r_{3-k}$, for $k\in\\{1,2\\}$. Given $i,j\geq 0$, we write
$(q_{i},v_{r_{1}},v_{r_{2}})\Rightarrow_{M}(q_{j},v^{\prime}_{r_{1}},v^{\prime}_{r_{2}})$
iff one of the following conditions hold:

  * •

$I_{i}=+(r,q_{j})$, $v^{\prime}_{r}=v_{r}+1$ and
$v^{\prime}_{\overline{r}}=v_{\overline{r}}$;

  * •

$I_{i}=-(r,q_{j},q^{\prime})$, $v_{r}>0$, $v^{\prime}_{r}=v_{r}-1$, and
$v^{\prime}_{\overline{r}}=v_{\overline{r}}$;

  * •

$I_{i}=-(r,q,q_{j})$, $v_{r}=v^{\prime}_{r}=0$, and
$v^{\prime}_{\overline{r}}=v_{\overline{r}}$.

Given an _input_ $(u,t)\in\mathbb{N}\times\mathbb{N}$, the _computation of $M$
on input $(u,t)$_ is the (unique) longest sequence of configurations
$(p_{0},v^{0}_{r_{1}},v^{0}_{r_{2}})\Rightarrow_{M}(p_{1},v^{1}_{r_{1}},v^{1}_{r_{2}})\Rightarrow_{M}\ldots$,
such that $p_{0}=q_{0}$, $v^{0}_{r_{1}}=u$ and $v^{0}_{r_{2}}=t$. We say that
$M$ _halts_ _on input_ $(0,0)$ if the computation of $M$ on input $(0,0)$ is
finite: thus, its initial configuration takes the form $(q_{0},0,0)$, while
its last configuration has the form $(q_{L},v_{r_{1}},v_{r_{2}})$. The
_halting problem for Minsky machines_ is the problem of deciding, given a
Minsky machine $M$, whether $M$ halts on input $(0,0)$. This problem is known
to be undecidable [31, 32].

To represent the computation of a Minsky machine $M$, we use the temporal
dimension to model successive configurations in the computation of $M$ on
input $(0,0)$. We introduce a concept name $Q_{i}$, for each state $q_{i}$ of
$M$. Concept names $R_{1},R_{2}$ are used to represent the registers
$r_{1},r_{2}$, respectively: the cardinality of their extensions at a given
instant will capture the values of the registers at one step of the
computation. The incrementation, respectively, the decrementation, by one unit
to the value of register $r_{k}$ is modelled by requiring the extensions of
concepts $\lnot
R_{k}\sqcap{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}R_{k}$,
respectively
$R_{k}\sqcap{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}\lnot
R_{k}$, to be included in those of nominals $\\{a_{r_{k}}\\}$ and
$\\{b_{r_{k}}\\}$, respectively. Since the individual names $a_{r_{k}}$ and
$b_{r_{k}}$ are interpreted _non-rigidly_ , the (unique) element added or
subtracted from the extension of $R_{k}$ is forced to vary over time. In the
following, for $k\in\\{1,2\\}$, we set $\overline{R_{k}}=R_{3-k}$.

The initial configuration $(q_{0},0,0)$ of $M$, together with the assumptions
that at each configuration the machine is in exactly one state, and that the
halting state is reached only at the last configuration, are represented by
the conjunction of the following formulas (recall that
$\textit{last}:=\Box\bot$):

  1. $(\textbf{S1})$

$R_{1}\sqsubseteq\bot$;

  2. $(\textbf{S2})$

$R_{2}\sqsubseteq\bot$;

  3. $(\textbf{S3})$

$\top\sqsubseteq Q_{0}$;

  4. $(\textbf{S4})$

$\Box^{+}(\top\sqsubseteq\bigsqcup_{i=1}^{L}Q_{i})$;

  5. $(\textbf{S5})$

$\bigwedge_{i=1}^{L}\Box^{+}(Q_{i}\sqsubseteq\bigsqcap_{j\neq i}\lnot Q_{j})$;

  6. $(\textbf{S6})$

$\Box^{+}(Q_{L}\equiv\textit{last})$.

Instructions of the form $I_{i}=+(r_{k},q_{j})$ are represented by the
conjunction of the following formulas:

  1. $(\textbf{I1})$

$\Box^{+}(Q_{i}\sqsubseteq\exists u.(\lnot
R_{k}\sqcap{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}R_{k}))$;

  2. $(\textbf{I2})$

$\Box^{+}(Q_{i}\sqsubseteq\forall u.(\lnot
R_{k}\sqcap{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}R_{k}\Rightarrow\\{a_{r_{k}}\\}))$;

  3. $(\textbf{I3})$

$\Box^{+}(Q_{i}\sqsubseteq\forall
u.(R_{k}\Rightarrow{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}R_{k}))$;

  4. $(\textbf{I4})$

$\Box^{+}(Q_{i}\sqsubseteq\forall
u.(\overline{R_{k}}\Leftrightarrow{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}\overline{R_{k}}))$;

  5. $(\textbf{I5})$

$\Box^{+}(Q_{i}\sqsubseteq{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}Q_{j})$.

Instructions of the form $I_{i}=-(r_{k},q_{j},q_{h})$ are represented by the
conjunction of the following formulas:

  1. $(\textbf{D1})$

$\Box^{+}(Q_{i}\sqcap\exists u.R_{k}\sqsubseteq\exists
u.(R_{k}\sqcap{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}\lnot
R_{k}))$;

  2. $(\textbf{D2})$

$\Box^{+}(Q_{i}\sqcap\exists u.R_{k}\sqsubseteq\forall
u.(R_{k}\sqcap{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}\lnot
R_{k}\Rightarrow\\{b_{r_{k}}\\}))$;

  3. $(\textbf{D3})$

$\Box^{+}(Q_{i}\sqcap\exists u.R_{k}\sqsubseteq\forall
u.({\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}R_{k}\Rightarrow
R_{k}))$;

  4. $(\textbf{D4})$

$\Box^{+}(Q_{i}\sqcap\exists u.R_{k}\sqsubseteq\forall
u.(\overline{R_{k}}\Leftrightarrow{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}\overline{R_{k}}))$;

  5. $(\textbf{D5})$

$\Box^{+}(Q_{i}\sqcap\lnot\exists u.R_{k}\sqsubseteq\forall
u.({R_{1}}\Leftrightarrow{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}{R_{1}})\sqcap\forall
u.({R_{2}}\Leftrightarrow{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}{R_{2}}))$;

  6. $(\textbf{D6})$

$\Box^{+}(Q_{i}\sqcap\exists
u.R_{k}\sqsubseteq{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}Q_{j})$;

  7. $(\textbf{D7})$

$\Box^{+}(Q_{i}\sqcap\lnot\exists
u.R_{k}\sqsubseteq{\raisebox{1.07639pt}{\text{\scriptsize{$\bigcirc$}}}}Q_{h})$.

Let $\chi^{M}$ be the conjunction of the CIs above, for $0\leq i<L$. We
require the following claim.

######  Claim 2.

A Minsky machine $M$ halts on input $(0,0)$ iff $\chi_{M}$ is satisfiable on
finite total traces without the RDA.

###### Proof of Claim 2.

$(\Rightarrow)$ Let $M$ be a Minsky machine that halts on input $(0,0)$, and
let
$(p_{0},0,0)\Rightarrow_{M}\ldots\Rightarrow_{M}(p_{n},v^{n}_{r_{1}},v^{n}_{r_{2}})$
be the computation of $M$ on input $(0,0)$, where $p_{0}=q_{0}$, $n\geq 0$ and
$p_{n}=q_{L}$. We construct a finite total trace
$\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in\mathfrak{T}})$ such that
$\mathfrak{M},0\models\chi_{M}$. Let $\mathfrak{T}=[0,n]$, and let $\Delta$ be
a fixed countable set. Given $t\in[0,n]$ and $p_{t}=q_{i}$, for some $0\leq
i\leq L$, we set $Q_{i}^{\mathcal{I}_{t}}=\Delta$ and
$Q_{j}^{\mathcal{I}_{t}}=\emptyset$, for all $j\neq i$. In addition, we set
$R_{1}^{\mathcal{I}_{0}}=R_{2}^{\mathcal{I}_{0}}=\emptyset$, while
$a_{r_{k}}^{\mathcal{I}_{0}}=d\in\Delta$, and
$b_{r_{k}}^{\mathcal{I}_{0}}=e\in\Delta$, for some $d\neq e$. Moreover, for an
instant $0\leq t<n$, we define the interpretations
$R_{1}^{\mathcal{I}_{t+1}}$, $R_{2}^{\mathcal{I}_{t+1}}$,
$a_{r_{k}}^{\mathcal{I}_{t+1}}$, and $b_{r_{k}}^{\mathcal{I}_{t+1}}$
inductively as follows.

  * •

If $p_{t}=q_{i}$ and $I_{i}=+(r_{k},q_{j})$, then we set:
$R_{k}^{\mathcal{I}_{t+1}}=R_{k}^{\mathcal{I}_{t}}\cup\\{d\\}$, where
$d=a_{r_{k}}^{\mathcal{I}_{t}}$; $a_{r_{k}}^{\mathcal{I}_{t+1}}=d^{\prime}$,
for a $d^{\prime}\not\in R_{k}^{\mathcal{I}_{t}}$;
$b_{r_{k}}^{\mathcal{I}_{t+1}}=a_{r_{k}}^{\mathcal{I}_{t}}$;
$\overline{R_{k}}^{\mathcal{I}_{t+1}}=\overline{R_{k}}^{\mathcal{I}_{t}}$.

  * •

If $p_{t}=q_{i}$ and $I_{i}=-(r_{k},q_{j},q_{h})$, then:

    * –

if $R_{k}^{\mathcal{I}_{t}}\neq\emptyset$, then we set:
$R_{k}^{\mathcal{I}_{t+1}}=R_{k}^{\mathcal{I}_{t}}\setminus\\{e\\}$, where
$e=b_{r_{k}}^{\mathcal{I}_{t}}$; $b_{r_{k}}^{\mathcal{I}_{t+1}}=e^{\prime}$,
for an $e^{\prime}\in R_{k}^{\mathcal{I}_{t+1}}$, if
$R_{k}^{\mathcal{I}_{t+1}}\neq\emptyset$, and $b_{r_{k}}^{\mathcal{I}_{t+1}}$
arbitrary, otherwise;
$a_{r_{k}}^{\mathcal{I}_{t+1}}=a_{r_{k}}^{\mathcal{I}_{t}}$;
$\overline{R_{k}}^{\mathcal{I}_{t+1}}=\overline{R_{k}}^{\mathcal{I}_{t}}$.

    * –

if $R_{k}^{\mathcal{I}_{t}}=\emptyset$, then we set:
$R_{1}^{\mathcal{I}_{t+1}}=R_{1}^{\mathcal{I}_{t}}$,
$R_{2}^{\mathcal{I}_{t+1}}=R_{2}^{\mathcal{I}_{t}}$;
$a_{r_{k}}^{\mathcal{I}_{t+1}}=a_{r_{k}}^{\mathcal{I}_{t}}$;
$b_{r_{k}}^{\mathcal{I}_{t+1}}=b_{r_{k}}^{\mathcal{I}_{t}}$.

It can be seen that, by construction, $\mathfrak{M},0\models\chi_{M}$.

$(\Leftarrow)$ Given a Minsky machine $M$, suppose that $\chi_{M}$ is
satisfied on a finite total trace
$\mathfrak{M}=(\Delta,(\mathcal{I}_{t})_{t\in\mathfrak{T}})$, with
$\mathfrak{T}=[0,n]$. To each time point $t\in[0,n]$, we associate a
configuration of $M$ of the form $(p_{t},v^{t}_{r_{1}},v^{t}_{r_{2}})$ so that
$p_{t}=q_{j}$, where $q_{j}$ is the state of $M$ such that
$\mathfrak{M},t\models\top\sqsubseteq Q_{j}$, which is entailed by
$(\textbf{S4})$ and $(\textbf{S5})$, and
$v^{t}_{r_{k}}=|R_{k}^{\mathcal{I}_{t}}|$.

Let $t=0$. By $(\textbf{S3})$, we have $p_{0}=q_{0}$, and
$v^{0}_{r_{k}}=|R_{k}^{\mathcal{I}_{0}}|=0$, by $(\textbf{S1})$,
$(\textbf{S2})$. Thus, the initial configuration of the computation of $M$ is
$(q_{0},0,0)$.

For $0\leq t<n$, we show that
$(p_{t},v^{t}_{r_{1}},v^{t}_{r_{2}})\Rightarrow_{M}(p_{t+1},v^{t+1}_{r_{1}},v^{t+1}_{r_{2}})$.
Let $p_{t}=q_{i}$.

  * •

Suppose $I_{i}=+(r_{k},q_{j})$. By $(\textbf{I5})$, we have that
$\mathfrak{M},t+1\models\top\sqsubseteq Q_{j}$, and thus $p_{t+1}=q_{j}$.
Moreover, by $(\textbf{I1})$, $(\textbf{I2})$, and $(\textbf{I3})$, we have
that $|R_{k}^{\mathcal{I}_{t+1}}|=|R_{k}^{\mathcal{I}_{t}}|+1$, thus
$v^{t+1}_{r_{k}}=v^{t}_{r_{k}}+1$. Instead, by $(\textbf{I4})$,
$|\overline{R_{k}}^{\mathcal{I}_{t+1}}|=|\overline{R_{k}}^{\mathcal{I}_{t}}|$,
hence $v^{t+1}_{\overline{r_{k}}}=v^{t}_{\overline{r_{k}}}$.

  * •

Suppose $I_{i}=-(r_{k},q_{j},q_{h})$.

    * –

If $\mathfrak{M},t\models\top\sqsubseteq\exists u.R_{k}$, we have by
$(\textbf{D6})$ that $\mathfrak{M},t+1\models\top\sqsubseteq Q_{j}$, and thus
$p_{t+1}=q_{j}$. Moreover, by $(\textbf{D1})$, $(\textbf{D2})$, and
$(\textbf{D3})$, we have that
$|R_{k}^{\mathcal{I}_{t+1}}|=|R_{k}^{\mathcal{I}_{t}}|-1$, thus
$v^{t+1}_{r_{k}}=v^{t}_{r_{k}}-1$. Instead, by $(\textbf{D4})$,
$|\overline{R_{k}}^{\mathcal{I}_{t+1}}|=|\overline{R_{k}}^{\mathcal{I}_{t}}|$,
hence $v^{t+1}_{\overline{r_{k}}}=v^{t}_{\overline{r_{k}}}$.

    * –

If $\mathfrak{M},t\not\models\top\sqsubseteq\exists u.R_{k}$, we have by
$(\textbf{D7})$ that $\mathfrak{M},t+1\models\top\sqsubseteq Q_{h}$, and thus
$p_{t+1}=q_{h}$. Moreover, by $(\textbf{D5})$, we have both that
$|R_{k}^{\mathcal{I}_{t+1}}|=|R_{k}^{\mathcal{I}_{t}}|=0$, thus
$v^{t+1}_{r_{k}}=v^{t}_{r_{k}}=0$, and
$|\overline{R_{k}}^{\mathcal{I}_{t+1}}|=|\overline{R_{k}}^{\mathcal{I}_{t}}|$,
hence $v^{t+1}_{\overline{r_{k}}}=v^{t}_{\overline{r_{k}}}$.

Finally, since $n$ is the last instant of the trace, i.e.,
$\mathfrak{M},n\models\top\sqsubseteq\textit{last}$, we have by
$(\textbf{S6})$ that $\mathfrak{M},n\models\top\sqsubseteq Q_{L}$, Therefore,
the last configuration of the computation of $M$ (and the last only) takes the
form $(q_{L},v^{n}_{r_{1}},v^{n}_{r_{2}})$, as required. ∎

Thanks to the previous claim, and the fact that the halting problem for Minsky
machines is undecidable [31, 32], we conclude the proof. ∎

As a next step, we require the following polynomial-time reduction, from
formula satisfiability on finite traces to the same problem over infinite
traces.

######  Lemma 4.

Partial and total
$\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}}}$ formula
satisfiability without the RDA are polynomial-time reducible to, respectively,
partial and total $\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}}}$ formula
satisfiability without the RDA.

###### Proof.

It is enough to observe that a $\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}}}$
formula $\varphi$ can be transformed, by using the standard translation of
temporal DLs into temporal first-order logic [28], into an equisatisfiable
${\mathcal{T}_{\mathbin{\mathcal{U}}}\mathcal{QL}}$ formula
$\varphi^{\prime}$. Such a ${\mathcal{T}_{\mathbin{\mathcal{U}}}\mathcal{QL}}$
formula $\varphi^{\prime}$ can be then mapped, by using the translation
$\cdot^{\dagger}$ given in [33], into a
${\mathcal{T}_{\mathbin{\mathcal{U}}}\mathcal{QL}}$ formula
$\varphi^{\prime\dagger}$ such that $\varphi^{\prime}$ is satisfiable on
finite, respectively partial or total, traces iff $\varphi^{\prime\dagger}$ is
satisfiable on infinite traces, respectively partial or total (the notion of
partial trace, given for $\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}}}$, can
be naturally extended to the
${\mathcal{T}_{\mathbin{\mathcal{U}}}\mathcal{QL}}$ case). ∎

Given that $\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}}}$ is a syntactic
fragment of $\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$, as
an immediate consequence of Theorem 3 and the reductions given in Lemmas 1 and
4, we obtain the following result, holding for total, and hence partial,
interpretations.

######  Theorem 4.

$\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}}}$,
$\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ and
$\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
formula satisfiability without the RDA are undecidable.

Preserving RDA is not enough to regain decidability for the temporal DLs with
definite descriptions. Indeed, by exploiting definite descriptions that behave
non-rigidly we can still encode incrementation and decrementation of counters’
values (in place of non-rigid nominals), yielding the following result, proved
for total interpretations, and hence holding for partial interpretations, too.

######  Corollary 1.

$\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ and
$\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
formula satisfiability with the RDA is undecidable.

##  6 Discussion and Future Work

We moved first steps in the study of modal free description logics, focussing
in particular on the epistemic free DL
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$, and on the
temporal free DLs
$\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ and
$\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$.
Syntactically, these DLs extend the classical $\smash{\mathcal{ALCO}_{\\!u}}$,
with nominals and the universal role, by including definite descriptions and
modal or temporal operators. Semantically, adapting ideas from the non-modal
$\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}$ case, we interpret these DLs
over modal (epistemic or temporal) interpretations that allow for: (i) _non-
denoting_ terms, that is, individual expressions that can be left
uninterpreted at certain states, hence encoding “error” or “empty” values; and
(ii) _non-rigid_ designators, making individual names and definite
descriptions referential devices capable of picking different objects at
different states, to represent “dynamic” or “flexible” values. The main
technical results concern formula satisfiability: we show that, while this
problem is NExpTime-complete for
$\mathbf{S5}_{\smash{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ on epistemic
frames, it becomes undecidable both for
$\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$ and
$\smash{\mathbf{LTL}^{\boldsymbol{f}}_{\mathcal{ALCO}_{\\!u}^{\smash{\iota}}}}$
on, respectively, infinite and finite temporal traces.

As future work, we intend to strengthen our results, as well as deepen the
connections between free DLs with definite descriptions, on the one hand, and
modal operators, on the other. On the epistemic side, we are interested in:
(i) considering frames for the propositional modal logics $\mathbf{K4}$,
$\mathbf{T}$, $\mathbf{S4}$, or $\mathbf{KD45}$, to model different doxastic
or epistemic attitudes that might satisfy or not the so-called _factivity_ and
_introspection_ principles [28]; (ii) investigating of non-rigid descriptions
and names in the context of _non-normal_ modal DLs, such as the ones obtained
from the systems $\mathbf{E}$, $\mathbf{M}$, $\mathbf{C}$, and $\mathbf{N}$
[34, 35, 36], to avoid the _logical omniscience_ problem (i.e., an agent knows
all the logical truths and all the consequences of their background
knowledge), which affects all the systems extending $\mathbf{K}$ [37, 38];
(iii) addressing less expressive DL languages, such as
$\smash{\mathcal{ELO}_{\\!u}^{\smash{\iota}}}$, in an epistemic setting, and
connect them with the recently investigated _standpoint DL_ family [39, 40].

On the temporal side, and in particular concerning our undecidability proofs,
we observe the following. Degtyarev et al. [31] use equality to encode a one-
unit addition or subtraction from a register’s value at subsequent steps of a
two-counter Minsky machine computation. In our case, the same effect is due to
the interplay between non-rigid (and possibly non-denoting) nominals and the
universal role. Related results appear also in Hampson and Kurucz [41], where
the undecidability of _one-variable first-order temporal logic with counting
to two_ , denoted by FOLTL≠, is proved. In their setting, the _difference_
existential quantifier $\exists^{\neq}x$ extends the language of one-variable
(monadic) first-order temporal logic: formulas like $\exists^{\neq}x\varphi$
enforce that $\varphi$ holds for some individual different from the one
assigned to $x$. Their undecidability proof for satisfiability of FOLTL≠ on
finite or infinite traces with constant domains is also based on an encoding
of the computation of two-counter Minsky machines.

It seems thus that a form of interaction between the universal role and
counting constructors (even simply up to one, as in
$\smash{\mathbf{LTL}_{\mathcal{ALCO}_{\\!u}}}$, with non-rigid and possibly
non-denoting nominals) plays a role in these kinds of undecidability proofs.
However, it is not yet clear whether already
$\smash{\mathbf{LTL}_{\mathcal{ALCO}}}$ or
$\smash{\mathbf{LTL}_{\mathcal{ALCO}^{\smash{\iota}}}}$ satisfiability, on
partial temporal interpretations and with non-rigid nominals, but _without_
the universal quantifier, is undecidable. To obtain a similar proof, one would
have to suitably replace the universal role with dedicated roles for counters,
while forcing them to stay “global” enough not to lose any information about
the values of the counters at subsequent computation steps. We leave this open
question for future work.

Finally, we remark that the preliminary negative results presented here for
temporal free DLs might not entirely undermine the use of definite
descriptions on a temporal dimension. For applications in temporal conceptual
modelling and ontology-mediated query answering [23, 42], it is worth
exploring whether more encouraging results can be obtained in fragments
restricting the use of temporal operators (limited, e.g., to the $\Box$
operator only), or constraining the DL dimension (such as the already
mentioned $\smash{\mathbf{LTL}_{\mathcal{ALCO}^{\smash{\iota}}}}$, without the
universal role, or lightweight members of the TDL-Lite family [43]). Any of
these restrictions should, of course, be designed to preserve an interesting
degree of interaction between the DL constructors and the non-rigidity of
names and descriptions.

Finally, we are interested in studying in this setting the complexities of
other problems than formula satisfiability. Related to _interpolant_ and
_explicit definition existence_ [44, 45, 46], the _referring expression
existence_ problem [11], which asks whether there exists a description for an
individual under an ontology and a given signature, is of particular interest
to epistemic and temporal scenarios with definite descriptions.

## Acknowledgements

Andrea Mazzullo acknowledges the support of the MUR PNRR project FAIR - Future
AI Research (PE00000013) funded by the NextGenerationEU.

## References

  * Borgida et al. [2016] A. Borgida, D. Toman, G. E. Weddell,  On referring expressions in query answering over first order knowledge bases,  in: Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR-16), AAAI Press, 2016, pp. 319–328.
  * Borgida et al. [2017] A. Borgida, D. Toman, G. E. Weddell,  Concerning referring expressions in query answers,  in: Proceedings of the 26th International Joint Conference on Artificial Intelligence, (IJCAI-17), ijcai.org, 2017, pp. 4791–4795.
  * Toman and Weddell [2018] D. Toman, G. E. Weddell,  Identity resolution in conjunctive querying over dl-based knowledge bases,  in: Proceedings of the 31st International Workshop on Description Logics (DL-18), volume 2211 of CEUR Workshop Proceedings, CEUR-WS.org, 2018.
  * Bencivenga [2002] E. Bencivenga,  Free logics,  in: Handbook of Philosophical Logic, Springer, 2002, pp. 147–196.
  * Lehmann [2002] S. Lehmann,  More free logic,  in: Handbook of Philosophical Logic, Springer, 2002, pp. 197–259.
  * Indrzejczak [2021] A. Indrzejczak,  Free logics are cut-free,  Stud Logica 109 (2021) 859–886.
  * Indrzejczak and Zawidzki [2021] A. Indrzejczak, M. Zawidzki,  Tableaux for free logics with descriptions,  in: A. Das, S. Negri (Eds.), Proceedings of the 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-21), volume 12842 of Lecture Notes in Computer Science, Springer, 2021, pp. 56–73.
  * Russell [1905] B. Russell,  On Denoting,  Mind 14 (1905) 479–493.
  * Neuhaus et al. [2020] F. Neuhaus, O. Kutz, G. Righetti,  Free description logic for ontologists,  in: Proceedings of the Joint Ontology Workshops (JOWO-20), volume 2708 of CEUR Workshop Proceedings, CEUR-WS.org, 2020.
  * Artale et al. [2020] A. Artale, A. Mazzullo, A. Ozaki, F. Wolter,  On free description logics with definite descriptions,  in: Proceedings of the 33rd International Workshop on Description Logics (DL-20), volume 2663 of CEUR Workshop Proceedings, CEUR-WS.org, 2020.
  * Artale et al. [2021] A. Artale, A. Mazzullo, A. Ozaki, F. Wolter,  On free description logics with definite descriptions,  in: Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR-21), 2021, pp. 63–73.
  * Fitting [2004] M. Fitting,  First-order intensional logic,  Ann. Pure Appl. Log. 127 (2004) 171–193.
  * Fitting and Mendelsohn [2012] M. Fitting, R. L. Mendelsohn, First-order Modal Logic, Springer Science & Business Media, 2012.
  * Cocchiarella [1984] N. B. Cocchiarella,  Philosophical perspectives on quantification in tense and modal logic II: Extensions of Classical Logic (1984) 309–353.
  * Garson [2001] J. W. Garson,  Quantification in modal logic,  in: Handbook of philosophical logic, volume II: Extensions of Classical Logic, Springer, 2001, pp. 267–323.
  * Braüner and Ghilardi [2007] T. Braüner, S. Ghilardi,  First-order Modal Logic,  in: Handbook of Modal Logic, Elsevier, 2007, pp. 549–620.
  * Kröger and Merz [2008] F. Kröger, S. Merz, Temporal Logic and State Systems, Texts in Theoretical Computer Science. An EATCS Series, Springer, 2008\.
  * Corsi and Orlandelli [2013] G. Corsi, E. Orlandelli,  Free quantified epistemic logics,  Studia Logica 101 (2013) 1159–1183.
  * Indrzejczak [2020] A. Indrzejczak,  Existence, definedness and definite descriptions in hybrid modal logic,  in: Proceedings of the 13th Conference on Advances in Modal Logic (AiML-20), College Publications, 2020, pp. 349–368.
  * Orlandelli [2021] E. Orlandelli,  Labelled calculi for quantified modal logics with definite descriptions,  J. Log. Comput. 31 (2021) 923–946.
  * Wolter and Zakharyaschev [1998] F. Wolter, M. Zakharyaschev,  Temporalizing description logics,  in: Proceedings of the 2nd International Symposium on Frontiers of Combining Systems (FroCoS-98), Research Studies Press/Wiley, 1998, pp. 104–109.
  * Artale and Franconi [2005] A. Artale, E. Franconi,  Temporal description logics,  in: Handbook of Temporal Reasoning in Artificial Intelligence, volume 1 of Foundations of Artificial Intelligence, Elsevier, 2005, pp. 375–388.
  * Lutz et al. [2008] C. Lutz, F. Wolter, M. Zakharyaschev,  Temporal description logics: A survey,  in: Proceedings of the 15th International Symposium on Temporal Representation and Reasoning (TIME-08), IEEE Computer Society, 2008, pp. 3–14.
  * Donini et al. [1998] F. M. Donini, M. Lenzerini, D. Nardi, W. Nutt, A. Schaerf,  An epistemic operator for description logics,  Artif. Intell. 100 (1998) 225–274.
  * Calvanese et al. [2008] D. Calvanese, G. D. Giacomo, D. Lembo, M. Lenzerini, R. Rosati,  Inconsistency tolerance in P2P data integration: An epistemic logic approach,  Inf. Syst. 33 (2008) 360–384.
  * Console and Lenzerini [2020] M. Console, M. Lenzerini,  Epistemic integrity constraints for ontology-based data management,  in: Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI-20), AAAI Press, 2020, pp. 2790–2797.
  * Mehdi and Rudolph [2011] A. Mehdi, S. Rudolph,  Revisiting semantics for epistemic extensions of description logics,  in: Proceedings of the 25th AAAI Conference on Artificial Intelligence (AAAI-11), AAAI Press, 2011\.
  * Gabbay et al. [2003] D. M. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Many-dimensional Modal Logics: Theory and Applications, North Holland Publishing Company, 2003.
  * Baader et al. [2003] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, P. F. Patel-Schneider (Eds.), The Description Logic Handbook: Theory, Implementation, and Applications, Cambridge University Press, 2003.
  * Rudolph [2011] S. Rudolph,  Foundations of description logics,  in: Tutorial Lectures of the 7th International Summer School 2011 on Reasoning Web, volume 6848 of Lecture Notes in Computer Science, Springer, 2011, pp. 76–136.
  * Degtyarev et al. [2002] A. Degtyarev, M. Fisher, A. Lisitsa,  Equality and monodic first-order temporal logic,  Studia Logica 72 (2002) 147–156.
  * Baader et al. [2017] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge University Press, 2017.
  * Artale et al. [2022] A. Artale, A. Mazzullo, A. Ozaki,  First-order temporal logic on finite traces: Semantic properties, decidable fragments, and applications,  CoRR abs/2202.00610 (2022).
  * Dalmonte et al. [2019] T. Dalmonte, A. Mazzullo, A. Ozaki,  On non-normal modal description logics,  in: M. Simkus, G. E. Weddell (Eds.), DL, volume 2373, CEUR-WS.org, 2019.
  * Dalmonte et al. [2022] T. Dalmonte, A. Mazzullo, A. Ozaki,  Reasoning in non-normal modal description logics,  in: C. Benzmüller, J. Otten (Eds.), ARQNL@IJCAR, volume 2095, 2022, pp. 28–45.
  * Dalmonte et al. [2023] T. Dalmonte, A. Mazzullo, A. Ozaki, N. Troquard,  Non-normal modal description logics,  in: Proceedings of the 18th European Conference on Logics in Artificial Intelligence (JELIA-23), to appear, 2023\.
  * Vardi [1986] M. Y. Vardi,  On epistemic logic and logical omniscience,  in: J. Y. Halpern (Ed.), Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK-86), Morgan Kaufmann, 1986, pp. 293–305.
  * Vardi [1989] M. Y. Vardi,  On the complexity of epistemic reasoning,  in: Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS-89), IEEE Computer Society, 1989, pp. 243–252.
  * Gómez Álvarez et al. [2022] L. Gómez Álvarez, S. Rudolph, H. Strass,  How to agree to disagree - managing ontological perspectives using standpoint logic,  in: Proceedings of the 21st International Semantic Web Conference (ISWC-22), volume 13489, 2022, pp. 125–141.
  * Gómez Álvarez et al. [2023] L. Gómez Álvarez, S. Rudolph, H. Strass,  Tractable diversity: Scalable multiperspective ontology management via standpoint EL,  CoRR abs/2302.13187 (2023).
  * Hampson and Kurucz [2015] C. Hampson, A. Kurucz,  Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting,  ACM Trans. Comput. Log. 16 (2015) 27:1–27:36.
  * Artale et al. [2017] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, M. Zakharyaschev,  Ontology-mediated query answering over temporal data: A survey (invited talk),  in: Proceedings of the 24th International Symposium on Temporal Representation and Reasoning, (TIME-17), volume 90 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, pp. 1:1–1:37.
  * Artale et al. [2014] A. Artale, R. Kontchakov, V. Ryzhikov, M. Zakharyaschev,  A cookbook for temporal conceptual data modelling with description logics,  ACM Trans. Comput. Log. 15 (2014) 25:1–25:50.
  * Artale et al. [2021] A. Artale, J. C. Jung, A. Mazzullo, A. Ozaki, F. Wolter,  Living without beth and craig: Definitions and interpolants in description logics with nominals and role inclusions,  in: Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI-21), AAAI Press, 2021, pp. 6193–6201.
  * Artale et al. [2023] A. Artale, J. C. Jung, A. , Mazzullo, A. Ozaki, F. Wolter,  Living without beth and craig: Definitions and interpolants in description and modal logics with nominals and role inclusions,  ACM Trans. Comput. Log. Online (Just Accepted) (2023).
  * Kurucz et al. [2023] A. Kurucz, F. Wolter, M. Zakharyaschev,  Definitions and (uniform) interpolants in first-order modal logic,  CoRR abs/2303.04598 (2023).