11institutetext:  Free University of Bozen-Bolzano 11email:
<EMAIL_ADDRESS>22institutetext: University of Trento 22email:
<EMAIL_ADDRESS>33institutetext: University of Oslo & University of
Bergen 33email<EMAIL_ADDRESS>
# Non-Normal Modal Description Logics
(Extended Version)

Tiziano Dalmonte1 Andrea Mazzullo2 Ana Ozaki3 Nicolas Troquard1

###### Abstract

Modal logics are widely used in multi-agent systems to reason about actions,
abilities, norms, or epistemic states. Combined with description logic
languages, they are also a powerful tool to formalise modal aspects of
ontology-based reasoning over an object domain. However, the standard
relational semantics for modalities is known to validate principles deemed
problematic in agency, deontic, or epistemic applications. To overcome these
difficulties, weaker systems of so-called _non-normal_ modal logics, equipped
with _neighbourhood semantics_ that generalise the relational one, have been
investigated both at the propositional and at the description logic level. We
present here a family of _non-normal modal description logics_ , obtained by
extending $\smash{\mathcal{ALC}}$-based languages with non-normal modal
operators. For formulas interpreted on neighbourhood models over varying
domains, we provide a modular framework of terminating, correct, and complete
tableau-based satisfiability checking algorithms in NExpTime. For a subset of
these systems, we also consider a reduction to satisfiability on constant
domain relational models. Moreover, we investigate the satisfiability problem
in fragments obtained by disallowing the application of modal operators to
description logic concepts, providing tight ExpTime complexity results.

##  1 Introduction

_Modal logics_ are powerful tools used to represent and reason about actions
and abilities [10, 15], coalitions [30, 38], knowledge and beliefs [1, 8, 39,
25], obligations and permissions [2, 19, 41], etc. In combination with
_description logics_ , they give rise to _modal description logics_ [42, 17],
knowledge representation formalisms used for modal reasoning over an object
domain and with a good trade-off between expressive power and decidability.

The standard _relational semantics_ for modal operators is given in terms of
_frames_ consisting of a set of _possible worlds_ equipped with binary
_accessibility relations_. The foundations of modal description logics, so
far, have also mostly been studied with relational semantics. However, all the
modal systems interpreted with respect to this semantics, known as _normal_ ,
validate principles that have been considered problematic or debatable for
agency-based, coalitional, epistemic, or deontic applications, in that they
lead to unacceptable conclusions, e.g., _logical omniscience_ in epistemic
settings [39], as well as _agency_ or _deontic paradoxes_ in the
representation of agents’ abilities [15] and obligations [31, 3, 16].

To overcome these problems, a generalisation of relational semantics, known as
_neighbourhood semantics_ , was introduced by Scott [33] and Montague [26].
Since it avoids in general the problematic principles validated by relational
semantics, it has been used to interpret a number of _non-normal_ modal
logics, first studied by C.I. Lewis [24], Lemmon [23], Kripke [22], Segerberg
[34], and Chellas [11], among others. A _neighbourhood frame_ consists of a
set of worlds, each one associated with a “neighbourhood”, i.e., a set of
subsets of worlds. Intuitively, a subset of worlds can be thought of as
representing a fact in a model, namely, those worlds where that fact holds.
Hence, the idea is that every world is assigned to a collection of facts,
those that are brought about, known, obligatory, etc., in that world of the
model.

These are the neighbourhood semantics ingredients for _propositional_ non-
normal modal logics. A further line of research focuses on the behaviour of
modal operators interpreted on neighbourhood frames in combination with
_first-order_ logic. In this direction, completeness results for first-order
non-normal modal logics have been provided [4, 5]. In addition, _non-normal
modal_ _description logics_ , extending standard description logics, with
modal operators interpreted on neighbourhood frames, have been considered for
knowledge representation applications [35, 13, 14], also in multi-agent
coalitional settings [37, 36].

To illustrate the expressivity of non-normal modal description logic
languages, as well some of the limitations of relational frames behind
adoption of neighbourhood semantics, we provide an example based on a classic
multi-agent purchase choreography scenario [27] (see the Appendix for a
detailed version). Our multi-agent setting involves a customer $\mathit{c}$
and a seller $\mathit{s}$, as well as agency operators $\mathbb{D}_{i}$ and
$\mathbb{C}_{i}$, for $i\in\\{c,s\\}$, read as ‘agent $i$ does/makes’ and
‘agent $i$ can do/make’, respectively [15, 20]. The formula
$\mathsf{Ord}\equiv\mathbb{D}_{c}\exists\mathsf{req}.(\mathsf{Prod}\sqcap\mathsf{InCatal})$
defines an order $\mathsf{Ord}$ as a request made by customer $c$ of an in-
catalogue product.

By stating
$\exists\mathsf{req}.(\mathsf{Prod}\sqcap\mathsf{InCatal})\sqsubseteq\mathsf{Confirm}\sqcup\lnot\mathsf{Confirm},$
we can also enforce that any request of an in-catalogue product is either
confirmed or not confirmed. However, relational semantics validates the so-
called _$\mathbf{M}$ -principle_ (often called _monotonicity_) as well,
according to which $C\sqsubseteq D$ always entails
$\mathbb{D}_{c}C\sqsubseteq\mathbb{D}_{c}D$, for any concepts $C,D$. Thus,
from the $\mathbf{M}$-principle and $\mathsf{Ord}$ definition, we obtain
$\mathsf{Ord}\sqsubseteq\mathbb{D}_{c}(\mathsf{Confirm}\sqcup\lnot\mathsf{Confirm}),$
meaning that any order is made confirmed or not confirmed by $c$. This is an
unwanted conclusion in our agency-based scenario, since customers’ actions
should be unrelated to order confirmation aspects.111Other approaches (out of
the scope of this paper) to avoid such consequences would involve rejecting
the principle of _excluded middle_ , as done e.g. in _intuitionistic
description logics_ [29, 9, 32].

Moreover, the formula
$\mathsf{SubmitOrd}\sqsubseteq\mathbb{C}_{s}\mathsf{Confirm}\sqcap\mathbb{C}_{s}\mathsf{PartConf}\sqcap\mathbb{C}_{s}\mathsf{Reject}$
states that a submitted order can be confirmed, can be partially confirmed,
and can be rejected by the seller $s$. On relational frames,
$\mathbb{C}_{s}C\sqcap\mathbb{C}_{s}D\sqsubseteq\mathbb{C}_{s}(C\sqcap D)$ is
a valid formula, for any concepts $C,D$, known as the _$\mathbf{C}$
-principle_ (or _agglomeration_). Therefore, by the $\mathbf{C}$-principle,
under relational semantics we would be forced to conclude that
$\mathsf{SubmitOrd}\sqsubseteq\mathbb{C}_{s}(\mathsf{Confirm}\sqcap\mathsf{PartConf}\sqcap\mathsf{Reject}),$
meaning that any submitted order is such that the seller $s$ has the ability
to make it confirmed, partially confirmed, and rejected, all _at once_ , which
is unreasonable.

Finally, consider the formula
$\top\sqsubseteq\mathsf{Confirm}\sqcup\lnot\mathsf{Confirm},$ i.e., the truism
stating that anything is either confirmed or not confirmed. By the so called
_$\mathbf{N}$ -principle_ (or _necessitation_) of relational semantics, we
have that if $\top\sqsubseteq C$ is valid on relational frames, then
$\top\sqsubseteq\mathbb{D}_{c}C$ holds as well, for any concept $C$. Thus,
from the $\mathbf{N}$-principle it would follow on relational semantics that
$\top\sqsubseteq\mathbb{D}_{c}(\mathsf{Confirm}\sqcup\lnot\mathsf{Confirm}),$
thereby forcing us to the consequence that every object is made by customer
$c$ to be either confirmed or not confirmed, hence leading again to an
unreasonable connection between customer’s actions and confirmation of orders.

The $\mathbb{D}_{i}$ and $\mathbb{C}_{i}$ modalities are axiomatised similarly
to [15], by means of additional principles as well: $\mathbb{D}_{i}$ obeys the
$\mathbf{C}$\- (seen above) and _$\mathbf{T}$ -principle_
($\mathbb{D}_{w}C\sqsubseteq C$), stating a _factivity of actions_ principle,
well-known also in epistemic logic; and both satisfy the _$\mathbf{Q}$
-principle_ ($\top\sqsubseteq\lnot\mathbb{D}_{c}\top$), asserting a principle
of _impotence towards tautologies_ that is unsatisfiable in relational frames,
but admissible over neighbourhood ones, and the _$\mathbf{E}$ -principle_
($C\equiv D$ entails $\mathbb{D}_{i}C\equiv\mathbb{D}_{i}D$ and
$\mathbb{C}_{i}C\equiv\mathbb{C}_{i}D$), valid both on relational and
neighbourhood frames.

In this paper, which is an extension of [13, 14], we investigate reasoning in
a family of non-normal modal description logics, providing terminating, sound,
and complete tableau algorithms for checking formula satisfiability on
neighbourhood models based on _varying domains_ of objects. Moreover, we study
the complexity of reasoning in a restricted fragment that disallows modalities
on description logic concepts. Finally, for two modal description logics
interpreted on _constant domain_ neighbourhood models, we adjust a reduction
(known from the propositional case) to satisfiability with respect to standard
relational semantics.

The paper is structured as follows. Section 2 provides the necessary
definitions and the preliminary results on non-normal modal description
logics. In Section 3 we present the tableau algorithms for the family of
logics here considered. The case of fragments without modalised concepts is
then studied in Section 4. Section 5 contains the results for the constant
domain case. Finally, Section 6 concludes the paper, discussing related work
and possible future research directions.

##  2 Preliminaries

Here we introduce modal description logics, first presenting their syntax, and
then their semantics based on neighbourhood and relational models,
respectively. Finally, we introduce the family of frame conditions here
considered.

###  2.1 Syntax

Let ${\sf N_{C}}$, ${\sf N_{R}}$ and ${\sf N_{I}}$ be countably infinite and
pairwise disjoint sets of _concept_ , _role_ , and _individual names_ ,
respectively. An $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ _concept_ is an
expression of the form $C::=A\mid\lnot C\mid C\sqcap C\mid\exists
r.C\mid\Box_{i}C,$ where $A\in{\sf N_{C}}$, $r\in{\sf N_{R}}$, and $\Box_{i}$
such that $i\in J=\\{1,\ldots,n\\}$. An
_$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ atom_ is a _concept inclusion_
(_CI_) of the form $(C\sqsubseteq D)$, or an _assertion_ of the form $C(a)$ or
$r(a,b)$, with $C,D$ $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ concepts,
$r\in{\sf N_{R}}$, and $a,b\in{\sf N_{I}}$. An
_$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ formula_ has the form
$\varphi::=\pi\mid\neg\varphi\mid\varphi\land\varphi\mid\Box_{i}\varphi,$
where $\pi$ is an $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ atom and $i\in
J$. We use the following standard definitions for concepts: $\forall
r.C:=\lnot\exists r.\lnot C$; $(C\sqcup D):=\lnot(\lnot C\sqcap\lnot D)$;
$\bot:=A\sqcap\lnot A$, $\top:=A\sqcup\lnot A$ (for an arbitrarily fixed
$A\in{\sf N_{C}}$); $\Diamond_{i}C:=\lnot\Box_{i}\lnot C$. Concepts of the
form $\Box_{i}C$, $\Diamond_{i}C$ are _modalised concepts_. Analogous
conventions hold for formulas, writing $C\equiv D$ for $(C\sqsubseteq
D)\land(D\sqsubseteq C)$ and setting $\mathsf{false}:=(\top\sqsubseteq\bot)$,
$\mathsf{true}:=(\bot\sqsubseteq\top)$.

###  2.2 Semantics

We now define neighbourhood semantics, which (as already mentioned) can be
seen as a generalisation of the relational semantics, introduced immediately
after.

####  2.2.1 Neighbourhood Semantics

A _neighbourhood frame_ , or simply _frame_ , is a pair
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$, where
$\mathcal{W}$ is a non-empty set of _worlds_ and
$\mathcal{N}_{i}\colon\mathcal{W}\rightarrow 2^{2^{\mathcal{W}}}$ is a
_neighbourhood function_ , for each _agent_ $i\in J=\\{1,\ldots,n\\}$. An
_$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ varying domain neighbourhood
model_, or simply _model_ , based on a neighbourhood frame $\mathcal{F}$ is a
pair $\mathcal{M}=(\mathcal{F},\mathcal{I})$, where
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$ is a neighbourhood
frame and $\mathcal{I}$ is a function associating with every $w\in\mathcal{W}$
an _$\smash{\mathcal{ALC}}$ interpretation_
$\mathcal{I}_{w}=(\Delta_{w},\cdot^{\mathcal{I}_{w}})$, with non-empty
_domain_ $\Delta_{w}$, and where $\cdot^{\mathcal{I}_{w}}$ is a function such
that: for all $A\in{\sf N_{C}}$, $A^{\mathcal{I}_{w}}\subseteq\Delta_{w}$; for
all $r\in{\sf N_{R}}$,
$r^{\mathcal{I}_{w}}\subseteq\Delta_{w}{\times}\Delta_{w}$; for all $a\in{\sf
N_{I}}$, $a^{\mathcal{I}_{w}}\in\Delta_{w}$. An
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ _constant domain neighbourhood
model_ is defined in the same way, except that, for all
$w,w^{\prime}\in\mathcal{W}$, we have that $\Delta_{w}=\Delta_{w^{\prime}}$
and, for all $u,v\in\mathcal{W}$, we require
$a^{\mathcal{I}_{u}}=a^{\mathcal{I}_{v}}$ (denoted by $a^{\mathcal{I}}$), that
is, individual names are _rigid designators_. We often write
$\mathcal{M}=(\mathcal{F},\Delta,\mathcal{I})$ to denote a constant domain
neighbourhood model $\mathcal{M}=(\mathcal{F},\mathcal{I})$ with domain
$\Delta=\Delta_{w}$, for every $w\in\mathcal{W}$. Given a model
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ and a world $w\in\mathcal{W}$ of
$\mathcal{F}$ (or simply _$w$ in $\mathcal{F}$_), the _interpretation
$C^{\mathcal{I}_{w}}$ of a concept $C$ in $w$_ is defined as: $(\neg
D)^{\mathcal{I}_{w}}=\Delta_{w}\setminus D^{\mathcal{I}_{w}},\quad(D\sqcap
E)^{\mathcal{I}_{w}}=D^{\mathcal{I}_{w}}\cap E^{\mathcal{I}_{w}},$ $(\exists
r.D)^{\mathcal{I}_{w}}=\\{d\in\Delta_{w}\mid\exists e\in
D^{\mathcal{I}_{w}}{:}(d,e)\in r^{\mathcal{I}_{w}}\\},$
$(\Box_{i}D)^{\mathcal{I}_{w}}=\\{d\in\Delta_{w}\mid\llbracket
D\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)\\},$ where, for all
$d\in\bigcup_{w\in\mathcal{W}}\Delta_{w}$, the set $\llbracket
D\rrbracket^{\mathcal{M}}_{d}=\\{v\in\mathcal{W}\mid d\in
D^{\mathcal{I}_{v}}\\}$ is called the _truth set of $D$ with respect to
$\mathcal{M}$ and $d$_. We say that a concept $C$ is _satisfied in
$\mathcal{M}$_ if there is $w$ in $\mathcal{F}$ such that
$C^{\mathcal{I}_{w}}\neq\emptyset$, and that $C$ is _satisfiable_ (over
varying or constant neighbourhood models, respectively) if there is a (varying
or constant domain, respectively) neighbourhood model in which it is
satisfied. The _satisfaction of an $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$
formula $\varphi$ in $w$ of $\mathcal{M}$_, written
$\mathcal{M},w\models\varphi$, is defined as follows:

$\displaystyle\mathcal{M},w\models C\sqsubseteq D$ iff $\displaystyle
C^{\mathcal{I}_{w}}\subseteq D^{\mathcal{I}_{w}},$ $\displaystyle\ \
\mathcal{M},w\models C(a)$ iff $\displaystyle a^{\mathcal{I}_{w}}\in
C^{\mathcal{I}_{w}},$ $\displaystyle\mathcal{M},w\models r(a,b)$ iff
$\displaystyle(a^{\mathcal{I}_{w}},b^{\mathcal{I}_{w}})\in
r^{\mathcal{I}_{w}},$ $\displaystyle\ \ \mathcal{M},w\models\neg\psi$ iff
$\displaystyle\mathcal{M},w\not\models\psi,$
$\displaystyle\mathcal{M},w\models\psi\land\chi$ iff
$\displaystyle\mathcal{M},w\models\psi\text{ and }\mathcal{M},w\models\chi,$
$\displaystyle\ \ \mathcal{M},w\models\Box_{i}\psi$ iff
$\displaystyle\llbracket\psi\rrbracket^{\mathcal{M}}\in\mathcal{N}_{i}(w),$

where
$\llbracket\psi\rrbracket^{\mathcal{M}}=\\{v\in\mathcal{W}\mid\mathcal{M},v\models\psi\\}$
is the _truth set of $\psi$_. As a consequence of the above definition, we
obtain the following condition for $\Diamond_{i}$ formulas:
$\mathcal{M},w\models\Diamond_{i}\psi$ iff
$\llbracket\neg\psi\rrbracket^{\mathcal{M}}\notin\mathcal{N}_{i}(w)$. Given a
neighbourhood frame $\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$
and a neighbourhood model $\mathcal{M}=(\mathcal{F},\mathcal{I})$, we say that
$\varphi$ is _satisfied in $\mathcal{M}$_ if there is $w\in\mathcal{W}$ such
that $\mathcal{M},w\models\varphi$, and that $\varphi$ is _satisfiable_ (over
varying or constant domain neighbourhood models, respectively) if it is
satisfied in some (varying or constant domain, respectively) neighbourhood
model. Also, $\varphi$ is _valid in $\mathcal{M}$_,
$\mathcal{M}\models\varphi$, if it is satisfied in all $w$ of $\mathcal{M}$,
and it is _valid on $\mathcal{F}$_ if, for all $\mathcal{M}$ based on
$\mathcal{F}$, $\varphi$ is valid in $\mathcal{M}$, writing
$\mathcal{F}\models\varphi$.

####  2.2.2 Relational Semantics

A _relational frame_ is a pair $F=(W,\\{R_{i}\\}_{i\in J})$, with $W$ non-
empty set and $R_{i}$ binary relation on $W$, for $i\in J=\\{1,\ldots,n\\}$.
An _$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ (constant domain) relational
model_ based on a relational frame $F=(W,\\{R_{i}\\}_{i\in J})$ is a pair
$M=(F,I)$, where $I$ is a function associating with every $w\in W$ an
$\smash{\mathcal{ALC}}$ _interpretation_ $I_{w}=(\Delta,\cdot^{I_{w}})$,
having non-empty _constant domain_ $\Delta$, and where $\cdot^{I_{w}}$ is a
function such that: for all $A\in{\sf N_{C}}$, $A^{I_{w}}\subseteq\Delta$; for
all $r\in{\sf N_{R}}$, $r^{I_{w}}\subseteq\Delta{\times}\Delta$; for all
$a\in{\sf N_{I}}$, $a^{I_{w}}\in\Delta$, and for all $u,v\in W$,
$a^{I_{u}}=a^{I_{v}}$(denoted by $a^{I}$). Given a relational model $M=(F,I)$
and a world $w\in W$ of $F$ (or simply $w$ in $F$), the _interpretation of a
concept $C$ in $w$_, written $C^{I_{w}}$, is defined by taking: $(\neg
C)^{I_{w}}=\Delta\setminus C^{I_{w}},$ $(C\sqcap D)^{I_{w}}=C^{I_{w}}\cap
D^{I_{w}},$ $(\exists r.C)^{I_{w}}=\\{d\in\Delta\mid\exists e\in
C^{I_{w}}{:}(d,e)\in r^{I_{w}}\\},$ $(\Box_{i}C)^{I_{w}}=\\{d\in\Delta\mid\
\forall v\in W:wR_{i}v\Rightarrow d\in C^{I_{v}}\\}.$

A concept $C$ is _satisfied in $M$_ if there is $w$ in $F$ such that
$C^{I_{w}}\neq\emptyset$, and that $C$ is _satisfiable on relational models_
if there is a relational model in which it is satisfied. The _satisfaction of
a $\smash{\mathcal{ML}_{\mathcal{ALC}}}$ formula $\varphi$ in $w$ of $M$_,
written $M,w\models\varphi$, is defined, for atoms, negation and conjunction,
similarly to the previous case, and as follows for the $\Box_{i}$ case:
$M,w\models\Box_{i}\varphi\text{ \ iff \ }\forall v\in W:wR_{i}v\Rightarrow
M,v\models\varphi.$ Given a relational frame $F=(W,\\{R_{i}\\}_{i\in J})$ and
a relational model $M=(F,\Delta,I)$, we say that $\varphi$ is _satisfied in
$M$_ if there is $w\in W$ such that $M,w\models\varphi$, and that $\varphi$ is
_satisfiable on relational models_ if it is satisfied in some relational
model. Also, $\varphi$ is said to be _valid in $M$_, $M\models\varphi$, if it
is satisfied in all $w$ of $M$, and it is _valid on $F$_ if, for all $M$ based
on $F$, $\varphi$ is valid in $M$, writing $F\models\varphi$.

###  2.3 Frame Conditions and Formula Satisfiability

We consider the following conditions on neighbourhood frames
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$. We say that
_$\mathcal{F}$ satisfies the_:

$\mathbf{E}$-condition iff $\mathcal{N}_{i}$ is a neighbourhood function;
$\mathbf{M}$-condition iff $\alpha\in\mathcal{N}_{i}(w)$ and
$\alpha\subseteq\beta$ implies $\beta\in\mathcal{N}_{i}(w)$;
$\mathbf{C}$-condition iff $\alpha\in\mathcal{N}_{i}(w)$ and
$\beta\in\mathcal{N}_{i}(w)$ implies $\alpha\cap\beta\in\mathcal{N}_{i}(w)$;
$\mathbf{N}$-condition iff $\mathcal{W}\in\mathcal{N}_{i}(w)$;
$\mathbf{T}$-condition iff $\alpha\in\mathcal{N}_{i}(w)$ implies $w\in\alpha$;
$\mathbf{D}$-condition iff $\alpha\in\mathcal{N}_{i}(w)$ implies
$\mathcal{W}\setminus\alpha\not\in\mathcal{N}_{i}(w)$; $\mathbf{P}$-condition
iff $\emptyset\not\in\mathcal{N}_{i}(w)$; $\mathbf{Q}$-condition iff
$\mathcal{W}\not\in\mathcal{N}_{i}(w)$;

for every $w\in\mathcal{W}$, $\alpha,\beta\subseteq\mathcal{W}$. Combinations
of conditions, such as the $\mathbf{EMCN}$-condition, are obtained by suitably
joining the ones above. Moreover, since the $\mathbf{E}$-condition is always
satisfied by any neighbourhood frame, we often omit the letter $\mathbf{E}$
from this naming scheme, writing for instance ‘$\mathbf{MCN}$’ in place of
‘$\mathbf{EMCN}$’.

On the relationships among (combinations of) neighbourhood frame conditions,
we make the following observations.

######  Theorem 2.1 ().

Given a neighbourhood frame
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$, the following
statements hold, for $i\in J$.

  1. 1.

If $\mathcal{N}_{i}$ satisfies the $\mathbf{MQ}$-condition then, for every
$w\in\mathcal{W}$, $\mathcal{N}_{i}(w)=\emptyset$. Hence, $\mathcal{N}_{i}$
satisfies all but the $\mathbf{N}$-condition.

  2. 2.

$\mathcal{N}_{i}$ satisfies the $\mathbf{P}$-condition, if $\mathcal{N}_{i}$
satisfies one of the following:
(i) $\mathbf{MD}$-condition;  (ii) $\mathbf{ND}$-condition; or  (iii)
$\mathbf{T}$-condition.

  3. 3.

$\mathcal{N}_{i}$ satisfies the $\mathbf{D}$-condition, if $\mathcal{N}_{i}$
satisfies one of the following:
(i) $\mathbf{CP}$-condition; or  (ii) $\mathbf{T}$-condition.

  4. 4.

$\mathcal{N}_{i}$ does not satisfy the $\mathbf{NQ}$-condition.

$\smash{\mathbf{EMCNT}}$$\smash{\mathbf{EMCNTD}}$$\smash{\mathbf{EMCNTP}}$$\smash{\mathbf{EMCTDP}}$$\smash{\mathbf{EMCND}}$$\smash{\mathbf{EMCNP}}$$\smash{\mathbf{EMCNDP}}$$\smash{\mathbf{EMCN}}$$\smash{\mathbf{EMCT}}$$\smash{\mathbf{EMCTD}}$$\smash{\mathbf{EMCTP}}$$\smash{\mathbf{EMCTDP}}$$\smash{\mathbf{EMCD}}$$\smash{\mathbf{EMCP}}$$\smash{\mathbf{EMCDP}}$$\smash{\mathbf{EMNT}}$$\smash{\mathbf{EMNTD}}$$\smash{\mathbf{EMNTP}}$$\smash{\mathbf{EMNTDP}}$$\smash{\mathbf{EMND}}$$\smash{\mathbf{EMNDP}}$$\smash{\mathbf{EMNP}}$$\smash{\mathbf{ECNT}}$$\smash{\mathbf{ECNTD}}$$\smash{\mathbf{ECNTP}}$$\smash{\mathbf{ECNTDP}}$$\smash{\mathbf{ECND}}$$\smash{\mathbf{ECNP}}$$\smash{\mathbf{ECNDP}}$$\smash{\mathbf{ECTQ}}$$\smash{\mathbf{ECTPQ}}$$\smash{\mathbf{ECTDQ}}$$\smash{\mathbf{ECTDPQ}}$$\smash{\mathbf{ECDQ}}$$\smash{\mathbf{ECPQ}}$$\smash{\mathbf{ECDPQ}}$$\smash{\mathbf{EDPQ}}$$\smash{\mathbf{EMC}}$$\smash{\mathbf{EMN}}$$\smash{\mathbf{EMT}}$$\smash{\mathbf{EMTD}}$$\smash{\mathbf{EMTP}}$$\smash{\mathbf{EMTDP}}$$\smash{\mathbf{EMD}}$$\smash{\mathbf{EMDP}}$$\smash{\mathbf{EMP}}$$\smash{\mathbf{ECN}}$$\smash{\mathbf{ECT}}$$\smash{\mathbf{ECTD}}$$\smash{\mathbf{ECTP}}$$\smash{\mathbf{ECTDP}}$$\smash{\mathbf{ECD}}$$\smash{\mathbf{ECP}}$$\smash{\mathbf{ECQ}}$$\smash{\mathbf{ENT}}$$\smash{\mathbf{ENTD}}$$\smash{\mathbf{ENTP}}$$\smash{\mathbf{EMTDP}}$$\smash{\mathbf{END}}$$\smash{\mathbf{ENP}}$$\smash{\mathbf{ETQ}}$$\smash{\mathbf{ETDQ}}$$\smash{\mathbf{ETDQ}}$$\smash{\mathbf{ETDPQ}}$$\smash{\mathbf{EDQ}}$$\smash{\mathbf{EDP}}$$\smash{\mathbf{EPQ}}$$\smash{\mathbf{EM}}$$\smash{\mathbf{EC}}$$\smash{\mathbf{EN}}$$\smash{\mathbf{ET}}$$\smash{\mathbf{ETD}}$$\smash{\mathbf{ETP}}$$\smash{\mathbf{ETDP}}$$\smash{\mathbf{ED}}$$\smash{\mathbf{EP}}$$\smash{\mathbf{EQ}}$$\smash{\mathbf{E}}$
Figure 1: Implications among $L$-conditions in $\smash{\mathsf{Pantheon}}$
(equivalent ones are listed in the same nodes, with underlined
representatives).

Based on these results, Figure 1 depicts the relations between combinations of
frame conditions: nodes are (groups of equivalent) conditions (with the
canonical representative underlined), and arrows represent logical
implications. Any combination containing the $\mathbf{NQ}$-condition has been
omitted, as it leads to inconsistency (Theorem 2.1, Point 4). Moreover, due to
Theorem 2.1, Point 1, any combination that includes the
$\mathbf{MQ}$-condition is not considered, since for any neighbourhood frame
$\mathcal{F}$ satisfying such condition and any
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ concept $C$, we have
$\mathcal{F}\models\Box_{i}C\equiv\bot$, and similarly for formulas, hence
trivialising the modal operators. Thus, we consider in the remainder the set
$\smash{\mathsf{Pantheon}}$ of 39 non-equivalent combinations shown (as nodes
or canonical representatives) in Figure 1.

For $\mathit{L}\in\smash{\mathsf{Pantheon}}$, we say that a neighbourhood
frame $\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$, with
$J=\\{1,\ldots,n\\}$, is an _$L^{n}$ frame_ iff its neighbourhood functions
$\mathcal{N}_{i}$, for $i\in J$, satisfy the _$\mathit{L}$ -condition_,
obtained by combining the conditions associated with letters in $\mathit{L}$.
For a class of neighbourhood frames $\mathcal{C}$, the _satisfiability in
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ on_ (_varying_ or _constant domain_
, resp.) _neighbourhood models based on a frame in $\mathcal{C}$_ is the
problem of deciding whether an $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$
formula is satisfied in a (varying or constant domain, resp.) neighbourhood
model based on a frame in $\mathcal{C}$. Satisfiability in
_$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ on_ (_varying_ or _constant domain_
, respectively) _neighbourhood models_ is satisfiability in
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ on (varying or constant domain,
resp.) neighbourhood models based on a frame in the class of $L^{n}$ frames.
Finally, _satisfiability in $\smash{\mathbf{K}^{n}_{\mathcal{ALC}}}$ on_
(_constant domain_) _relational models_ is satisfiability in
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ on relational models based on any
relational frame.

_${\mathbf{E}}$ -principle_ |  $S\models C\equiv D$ implies $S\models\Box_{i}C\equiv\Box_{i}D$.
---|---
$S\models\varphi\leftrightarrow\psi$ implies
$S\models\Box_{i}\varphi\leftrightarrow\Box_{i}\psi$.
_${\mathbf{M}}$ -principle_ |  $S\models C\sqsubseteq D$ implies $S\models\Box_{i}C\sqsubseteq\Box_{i}D$.
$S\models\varphi\to\psi$ implies $S\models\Box_{i}\varphi\to\Box_{i}\psi$.
_${\mathbf{C}}$ -principle_ |  $S\models\Box_{i}C\sqcap\Box_{i}D\sqsubseteq\Box_{i}(C\sqcap D)$.
$S\models\Box_{i}\varphi\land\Box_{i}\psi\to\Box_{i}(\varphi\land\psi)$.
_${\mathbf{N}}$ -principle_ |  $S\models\top\sqsubseteq C$ implies $S\models\top\sqsubseteq\Box_{i}C$.
$S\models\varphi$ implies $S\models\Box_{i}\varphi$.

_${\mathbf{T}}$ -principle_ |  $S\models\Box_{i}C\sqsubseteq C$.
---|---
$S\models\Box_{i}\varphi\to\varphi$.
_${\mathbf{D}}$ -principle_ |  $S\models\Box_{i}C\sqsubseteq\Diamond_{i}C$.
$S\models\Box_{i}\varphi\to\Diamond_{i}\varphi$.
_${\mathbf{P}}$ -principle_ |  $S\models\top\sqsubseteq\lnot\Box_{i}\bot$.
$S\models\lnot\Box_{i}\mathsf{false}$.
_${\mathbf{Q}}$ -principle_ |  $S\models\top\sqsubseteq\lnot\Box_{i}\top$.
$S\models\lnot\Box_{i}\mathsf{true}$.

Table 1: Principles over neighbourhood or relational frames and models $S$.

We now study the correspondence between conditions presented in Section 2.2
and the principles in Table 1, where $S$ is either a (neighbourhood or
relational) frame or a (neighbourhood or relational) model and the
$L$-principle is obtained by suitably combining the basic principles. We say
that the $L$-principle holds in $S$ if the corresponding expressions in Table
1 are satisfied. On the correspondence between the principles in Table 1 and
conditions over frames and models, we have the following results (see e.g.
[28] for the propositional case).

######  Proposition 1 ().

Given a neighbourhood frame $\mathcal{F}$, the $\mathit{L}$-principle holds in
$\mathcal{F}$ iff $\mathcal{F}$ satisfies the $\mathit{L}$-condition.

######  Proposition 2 ().

The following statements hold.

  1. 1.

For a (varying or constant domain) neighbourhood model $\mathcal{M}$, we have
that if $\mathcal{M}$ satisfies the $\mathit{L}$-condition, then the
$\mathit{L}$-principle holds in $\mathcal{M}$. However, in general, the
converse is not true.

  2. 2.

For a relational frame $F$ and a relational model $M$ based on $F$, the
$\mathbf{EMCN}$-principle holds in $M$, hence in $F$. Moreover, in $M$, hence
in $F$, the $\mathbf{D}$-principle holds iff the $\mathbf{P}$-principle holds,
and the $\mathbf{Q}$-principle does not hold.

##  3 Tableaux for Formula Satisfiability

We provide terminating, sound, and complete tableau algorithms to check
satisfiability of formulas in varying domain neighbourhood models. The
notation partly adheres to that of [17], while the model construction in the
soundness proof is based on the strategy of [12]. In this section, we use
concepts and formulas in _negation normal form_ (_NNF_) and, for this reason,
we consider all the logical connectives $\sqcup,\lor,\forall,\Diamond$ as
primitive, rather than defined. For a concept or formula $\gamma$, we denote
by $\dot{\lnot}\gamma$ the negation of $\gamma$ put in NNF, defined as
follows: a concept is in _NNF_ if negation occurs in it only in front of
concept names; a formula is in _NNF_ if all concepts in it are in NNF and
negation occurs in the formula only in front of CIs or assertions of the form
$r(a,b)$ (regarding assertions of the form $A(a)$, we recall that a formula
$\lnot\psi$, with $\psi=C(a)$, is equivalent to the assertion $D(a)$, with
$D=\lnot C$). Given an $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ formula
$\varphi$, we assume without loss of generality that $\varphi$ is in NNF
(using De Morgan laws) and it contains CIs only of the form $\top\sqsubseteq
C$, since $C\sqsubseteq D$ is equivalent to $\top\sqsubseteq\lnot C\sqcup D$).
We denote by $\mathsf{con}(\varphi)$ and $\mathsf{for}(\varphi)$ the set of
subconcepts and subformulas of $\varphi$, respectively, and then we set
$\mathsf{con}_{\dot{\lnot}}(\varphi)=\mathsf{con}(\varphi)\cup\\{\dot{\lnot}C\mid
C\in\mathsf{con}(\varphi)\\}\cup\\{\top\\}$ and
$\mathsf{for}_{\dot{\lnot}}(\varphi)=\mathsf{for}(\varphi)\cup\\{\dot{\lnot}\psi\mid\psi\in\mathsf{for}(\varphi)\\}$.
The sets $\mathsf{rol}(\varphi)$ and $\mathsf{ind}(\varphi)$ are,
respectively, the sets of role names and of individual names occurring in
$\varphi$. Let
$\mathsf{Fg}(\varphi)=\mathsf{for}_{\dot{\lnot}}(\varphi)\cup\mathsf{con}_{\dot{\lnot}}(\varphi)\cup\mathsf{rol}(\varphi)\cup\mathsf{ind}(\varphi)$
be the _fragment induced by $\varphi$_.

Moreover, let ${\sf N_{V}}$ be a countable set of _variables_ , denoted by the
letters $u,v$. The _terms for $\varphi$_, denoted by the letters $x,y$, are
either individual names in $\mathsf{ind}(\varphi)$ or variables in ${\sf
N_{V}}$. We assume that the set of terms for $\varphi$ is strictly well-
ordered by the relation $<$. In addition, let $\mathsf{N_{L}}$ be a countable
set of _labels_. Given an $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ formula
$\varphi$ and a label $n\in\mathsf{N_{L}}$, an _$n$ -labelled constraint for
$\varphi$_ takes the form $n:\psi$, or $n:C(x)$, or $n:r(x,y)$, where
$\psi\in\mathsf{for}_{\dot{\lnot}}(\varphi)$, $x,y$ are terms for $\varphi$,
$C\in\mathsf{con}_{\dot{\lnot}}(\varphi)$, and $r\in\mathsf{rol}(\varphi)$.
For every $n\in\mathsf{N_{L}}$, an _$n$ -labelled constraint system for
$\varphi$_ is a set $S_{n}$ of $n$-labelled constraints for $\varphi$. A
_labelled constraint for $\varphi$_ is an $n$-labelled constraint for
$\varphi$, for some $n\in\mathsf{N_{L}}$, and similarly for a _labelled
constraint system for $\varphi$_. A _completion set $\mathcal{T}$ for
$\varphi$_ is a non-empty union of labelled constraint systems for $\varphi$,
and we set $\mathsf{L}_{\mathcal{T}}=\\{n\in\mathsf{N_{L}}\mid
S_{n}\subseteq\mathcal{T}\\}$.

About terms, we adopt the following terminology. A term $x$ _occurs in
$S_{n}$_ if $S_{n}$ contains $n$-labelled constraints of the form $n:C(x)$ or
$n:r(\tau,\tau^{\prime})$, where $\tau=x$, or $\tau^{\prime}=x$, and
$n\in\mathsf{N_{L}}$. In addition, a variable $u$ is said to be _fresh for
$S_{n}$_ if $u$ does not occur in $S_{n}$. (These notions can be used with
respect to $\mathcal{T}$, whenever $S_{n}\subseteq\mathcal{T}$). Finally,
given variables $u,v$ in an $n$-labelled constraint system $S_{n}$, we say
that $u$ is _blocked by $v$ in $S_{n}$_ if $u>v$ and $\\{C\mid n:C(u)\in
S_{n}\\}\subseteq\\{C\mid n:C(v)\in S_{n}\\}$.

A completion set $\mathcal{T}$ contains a _clash_ if, for some
$m\in\mathsf{N_{L}}$, concept $C$, role $r$, and terms $x,y$, one of the
following holds: $\\{m:(\top\sqsubseteq C),m:\lnot(\top\sqsubseteq
C)\\}\subseteq\mathcal{T}$; or $\\{m:A(x),m:\lnot
A(x)\\}\subseteq\mathcal{T}$; or $\\{m:r(x,y),m:\lnot
r(x,y)\\}\subseteq\mathcal{T}$. A completion set that does not contain a clash
is _clash-free_.

For every $\mathit{L}\in\smash{\mathsf{Pantheon}}$, we associate to
$\mathit{L}$ the set of _$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ -rules_ from
Figure 2 (bottom part) containing $\mathsf{R}_{\land}$, $\mathsf{R}_{\sqcap}$,
$\mathsf{R}_{\lor}$, $\mathsf{R}_{\sqcup}$, $\mathsf{R}_{\exists}$,
$\mathsf{R}_{\forall}$, $\mathsf{R}_{\sqsubseteq}$,
$\mathsf{R}_{\not\sqsubseteq}$, $\mathsf{R}_{\mathit{L}}$, and
$\mathsf{R}_{\mathit{L}\mathbf{X}}$, for every
$\mathbf{X}\in\\{\mathbf{N,T,P,Q,D}\\}$ such that $\mathbf{X}\in\mathit{L}$.
Given $\mathit{L}\in\smash{\mathsf{Pantheon}}$, a completion set $\mathcal{T}$
is $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-_complete_ if no
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-rule is applicable to $\mathcal{T}$,
where $\gamma_{j}$ is either $\psi_{j}\in\mathsf{for}_{\dot{\lnot}}(\varphi)$
or $C_{j}(x_{j})$, with $C_{j}\in\mathsf{con}_{\dot{\lnot}}(\varphi)$, for
$j=1,\ldots,k$, and $\delta$ is either
$\chi\in\mathsf{for}_{\dot{\lnot}}(\varphi)$ or $D(y)$, with
$D\in\mathsf{con}_{\dot{\lnot}}(\varphi)$, with respect to the _application
conditions_ associated to each $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-rule
from Figure 2 (top part).

Application conditions

  1. $(\mathsf{R}_{\land})$

$\\{n:\psi,n:\chi\\}\not\subseteq\mathcal{T}$;

  2. $(\mathsf{R}_{\sqcap})$

$\\{n:C(x),n:D(x)\\}\not\subseteq\mathcal{T}$;

  3. $(\mathsf{R}_{\lor})$

$\\{n:\psi,n:\chi\\}\cap\mathcal{T}=\emptyset$;

  4. $(\mathsf{R}_{\sqcup})$

$\\{n:C(x),n:D(x)\\}\cap\mathcal{T}=\emptyset$;

  5. $(\mathsf{R}_{\exists})$

$x$ is not blocked by any variable in $S_{n}$, there is no $y$ such that
$\\{n:r(x,y),n:C(y)\\}\subseteq\mathcal{T}$, and $v$ is the $<$-minimal
variable fresh for $S_{n}$;

  6. $(\mathsf{R}_{\forall})$

$n:C(y)\notin\mathcal{T}$;

  7. $(\mathsf{R}_{\sqsubseteq})$

either $x$ occurs in $S_{n}$ and $n:C(x)\notin\mathcal{T}$; or no term occurs
in $S_{n}$ and $x$ is the $<$-minimal variable fresh for $S_{n}$;

  8. $(\mathsf{R}_{\not\sqsubseteq})$

there is no $x$ such that $n:\dot{\lnot}C(x)\in\mathcal{T}$ and $v$ is the
$<$-minimal variable fresh for $S_{n}$;

  9. $(\mathsf{R}_{\mathit{L}})$

$m$ is fresh for $\mathcal{T}$, and there is no $o\in\mathsf{N_{L}}$ such that
$\\{o:\gamma_{1},\ldots,o:\gamma_{k},o:\delta\\}\subseteq\mathcal{T}$, or
$\\{o:\dot{\lnot}\gamma_{j},o:\dot{\lnot}\delta\\}\subseteq\mathcal{T}$, for
some $j\leq k$;

  10. $(\mathsf{R}_{\mathit{L}\mathbf{N}})$

$m$ is fresh for $\mathcal{T}$, and there is no $o\in\mathsf{N_{L}}$ such that
$o:\gamma\in\mathcal{T}$;

  11. $(\mathsf{R}_{\mathit{L}\mathbf{T}})$

$n:\gamma\not\in\mathcal{T}$;

  12. $(\mathsf{R}_{\mathit{L}\mathbf{P}})$

$m$ is fresh for $\mathcal{T}$, and there is no $o\in\mathsf{N_{L}}$ such that
$\\{o:\gamma_{1},\ldots,o:\gamma_{k}\\}\subseteq\mathcal{T}$;

  13. $(\mathsf{R}_{\mathit{L}\mathbf{Q}})$

$m$ is fresh for $\mathcal{T}$, and there is no $o\in\mathsf{N_{L}}$ such that
$o:\dot{\lnot}\gamma_{j}\in\mathcal{T}$, for some $j\leq k$;

  14. $(\mathsf{R}_{\mathit{L}\mathbf{D}})$

$m$ is fresh for $\mathcal{T}$, and there is no $o\in\mathsf{N_{L}}$ such that
$\\{o:\gamma_{1},\ldots,o:\gamma_{k},o:\delta_{1},\ldots,o:\delta_{k}\\}\subseteq\mathcal{T}$,
or
$\\{o:\dot{\lnot}\gamma_{j},o:\dot{\lnot}\delta_{\ell}\\}\subseteq\mathcal{T}$,
for some $j\leq k$, $\ell\leq h$.

Rules

$n:\psi\land\chi$ ($\mathsf{R}_{\land}$)  $n:\psi$ , $n:\chi$ $n:\psi\lor\chi$
($\mathsf{R}_{\lor}$)  $n:\psi$ $n:\chi$ $n:C\sqcap D(x)$
($\mathsf{R}_{\sqcap}$)  $n:C(x)$, $n:D(x)$ $n:C\sqcup D(x)$
($\mathsf{R}_{\sqcup}$)  $n:C(x)$ $n:D(x)$

$n:\exists r.C(x)$ ($\mathsf{R}_{\exists}$)  $n:r(x,v)$, $n:C(v)$ $n:\forall
r.C(x)$, $n:r(x,y)$ ($\mathsf{R}_{\forall}$)  $n:C(y)$
$n:\top\sqsubseteq C$ ($\mathsf{R}_{\sqsubseteq}$)  $n:C(x)$
$n:\lnot(\top\sqsubseteq C)$ ($\mathsf{R}_{\not\sqsubseteq}$)
$n:\dot{\lnot}C(v)$

$n:\Box_{i}\gamma_{1}$, $\ldots$, $n:\Box_{i}\gamma_{k}$,
$n:\Diamond_{i}\delta$ ($\mathsf{R}_{\mathit{L}}$)  $m:\gamma_{1}$, $\ldots$,
$m:\gamma_{k}$ , $m:\delta$ $m:\dot{\lnot}\gamma_{1}$, $m:\dot{\lnot}\delta$
$\ \dots$ $m:\dot{\lnot}\gamma_{k}$, $m:\dot{\lnot}\delta$
$\underbrace{{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\qquad\qquad\qquad\qquad--\qquad\qquad\qquad\quad\
\ }}}_{\text{if }\mathbf{M}\not\in L}$ $n:\Diamond_{i}\gamma$
($\mathsf{R}_{\mathit{L}\mathbf{N}}$)  $m:\gamma$

$n:\Box_{i}\gamma$ ($\mathsf{R}_{\mathit{L}\mathbf{T}}$)  $n:\gamma$
$n:\Box_{i}\gamma_{1}$, $\ldots$, $n:\Box_{i}\gamma_{k}$
($\mathsf{R}_{\mathit{L}\mathbf{P}}$)  $m:\gamma_{1}$, $\ldots$,
$m:\gamma_{k}$ $n:\Box_{i}\gamma_{1}$, $\ldots$, $n:\Box_{i}\gamma_{k}$
($\mathsf{R}_{\mathit{L}\mathbf{Q}}$)  $m:\dot{\lnot}\gamma_{1}$ $\ \dots$
$m:\dot{\lnot}\gamma_{k}$

$n:\Box_{i}\gamma_{1}$ , $\ldots$ , $n:\Box_{i}\gamma_{k}$ ,
$n:\Box_{i}\delta_{1}$ , $\ldots$ , $n:\Box_{i}\delta_{h}$
($\mathsf{R}_{\mathit{L}\mathbf{D}}$)  $m:\gamma_{1}$, $\ldots$,
$m:\gamma_{k}$,  $m:\dot{\lnot}\gamma_{1}$,  $\ \dots$
$m:\dot{\lnot}\gamma_{k}$,  $\ \dots$ $m:\dot{\lnot}\gamma_{1}$,  $\ \dots$
$m:\dot{\lnot}\gamma_{k}$, $m:\delta_{1}$, $\ldots$, $m:\delta_{h}$
$m:\dot{\lnot}\delta_{1}$ $m:\dot{\lnot}\delta_{1}$ $m:\dot{\lnot}\delta_{h}$
$m:\dot{\lnot}\delta_{h}$
$\underbrace{{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\qquad\qquad\qquad\qquad--\qquad\qquad\qquad\qquad\qquad\qquad\qquad}}}_{\text{if
}\mathbf{M}\not\in L}$

Figure 2:  $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-rules, where $k,h\geq 1$
if $\mathbf{C}\in\mathit{L}$ and $k=h=1$ if $\mathbf{C}\not\in\mathit{L}$. In
the rules $\mathsf{R}_{\mathit{L}}$ and $\mathsf{R}_{\mathit{L}\mathbf{D}}$,
the number of possible expansions depend on whether $\mathbf{M}\in\mathit{L}$:
if $\mathbf{M}\in\mathit{L}$ only the first expansion is possible, if
$\mathbf{M}\notin\mathit{L}$ all other expansions are also possible.

The $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-rules essentially state how to
extend a completion set on the basis of the information contained in it.
Branching rules entail a _non-deterministic choice_ in the completion set
expansion.

For each $\mathit{L}\in\smash{\mathsf{Pantheon}}$, we now present a tableau-
based non-deterministic decision procedure for the
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ formula satisfiability problem on
varying domain neighbourhood models, based on Algorithm 1 (simply referred to
as _$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm_). We have that
a formula $\varphi$ is $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ satisfiable if
and only if there exists at least one execution of the
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm that constructs an
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete and clash-free completion
set for $\varphi$. This non-deterministic algorithm gives priority to non-
generating $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-rules, i.e., those that do
not introduce new variables or labels, with respect to generating ones, so to
minimise the size of the completion set constructed by its application, and
terminates in exponential time for every formula $\varphi$. Thus, we obtain
the following.

######  Theorem 3.1.

Satisfiability in $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ on varying domain
neighbourhood models is decidable in NExpTime.

Input: the initial completion set $\mathcal{T}:=\\{0:\varphi\\}$ of an
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ formula $\varphi$ in NNF.

Output: a completion set for $\varphi$, extending the initial one, that either
contains a clash, or is complete and clash-free.

1 while  _$\mathcal{T}$ is clash-free and not
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete_ do

2 if  _a rule
$\mathsf{R}\in\\{\mathsf{R}_{\land},\mathsf{R}_{\lor},\mathsf{R}_{\sqcap},\mathsf{R}_{\sqcup},\mathsf{R}_{\forall},\mathsf{R}_{\sqsubseteq},\mathsf{R}_{\mathit{L}\mathbf{T}}\\}$
is applicable to $\mathcal{T}$_ then

3 apply $\mathsf{R}$ to $\mathcal{T}$;

4 else if  _a rule
$\mathsf{R}\in\\{\mathsf{R}_{\exists},\mathsf{R}_{\mathit{L}},\mathsf{R}_{\mathit{L}\mathbf{N}},\mathsf{R}_{\mathit{L}\mathbf{P}},\mathsf{R}_{\mathit{L}\mathbf{Q}},\mathsf{R}_{\mathit{L}\mathbf{D}}\\}$
is applicable to $\mathcal{T}$_ then

5 apply $\mathsf{R}$ to $\mathcal{T}$;

6

7 end while

Algorithm 1 $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm on
varying domain neighbourhood models for $\varphi$

As an immediate consequence of the correctness of the tableau we also obtain a
(constructive) proof of the following kind of _exponential model property_.

######  Corollary 1 ().

Every $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ satisfiable formula $\varphi$
has a model with at most $p(|\mathsf{Fg}(\varphi)|)$ worlds, if
$\mathbf{C}\notin\mathit{L}$, and at most $2^{q(|\mathsf{Fg}(\varphi)|)}$)
worlds, if $\mathbf{C}\in\mathit{L}$, each of them having a domain with at
most $2^{r(|\mathsf{Fg}(\varphi)|)}$ elements, with $p$, $q$, $r$ polynomial
functions.

##  4 Fragments without Modalised Concepts

Here we study fragments of $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ without
modalised concepts. An _$\smash{\mathcal{ALC}\textnormal{-}\mathcal{ML}^{n}}$
formula_ is defined similarly to the
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ case, by disallowing modalised
concepts. Given $\mathit{L}\in\smash{\mathsf{Pantheon}}$, _satisfiability in
$\smash{{\mathcal{ALC}}\textnormal{-}{\mathit{L}^{n}}}$ on varying_ _domain
neighbourhood models_ is $\smash{\mathcal{ALC}\textnormal{-}\mathcal{ML}^{n}}$
satisfiability on varying domain neighbourhood models based on neighbourhood
frames in the respective class for $\mathit{L}$. An
_$\smash{\mathcal{ML}^{n}}$ formula_, instead, is defined analogously to
$\smash{\mathcal{ALC}\textnormal{-}\mathcal{ML}^{n}}$, except that we build it
from the standard propositional (rather than $\smash{\mathcal{ALC}}$) language
over a countable set of _propositional letters_ $\mathsf{N_{P}}$, disjoint
from ${\sf N_{C}}$, ${\sf N_{R}}$, and ${\sf N_{I}}$. The semantics of
$\smash{\mathcal{ML}^{n}}$ formulas is given in terms of _propositional
neighbourhood models_ (or simply _models_) $\mathcal{M}^{\sf
P}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J},\mathcal{V})$, where
$(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$ is a neighbourhood frame, with
$J=\\{1,\ldots,n\\}$ in the following, and $\mathcal{V}:{\sf N_{P}}\rightarrow
2^{\mathcal{W}}$ is a function mapping propositional letters to sets of worlds
(see [11, 40]). _Satisfiability in $\smash{\mathit{L}^{n}}$_ is satisfiability
in $\smash{\mathcal{ML}^{n}}$ on propositional neighbourhood models based on
neighbourhood frames in the respective class for $\mathit{L}$. A propositional
neighbourhood model based on a neighbourhood frame in the respective class for
$\mathit{L}$ is called _$\mathit{L}^{n}$ model_.

We prove tight complexity results for
$\smash{{\mathcal{ALC}}\textnormal{-}{\mathit{L}^{n}}}$ satisfiability on
varying domain neighbourhood models, where $L\in\smash{\mathsf{Pantheon}}$,
using the notion of a propositional abstraction of a formula (as in, e.g.,
[6]). Here, one can separate the satisfiability test into two parts, one for
the description logic dimension and one for the neighbourhood frame dimension.
For an $\smash{\mathcal{ALC}\textnormal{-}\mathcal{ML}^{n}}$ formula
$\varphi$, the _propositional abstraction_ $\varphi_{\sf prop}$ is the result
of replacing each $\smash{\mathcal{ALC}}$ atom $\pi$ in $\varphi$ by a
propositional variable $p_{\pi}\in{\sf N_{P}}$. Define the set
$\Sigma_{\varphi}=\\{p_{\pi}\in{\sf N_{P}}\mid\pi\text{ is an
$\smash{\mathcal{ALC}}$ atom in }\varphi\\}$. A (propositional neighbourhood)
$L^{n}$ model $\mathcal{M}^{\sf P}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in
J},\mathcal{V})$ is _$\Sigma_{\varphi}$ -consistent_ if, for all
$w\in\mathcal{W}$, the following $\smash{\mathcal{ALC}}$ formula is
satisfiable:
$\hat{\varphi}_{\mathcal{V},w}=\bigwedge_{p_{\pi}\in{\boldsymbol{f}}^{\mathcal{V},w}_{\varphi}}{\pi}\
\wedge\bigwedge_{p_{\pi}\in\Sigma_{\varphi}\setminus{\boldsymbol{f}}^{\mathcal{V},w}_{\varphi}}\neg{\pi},$
where
${\boldsymbol{f}}^{\mathcal{V},w}_{\varphi}=\\{p_{\pi}\in\Sigma_{\varphi}\mid
w\in\mathcal{V}(p_{\pi})\\}$. We formalise the connection between
$\smash{{\mathcal{ALC}}\textnormal{-}{\mathit{L}^{n}}}$ satisfiable formulas
and their propositional abstractions with the following lemma.

######  Lemma 1 ().

A formula $\varphi$ is $\smash{{\mathcal{ALC}}\textnormal{-}{\mathit{L}^{n}}}$
satisfiable on varying domain neighbourhood models iff $\varphi_{\sf prop}$ is
satisfied in a $\Sigma_{\varphi}$-consistent $L^{n}$ model.

We now introduce definitions and notation used to prove our complexity result
on fragments without modalised concepts. Let $\Sigma=\\{p_{\pi}\in{\sf
N_{P}}\mid\pi\text{ is an $\smash{\mathcal{ALC}}$}$ $\text{atom in
}\varphi\\}$, for a fixed but arbitrary
$\smash{\mathcal{ALC}\textnormal{-}\mathcal{ML}^{n}}$ formula $\varphi$, and
let $\phi$ be an $\smash{\mathcal{ML}^{n}}$ formula built from symbols in
$\Sigma$. We denote by ${\sf sub}(\phi)$ the set of subformulas of $\phi$
closed under single negation. A _valuation_ for $\phi$ is a function $\nu:{\sf
sub}(\phi)\rightarrow\\{0,1\\}$ that satisfies the conditions: (1) for all
$\neg\psi\in{\sf sub}(\phi)$, $\nu(\psi)=1$ iff $\nu(\neg\psi)=0$; (2) for all
$\psi_{1}\wedge\psi_{2}\in{\sf sub}(\phi)$, $\nu(\psi_{1}\wedge\psi_{2})=1$
iff $\nu(\psi_{1})=1$ and $\nu(\psi_{2})=1$; and (3) $\nu(\phi)=1$. A
valuation $\nu$ for $\phi$ is _$\Sigma$ -consistent_ if the following
$\smash{\mathcal{ALC}}$ formula is satisfiable:
$\textstyle\bigwedge_{\nu(p_{\pi})=1}\ {\pi}\ \wedge\
\bigwedge_{\nu(p_{\pi})=0}\ \neg{\pi},$ where $p_{\pi}\in\Sigma$. Lemma 2
establishes that satisfiability of $\phi$ in a $\Sigma$-consistent model is
characterised by the existence of a $\Sigma$-consistent valuation satisfying
suitable properties. In the following, we use $\mathsf{ff}$ as an abbreviation
for $p\land\neg p$, for a fixed but arbitrary $p\in\mathsf{N_{P}}$.

######  Lemma 2 ().

Given $\mathit{L}$ and an $\smash{\mathcal{ML}^{n}}$ formula $\phi$ built from
symbols in $\Sigma$ (defined as above), let:

$\boldsymbol{\kappa}=\begin{cases}|{\sf sub}({\phi})|,&\text{if
$\mathbf{C}\in\mathit{L}$}\\\ 1,&\text{if
$\mathbf{C}\not\in\mathit{L}$}\end{cases}.$

A formula $\phi$ is satisfied in a $\Sigma$-consistent $\mathit{L}^{n}$ model
iff there is a $\Sigma$-consistent valuation $\nu$ for $\phi$ such that, for
every $1\leq k\leq\boldsymbol{\kappa}$, if
$\Box_{i}\psi_{1},\dots,\Box_{i}\psi_{k},\Box_{i}\chi\in{\sf sub}(\phi)$,
$\nu(\Box_{i}\psi_{j})=1$ for all $1\leq j\leq k$, and $\nu(\Box_{i}\chi)=0$,
then

  1. 1.

$(\bigwedge^{k}_{j=1}\psi_{j}\wedge\neg\chi)\vee\boldsymbol{\vartheta}$ is
satisfied in a $\Sigma$-consistent $\mathit{L}^{n}$ model, where:
$\boldsymbol{\vartheta}=\mathsf{ff}$, if $\mathbf{M}\in\mathit{L}$;
$\boldsymbol{\vartheta}=\bigvee^{k}_{j=1}(\neg\psi_{j}\wedge\chi)$, if
$\mathbf{M}\not\in\mathit{L}$; and

  2. 2.

for $\mathbf{X}\in\\{\mathbf{N,T,P,Q,D}\\}$, if $\mathbf{X}\in\mathit{L}$,
then $\nu$ satisfies the condition $(\mathbf{X})$ below, for every $1\leq
k,h\leq\boldsymbol{\kappa}$:

     * ($\mathbf{N}$)

if $\Box_{i}\psi\in{\sf sub}(\phi)$ and $\nu(\Box_{i}\psi)=0$, then $\neg\psi$
is satisfied in a $\Sigma$-consistent $\mathit{L}^{n}$ model;

     * ($\mathbf{T}$)

if $\Box_{i}\psi\in{\sf sub}(\phi)$ and $\nu(\Box_{i}\psi)=1$ then
$\nu(\psi)=1$;

     * ($\mathbf{P}$)

if $\Box_{i}\psi_{1},\dots,\Box_{i}\psi_{k}\in{\sf sub}(\phi)$ and
$\nu(\Box_{i}\psi_{j})=1$ for all $1\leq j\leq k$, then
$\bigwedge^{k}_{j=1}\psi_{j}$ is satisfied in a $\Sigma$-consistent
$\mathit{L}^{n}$ model;

     * ($\mathbf{Q}$)

if $\Box_{i}\psi_{1},\dots,\Box_{i}\psi_{k}\in{\sf sub}(\phi)$ and
$\nu(\Box_{i}\psi_{j})=1$ for all $1\leq j\leq k$, then
$\bigvee^{k}_{j=1}\neg\psi_{j}$ is satisfied in a $\Sigma$-consistent
$\mathit{L}^{n}$ model;

     * ($\mathbf{D}$)

if
$\Box_{i}\psi_{1},\dots,\Box_{i}\psi_{k},\Box_{i}\chi_{1},\dots,\Box_{i}\chi_{h}\in{\sf
sub}(\phi)$, $\nu(\Box_{i}\psi_{j})=1$ for all $1\leq j\leq k$, and
$\nu(\Box_{i}\chi_{\ell})=1$ for all $1\leq\ell\leq h$, then
$(\bigwedge^{k}_{j=1}\psi_{j}\land\bigwedge^{h}_{\ell=1}\chi_{\ell})\vee\boldsymbol{\eta}$
is satisfied in a $\Sigma$-consistent $\mathit{L}^{n}$ model, where:

$\boldsymbol{\eta}=\begin{cases}\mathsf{ff},&\text{if
$\mathbf{M}\in\mathit{L}$}\\\
\neg(\bigwedge^{k}_{j=1}\psi_{j})\land\neg(\bigwedge^{h}_{\ell=1}\chi_{\ell}),&\text{if
$\mathbf{M}\not\in\mathit{L}$}\end{cases}.$

By using Lemmas 1-2, the following theorem provides a procedure that runs in
exponential time to check
$\smash{{\mathcal{ALC}}\textnormal{-}{\mathit{L}^{n}}}$ satisfiability on
varying domains. Since $\smash{\mathcal{ALC}}$ formula satisfiability is
already ExpTime-hard, our upper bound is tight.

######  Theorem 4.1 ().

Satisfiability in $\smash{{\mathcal{ALC}}\textnormal{-}{\mathit{L}^{n}}}$ on
varying domain neighbourhood models is ExpTime-complete.

##  5 Reasoning on Constant Domain

We now study the complexity of the formula satisfiability problem in
$\smash{\mathbf{E}^{n}_{\mathcal{ALC}}}$ and
$\smash{\mathbf{EM}^{n}_{\mathcal{ALC}}}$ on constant domain neighbourhood
models. We provide a NExpTime upper bound for satisfiability in
$\smash{\mathbf{E}^{n}_{\mathcal{ALC}}}$ and
$\smash{\mathbf{EM}^{n}_{\mathcal{ALC}}}$ by using a reduction, lifted from
the propositional case, to multi-modal
$\smash{\mathbf{K}^{m}_{\mathcal{ALC}}}$. The translation $\cdot^{\dagger}$
from $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ to
$\smash{\mathcal{ML}^{3n}_{\mathcal{ALC}}}$ is defined as [21, 18]:
$A^{\dagger}=A$, $(\lnot C)^{\dagger}=\lnot C^{\dagger}$, $(C\sqcap
D)^{\dagger}=C^{\dagger}\sqcap D^{\dagger}$, $(\exists r.C)^{\dagger}=\exists
r.C^{\dagger}$; $(C(a))^{\dagger}=C^{\dagger}(a)$,
$(r(a,b))^{\dagger}=r(a,b)$, $(C\sqsubseteq
D)^{\dagger}=C^{\dagger}\sqsubseteq D^{\dagger}$,
$(\lnot\psi)^{\dagger}=\lnot\psi^{\dagger}$,
$(\psi\land\chi)^{\dagger}=\psi^{\dagger}\land\chi^{\dagger}$;
$(\Box_{i}\gamma)^{\dagger}=\Diamond_{i_{1}}(\Box_{i_{2}}\gamma^{\dagger}\circ\Box_{i_{3}}\lnot\gamma^{\dagger})$;
where $A\in{\sf N_{C}}$, $r\in{\sf N_{R}}$, $\gamma$ is either an
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ concept or formula, and
$\circ\in\\{\sqcap,\land\\}$ accordingly. Using this translation, one can show
that satisfiability on neighbourhood models is reducible to satisfiability on
the relational models [21, 18]. Since satisfiability in
$\smash{\mathbf{K}^{3n}_{\mathcal{ALC}}}$ constant domain relational models is
NExpTime-complete [17, Theorem 15.15], we obtain the following complexity
result.

######  Theorem 5.1 ().

Satisfiability in $\smash{\mathbf{E}^{n}_{\mathcal{ALC}}}$ on constant domain
neighbourhood models is decidable in NExpTime.

The translation $\cdot^{\ddagger}$ from
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ to
$\smash{\mathcal{ML}^{2n}_{\mathcal{ALC}}}$ is defined as $\cdot^{\dagger}$ on
all concepts and formulas, except for the modalised concepts or formulas
$\gamma$:
$(\Box_{i}\gamma)^{\ddagger}=\Diamond_{i_{1}}\Box_{i_{2}}\gamma^{\ddagger}$.
We obtain an upper bound analogous to the one for
$\smash{\mathbf{E}^{n}_{\mathcal{ALC}}}$ by a reduction of the formula
satisfiability problem for $\smash{\mathbf{EM}^{n}_{\mathcal{ALC}}}$ to the
$\smash{\mathbf{K}^{2n}_{\mathcal{ALC}}}$ one [21, 18, 17].

######  Theorem 5.2 ().

Satisfiability in $\smash{\mathbf{EM}^{n}_{\mathcal{ALC}}}$ on constant domain
neighbourhood models is decidable in NExpTime.

##  6 Discussion

We investigated reasoning in non-normal modal description logics, focussing
on: $(i)$ tableaux algorithms to check satisfiability of multi-modal
description logics formulas in varying domain neighbourhood models based on
classes of frames for 39 different non-normal systems; $(ii)$ complexity of
satisfiability restricted to fragments with modal operators applied only over
formulas, and interpreted on varying domain models; $(iii)$ preliminary
reduction of formula satisfiability for two non-normal modal description
logics to satisfiability in the standard relational semantics on a constant
domain. We now discuss possible future work.

First, we intend to devise tableaux for formula satisfiability on
neighbourhood models with constant domain, by solving the problem of newly
introduced variables that do not occur in other previously expanded labelled
constraints systems. For instance, by applying the
$\mathbf{M}^{n}_{\smash{\mathcal{ALC}}}$-rules to the $n$-labelled constraint
system $S_{n}=\\{n:\Diamond_{i}\exists r.A(x),\Box_{i}\lnot A(x)\\}$, we get
the $m$-labelled constraint system $S_{m}=\\{m:\exists r.A(x),m:\lnot
A(x),m:r(x,y),m:A(y)\\}$. The fresh variable $y$ in $S_{m}$ does not allow for
the direct extraction of a constant domain model, as no object in the domain
of the world associated with $S_{n}$ would be capable of representing $y$
correctly. An alternative approach involves _quasimodels_ [17], to
characterise satisfiability on constant domain models in terms of structures
representing “abstractions” of the actual models of a formula. Objects across
worlds can be represented by means of _runs_ , i.e., functions to guarantee
their modal properties and the constant domain assumption. A similar strategy
is presented in [35, 37, 36], where the definition of runs (which is not
carried out in detail) involves the introduction of suitable world “copies”.
We conjecture that a quasimodel-based approach with _marked variables_ , as
illustrated in [17], can also be adopted to solve the constant domain model
extraction issue.

Moreover, we aim at tight complexities for
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ satisfiability, both in varying and
in constant domain models. While $\smash{\mathcal{ALC}}$ formula
satisfiability is ExpTime-complete, it is unclear whether the upper bound for
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ on varying or constant domain
neighbourhood models can be improved to ExpTime-membership, for any
$\mathit{L}\in\smash{\mathsf{Pantheon}}$. At the propositional level, the
formula satisfiability problem for the systems based on the $L$-condition,
with $\mathbf{C}\not\in L$, is NP-complete, rising to PSpace if the
$\mathbf{C}$-condition is included [40]. For normal modal description logics,
instead, the (tight) NExpTime-hardness results are based on complexity proofs
of _product logics_ over relational product frames [17], and cannot be
immediately adapted to neighbourhood semantics, where an analogous notion of
product is not yet well understood. Nonetheless, we conjecture that the
NExpTime-hardness known for, e.g., $\mathbf{K}_{\mathcal{ALC}}$ on constant
domain relational models, also holds in the neighbourhood case, at least in
presence of the $\mathbf{C}$-condition.

Finally, we plan to study: non-normal modal description logics in
_coalitional_ and _strategic_ settings [30, 38, 37], with an interplay between
abilities and powers of _groups_ of agents, rather than single ones;
additional description logics constructs (e.g. _nominals_ , _inverse roles_ ,
or _number restrictions_ [7]); and _interactions between modalities_ , with
axioms expressing e.g. that an agent _can do_ anything they _actually do_ , by
means of formulas of the form $\mathbb{D}_{i}C\sqsubseteq\mathbb{C}_{i}C$ or
$\mathbb{D}_{i}\varphi\to\mathbb{C}_{i}\varphi$.

## Acknowledgements

This research has been partially supported by the Province of Bolzano and DFG
through the project D2G2 (DFG grant n. 500249124). Andrea Mazzullo
acknowledges the support of the MUR PNRR project FAIR - Future AI Research
(PE00000013) funded by the NextGenerationEU. Ana Ozaki is supported by the
Research Council of Norway, project number 316022.

## References

  * [1] Ågotnes, T., Wáng, Y.N.: Somebody knows. In: KR. pp. 2–11 (2021)
  * [2] Anglberger, A.J., Gratzl, N., Roy, O.: Obligation, free choice, and the logic of weakest permissions. Rev. Symb. Logic 8(4), 807–827 (2015)
  * [3] Åqvist, L.: Good samaritans, contrary-to-duty imperatives, and epistemic obligations. Noûs 1(4), 361–379 (1967)
  * [4] Arló-Costa, H.L.: First Order Extensions of Classical Systems of Modal Logic; The role of the Barcan schemas. Stud. Logica 71(1), 87–118 (2002)
  * [5] Arló-Costa, H.L., Pacuit, E.: First-order classical modal logic. Stud. Logica 84(2), 171–210 (2006)
  * [6] Baader, F., Ghilardi, S., Lutz, C.: LTL over description logic axioms. ACM T. Comput. Logic 13(3), 21:1–21:32 (2012)
  * [7] Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017)
  * [8] Balbiani, P., Fernández-Duque, D., Lorini, E.: The dynamics of epistemic attitudes in resource-bounded agents. Studia Logica 107(3), 457–488 (2019)
  * [9] Bozzato, L., Ferrari, M., Fiorentini, C., Fiorino, G.: A constructive semantics for ALC. In: Proceedings of the 2007 International Workshop on Description Logics (DL2007), Brixen-Bressanone, near Bozen-Bolzano, Italy, 8-10 June, 2007\. CEUR Workshop Proceedings, vol. 250. CEUR-WS.org (2007)
  * [10] Brown, M.A.: On the logic of ability. Journal of philosophical logic pp. 1–26 (1988)
  * [11] Chellas, B.F.: Modal logic: an introduction. Cambridge University Press (1980)
  * [12] Dalmonte, T., Lellmann, B., Olivetti, N., Pimentel, E.: Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity. Journal of Logic and Computation 31(1), 67–111 (2021)
  * [13] Dalmonte, T., Mazzullo, A., Ozaki, A.: On non-normal modal description logics. In: Simkus, M., Weddell, G.E. (eds.) DL. vol. 2373. CEUR-WS.org (2019)
  * [14] Dalmonte, T., Mazzullo, A., Ozaki, A.: Reasoning in non-normal modal description logics. In: Benzmüller, C., Otten, J. (eds.) ARQNL@IJCAR. vol. 2095, pp. 28–45 (2022)
  * [15] Elgesem, D.: The modal logic of agency. Nordic Journal of Philosophical Logic (1997)
  * [16] Forrester, J.W.: Gentle murder, or the adverbial samaritan. The Journal of Philosophy 81(4), 193–197 (1984)
  * [17] Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional Modal Logics: Theory and Applications. Elsevier (2003)
  * [18] Gasquet, O., Herzig, A.: From classical to normal modal logics. In: Proof theory of modal logic, pp. 293–311. Springer (1996)
  * [19] Goble, L.: Prima facie norms, normative conflicts, and dilemmas. Handbook of deontic logic and normative systems 1, 241–351 (2013)
  * [20] Governatori, G., Rotolo, A.: On the axiomatisation of elgesem’s logic of agency and ability. Journal of Philosophical Logic 34(4), 403–431 (2005). https://doi.org/10.1007/s10992-004-6368-1
  * [21] Kracht, M., Wolter, F.: Normal monomodal logics can simulate all others. J. Symbolic Logic 64(1), 99–138 (1999)
  * [22] Kripke, S.A.: Semantical analysis of modal logic II: Non-normal modal propositional calculi. In: The theory of models, pp. 206–220. Elsevier (2014)
  * [23] Lemmon, E.J., Scott, D.: An Introduction to Modal logic. Blackwell (1977)
  * [24] Lewis, C.I., Langford, C.H., Lamprecht, P.: Symbolic logic, vol. 170. Dover Publications New York (1959)
  * [25] Lismont, L., Mongin, P.: A non-minimal but very weak axiomatization of common belief. Artificial Intelligence 70(1-2), 363–374 (1994). https://doi.org/10.1016/0004-3702(94)90111-2
  * [26] Montague, R.: Universal grammar. Theoria 36(3), 373–398 (1970)
  * [27] Montali, M., Pesic, M., van der Aalst, W.M.P., Chesani, F., Mello, P., Storari, S.: Declarative specification and verification of service choreographiess. ACM Trans. Web 4(1), 3:1–3:62 (2010)
  * [28] Pacuit, E.: Neighborhood Semantics for Modal Logic. Springer (2017)
  * [29] de Paiva, V.: Constructive description logics: what, why and how. In: Context Representation and Reasoning, Riva del Garda (2006)
  * [30] Pauly, M.: A modal logic for coalitional power in games. Journal of logic and computation 12(1), 149–166 (2002)
  * [31] Ross, A.: Imperatives and logic. Philosophy of Science 11(1), 30–46 (1944)
  * [32] Scheele, S.: Model and proof theory of constructive ALC: constructive description logics. Ph.D. thesis, University of Bamberg (2015)
  * [33] Scott, D.: Advice on modal logic. In: Philosophical problems in logic, pp. 143–173. Springer (1970)
  * [34] Segerberg, K.: An essay in classical modal logic. Ph.D. thesis, Stanford University (1971)
  * [35] Seylan, I., Erdur, R.C.: A tableau decision procedure for $\mathcal{ALC}$ with monotonic modal operators and constant domains. ENTCS 231, 113–130 (2009)
  * [36] Seylan, I., Jamroga, W.: Coalition description logic with individuals. ENTCS 262, 231–248 (2010)
  * [37] Seylan, I., Jamroga, W.: Description logic for coalitions. In: AAMAS. pp. 425–432 (2009)
  * [38] Troquard, N.: Reasoning about coalitional agency and ability in the logics of “bringing-it-about”. Autonomous Agents and Multi-Agent Systems 28(3), 381–407 (2014)
  * [39] Vardi, M.Y.: On epistemic logic and logical omniscience. In: TARK. pp. 293–305 (1986)
  * [40] Vardi, M.Y.: On the complexity of epistemic reasoning. In: LICS. pp. 243–252 (1989)
  * [41] Von Wright, G.H.: Deontic logic. Mind 60(237), 1–15 (1951)
  * [42] Wolter, F., Zakharyaschev, M.: On the decidability of description logics with modal operators. In: KR. pp. 512–523 (1998)

##  Appendix 0.A Modelling Scenario

In the following, we present the modelling of an example scenario in the
classic domain of multi-agent purchase choreography [27]. The aim is twofold.
First, it displays some of the limitations of modalities defined on relational
frames, motivating the adoption of neighbourhood semantics in modal extensions
of description logics. Second, it illustrates the expressivity of (non-normal)
modal description logic languages, showing interactions between modalities and
the constructs of the standard description logic $\smash{\mathcal{ALC}}$.

Our multi-agent setting involves a customer $\mathit{c}$, a marketplace
$\mathit{m}$, a seller $\mathit{s}$, and a warehouse $\mathit{w}$, with agency
operators $\mathbb{D}_{i}$ and $\mathbb{C}_{i}$, for $i\in\\{c,m,s,w\\}$, read
as ‘agent $i$ does/makes’ and ‘agent $i$ can do/make’, respectively [15, 20].
Concept names $\mathsf{Ord}$, $\mathsf{Prod}$, and $\mathsf{InCatal}$ are used
to represent, respectively, orders, products, and the class of objects
displayed as in-catalogue, while $\mathsf{req}$ is a role name for the request
relation. The formula
$\mathsf{Ord}\equiv\mathbb{D}_{c}\exists\mathsf{req}.(\mathsf{Prod}\sqcap\mathsf{InCatal})$
defines an order $\mathsf{Ord}$ as a request made by customer $c$ of an in-
catalogue product. Using the concept name $\mathsf{Confirm}$ to represent the
class of objects that are confirmed, we also have that
$\exists\mathsf{req}.(\mathsf{Prod}\sqcap\mathsf{InCatal})\sqsubseteq\mathsf{Confirm}\sqcup\lnot\mathsf{Confirm},$
meaning that any request of an in-catalogue product is either confirmed or not
confirmed. However, relational semantics validates the so-called _$\mathbf{M}$
-principle_ (often called _monotonicity_) as well, according to which
$C\sqsubseteq D$ always entails $\mathbb{D}_{c}C\sqsubseteq\mathbb{D}_{c}D$,
for any concepts $C,D$. Thus, from the $\mathbf{M}$-principle we would obtain
$\mathsf{Ord}\sqsubseteq\mathbb{D}_{c}(\mathsf{Confirm}\sqcup\lnot\mathsf{Confirm}),$
meaning that any order is made confirmed or not confirmed by $c$. This is an
unwanted conclusion in our agency-based scenario, since customers’ actions
should be unrelated to any aspect of order confirmation.

Moreover, assume that the concept name $\mathsf{SubmitOrd}$ stands for the
class of submitted orders, and that $\mathsf{PartConf}$ and $\mathsf{Reject}$
are used in our knowledge base to represent, respectively, the partially
confirmed and the rejected entities. Now consider the formula
$\mathsf{SubmitOrd}\sqsubseteq\mathbb{C}_{s}\mathsf{Confirm}\sqcap\mathbb{C}_{s}\mathsf{PartConf}\sqcap\mathbb{C}_{s}\mathsf{Reject},$
stating that a submitted order can be confirmed, can be partially confirmed,
and can be rejected by the seller $s$. On relational frames, however, we have
that $\mathbb{C}_{s}C\sqcap\mathbb{C}_{s}D\sqsubseteq\mathbb{C}_{s}(C\sqcap
D)$ is a valid formula, for any concepts $C,D$, known as the _$\mathbf{C}$
-principle_ (or _agglomeration_). Therefore, by the $\mathbf{C}$-principle,
under relational semantics we would be forced to conclude that
$\mathsf{SubmitOrd}\sqsubseteq\mathbb{C}_{s}(\mathsf{Confirm}\sqcap\mathsf{PartConf}\sqcap\mathsf{Reject}),$
meaning that any submitted order is such that the seller $s$ has the ability
to make it confirmed, partially confirmed, and rejected, all _at once_ , which
is unreasonable.

Consider now the formula
$\top\sqsubseteq\mathsf{Confirm}\sqcup\lnot\mathsf{Confirm},$ i.e., the truism
stating that anything is either confirmed or not confirmed. By the so called
_$\mathbf{N}$ -principle_ (or _necessitation_) of relational semantics, we
have that if $\top\sqsubseteq C$ is valid on relational frames, then
$\top\sqsubseteq\mathbb{D}_{c}C$ holds as well, for any concept $C$. Thus,
from the $\mathbf{N}$-principle of relational semantics it would follow that
$\top\sqsubseteq\mathbb{D}_{c}(\mathsf{Confirm}\sqcup\lnot\mathsf{Confirm}),$
thereby forcing us to the consequence that every object is made by customer
$c$ to be either confirmed or not confirmed, and hence leading again to an
unreasonable connection between customer’s actions and confirmation of orders.
In fact, since customer $c$ plays no role in confirmation actions, it is
sensible to assume that, for any object of the domain, it is not the case that
$c$ makes it confirmed or not confirmed. This can be achieved by the formula
$\top\sqsubseteq\lnot\mathbb{D}_{c}(\mathsf{Confirm}\sqcup\lnot\mathsf{Confirm}),$
an instance of a principle sometimes known as the _$\mathbf{Q}$ -principle_,
which is _unsatisfiable_ in relational frames, while admissible over
neighbourhood ones.

Finally, we consider additional principles that can be adopted both in
relational and neighbourhood semantics. The formula
$\mathbb{D}_{w}\mathsf{Avail}\sqsubseteq\mathsf{Avail}$ states that anything
that is _made_ available by the warehouse $w$ is _actually_ available. This is
an instance of the so-called _$\mathbf{T}$ -principle_ (also _factivity
principle_), well-known in modal logic, particularly for its epistemic
applications (if an agent _knows_ something, it has to be true). Both in
relational and neighbourhood semantics, the $\mathbf{T}$-principle entails the
so-called _$\mathbf{D}$ -principle_. This is instantiated by
$\mathbb{D}_{w}\mathsf{Avail}\sqsubseteq\lnot\mathbb{D}_{w}\lnot\mathsf{Avail},$
a formula asserting that anything that is _made available_ by the warehouse
$w$ is _not made unavailable_ by $w$. This principle, also well-known for its
epistemic implications (anything that is _known_ by an agent is _compatible_
with their knowledge), in relational semantics is _equivalent_ to a much
lesser known principle, sometimes called _$\mathbf{P}$ -principle_. An example
of it is given by the formula
$\top\sqsubseteq\lnot\mathbb{D}_{w}(\mathsf{Avail}\sqcap\lnot\mathsf{Avail}),$
which states that, for any object, it is not the case that the warehouse $w$
makes it both available _and_ unavailable. Neighbourhood semantics, under
which the $\mathbf{D}$\- and the $\mathbf{P}$-principle are _not equivalent_ ,
allows for distinctions between modal constraints that are hence more fine-
grained than in relational semantics.

$\begin{array}[]{@{}r@{~~}c@{~~}l@{\qquad}r@{~~}c<EMAIL_ADDRESS>\mathsf{Confirm}~{}~{}&\sqsubseteq\hfil~{}~{}&\lnot\mathsf{PartConf}&\mathsf{SubmitOrd}~{}~{}&\sqsubseteq\hfil~{}~{}&\mathbb{C}_{s}\forall\mathsf{req}.(\mathbb{D}_{w}\mathsf{Avail}\sqcup\mathbb{D}_{w}\lnot\mathsf{Avail})\\\
\mathsf{Confirm}~{}~{}&\sqsubseteq\hfil~{}~{}&\lnot\mathsf{Reject}&\mathsf{SubmitOrd}~{}~{}&\sqsubseteq\hfil~{}~{}&\mathbb{C}_{s}\mathsf{Confirm}\sqcap\mathbb{C}_{s}\mathsf{PartConf}\sqcap\mathbb{C}_{s}\mathsf{Reject}\\\
\mathsf{PartConf}~{}~{}&\sqsubseteq\hfil~{}~{}&\lnot\mathsf{Reject}&\mathbb{D}_{s}\mathsf{Confirm}~{}~{}&\sqsubseteq\hfil~{}~{}&\forall\mathsf{req}.\mathbb{D}_{w}\mathsf{Avail}\\\
\mathsf{Ord}~{}~{}&\equiv\hfil~{}~{}&\mathbb{D}_{c}\exists\mathsf{req}.(\mathsf{Prod}\sqcap\mathsf{InCatal})&\mathbb{C}_{s}\mathsf{PartConf}~{}~{}&\sqsupseteq\hfil~{}~{}&\exists\mathsf{req}.\mathbb{D}_{w}\mathsf{Avail}\
\sqcap\exists\mathsf{req}.\mathbb{D}_{w}\lnot\mathsf{Avail}\\\
\mathsf{SubmitOrd}~{}~{}&\equiv\hfil~{}~{}&\mathsf{Ord}\sqcap\mathbb{D}_{c}\mathsf{Submit}&\mathbb{C}_{s}\mathsf{Reject}~{}~{}&\sqsupseteq\hfil~{}~{}&\forall\mathsf{req}.\mathbb{D}_{w}\lnot\mathsf{Avail}\\\
\mathsf{IncomplOrd}~{}~{}&\equiv\hfil~{}~{}&\mathsf{Ord}\sqcap\lnot\mathbb{D}_{c}\mathsf{Submit}&\mathbb{D}_{m}(\mathsf{ConfirmOrd}~{}~{}&\sqsubseteq\hfil~{}~{}&\lnot\mathbb{C}_{s}\mathsf{Reject})\\\
\mathsf{InvalidOrd}~{}~{}&\equiv\hfil~{}~{}&\mathsf{Ord}\sqcap\lnot\mathbb{C}_{c}\mathsf{Submit}&\mathsf{DispatchOrd}~{}~{}&\equiv\hfil~{}~{}&\mathsf{Ord}\sqcap\mathbb{D}_{s}\mathbb{D}_{w}\mathsf{Dispatch}\\\
\mathsf{ConfirmOrd}~{}~{}&\equiv\hfil~{}~{}&\mathsf{Ord}\sqcap\mathbb{D}_{s}\mathsf{Confirm}&\mathbb{D}_{m}(\mathsf{ConfirmOrd}~{}~{}&\sqsubseteq\hfil~{}~{}&\mathsf{DispatchOrd})\end{array}$
Figure 3: Purchase choreography knowledge base.

The full knowledge base describing the purchase choreography scenario is
reported in Figure 3. Notably, it displays a great range of interactions
between modal and description logics constructs. The modal operators
$\mathbb{D}_{i}$ and $\mathbb{C}_{i}$ are axiomatized similarly to [15]:
$\mathbb{D}_{i}$ obeys the $\mathbf{C}$\- and $\mathbf{T}$-principles; and
both satisfy the $\mathbf{Q}$-principle, and the $\mathbf{E}$-principle:
$C\equiv D$ entails $\mathbb{D}_{i}C\equiv\mathbb{D}_{i}D$ and
$\mathbb{C}_{i}C\equiv\mathbb{C}_{i}D$.

On the left column, the first four axioms impose that the range of the request
relation is a product, and that the classes of confirmed, partially confirmed,
and rejected objects are all disjoint. We have already discussed the fifth
axiom, which is the definition of an order as a request, made by a customer,
for some in-catalogue product. The last four axioms on the left column define,
respectively: a submitted order as an order that is actually submitted by a
customer; an incomplete order as an order that is not submitted by the
customer; an invalid order as an order that cannot be submitted by the
customer; and a confirmed order as an order that is confirmed by the seller.

On the right column, the first formula states that an invalid order can be
cancelled by the seller. The second axiom asserts that, given a submitted
order, the seller can check at the warehouse for availability of all of its
requested products. The third formula, as already discussed, requires that a
submitted order can be confirmed, can be partially confirmed, and can be
rejected by the seller. The subsequent three axioms impose, respectively, the
following constraints: anything that is confirmed by the seller has to request
only products made available by the warehouse; anything that requests products
that are made available, as well as products that are brought about to be
unavailable by the warehouse, can be partially confirmed by the seller;
finally, any request of products that are all unavailable at the warehouse can
be rejected by the seller. The third formula from the bottom of the right
column states that the marketplace enforces that a confirmed order cannot be
rejected by the seller. The second last axiom defines a dispatched order as an
order that the seller makes the warehouse dispatch. Finally, the last formula
imposes that the marketplace brings it about that any confirmed order is also
dispatched.

##  Appendix 0.B Proofs for Section 2

See 2.1

###### Proof.

Point 1. Suppose that, for every $w\in\mathcal{W}$,
$\alpha,\beta\subseteq\mathcal{W}$, we have: ($\mathbf{M}$-condition)
$\alpha\in\mathcal{N}_{i}(w)$ and $\alpha\subseteq\beta$ implies
$\beta\in\mathcal{N}_{i}(w)$; and ($\mathbf{Q}$-condition)
$\mathcal{W}\not\in\mathcal{N}_{i}(w)$. This means that
$\alpha\not\in\mathcal{N}_{i}(w)$, for every $\alpha\subseteq\mathcal{W}$,
i.e., $\mathcal{N}_{i}(w)=\emptyset$. Thus, every condition, except for the
$\mathbf{N}$-condition, is satisfied by $\mathcal{N}_{i}$.

Point 2. Suppose $(i)$ that, for every $w\in\mathcal{W}$,
$\alpha,\beta\subseteq\mathcal{W}$, we have: ($\mathbf{M}$-condition)
$\alpha\in\mathcal{N}_{i}(w)$ and $\alpha\subseteq\beta$ implies
$\beta\in\mathcal{N}_{i}(w)$; and ($\mathbf{D}$-condition)
$\alpha\in\mathcal{N}_{i}(w)$ implies
$\mathcal{W}\setminus\alpha\not\in\mathcal{N}_{i}(w)$. Towards a
contradiction, suppose that $\emptyset\in\mathcal{N}_{i}(w)$. Then, we have
$\mathcal{W}=\mathcal{W}\setminus\emptyset\not\in\mathcal{N}_{i}(w)$ as well.
By contraposition, this implies in particular that
$\emptyset\not\in\mathcal{N}_{i}(w)$, a contradiction. Thus,
($\mathbf{P}$-condition) $\emptyset\not\in\mathcal{N}_{i}(w)$

Moreover, suppose $(ii)$ that, for every $\alpha\subseteq\mathcal{W}$, we
have: ($\mathbf{N}$-condition) $\mathcal{W}\in\mathcal{N}_{i}(w)$, i.e.,
$\mathcal{W}\setminus\emptyset\in\mathcal{N}_{i}(w)$; and
($\mathbf{D}$-condition) $\alpha\in\mathcal{N}_{i}(w)$ implies
$\mathcal{W}\setminus\alpha\not\in\mathcal{N}_{i}(w)$. By contraposition, we
obtain that ($\mathbf{P}$-condition) $\emptyset\not\in\mathcal{N}_{i}(w)$.

Finally, suppose $(iii)$ that, for every $w\in\mathcal{W}$,
$\alpha,\beta\subseteq\mathcal{W}$, we have: ($\mathbf{T}$-condition)
$\alpha\in\mathcal{N}_{i}(w)$ implies $w\in\alpha$. Then, we have
($\mathbf{P}$-condition) $\emptyset\not\in\mathcal{N}_{i}(w)$, for otherwise
we would get a contradiction.

Point 3. Suppose $(i)$ that, for every $w\in\mathcal{W}$,
$\alpha,\beta\subseteq\mathcal{W}$, we have: ($\mathbf{C}$-condition)
$\alpha\in\mathcal{N}_{i}(w)$ and $\beta\in\mathcal{N}_{i}(w)$ implies
$\alpha\cap\beta\in\mathcal{N}_{i}(w)$; and ($\mathbf{P}$-condition)
$\emptyset\not\in\mathcal{N}_{i}(w)$. Given $\alpha\in\mathcal{N}_{i}(w)$,
suppose towards a contradiction that
$\mathcal{W}\setminus\alpha\in\mathcal{N}_{i}(w)$. From this, we obtain that
$\emptyset=\alpha\cap(\mathcal{W}\setminus\alpha)\in\mathcal{N}_{i}(w)$, a
contradiction. Thus, we have that ($\mathbf{D}$-condition)
$\alpha\in\mathcal{N}_{i}(w)$ implies
$\mathcal{W}\setminus\alpha\not\in\mathcal{N}_{i}(w)$.

Moreover, suppose $(ii)$ that, for every $w\in\mathcal{W}$,
$\alpha,\beta\subseteq\mathcal{W}$, we have: ($\mathbf{T}$-condition)
$\alpha\in\mathcal{N}_{i}(w)$ implies $w\in\alpha$. Consider
$\alpha\in\mathcal{N}_{i}(w)$ and suppose, towards a contradiction, that also
$\mathcal{W}\setminus\alpha\in\mathcal{N}_{i}(w)$. We obtain that $w\in\alpha$
and $w\in\mathcal{W}\setminus\alpha$ as well, a contradiction. Hence, we have
that ($\mathbf{D}$-condition) $\alpha\in\mathcal{N}_{i}(w)$ implies
$\mathcal{W}\setminus\alpha\not\in\mathcal{N}_{i}(w)$.

Point 4. Straightforward, because otherwise we immediately have a
contradiction. ∎

See 1

###### Proof.

Here we present a proof only for $\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$
concept inclusions and only for the basic principles
$L\in\\{\mathbf{E,M,C,N,P,Q,D,T}\\}$. For
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ formulas, the proof is similar to
the case of propositional non-normal modal logics (see e.g. [28]). More
complex principles (e.g. $\mathbf{EMCN}$) can be obtained by suitably
combining the basic principles. Let
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$ be a neighbourhood
frame and let $L$ be as above.

$\mathit{L=\mathbf{E}}$.

If $C\equiv D$ is valid on $\mathcal{F}$, then for all
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$, and all $w$ in
$\mathcal{M}$, we have $C^{\mathcal{I}_{w}}=D^{\mathcal{I}_{w}}$. Thus, for
all $d\in\Delta_{w}$, $\llbracket C\rrbracket^{\mathcal{M}}_{d}=\llbracket
D\rrbracket^{\mathcal{M}}_{d}$. So for all $v\in\mathcal{W}$, $\llbracket
C\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(v)$ iff $\llbracket
D\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(v)$, which implies
$d\in(\Box_{i}C)^{\mathcal{I}_{v}}$ iff $d\in(\Box_{i}D)^{\mathcal{I}_{v}}$,
that is $(\Box_{i}C)^{\mathcal{I}_{v}}=(\Box_{i}D)^{\mathcal{I}_{v}}$. Then,
$\Box_{i}C\equiv\Box_{i}D$ is valid on $\mathcal{F}$, for all $i\in J$.

$\mathit{L=\mathbf{M}}$.

From right to left, assume that $\mathcal{F}$ is supplemented and
$C\sqsubseteq D$ is valid on $\mathcal{F}$. Then, for all
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$, and all $w$ in
$\mathcal{M}$, we have $C^{\mathcal{I}_{w}}\subseteq D^{\mathcal{I}_{w}}$.
Thus, for all $d\in\Delta_{w}$, $\llbracket
C\rrbracket^{\mathcal{M}}_{d}\subseteq\llbracket
D\rrbracket^{\mathcal{M}}_{d}$. By supplementation we have that, for all
$v\in\mathcal{W}$, $\llbracket
C\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(v)$ implies $\llbracket
D\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(v)$. So
$d\in(\Box_{i}C)^{\mathcal{I}_{v}}$ implies
$d\in(\Box_{i}D)^{\mathcal{I}_{v}}$, that is
$(\Box_{i}C)^{\mathcal{I}_{v}}\subseteq(\Box_{i}D)^{\mathcal{I}_{v}}$. Then
$\Box_{i}C\sqsubseteq\Box_{i}D$ is valid on $\mathcal{F}$. For the left-to-
right direction, assume that $\mathcal{F}$ is not supplemented. Then there are
$w\in\mathcal{W}$, $\alpha,\beta\subseteq\mathcal{W}$ such that
$\alpha\subseteq\beta$, $\alpha\in\mathcal{N}_{i}(w)$ and
$\beta\notin\mathcal{N}_{i}(w)$. We define over $\mathcal{F}$ the model
$\mathcal{M}=(\mathcal{F},\mathcal{I})$, where $\Delta_{w}=\\{d\\}$, for every
$w\in\mathcal{W}$, and the interpretation of two concept names $A,B\in{\sf
N_{C}}$ is defined as follows: $d\in A^{\mathcal{I}_{v}}$ iff $v\in\alpha$,
and $d\in B^{\mathcal{I}_{v}}$ iff $v\in\beta$ (and defined arbitrarily on all
other symbols in $({\sf N_{C}}\cup{\sf N_{R}})\setminus\\{A,B\\}$). As a
consequence, we have that $\llbracket A\rrbracket_{d}^{\mathcal{M}}=\alpha$
and $\llbracket B\rrbracket_{d}^{\mathcal{M}}=\beta$, which implies
$\llbracket A\rrbracket_{d}^{\mathcal{M}}=\llbracket
A\rrbracket_{d}^{\mathcal{M}}\cap\llbracket
B\rrbracket_{d}^{\mathcal{M}}=\llbracket A\sqcap
B\rrbracket_{d}^{\mathcal{M}}$. Thus $\llbracket A\sqcap
B\rrbracket_{d}^{\mathcal{M}}\in\mathcal{N}_{i}(w)$ and $\llbracket
B\rrbracket_{d}^{\mathcal{M}}\notin\mathcal{N}_{i}(w)$. By definition we have
$d\in(\Box_{i}(A\sqcap B))^{\mathcal{I}_{w}}$ and
$d\notin(\Box_{i}B)^{\mathcal{I}_{w}}$.

$\mathit{L=\mathbf{C}}$.

From right-to-left, assume that $\mathcal{F}$ is closed under intersection.
Moreover, let $\mathcal{M}=(\mathcal{F},\mathcal{I})$ be a model based on
$\mathcal{F}$, with $w$ world of $\mathcal{M}$, and $d\in\Delta$ such that
$d\in(\Box_{i}C\sqcap\Box_{i}D)^{\mathcal{I}_{w}}$. Thus
$d\in(\Box_{i}C)^{\mathcal{I}_{w}}$ and $d\in(\Box_{i}D)^{\mathcal{I}_{w}}$,
that is $[C]_{d}^{\mathcal{M}},[D]_{d}^{\mathcal{M}}\in\mathcal{N}_{i}(w)$. By
closure under intersection,
$[C]_{d}^{\mathcal{M}}\cap[D]_{d}^{\mathcal{M}}=[C\sqcap
D]_{d}^{\mathcal{M}}\in\mathcal{N}_{i}(w)$. Then $d\in(\Box_{i}(C\sqcap
D))^{\mathcal{I}_{w}}$. For the left-to-right direction, assume that
$\mathcal{F}$ is not closed under intersection. Then, there are
$w\in\mathcal{W}$, $\alpha,\beta\subseteq\mathcal{W}$ such that
$\alpha,\beta\in\mathcal{N}_{i}(w)$ and
$\alpha\cap\beta\notin\mathcal{N}_{i}(w)$. We define over $\mathcal{F}$ the
model $\mathcal{M}=(\mathcal{F},\mathcal{I})$, where $\Delta_{w}=\\{d\\}$, for
all $w\in\mathcal{W}$, and the interpretation of two concept names $A,B\in{\sf
N_{C}}$ is defined as follows: $d\in A^{\mathcal{I}_{v}}$ iff $v\in\alpha$,
and $d\in B^{\mathcal{I}_{v}}$ iff $v\in\beta$ (and defined arbitrarily on all
other symbols in $({\sf N_{C}}\cup{\sf N_{R}})\setminus\\{A,B\\}$). We have
$\llbracket A\rrbracket_{d}^{\mathcal{M}}=\alpha$ and $\llbracket
B\rrbracket_{d}^{\mathcal{M}}=\beta$, which implies
$d\in(\Box_{i}A)^{\mathcal{I}_{w}}$ and $d\in(\Box_{i}B)^{\mathcal{I}_{w}}$.
Moreover, $\llbracket A\sqcap B\rrbracket_{d}^{\mathcal{M}}=\llbracket
A\rrbracket_{d}^{\mathcal{M}}\cap\llbracket
B\rrbracket_{d}^{\mathcal{M}}=\alpha\cap\beta\notin\mathcal{N}_{i}(w)$. Thus
$d\notin(\Box_{i}(A\sqcap B))^{\mathcal{I}_{w}}$.

$\mathit{L=\mathbf{N}}$.

From right-to-left, assume that $\mathcal{F}$ contains the unit and
$\top\sqsubseteq C$ is valid on $\mathcal{F}$. Then for all
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$, and all $w$ in
$\mathcal{M}$, we have $C^{\mathcal{I}_{w}}=\Delta_{w}$. As a consequence, for
all $d\in\Delta_{w}$, $\llbracket C\rrbracket^{\mathcal{M}}_{d}=\mathcal{W}$.
By the property of containing the unit we have that, for all
$v\in\mathcal{W}$, $\llbracket
C\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(v)$. So
$d\in(\Box_{i}C)^{\mathcal{I}_{v}}$ for all $d\in\Delta_{v}$, that is,
$\top\sqsubseteq\Box_{i}C$ is valid on $\mathcal{F}$. For the left-to-right
direction, assume that $\mathcal{F}$ does not contain the unit, i.e., there is
$w\in\mathcal{W}$ such that $\mathcal{W}\notin\mathcal{N}_{i}(w)$. Then, for
all models $\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$, all
$w\in\mathcal{W}$, and all $d\in\Delta_{w}$, we have
$d\in\top^{\mathcal{I}_{w}}$. Moreover, since
$d\in(\Box_{i}\top)^{\mathcal{I}_{w}}$ iff
$\llbracket\top\rrbracket_{d}^{\mathcal{M}}\in\mathcal{N}_{i}(w)$ iff
$\mathcal{W}\in\mathcal{N}_{i}(w)$, we also have
$d\notin(\Box_{i}\top)^{\mathcal{I}_{w}}$.

$\mathit{L=\mathbf{P}}$.

From right-to-left, assume that
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$ satisfies the
$\mathbf{P}$-condition. I.e., for all $w\in\mathcal{W}$ and $i\in J$,
$\emptyset\not\in\mathcal{N}_{i}(w)$. Then, for all models
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$, all
$w\in\mathcal{W}$, and all $d\in\Delta_{w}$, we have
$\emptyset=\llbracket\bot\rrbracket^{\mathcal{M}}_{d}\not\in\mathcal{N}_{i}(w)$.
So $d\not\in(\Box_{i}\bot)^{\mathcal{I}_{w}}$, or equivalently
$d\in(\lnot\Box_{i}\bot)^{\mathcal{I}_{w}}$. Also,
$d\in\Delta_{w}=\top^{\mathcal{I}_{w}}$. So
$\top^{\mathcal{I}_{w}}\subseteq(\lnot\Box_{i}\bot)^{\mathcal{I}_{w}}$. Then
$\mathcal{M},w\models\top\sqsubseteq\lnot\Box_{i}\bot$. Hence
$\top\sqsubseteq\lnot\Box_{i}\bot$ is valid on $\mathcal{F}$. For the left-to-
right direction, assume that $\mathcal{F}$ does not satisfy the $P$-condition
for some $i\in J$. This means that there is $w\in\mathcal{W}$ such that
$\emptyset\in\mathcal{N}_{i}(w)$. So there exists a model
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$, a
$w\in\mathcal{W}$, and a $d\in\Delta_{w}$, such that
$\emptyset=\llbracket\bot\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)$.
So $d\in(\Box_{i}\bot)^{\mathcal{I}_{w}}$, or equivalently
$d\not\in(\lnot\Box_{i}\bot)^{\mathcal{I}_{w}}$. But
$d\in\Delta_{w}=\top^{\mathcal{I}_{w}}$. So
$\top^{\mathcal{I}_{w}}\not\subseteq(\lnot\Box_{i}\bot)^{\mathcal{I}_{w}}$.
Then $\mathcal{M},w\not\models\top\sqsubseteq\lnot\Box_{i}\bot$. Hence
$\top\sqsubseteq\lnot\Box_{i}\bot$ is not valid on $\mathcal{F}$.

$\mathit{L=\mathbf{Q}}$.

From right to left, assume that
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$ satisfies the
$\mathbf{Q}$-condition. I.e., for all $w\in\mathcal{W}$ and $i\in J$,
$\mathcal{W}\not\in\mathcal{N}_{i}(w)$. Then, for all models
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$, all
$w\in\mathcal{W}$, and all $d\in\Delta_{w}$, we have
$\mathcal{W}=\llbracket\top\rrbracket^{\mathcal{M}}_{d}\not\in\mathcal{N}_{i}(w)$.
So $d\not\in(\Box_{i}\top)^{\mathcal{I}_{w}}$, or equivalently
$d\in(\lnot\Box_{i}\top)^{\mathcal{I}_{w}}$. Also
$d\in\Delta=\top^{\mathcal{I}_{w}}$. So
$\top^{\mathcal{I}_{w}}\subseteq(\lnot\Box_{i}\top)^{\mathcal{I}_{w}}$. Then
$\mathcal{M},w\models\top\sqsubseteq\lnot\Box_{i}\top$. Hence
$\top\sqsubseteq\lnot\Box_{i}\top$ is valid on $\mathcal{F}$. For the other
direction, assume that $\mathcal{F}$ does not satisfy the
$\mathbf{Q}$-condition for some $i\in J$. This means that there is
$w\in\mathcal{W}$ such that $\mathcal{W}\in\mathcal{N}_{i}(w)$. So there
exists a model $\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$,
a $w\in\mathcal{W}$, and a $d\in\Delta_{w}$, such that
$\mathcal{W}=\llbracket\top\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)$.
So $d\in(\Box_{i}\top)^{\mathcal{I}_{w}}$, or equivalently
$d\not\in(\lnot\Box_{i}\top)^{\mathcal{I}_{w}}$. But
$d\in\Delta=\top^{\mathcal{I}_{w}}$. So
$\top^{\mathcal{I}_{w}}\not\subseteq(\lnot\Box_{i}\top)^{\mathcal{I}_{w}}$.
Then $\mathcal{M},w\not\models\top\sqsubseteq\lnot\Box_{i}\top$. Hence
$\top\sqsubseteq\lnot\Box_{i}\top$ is not valid on $\mathcal{F}$.

$\mathit{L=\mathbf{D}}$.

From right-to-left, assume that
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$ satisfies the
$\mathbf{D}$-condition. Moreover, let $\mathcal{M}=(\mathcal{F},\mathcal{I})$
based on $\mathcal{F}$, with a world $w\in\mathcal{W}$, and $d\in\Delta_{w}$,
a concept $C$, and $i\in J$, all arbitrarily chosen. Suppose that
$d\in(\Box_{i}C)^{\mathcal{I}_{w}}$. It means that
$[C]^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)$. By the $\mathbf{D}$-condition,
$\mathcal{W}\setminus[C]^{\mathcal{M}}_{d}\not\in\mathcal{N}_{i}(w)$.
Equivalently, $[\lnot C]^{\mathcal{M}}_{d}\not\in\mathcal{N}_{i}(w)$. This
means that $d\not\in(\Box_{i}\lnot C)^{\mathcal{I}_{w}}$, or equivalently,
that $d\in(\lnot\Box_{i}\lnot C)^{\mathcal{I}_{w}}$. So
$(\Box_{i}C)^{\mathcal{I}_{w}}\subseteq(\lnot\Box_{i}\lnot
C)^{\mathcal{I}_{w}}$. Then
$\mathcal{M},w\models\Box_{i}C\sqsubseteq\Diamond_{i}C$. Hence,
$\Box_{i}C\sqsubseteq\Diamond_{i}C$ is valid on $\mathcal{F}$. For the left-
to-right direction, assume that $\mathcal{F}$ does not satisfy the
$\mathbf{D}$-condition for $i\in J$. So there is a $w\in\mathcal{W}$, such
that, for some $\alpha\subseteq\mathcal{W}$, we have
$\alpha\in\mathcal{N}_{i}(w)$ and
$\mathcal{W}\setminus\alpha\in\mathcal{N}_{i}(w)$. We define
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$, where, for any
$v\in\mathcal{W}$, $\Delta_{v}=\\{d\\}$, and $A^{\mathcal{I}_{v}}=\\{d\\}$ iff
$v\in\alpha$ (and defined arbitrarily on all other symbols in $({\sf
N_{C}}\cup{\sf N_{R}})\setminus\\{A\\}$). We have $\llbracket
A\rrbracket^{\mathcal{M}}_{d}=\\{v\in\mathcal{W}\mid d\in
A^{\mathcal{I}_{w}}\\}=\alpha$, and $\llbracket\lnot
A\rrbracket^{\mathcal{M}}_{d}=\mathcal{W}\setminus\alpha$. So
$d\in(\Box_{i}A)^{\mathcal{I}_{w}}$ and $d\in(\Box_{i}\lnot
A)^{\mathcal{I}_{w}}$, and then $d\not\in(\lnot\Box_{i}\lnot
A)^{\mathcal{I}_{w}}$. So
$(\Box_{i}A)^{\mathcal{I}_{w}}\not\subseteq(\lnot\Box_{i}\lnot
A)^{\mathcal{I}_{w}}$. This means that,
$\mathcal{M},w\not\models\Box_{i}A\sqsubseteq\Diamond_{i}A$. Hence,
$\Box_{i}C\sqsubseteq\Diamond_{i}C$ is not valid on $\mathcal{F}$.

$\mathit{L=\mathbf{T}}$.

From right-to-left, assume that
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$ satisfies the
$\mathbf{T}$-condition. Moreover, let $\mathcal{M}=(\mathcal{F},\mathcal{I})$
based on $\mathcal{F}$, with a world $w\in\mathcal{W}$, and $d\in\Delta_{w}$,
a concept $C$, and $i\in J$, all arbitrarily chosen. Suppose that
$d\in(\Box_{i}C)^{\mathcal{I}_{w}}$. It means that $\llbracket
C\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)$. By the
$\mathbf{T}$-condition, $w\in\llbracket C\rrbracket^{\mathcal{M}}_{d}$. So
$d\in C^{\mathcal{I}_{w}}$. So $(\Box_{i}C)^{\mathcal{I}_{w}}\subseteq
C^{\mathcal{I}_{w}}$. Then $\mathcal{M},w\models\Box_{i}C\sqsubseteq C$.
Hence, $\Box_{i}C\sqsubseteq C$ is valid on $\mathcal{F}$. For the left-to-
right direction, assume that $\mathcal{F}$ does not satisfy the
$\mathbf{T}$-condition for $i\in J$. So there is a $w\in\mathcal{W}$, such
that for some $\alpha\subseteq\mathcal{W}$ we have
$\alpha\in\mathcal{N}_{i}(w)$ and $w\not\in\alpha$. We define
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ based on $\mathcal{F}$, where
$\Delta_{v}=\\{d\\}$, for any $v\in\mathcal{W}$, and
$A^{\mathcal{I}_{v}}=\\{d\\}$ iff $v\in\alpha$ (and defined arbitrarily on all
other symbols in $({\sf N_{C}}\cup{\sf N_{R}})\setminus\\{A\\}$). We have
$\llbracket A\rrbracket^{\mathcal{M}}_{d}=\\{v\in\mathcal{W}\mid d\in
A^{\mathcal{I}_{w}}\\}=\alpha$. So $d\in(\Box_{i}A)^{\mathcal{I}_{w}}$. Since
$w\not\in\alpha$, $w\in\mathcal{W}\setminus\alpha$. That is,
$w\in\mathcal{W}\setminus\llbracket A\rrbracket^{\mathcal{M}}_{d}$, or
equivalently $w\in\llbracket\lnot A\rrbracket^{\mathcal{M}}_{d}$. Then,
$d\in(\lnot A)^{\mathcal{I}_{w}}$, or equivalently
$d\not\in(A)^{\mathcal{I}_{w}}$. So,
$(\Box_{i}A)^{\mathcal{I}_{w}}\not\subseteq A^{\mathcal{I}_{w}}$, meaning that
$\mathcal{M},w\not\models\Box_{i}A\sqsubseteq A$. Hence, $\Box_{i}C\sqsubseteq
C$ is not valid on $\mathcal{F}$, as required. ∎

See 2

###### Proof.

_Point 1._ The $(\Rightarrow)$ direction follows from the proof of Proposition
1. To see that the $(\Leftarrow)$ direction does not hold in general, we
provide the following counterexample showing that the $\mathbf{T}$-principle
holds in a model that does not satisfy the $\mathbf{T}$-condition. Consider
$\mathcal{M}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J},\mathcal{I})$, where

  * •

$\mathcal{W}=\\{w,v\\}$;

  * •

$\mathcal{N}_{i}(w)=\\{\\{v\\},\mathcal{W}\\}$ and
$\mathcal{N}_{i}(v)=\\{\\{w\\},\mathcal{W}\\}$, for $i\in J$;

  * •

$\mathcal{I}_{w}=\mathcal{I}_{v}$, with $\Delta_{w}=\Delta_{v}=\\{d\\}$.

$\mathcal{M}$ does not satisfy the $\mathbf{T}$-condition, since
$\\{v\\}\in\mathcal{N}_{i}(w)$ but $w\notin\\{v\\}$. We show that the
$\mathbf{T}$-principle holds in $\mathcal{M}$.

######  Claim 1.

For all concepts $C$, $\llbracket C\rrbracket^{\mathcal{M}}_{d}=\emptyset$ or
$\llbracket C\rrbracket^{\mathcal{M}}_{d}=\mathcal{W}$.

###### Proof of Claim.

By induction on the construction of $C$.

For the base case $C=A\in{\sf N_{C}}$, it follows from the definition that
either $d\in A^{\mathcal{I}_{w}}$ and $d\in A^{\mathcal{I}_{v}}$, hence
$\llbracket A\rrbracket^{\mathcal{M}}_{d}=\mathcal{W}$, or $d\notin
A^{\mathcal{I}_{w}}$ and $d\notin A^{\mathcal{I}_{v}}$, hence $\llbracket
A\rrbracket^{\mathcal{M}}_{d}=\emptyset$.

We now show the inductive cases. For $C=\lnot D,D\sqcap E$, the proof is
immediate by applying the induction hypothesis.

For $C=\exists r.D$, the proof follows by the application of the induction
hypothesis and the fact that $r^{\mathcal{I}_{w}}=r^{\mathcal{I}_{v}}$.

For $C=\Box_{i}D$, by induction hypothesis $\llbracket
D\rrbracket^{\mathcal{M}}_{d}=\emptyset$ or $\llbracket
D\rrbracket^{\mathcal{M}}_{d}=\mathcal{W}$. In the first case, $\llbracket
D\rrbracket^{\mathcal{M}}_{d}\notin\mathcal{N}_{i}(w)$ and $\llbracket
D\rrbracket^{\mathcal{M}}_{d}\notin\mathcal{N}_{i}(v)$, hence
$w\notin\llbracket\Box_{i}D\rrbracket^{\mathcal{M}}_{d}$ and
$v\notin\llbracket\Box_{i}D\rrbracket^{\mathcal{M}}_{d}$, thus
$\llbracket\Box_{i}D\rrbracket^{\mathcal{M}}_{d}=\emptyset$. In the second
case, $\llbracket D\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)$ and
$\llbracket D\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(v)$, hence
$w\in\llbracket\Box_{i}D\rrbracket^{\mathcal{M}}_{d}$ and
$v\in\llbracket\Box_{i}D\rrbracket^{\mathcal{M}}_{d}$, thus
$\llbracket\Box_{i}D\rrbracket^{\mathcal{M}}_{d}=\mathcal{W}$. ∎

Now, given a concept $C$, suppose that $d\in(\Box_{i}C)^{\mathcal{I}_{w}}$,
that is, $\llbracket C\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)$. By
the claim, $\llbracket C\rrbracket^{\mathcal{M}}_{d}=\emptyset$ or $\llbracket
C\rrbracket^{\mathcal{M}}_{d}=\mathcal{W}$. Since
$\emptyset\notin\mathcal{N}_{i}(w)$, we have that $\llbracket
C\rrbracket^{\mathcal{M}}_{d}=\mathcal{W}$, and thus $w\in\llbracket
C\rrbracket^{\mathcal{M}}_{d}$. This means that $d\in C^{\mathcal{I}_{w}}$. By
the same argument, we can show that $d\in(\Box_{i}C)^{\mathcal{I}_{v}}$
implies $d\in C^{\mathcal{I}_{v}}$. Therefore
$\mathcal{M}\models\Box_{i}C\sqsubseteq C$. Similarly we can prove that
$\mathcal{M}\models\Box_{i}\varphi\to\varphi$, for any formula $\varphi$.

_Point 2._ Let $F=(W,\\{R_{i}\\}_{i\in J})$ be a relational frame, and let
$M=(F,\Delta,I)$ be a relational model based on $F$.

($\mathbf{E}$-principle) Follows directly from the ($\mathbf{M}$-principle)
case below.

($\mathbf{M}$-principle) Assume $C\sqsubseteq D$ valid in $M$. Then
$C^{I_{w}}\subseteq D^{I_{w}}$, for all $w\in W$. Now, suppose that
$d\in(\Box_{i}C)^{I_{w}}$, for $d\in\Delta$ and $w\in W$. For all $v\in W$,
$wR_{i}v$ implies $d\in C^{I_{v}}$, hence $d\in D^{I_{v}}$. Therefore,
$d\in(\Box_{i}D)^{I_{w}}$.

($\mathbf{C}$-principle) Assume $d\in(\Box_{i}C\sqcap\Box_{i}D)^{I_{w}}$, that
is, $d\in(\Box_{i}C)^{I_{w}}$ and $d\in(\Box_{i}D)^{I_{w}}$. Then, for all
$v\in W$, $wR_{i}v$ implies $d\in C^{I_{v}}$ and $d\in D^{I_{v}}$, that is
$d\in(C\sqcap D)^{I_{v}}$. Therefore, $d\in(\Box_{i}(C\sqcap D))^{I_{w}}$.

($\mathbf{N}$-principle) Assume $\top\sqsubseteq C$ valid in $M$. Then, for
all $w\in W$, $C^{I_{w}}=\Delta$. Thus, for all $d\in\Delta$ and all $v\in W$,
$wR_{i}v$ implies $d\in C^{I_{v}}$. In conclusion, for all $d\in\Delta$,
$d\in(\Box_{i}C)^{I_{w}}$.

In conclusion, the $\mathbf{E}$-, $\mathbf{M}$-, $\mathbf{C}$-, and
$\mathbf{N}$-principle hold in $M$, and hence in $F$.

($\mathbf{D}$-principle and $\mathbf{P}$-principle are equivalent) It is easy
to see that both the $\mathbf{D}$\- and the $\mathbf{P}$-principle hold if and
only if $R_{i}$ is serial, for all $i\in J$ (that is, for all $w\in W$, there
is $v\in W$ such that $wR_{i}v$).

($\mathbf{Q}$-principle does not hold) The $\mathbf{Q}$-principle is
incompatible with the $\mathbf{N}$-principle, whcih holds in relational
models. Indeed, if both principles hold in the relational model $M$, then
$M\models\top\sqsubseteq\Box_{i}\top\sqcap\lnot\Box_{i}\top$, against the fact
that $\smash{\mathcal{ALC}}$ domains are non-empty. ∎

##  Appendix 0.C Proofs for Section 3

Here is an $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm example
application.

######  Example 1.

Consider the formula

$\varphi=\lnot(\mathbb{D}_{c}\exists\mathsf{req}.(\mathsf{Prod}\sqcap\mathsf{InCatal})\sqsubseteq\mathbb{D}_{c}(\mathsf{Conf}\sqcup\lnot\mathsf{Conf})),$

related to the discussion in Section 0.A. We recall that the formula is
unsatisfiable in models validating the $\mathbf{M}$-condition, and it is
satisfiable otherwise. Here we show that the algorithm provides different
answers depending whether $\mathbf{M}\in\mathit{L}$. First, we rewrite
$\varphi$ in NNF, using $\widehat{\mathbb{D}}_{c}$ as the dual operator of
$\mathbb{D}_{c}$, thus obtaining

$\lnot(\top\sqsubseteq\widehat{\mathbb{D}}_{c}\forall\mathsf{req}.(\lnot\mathsf{Prod}\sqcup\lnot\mathsf{InCatal})\sqcup\mathbb{D}_{c}(\mathsf{Conf}\sqcup\lnot\mathsf{Conf})).$

We then consider the following applications of the tableau algorithm. In the
first case we assume $\mathbf{M}\in\mathit{L}$:

$0:\varphi$

$0:\mathbb{D}_{c}\exists\mathsf{req}.(\mathsf{Prod}\sqcap\mathsf{InCatal})\sqcap\widehat{\mathbb{D}}_{c}(\lnot\mathsf{Conf}\sqcap\mathsf{Conf})(v)$
($\mathsf{R}_{\not\sqsubseteq}$)

$1:\exists\mathsf{req}.(\mathsf{Prod}\sqcap\mathsf{InCatal})(v)$
($\mathsf{R}_{\mathit{L}}$)

$1:\lnot\mathsf{Conf}\sqcap\mathsf{Conf}(v)$ ($\mathsf{R}_{\mathit{L}}$)

$1:\lnot\mathsf{Conf}(v)$ ($\mathsf{R}_{\sqcap}$)

$1:\mathsf{Conf}(v)$ ($\mathsf{R}_{\sqcap}$)

The completion set constructed by the application of the
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm contains a clash,
hence the algorithm returns $\mathsf{unsatisfiable}$ on input $\varphi$. Now,
assume $\mathbf{M}\notin\mathit{L}$:

$0:\varphi$

$0:\mathbb{D}_{c}\exists\mathsf{req}.(\mathsf{Prod}\sqcap\mathsf{InCatal})\sqcap\widehat{\mathbb{D}}_{c}(\lnot\mathsf{Conf}\sqcap\mathsf{Conf})(v)$
($\mathsf{R}_{\not\sqsubseteq}$)

$1:\forall\mathsf{req}.(\lnot\mathsf{Prod}\sqcup\lnot\mathsf{InCatal})(v)$
($\mathsf{R}_{\mathit{L}}$)

$1:\mathsf{Conf}\sqcup\lnot\mathsf{Conf}(v)$ ($\mathsf{R}_{\mathit{L}}$)

$1:\mathsf{Conf}(v)$ ($\mathsf{R}_{\sqcup}$)

The completion set is clash-free and
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete, hence the algorithm returns
$\mathsf{satisfiable}$ on input $\varphi$. Note that the latter applications
of $\mathsf{R}_{\mathit{L}}$ are only possible if
$\mathbf{M}\notin\mathit{L}$.

In this appendix we prove termination, soundness, and completeness of the
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm. We define the
_weight_ $|C|$ of a concept $C$ in NNF as follows: $|A|=|\lnot A|=0$;
$|\exists r.D|=|\forall r.D|=|\Box_{i}D|=|\Diamond_{i}D|=|D|+1$; $|D\sqcap
E|=|D\sqcup E|=|D|+|E|+1$. The _weight $|\varphi|$_ of a formula $\varphi$ in
NNF is defined as: $|C(a)|=|r(a,b)|=|\lnot r(a,b)|=|(C\sqsubseteq
D)|=|\lnot(C\sqsubseteq D)|=0$; $|\Box_{i}\psi|=|\Diamond_{i}\psi|=|\psi|+1$;
$|\psi\land\chi|=|\psi\lor\chi|=|\psi|+|\chi|+1$. Observe that, for a concept
or formula $\gamma$, we have that $|\gamma|=|\dot{\lnot}\gamma|$.

######  Theorem 0.C.1 (Termination).

The $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm for $\varphi$
terminates after at most $2^{p(|\mathsf{Fg}(\varphi)|)}$ steps, where $p$ is a
polynomial function.

###### Proof.

We first require the following claims.

######  Claim 2.

Let $\mathcal{T}$ be a completion set obtained by applying the
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm for $\varphi$. For
each $n\in\mathsf{L}_{\mathcal{T}}$, the number of $n$-labelled constraints
for $\varphi$ in $\mathcal{T}$ does not exceed
$2^{q(|\mathsf{Fg}(\varphi)|)}$, where $q$ is a polynomial function.

###### Proof of Claim.

We remark that, for each $S_{n}\subseteq\mathcal{T}$, the
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableaux algorithm behaves exactly
like a standard (non-modal) $\smash{\mathcal{ALC}}$ tableaux algorithm (cf.
e.g. [17, Theorem 15.4]), except possibly for the additional rule
$\mathsf{R}_{\mathit{L}\mathbf{T}}$ which introduces at most
$|\mathsf{Fg}(\varphi)|$ $n$-labelled contraints. ∎

######  Claim 3.

Let $\mathcal{T}$ be a completion set obtained by applying the
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm for $\varphi$. Then
$|\mathsf{L}_{\mathcal{T}}|\leq r(|\mathsf{Fg}(\varphi)|)$ if
$\mathbf{C}\notin\mathit{L}$, and $|\mathsf{L}_{\mathcal{T}}|\leq
2^{r^{\prime}(|\mathsf{Fg}(\varphi)|)}$ if $\mathbf{C}\in\mathit{L}$, for some
for some polynomial functions $r$ and $r^{\prime}$.

###### Proof of Claim.

Labels $n$ are generated in $\mathcal{T}$ by means of the application of the
rules $\mathsf{R}_{\mathit{L}}$, $\mathsf{R}_{\mathit{L}\mathbf{N}}$,
$\mathsf{R}_{\mathit{L}\mathbf{P}}$, $\mathsf{R}_{\mathit{L}\mathbf{Q}}$,
$\mathsf{R}_{\mathit{L}\mathbf{D}}$. If $\mathbf{C}\notin\mathit{L}$, these
rules are applied to either one or two $n$-labelled contraints, while if
$\mathbf{C}\in\mathit{L}$, they are applied to $k$, $k+1$ or $k+h$
$n$-labelled contraints. By the application conditions of the rules, each such
combination of constraints generates at most one label $m$. Therefore, the
number of labels that can be generated in $\mathcal{T}$ is bounded by the
number of possible such combinations, which is at most
$2\cdot|\mathsf{Fg}(\varphi)|^{2}+3\cdot|\mathsf{Fg}(\varphi)|$, if
$\mathbf{C}\not\in\mathit{L}$, and at most
$2^{|\mathsf{Fg}(\varphi)|}\cdot|\mathsf{Fg}(\varphi)|+|\mathsf{Fg}(\varphi)|+2^{|\mathsf{Fg}(\varphi)|+1}+2^{2|\mathsf{Fg}(\varphi)|}$,
if $\mathbf{C}\in\mathit{L}$. ∎

The theorem is then a consequence of the following observations. Given a
completion set $\mathcal{T}$ constructed by the
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm for $\varphi$, we
have by Claim 3 that the number of applications of the rules
$\mathsf{R}_{\mathit{L}}$, $\mathsf{R}_{\mathit{L}\mathbf{N}}$,
$\mathsf{R}_{\mathit{L}\mathbf{P}}$, $\mathsf{R}_{\mathit{L}\mathbf{Q}}$, and
$\mathsf{R}_{\mathit{L}\mathbf{D}}$ is bounded by
$|\mathsf{L}_{\mathcal{T}}|$, which is at most $r(|\mathsf{Fg}(\varphi)|)$,
for $\mathit{L}$ such that $\mathbf{C}\notin\mathit{L}$, and at most
$2^{r^{\prime}(|\mathsf{Fg}(\varphi)|)}$, for $\mathit{L}$ such that
$\mathbf{C}\in\mathit{L}$, where $r$ and $r^{\prime}$ are polynomial
functions. Moreover, for a given label $n$, the number of possible
applications of the rules $\mathsf{R}_{\land}$, $\mathsf{R}_{\lor}$ and
$\mathsf{R}_{\mathit{L}\mathbf{T}}$ to constraints of the form $n:\psi$ is
linearly bounded by $\mathsf{Fg}(\varphi)$, hence there are at most
$|\mathsf{L}_{\mathcal{T}}|\cdot q^{\prime}(|\mathsf{Fg}(\varphi)|)$ such rule
applications, where $q^{\prime}$ is a polynominal function. Finally, by Claim
2, for each label $n$, the number of applications of the rules
$\mathsf{R}_{\sqcap},\mathsf{R}_{\sqcup},\mathsf{R}_{\forall},\mathsf{R}_{\exists},\mathsf{R}_{\sqsubseteq},\mathsf{R}_{\not\sqsubseteq}$
and $\mathsf{R}_{\mathit{L}\mathbf{T}}$ to constraints of the form $n:C(x)$ or
$n:r(x,y)$ is bounded by $2^{q(|\mathsf{Fg}(\varphi)|)}$, where $q$ is a
polynomial function, hence there are at most $|\mathsf{L}_{\mathcal{T}}|\cdot
2^{q(|\mathsf{Fg}(\varphi)|)}$ such rule applications. It follows that the
overall number of rule applications is bounded by
$2^{p(|\mathsf{Fg}(\varphi)|)}$ for some polynomial function $p$. ∎

We now proceed to prove that the $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$
tableau algorithm is sound.

######  Theorem 0.C.2 (Soundness).

If there exists an execution of the $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$
tableau algorithm for $\varphi$ that constructs a complete and clash-free
completion set, then $\varphi$ is $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$
satisfiable.

###### Proof.

Suppose that the $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm
for $\varphi$ constructs an $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete
and clash-free completion set $\mathcal{T}$ for $\varphi$. We define, for
$n\in\mathsf{L}_{\mathcal{T}}$, $\psi\in\mathsf{for}_{\dot{\lnot}}(\varphi)$,
$C\in\mathsf{con}_{\dot{\lnot}}(\varphi)$, and $x$ occurring in $\mathcal{T}$,

$\displaystyle\lfloor C\rfloor_{x}$
$\displaystyle=\\{n\in\mathsf{L}_{\mathcal{T}}\mid n:C(x)\in S_{n}\\},$
$\displaystyle\lceil C\rceil_{x}$
$\displaystyle=\mathsf{L}_{\mathcal{T}}\setminus\\{n\in\mathsf{L}_{\mathcal{T}}\mid
n:\dot{\lnot}C(x)\in S_{n}\\},$ $\displaystyle\lfloor\psi\rfloor$
$\displaystyle=\\{n\in\mathsf{L}_{\mathcal{T}}\mid n:\psi\in S_{n}\\},$
$\displaystyle\lceil\psi\rceil$
$\displaystyle=\mathsf{L}_{\mathcal{T}}\setminus\\{n\in\mathsf{L}_{\mathcal{T}}\mid
n:\dot{\lnot}\psi\in S_{n}\\}.$

Moreover, define $\Gamma^{x}_{n}=\\{\psi\mid n:\psi\in S_{n}\\}\cup\\{C\mid
n:C(x)\in S_{n}\\}$ and let $\gamma,\delta$ range over
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ formulas or concepts, where:
$\lfloor\gamma\rfloor_{x}=\lfloor\psi\rfloor$, if $\gamma=\psi$, and
$\lfloor\gamma\rfloor_{x}=\lfloor C\rfloor_{x}$, if $\gamma=C$; and similarly
for $\lceil\gamma\rceil_{x}$. We set $\mathcal{M}=(\mathcal{F},\mathcal{I})$,
with $\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in J})$ and
$\mathcal{I}_{n}=(\Delta_{n},\cdot^{\mathcal{I}_{n}})$, for $n\in\mathcal{W}$,
defined as follows:

  * •

$\mathcal{W}=\mathsf{L}_{\mathcal{T}}$;

  * •

for every $i\in J=\\{1,\ldots,n\\}$, we set
$\mathcal{N}_{i}\colon\mathcal{W}\rightarrow 2^{2^{\mathcal{W}}}$ such that:

$\displaystyle\mathcal{N}_{i}(n)=\big{\\{}\alpha\mid$
$\displaystyle\textnormal{\ for some \
}\Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{\mathsf{k}}\in\Gamma^{{x}_{\mathsf{k}}}_{n}\colon$
$\displaystyle\mathsf{LB}(\overline{\gamma_{\mathsf{k}}})\subseteq\alpha\subseteq\mathsf{UB}(\overline{\gamma_{\mathsf{k}}})\big{\\}}\cup\mathsf{S};$

where:

    * –

$\mathsf{LB}(\overline{\gamma_{\mathsf{k}}})=\bigcap^{\mathsf{k}}_{j=1}\lfloor\gamma_{j}\rfloor_{{{x}_{j}}}$;

    * –

$\mathsf{UB}(\overline{\gamma_{\mathsf{k}}})=\begin{cases}\mathcal{W},&\text{if
$\mathbf{M}\in L$}\\\
\bigcap^{\mathsf{k}}_{j=1}\lceil\gamma_{j}\rceil_{{{x}_{j}}},&\text{if
$\mathbf{M}\not\in L$}\end{cases};$

    * –

$\mathsf{k}\begin{cases}\geq 1,&\text{if $\mathbf{C}\in L$}\\\ =1,&\text{if
$\mathbf{C}\not\in L$}\end{cases};$

    * –

$\mathsf{S}=\begin{cases}\\{\mathcal{W}\\},&\text{if $\mathbf{N}\in L$}\\\
\emptyset,&\text{if $\mathbf{N}\not\in L$}\end{cases};$

  * •

$\Delta_{n}=\\{x\mid x\ \text{is a term occurring in}\ S_{n}\\}$;

  * •

$A^{\mathcal{I}_{n}}=\\{x\in\Delta_{n}\mid n:A(x)\in S_{n}\\}$;

  * •

$a^{\mathcal{I}_{n}}=\begin{cases}a,&\text{if $a$ occurs in $S_{n}$}\\\
\text{arbitrary},&\text{otherwise}\end{cases}$ ;

  * •

$r^{\mathcal{I}_{n}}=\\{(x,y)\in\Delta_{n}\times\Delta_{n}\mid n:r(x,y)\in
S_{n}\ \text{or}\ n:r(z,y)\in S_{n},$ for some $z$ blocking $x$ in $S_{n}\\}$.

We require the following claims.

######  Claim 4.

For $\mathbf{X}\in\\{\mathbf{M,C,N,T,P,Q,D}\\}$, if $\mathbf{X}\in\mathit{L}$,
then $\mathcal{M}$ satisfies the $X$-condition.

###### Proof of Claim.

  1. $\mathbf{M}\in\mathit{L}$.

Suppose that $\alpha\in\mathcal{N}_{i}(n)$ and
$\alpha\subseteq\beta\subseteq\mathcal{W}$. By definition, there are
$\Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{{x}_{k}}_{n}$
such that $\mathsf{LB}(\overline{\gamma_{k}})\subseteq\alpha$. Then
$\mathsf{LB}(\overline{\gamma_{k}})\subseteq\beta$, hence
$\beta\in\mathcal{N}_{i}(n)$.

  2. $\mathbf{C}\in\mathit{L}$.

Suppose that $\alpha,\beta\in\mathcal{N}_{i}(n)$. Then there are
$\Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{{x}_{k}}_{n}$
such that
$\mathsf{LB}(\overline{\gamma_{k}})\subseteq\alpha\subseteq\mathsf{UB}(\overline{\gamma_{k}})$,
and there are
$\Box_{i}\delta_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\delta_{h}\in\Gamma^{{x}_{h}}_{n}$
such that
$\mathsf{LB}(\overline{\delta_{h}})\subseteq\beta\subseteq\mathsf{UB}(\overline{\delta_{h}})$.
Then
$\mathsf{LB}(\overline{\gamma_{k}})\cap\mathsf{LB}(\overline{\delta_{h}})=\mathsf{LB}(\overline{\gamma_{k},\delta_{h}})\subseteq\alpha\cap\beta\subseteq\mathsf{UB}(\overline{\gamma_{k}})\cap\mathsf{UB}(\overline{\delta_{h}})=\mathsf{UB}(\overline{\gamma_{k},\delta_{h}})$,
which implies $\alpha\cap\beta\in\mathcal{N}_{i}(n)$.

  3. $\mathbf{N}\in\mathit{L}$.

By construction, $\mathcal{W}\in\mathcal{N}_{i}(n)$ for all $n\in\mathcal{W}$.

  4. $\mathbf{P}\in\mathit{L}$.

Suppose that $\alpha\in\mathcal{N}_{i}(n)$. Then there are
$\Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{{x}_{k}}_{n}$
such that
$\mathsf{LB}(\overline{\gamma_{k}})\subseteq\alpha\subseteq\mathsf{UB}(\overline{\gamma_{k}})$.
Since $\mathcal{T}$ is $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete, by
the rule $\mathsf{R}_{\mathit{L}\mathbf{P}}$, there is $m$ such that
$m:\gamma_{j}\in\mathcal{T}$ for all $1\leq j\leq k$, that is
$m\in\mathsf{LB}(\overline{\gamma_{k}})$. Then $\alpha\not=\emptyset$.

  5. $\mathbf{Q}\in\mathit{L}$.

Suppose that $\alpha\in\mathcal{N}_{i}(n)$. Then there are
$\Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{{x}_{k}}_{n}$
such that
$\mathsf{LB}(\overline{\gamma_{k}})\subseteq\alpha\subseteq\mathsf{UB}(\overline{\gamma_{k}})$.
Since $\mathcal{T}$ is $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete, by
the rule $\mathsf{R}_{\mathit{L}\mathbf{Q}}$, there is $m$ such that
$m:\dot{\lnot}\gamma_{j}\in\mathcal{T}$ for some $1\leq j\leq k$, that is
$m\in\mathcal{W}$ and $m\notin\lceil\gamma_{j}\rceil_{{{x}_{j}}}$, hence
$m\notin\mathsf{UB}(\overline{\gamma_{k}})$. Then $\alpha\not=\mathcal{W}$.

  6. $\mathbf{D}\in\mathit{L}$.

Suppose that $\alpha,\beta\in\mathcal{N}_{i}(n)$. Then there are
$\Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{{x}_{k}}_{n}$
such that
$\mathsf{LB}(\overline{\gamma_{k}})\subseteq\alpha\subseteq\mathsf{UB}(\overline{\gamma_{k}})$,
and there are
$\Box_{i}\delta_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\delta_{h}\in\Gamma^{{x}_{h}}_{n}$
such that
$\mathsf{LB}(\overline{\delta_{h}})\subseteq\beta\subseteq\mathsf{UB}(\overline{\delta_{h}})$.
Since $\mathcal{T}$ is $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete, b
the rule $\mathsf{R}_{\mathit{L}\mathbf{D}}$, there is $m$ such that
$m:\gamma_{j},m:\delta_{\ell}\in\mathcal{T}$ for all $1\leq j\leq k$,
$1\leq\ell\leq h$; or
$m:\dot{\lnot}\gamma_{j},m:\dot{\lnot}\delta_{\ell}\in\mathcal{T}$ for some
$1\leq j\leq k$, $1\leq\ell\leq h$. In the first case,
$m\in\mathsf{LB}(\overline{\gamma_{k}})\cap\mathsf{LB}(\overline{\delta_{h}})$,
hence $m\in\alpha\cap\beta$. In the second case,
$m\in(\mathcal{W}\setminus\mathsf{UB}(\overline{\gamma_{k}}))\cap(\mathcal{W}\setminus\mathsf{UB}(\overline{\delta_{h}}))$,
hence $m\in(\mathcal{W}\setminus\alpha)\cap(\mathcal{W}\setminus\beta)$. In
either case $\beta\neq\mathcal{W}\setminus\alpha$.

  7. $\mathbf{T}\in\mathit{L}$.

Suppose that $\alpha\in\mathcal{N}_{i}(n)$. Then there are
$\Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{{x}_{k}}_{n}$
such that
$\mathsf{LB}(\overline{\gamma_{k}})\subseteq\alpha\subseteq\mathsf{UB}(\overline{\gamma_{k}})$.
Since $\mathcal{T}$ is $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete, by
the rule $\mathsf{R}_{\mathit{L}\mathbf{T}}$, $n:\gamma_{j}\in\mathcal{T}$ for
all $1\leq j\leq k$, then $n\in\mathsf{LB}(\overline{\gamma_{k}})$, thus
$n\in\alpha$.∎

######  Claim 5.

For every $n\in\mathcal{W}$, $C\in\mathsf{con}_{\dot{\lnot}}(\varphi)$, and
$x\in\Delta_{n}$: if $n:C(x)\in S_{n}$, then $x\in C^{\mathcal{I}_{n}}$.

###### Proof of Claim.

We show the claim by induction on the weight of $C$ (in NNF). The base case of
$C=A$ comes immediately from the definitions. For the base case of $C=\lnot
A$, suppose that $n:\lnot A(x)\in S_{n}$. Since $\mathcal{T}$ is clash-free,
we have that $n:A(x)\not\in S_{n}$, and thus $x\not\in A^{\mathcal{I}_{n}}$ by
definition of $A^{\mathcal{I}_{n}}$, meaning $x\in(\lnot
A)^{\mathcal{I}_{n}}$. The inductive cases of $C=D\sqcap E$ and $C=D\sqcup E$
come from the fact that $S_{n}$ is closed under $\mathsf{R}_{\sqcap}$ and
$\mathsf{R}_{\sqcup}$, respectively, and straightforward applications of the
inductive hypothesis. We show the remaining cases (cf. also [17, Claim 15.2]).

  1. $C=\exists r.D$.

Let $n:\exists r.D(x)\in S_{n}$, meaning that $\exists r.D\in\Gamma^{x}_{n}$.
We distinguish two cases.

     * $(i)$

$x$ is not blocked by any variable in $S_{n}$. Since $S_{n}$ is closed under
$\mathsf{R}_{\exists}$, there exists $y$ occurring in $S_{n}$ such that
$n:r(x,y)\in S_{n}$ and $n:D(y)\in S_{n}$. Thus, by definition, $(x,y)\in
r^{\mathcal{I}_{n}}$ and $n:D(y)\in S_{n}$. By inductive hypothesis, we obtain
that $x\in(\exists r.D)^{\mathcal{I}_{n}}$.

     * $(ii)$

$x$ is blocked by a variable in $S_{n}$, implying that there exists a
$<$-minimal (since $<$ is a well-ordering) $y$ occurring in $S_{n}$ such that
$y<x$ and $\\{E\mid n:E(x)\in S_{n}\\}\subseteq\\{E\mid n:E(y)\in S_{n}\\}$.
In turn, this implies that $y$ is not blocked by any other variable $z$ in
$S_{n}$ (for otherwise $z$ would block $x$, with $z<y$, against the fact that
$y$ is $<$-minimal). By reasoning as in the case above, since $y$ is not
blocked and $S_{n}$ is closed under $\mathsf{R}_{\exists}$, we have a variable
$z$ occurring in $S_{n}$ such that $n:r(y,z)\in S_{n}$ and $n:D(z)\in S_{n}$.
Since $y$ blocks $x$, by definition we have that $(x,z)\in
r^{\mathcal{I}_{n}}$, and by inductive hypothesis we get from $n:D(z)$ that
$z\in D^{\mathcal{I}_{n}}$. Thus, $x\in(\exists r.D)^{\mathcal{I}_{n}}$.

  2. $C=\forall r.D$.

Let $n:\forall r.D(x)\in S_{n}$, meaning that $\forall r.D\in\Gamma^{x}_{n}$,
and suppose that $(x,y)\in r^{\mathcal{I}_{n}}$. By definition, either
$n:r(x,y)\in S_{n}$ or $n:r(z,y)\in S_{n}$, for some $z$ blocking $x$ in
$S_{n}$. In the former case, since $S_{n}$ is closed under
$\mathsf{R}_{\forall}$, we get that $n:D(y)\in S_{n}$. In the latter case,
since $z$ blocks $x$ in $S_{n}$, we obtain $n:\forall r.D(z)\in S_{n}$; again,
since $S_{n}$ is closed under $\mathsf{R}_{\forall}$, this implies that
$n:D(y)\in S_{n}$. Hence, in both cases, we have $n:D(y)\in S_{n}$. By
inductive hypothesis, this means that $y\in D^{\mathcal{I}_{n}}$. Since $y$
was arbitrary, we conclude that $x\in(\forall r.D)^{\mathcal{I}_{n}}$.

  3. $C=\Box_{i}D$.

Let $n:\Box_{i}D(x)\in S_{n}$, meaning that $\Box_{i}D\in\Gamma^{x}_{n}$. We
have by inductive hypothesis that $\lfloor D\rfloor_{x}=\\{n\in\mathcal{W}\mid
n:D(x)\in S_{n}\\}\subseteq\\{n\in\mathcal{W}\mid x\in
D^{\mathcal{I}_{n}}\\}=\llbracket D\rrbracket^{\mathcal{M}}_{x}$. By inductive
hypothesis (since $|\dot{\lnot}D|=|D|$), we also have that
$\\{n\in\mathcal{W}\mid n:\dot{\lnot}D(x)\in
S_{n}\\}\subseteq\\{n\in\mathcal{W}\mid
x\in(\dot{\lnot}D)^{\mathcal{I}_{n}}\\}=\llbracket\dot{\lnot}D\rrbracket^{\mathcal{M}}_{x}=\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}$. Hence, $\llbracket
D\rrbracket^{\mathcal{M}}_{x}\subseteq\mathcal{W}\setminus\\{w\in\mathcal{W}\mid
n:\dot{\lnot}D(x)\in S_{n}\\}=\lceil D\rceil_{x}$. In conclusion, we have
$\Box_{i}D\in\Gamma^{x}_{n}$ such that $\lfloor
D\rfloor_{x}\subseteq\llbracket D\rrbracket^{\mathcal{M}}_{x}\subseteq\lceil
D\rceil_{x}$. Thus, by definition, $\llbracket
D\rrbracket^{\mathcal{M}}_{x}\in\mathcal{N}_{i}(n)$, as required. (If
$\mathbf{M}\in\mathit{L}$, $\lfloor D\rfloor_{x}\subseteq\llbracket
D\rrbracket^{\mathcal{M}}_{x}$, and by definition this means $\llbracket
D\rrbracket^{\mathcal{M}}_{x}\in\mathcal{N}_{i}(n)$, as required.)

  4. $C=\Diamond_{i}D$.

Let $n:\Diamond_{i}D(x)\in S_{n}$. We distinguish two cases.

     * $(i)$

There exists no $\Box_{i}\gamma\in\Gamma^{y}_{n}$. Then if
$\mathbf{N}\notin\mathit{L}$, $\mathcal{N}_{i}(n)=\emptyset$, thus
$\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}\not\in\mathcal{N}_{i}(n)$, meaning that
$x\in(\Diamond_{i}D)^{\mathcal{I}_{n}}$. If instead $\mathbf{N}\in\mathit{L}$,
then $\mathcal{N}_{i}(n)=\mathcal{W}$. Moreover, since $\mathcal{T}$ is
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete, by the rule
$\mathsf{R}_{\mathit{L}\mathbf{N}}$, there is $m$ such that $m:D(x)\in S_{m}$.
By inductive hypothesis, this implies $x\in D^{\mathcal{I}_{m}}$, that is,
$\llbracket D\rrbracket^{\mathcal{M}}_{x}\neq\emptyset$. Then we have
$\mathcal{W}\setminus\llbracket D\rrbracket^{\mathcal{M}}_{x}\neq\mathcal{W}$,
and thus $\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}\not\in\mathcal{N}_{i}(n)$. Hence,
$x\in(\Diamond_{i}D)^{\mathcal{I}_{n}}$.

     * $(ii)$

There exist
$\Box_{i}\gamma_{1}\in\Gamma^{y_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{y_{k}}_{n}$.
Since $\mathcal{T}$ is $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-complete,
there exists $m\in\mathcal{W}$ such that:
$\gamma_{1}\in\Gamma^{y_{1}}_{m},\ldots,\gamma_{k}\in\Gamma^{y_{k}}_{m}$ and
$D\in\Gamma^{x}_{m}$; or $\dot{\lnot}\gamma_{j}\in\Gamma^{y_{j}}_{m}$ and
$\dot{\lnot}D\in\Gamma^{x}_{m}$, for some $j\leq k$. By inductive hypothesis,
the previous step implies that there exists $m\in\mathcal{W}$ such that:
$\gamma_{1}\in\Gamma^{y_{1}}_{m},\ldots,\gamma_{k}\in\Gamma^{y_{k}}_{m}$ and
$x\in D^{\mathcal{I}_{m}}$; or $\dot{\lnot}\gamma_{j}\in\Gamma^{y_{j}}_{m}$
and $x\in\dot{\lnot}D^{\mathcal{I}_{m}}$, for some $j\leq k$. Thus
$\bigcap_{j=1}^{k}\lfloor\gamma_{j}\rfloor_{y_{j}}\not\subseteq\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}$; or $\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}\not\subseteq\bigcap_{j=1}^{k}\lceil\gamma_{l}\rceil_{y_{l}}$.
Since this holds for every
$\Box_{i}\gamma_{1}\in\Gamma^{y_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{y_{k}}_{n}$,
we conclude that $\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}\not\in\mathcal{N}_{i}(n)$, i.e.,
$x\in(\Diamond_{i}D)^{\mathcal{I}_{n}}$, as required. (If
$\mathbf{M}\in\mathit{L}$, there exists $m\in\mathcal{W}$ such that
$\gamma_{1}\in\Gamma^{y_{1}}_{m},\ldots,\gamma_{k}\in\Gamma^{y_{k}}_{m}$ and
$D\in\Gamma^{x}_{m}$, thus $x\in D^{\mathcal{I}_{m}}$, hence
$\bigcap_{j=1}^{k}\lfloor\gamma_{j}\rfloor_{y_{j}}\not\subseteq\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}$, therefore $\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}\not\in\mathcal{N}_{i}(n)$.)∎

######  Claim 6.

For every $n\in\mathcal{W}$ and $\psi\in\mathsf{con}_{\dot{\lnot}}(\varphi)$:
if $n:\psi\in S_{n}$, then $\mathcal{M},n\models\psi$.

###### Proof of Claim.

We prove the claim by induction on the weight of $\varphi$ (in NNF).

  1. $\psi=C(a)$.

Let $n:C(a)\in S_{n}$. By definition of $\mathcal{I}_{n}$ and Claim 5, we have
that $a^{\mathcal{I}_{n}}\in C^{\mathcal{I}_{n}}$, hence $\mathcal{M},n\models
C(a)$. (For $\psi=\lnot C(a)$, recall that $\lnot C(a)$ is equivalent to
$D(a)$ with $D=\lnot C$).

  2. $\psi=r(a,b)$.

Let $n:r(a,b)\in S_{n}$. By definition of $\mathcal{I}_{n}$, this implies
$(a^{\mathcal{I}_{n}},b^{\mathcal{I}_{n}})\in r^{\mathcal{I}_{n}}$, hence
$\mathcal{M},n\models r(a,b)$.

  3. $\psi=\lnot r(a,b)$.

Let $n:\lnot r(a,b)\in S_{n}$. Since $\mathbf{T}$ is clash-free, we have that
$n:r(a,b)\not\in S_{n}$. Thus, by definition of $\mathcal{I}_{n}$ we have
$(a^{\mathcal{I}_{n}},b^{\mathcal{I}_{n}})\not\in r^{\mathcal{I}_{n}}$,
meaning that $\mathcal{M},n\not\models r(a,b)$.

  4. $\psi=(\top\sqsubseteq C)$.

Let $n:\top\sqsubseteq C\in S_{n}$ and let $x\in\Delta_{n}$. Since $S_{n}$ is
closed under $(\mathsf{R}_{\sqsubseteq})$ and $x$ occurs in $S_{n}$, we have
that $n:C(x)\in S_{n}$. By Claim 5, we have that $x\in C^{\mathcal{I}_{n}}$.
Given that $x$ is arbitrary, we conclude that
$\mathcal{M},n\models\top\sqsubseteq C$.

  5. $\psi=\lnot(\top\sqsubseteq C)$.

Let $n:\lnot(\top\sqsubseteq C)\in S_{n}$. Since $S_{n}$ is closed under
$(\mathsf{R}_{\not\sqsubseteq})$, there exists $x$ occurring in $S_{n}$ such
that $n:\dot{\lnot}C(x)\in S_{n}$. By Claim 5, we obtain that
$x\in(\dot{\lnot}C)^{\mathcal{I}_{n}}$, for some $x\in\Delta_{w}$. Hence,
$\mathcal{M},n\models\lnot(\top\sqsubseteq C)$.

The inductive cases of $\psi=\chi\land\vartheta$ and $\psi=\chi\lor\vartheta$
follow from the definitions and straighforward applications of the inductive
hypothesis. Moreover the inductive cases of $\psi=\Box_{i}\chi$ and
$\psi=\Diamond_{i}\chi$ can be proved analogously to Claim 5. ∎

Since, by definition, we have $0:\varphi\in S_{0}\subseteq\mathbf{T}$, thanks
to Claim 6 we obtain $\mathcal{M},0\models\varphi$. Moreover, by Claim 4,
$\mathcal{M}$ is a $\mathit{L}^{n}$ model. Therefore $\varphi$ is
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ satisfiable. ∎

We finally show completeness of the $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$
tableau algorithm.

######  Theorem 0.C.3 (Completeness).

If $\varphi$ is $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$ satisfiable, then
there exists an execution of the $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$
tableau algorithm for $\varphi$ that constructs a complete and clash-free
completion set.

###### Proof.

In the proof we assume $\mathbf{C}\in\mathit{L}$, for the case
$\mathbf{C}\notin\mathit{L}$ consider $k=h=1$. Let
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ be an
$\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-model satisfying $\varphi$, with
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}\\}_{i\in J})$, i.e.,
$\mathcal{M},w_{\varphi}\models\varphi$, for some $w_{\varphi}\in\mathcal{W}$.
We require the following definitions and technical results. First, we let
$\gamma,\delta$ (possibly indexed) range over
$\smash{\mathcal{ML}^{n}_{\mathcal{ALC}}}$ concepts and formulas, with
$\llbracket\gamma\rrbracket^{\mathcal{M}}_{d}=\llbracket\psi\rrbracket^{\mathcal{M}}$,
if $\gamma=\psi$, and $\llbracket\gamma\rrbracket^{\mathcal{M}}_{d}=\llbracket
C\rrbracket^{\mathcal{M}}_{d}$, if $\gamma=C$. Then, for $w\in\mathcal{W}$ and
$d\in\bigcup_{v\in\mathcal{W}}\Delta_{v}$, define
$\Phi^{d}_{w}=\\{\psi\in\mathsf{for}_{\dot{\lnot}}(\varphi)\mid\mathcal{M},w\models\psi\\}\cup\\{C\in\mathsf{con}_{\dot{\lnot}}(\varphi)\mid
d\in C^{\mathcal{I}_{w}}\\}$. Observe that, if $C\in\Phi^{d}_{w}$, then
$d\in\Delta_{w}$. Moreover, given a completion set $\mathcal{T}$ for $\varphi$
and $S_{n}\subseteq\mathcal{T}$, let $\Gamma^{x}_{n}=\\{\psi\mid n:\psi\in
S_{n}\\}\cup\\{C\mid n:C(x)\in S_{n}\\}$. We say that a completion set
$\mathcal{T}$ for $\varphi$ is _$\mathcal{M}$ -compatible_ if there exists a
function $\pi$ from $\mathsf{L}_{\mathcal{T}}$ to $\mathcal{W}$, and, for
every $n\in\mathsf{L}_{\mathcal{T}}$, there exists a function $\pi_{n}$ from
the set of terms occurring in $S_{n}$ to $\Delta_{\pi(n)}$, such that
$\gamma\in\Gamma^{x}_{n}$ implies $\gamma\in\Phi^{\pi_{n}(x)}_{\pi(n)}$. We
require the following claim.

######  Claim 7.

If a completion set $\mathcal{T}$ for $\varphi$ is $\mathcal{M}$-compatible
and $\mathcal{M}$ is an $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-model, then
for every $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-rule $\mathsf{R}$
applicable to $\mathcal{T}$, there exists a completion set
$\mathcal{T}^{\prime}$ obtained from $\mathcal{T}$ by an application of
$\mathsf{R}$ such that $\mathcal{T}^{\prime}$ is $\mathcal{M}$-compatible.

###### Proof.

Given an $\mathcal{M}$-compatible completion set $\mathcal{T}$ for $\varphi$
and a label $n\in\mathsf{L}_{\mathcal{T}}$, let $\pi$ and $\pi_{n}$ be the
functions provided by the definition of $\mathcal{M}$-compatibility. We need
to consider each $\mathit{L}^{n}_{\smash{\mathcal{ALC}}}$-rule $\mathsf{R}$.
For
$\mathsf{R}\in\\{\mathsf{R}_{\land},\mathsf{R}_{\lor},\mathsf{R}_{\sqcap},\mathsf{R}_{\sqcup},\mathsf{R}_{\forall},\mathsf{R}_{\exists},\mathsf{R}_{\sqsubseteq},\mathsf{R}_{\not\sqsubseteq}\\}$,
we proceed similarly to [17, Claim 15.14]. Here we consider the modal rules.

  1. ($\mathsf{R}_{\mathit{L}}$)

Suppose that $\mathsf{R}_{\mathit{L}}$ is applicable to $\mathcal{T}$. Then
there are
$\Box_{i}\gamma_{1}\in\Gamma^{x_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{x_{k}}_{n},\Diamond_{i}\delta\in\Gamma^{y}_{n}$.
Since $\mathcal{T}$ is $\mathcal{M}$-compatible, we have that
$\Box_{i}\gamma_{1}\in\Phi^{\pi_{n}(x_{1})}_{\pi(n)},\ldots,\Box_{i}\gamma_{k}\in\Phi^{\pi_{n}(x_{k})}_{\pi(n)}$
and $\Diamond_{i}\delta\in\Phi^{\pi_{n}(y)}_{\pi(n)}$, meaning that
$\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\in\mathcal{N}_{i}(\pi(n))$,
for $j=1,\ldots,k$, hence by the $C$-condition
$\bigcap_{j=1}^{k}\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\in\mathcal{N}_{i}(\pi(n))$,
and
$\mathcal{W}\setminus\llbracket\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(\pi(n))$,
i.e.,
$\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(\pi(n))$.
Then
$\bigcap_{j=1}^{k}\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\neq\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}$
(if $\mathbf{M}\in\mathit{L}$,
$\bigcap_{j=1}^{k}\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\not\subseteq\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}$).
It follows that there exists $v\in\mathcal{W}$ such that
$\gamma_{1}\in\Phi^{\pi_{n}(x_{1})}_{v},\ldots,\gamma_{k}\in\Phi^{\pi_{n}(x_{k})}_{v}$
and $\delta\in\Phi^{\pi_{n}(y)}_{v}$; or
$\dot{\lnot}\gamma_{j}\in\Phi^{\pi_{n}(x_{j})}_{v}$ and
$\dot{\lnot}\delta\in\Phi^{\pi_{n}(y)}_{v}$, for some $j\leq k$. Then by
applying the rule $\mathsf{R}_{\mathit{L}}$ accordingly, we expand
$\mathcal{T}$ to $\mathcal{T}^{\prime}$ with
$m:\gamma_{1},\ldots,m:\gamma_{k},m:\delta$, or with
$m:\dot{\lnot}\gamma_{j},m:\dot{\lnot}\delta$, for some $j\leq k$, for some
$m$ satisfying the application condition of $\mathsf{R}_{\mathit{L}}$. Since
$m$ is fresh, we can extend $\pi$ with $\pi(m)=v$, and $\pi_{m}$ with
$\pi_{m}(x_{1})=\pi_{n}(x_{1})$, …, $\pi_{m}(x_{k})=\pi_{n}(x_{k})$,
$\pi_{m}(y)=\pi_{n}(y)$, thus obtaining that $\mathcal{T}^{\prime}$ is
$\mathcal{M}$-compatible.

  2. ($\mathsf{R}_{\mathit{L}\mathbf{N}}$)

Suppose that $\mathsf{R}_{\mathit{L}\mathbf{N}}$ is applicable to
$\mathcal{T}$. Then there is $\Diamond_{i}\delta\in\Gamma^{y}_{n}$. Since
$\mathcal{T}$ is $\mathcal{M}$-compatible, we have that
$\Diamond_{i}\delta\in\Phi^{\pi_{n}(y)}_{\pi(n)}$, meaning that
$\mathcal{W}\setminus\llbracket\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(\pi(n))$.
At the same time, by the $N$-condition,
$\mathcal{W}\in\mathcal{N}_{i}(\pi(n))$, hence
$\llbracket\delta\rrbracket^{\mathcal{M}}_{e}\not=\emptyset$, that is there
exists $v\in\mathcal{W}$ such that $\delta\in\Phi^{\pi_{n}(y)}_{v}$. Then we
expand $\mathcal{T}$ with $m:\delta$, for some $m$ satisfying the application
condition of $\mathsf{R}_{\mathit{L}\mathbf{N}}$. Since $m$ is fresh, we can
extend $\pi$ with $\pi(m)=v$, and $\pi_{m}$ with $\pi_{m}(y)=\pi_{n}(y)$, thus
obtaining that $\mathcal{T}^{\prime}$ is $\mathcal{M}$-compatible.

  3. ($\mathsf{R}_{\mathit{L}\mathbf{P}}$)

Suppose that $\mathsf{R}_{\mathit{L}\mathbf{P}}$ is applicable to
$\mathcal{T}$. Then there are
$\Box_{i}\gamma_{1}\in\Gamma^{x_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{x_{k}}_{n}$.
Since $\mathcal{T}$ is $\mathcal{M}$-compatible, we have that
$\Box_{i}\gamma_{1}\in\Phi^{\pi_{n}(x_{1})}_{\pi(n)},\ldots,\Box_{i}\gamma_{k}\in\Phi^{\pi_{n}(x_{k})}_{\pi(n)}$,
meaning that
$\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\in\mathcal{N}_{i}(\pi(n))$,
for $j=1,\ldots,k$, hence
$\bigcap_{j=1}^{k}\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\in\mathcal{N}_{i}(\pi(n))$.
At the same time, by the $P$-condition,
$\bigcap_{j=1}^{k}\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\neq\emptyset$,
that is there exists $v\in\mathcal{W}$ such that
$\gamma_{1}\in\Phi^{\pi_{n}(x_{1})}_{v},\ldots,\gamma_{k}\in\Phi^{\pi_{n}(x_{k})}_{v}$.
Then we expand $\mathcal{T}$ with $m:\gamma_{1},\ldots,m:\gamma_{k}$, for some
$m$ satisfying the application condition of
$\mathsf{R}_{\mathit{L}\mathbf{P}}$. Since $m$ is fresh, we can extend $\pi$
with $\pi(m)=v$, and $\pi_{m}$ with $\pi_{m}(x_{1})=\pi_{n}(x_{1})$, …,
$\pi_{m}(x_{k})=\pi_{n}(x_{k})$, thus obtaining that $\mathcal{T}^{\prime}$ is
$\mathcal{M}$-compatible.

  4. ($\mathsf{R}_{\mathit{L}\mathbf{Q}}$)

Suppose that $\mathsf{R}_{\mathit{L}\mathbf{Q}}$ is applicable to
$\mathcal{T}$. Then there are
$\Box_{i}\gamma_{1}\in\Gamma^{x_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{x_{k}}_{n}$.
Since $\mathcal{T}$ is $\mathcal{M}$-compatible, we have that
$\Box_{i}\gamma_{1}\in\Phi^{\pi_{n}(x_{1})}_{\pi(n)},\ldots,\Box_{i}\gamma_{k}\in\Phi^{\pi_{n}(x_{k})}_{\pi(n)}$,
meaning that
$\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\in\mathcal{N}_{i}(\pi(n))$,
for $j=1,\ldots,k$, hence
$\bigcap_{j=1}^{k}\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\in\mathcal{N}_{i}(\pi(n))$.
At the same time, by the $Q$-condition,
$\bigcap_{j=1}^{k}\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\neq\mathcal{W}$,
that is there exists $v\in\mathcal{W}$ such that
$\gamma_{j}\notin\Phi^{\pi_{n}(x_{j})}_{v}$ for some $j\leq k$. Then by
applying $\mathsf{R}_{\mathit{L}\mathbf{Q}}$ accordingly, we expand
$\mathcal{T}$ with $m:\dot{\lnot}\gamma_{j}$, for some $m$ satisfying the
application condition of $\mathsf{R}_{\mathit{L}\mathbf{Q}}$. Since $m$ is
fresh, we can extend $\pi$ with $\pi(m)=v$, and $\pi_{m}$ with
$\pi_{m}(x_{j})=\pi_{n}(x_{j})$, thus obtaining that $\mathcal{T}^{\prime}$ is
$\mathcal{M}$-compatible.

  5. ($\mathsf{R}_{\mathit{L}\mathbf{D}}$)

Suppose that $\mathsf{R}_{\mathit{L}\mathbf{D}}$ is applicable to
$\mathcal{T}$. Then there are