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

ARQNL22: 4th International Workshop on Automated Reasoning in Quantified Non-
Classical Logics, 11 August 2022, Haifa, Israel

[orcid=0000-0002-7153-0506<EMAIL_ADDRESS>]

[orcid=0000-0001-8512-1933<EMAIL_ADDRESS>]

[orcid=0000-0002-3889-6207<EMAIL_ADDRESS>url=https://www.uib.no/en/persons/Ana.Ozaki, ]

# Reasoning in Non-normal Modal Description Logics

Tiziano Dalmonte  Andrea Mazzullo  Free University of Bozen-Bolzano  Ana Ozaki
University of Bergen, Norway

(2022)

###### Abstract

Non-normal modal logics, interpreted on neighbourhood models which generalise
the usual relational semantics, have found application in several areas, such
as epistemic, deontic, and coalitional reasoning. We present here preliminary
results on reasoning in a family of modal description logics obtained by
combining $\smash{\mathcal{ALC}}$ with non-normal modal operators. First, we
provide a framework of terminating, correct, and complete tableau algorithms
to check satisfiability of formulas in such logics with the semantics based on
varying domains. We then investigate the satisfiability problems in fragments
of these languages obtained by restricting the application of modal operators
to formulas only, and interpreted on models with constant domains, providing
tight complexity results.

###### keywords:

Non-normal modal logics Description logics Tableau algorithms

##  1 Introduction

Contexts involving epistemic and doxastic [1, 2, 3], agency-based [4, 5] and
coalitional [6, 7], as well as deontic [8, 9, 10], reasoning capabilities
populate the wide spectrum of settings where modal logics have found natural
applications. In such scenarios, modal operators can be used to represent and
reason about what agents, or groups of agents, respectively know, believe,
have the capability, or have the permission, to bring about.

The semantics of modal operators is usually given in terms of _relational
models_ , based on frames consisting of a set of possible worlds equipped with
suitable accessibility relations. However, all the modal systems interpreted
by means of this kind of semantics, known as _normal_ , validate principles
that have been considered problematic or debatable for the aforementioned
applications, leading to counterintuitive or unacceptable conclusions. Among
the unpleasant features discussed in the literature, one encounters for
instance the problem of logical omniscience [3], as well as a number of so-
called paradoxes in the representation of agents’ abilities [5] and
obligations [11, 12, 13].

To avoid the unwanted consequences of the relational semantics, several _non-
normal_ modal logics have been proposed and studied, tracing back to the
seminal works by C.I. Lewis [14], Lemmon [15], Kripke [16], Scott [17],
Montague [18], Segerberg [19], and Chellas [20]. The semantics of such systems
can be given in terms of _neighbourhood models_ , generalisations of the
relational ones that were first introduced by Scott [17] and Montague [18]. In
this setting, a frame consists of a set of worlds, each of which is associated
with a set of subsets of worlds. Since a subset of worlds can be thought as a
proposition (that is true in those worlds), this means that every world in a
neighbourhood model is assigned to a set of propositions, those considered
necessary with respect to that world. This semantics both generalises the
relational one, and avoids the drawbacks of the latter, since the modal
principles validated on relational frames that are deemed as problematic for
epistemic, coalitional or deontic applications do not hold in general on
neighbourhood models.

Non-normal modalities have been widely investigated as a way to extend
propositional logic. 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, a few works have provided completeness results
for first-order non-normal modal logics [21, 22]. In addition, non-normal
modal extensions of _description logics_ , seen as fragments of first-order
logic with a good trade-off between expressive power and computational
complexity, have been considered for knowledge representation applications
[23, 24], also in multi-agent coalitional settings [25, 26].

In this paper, we investigate satisfiability of non-normal modal extensions of
description logics. In particular, we study the logics characterised by the
class of all neighbourhood frames ($\mathbf{E}$), supplemented neighbourhood
frames ($\mathbf{M}$), neighbourhood frames closed under intersection
($\mathbf{C}$), and neighbourhood frames containing the unit ($\mathbf{N}$),
and combine them with the prototypical $\smash{\mathcal{ALC}}$ description
logic. We provide a framework of terminating, correct, and complete tableau
algorithms to check satisfiability in such logics interpreted in neighbourhood
models with _varying domains_ (in this kind of semantics, the domains of the
interpretations at each world can differ; cf. Section 2 for details). We then
investigate the satisfiability problems in fragments of these languages
obtained by restricting the application of modal operators to formulas only,
and provide complexity upper bounds with _constant domains_ (in this case the
domains of the interpretations at every world are the same). We leave
satisfiability checking procedures for non-restricted languages interpreted on
models with constant domain as open problems.

##  2 Preliminaries

In this section, we provide preliminary definitions for non-normal modal
description logics, first introducing their syntax, and then giving their
semantics based on neighbourhood models.

### Syntax

Let ${\sf N_{C}}$ and ${\sf N_{R}}$ be countably infinite and pairwise
disjoint sets of _concept names_ and _role names_ respectively. An
$\smash{\mathit{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}$, with $i\in
I=\\{1,\ldots,n\\}$, are modal operators called _boxes_. A _concept inclusion_
(_CI_) is an expression of the form $C\sqsubseteq D$, where $C,D$ are
$\smash{\mathit{ML}^{n}_{\mathcal{ALC}}}{}$ concepts. An
_$\smash{\mathit{ML}^{n}_{\mathcal{ALC}}}$ formula_ takes the form

$\varphi::=C\sqsubseteq
D\mid\neg\varphi\mid\varphi\land\varphi\mid\Box_{i}\varphi,$

where $i\in I$. We will use the following standard definitions for concepts:
$\bot:=A\sqcap\lnot A$, $\top:=\lnot\bot$; $\forall r.C:=\lnot\exists r.\lnot
C$; $(C\sqcup D):=\lnot(\lnot C\sqcap\lnot D)$;
$\Diamond_{i}C:=\lnot\Box_{i}\lnot C$ (operators $\Diamond_{i}$ are called
_diamonds_). Concepts of the form $\Box_{i}C$, $\Diamond_{i}C$ are called
_modalised concepts_. Analogous conventions also hold for formulas, for which
we set $\mathsf{true}:=(\bot\sqsubseteq\top)$.

### Semantics

A _neighbourhood frame_ , or simply _frame_ , is a pair
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in I})$, where
$\mathcal{W}$ is a non-empty set of _worlds_ and, for each $i\in
I=\\{1,\ldots,n\\}$, $\mathcal{N}_{i}\colon\mathcal{W}\rightarrow
2^{2^{\mathcal{W}}}$ is called a _neighbourhood function_. A frame is:
_supplemented_ if, for all $i\in I$, $w\in\mathcal{W}$,
$\alpha,\beta\subseteq\mathcal{W}$, $\alpha\in\mathcal{N}_{i}(w)$ and
$\alpha\subseteq\beta$ implies $\beta\in\mathcal{N}_{i}(w)$; _closed under
intersection_ if, for all $i\in I$, $w\in\mathcal{W}$,
$\alpha,\beta\subseteq\mathcal{W}$, $\alpha\in\mathcal{N}_{i}(w)$ and
$\beta\in\mathcal{N}_{i}(w)$ implies $\alpha\cap\beta\in\mathcal{N}_{i}(w)$;
and _contains the unit_ if, for all $i\in I$,
$w\in\mathcal{W},\mathcal{W}\in\mathcal{N}_{i}(w)$. An
_$\smash{\mathit{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 I})$ 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}$. An
$\smash{\mathit{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}}$.
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:

$\displaystyle(\neg D)^{\mathcal{I}_{w}}$ $\displaystyle=\Delta_{w}\setminus
D^{\mathcal{I}_{w}},$ $\displaystyle(D\sqcap E)^{\mathcal{I}_{w}}$
$\displaystyle=D^{\mathcal{I}_{w}}\cap E^{\mathcal{I}_{w}},$
$\displaystyle(\exists r.D)^{\mathcal{I}_{w}}$
$\displaystyle=\\{d\in\Delta_{w}\mid\exists e\in D^{\mathcal{I}_{w}}:(d,e)\in
r^{\mathcal{I}_{w}}\\},$ $\displaystyle(\Box_{i}D)^{\mathcal{I}_{w}}$
$\displaystyle=\\{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 $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{\mathit{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$ $\displaystyle\text{\quad
iff \quad}C^{\mathcal{I}_{w}}\subseteq D^{\mathcal{I}_{w}},$
$\displaystyle\mathcal{M},w\models\neg\psi$ $\displaystyle\text{\quad iff
\quad}\mathcal{M},w\not\models\psi,$
$\displaystyle\mathcal{M},w\models\psi\land\chi$ $\displaystyle\text{\quad iff
\quad}\mathcal{M},w\models\psi\text{ and }\mathcal{M},w\models\chi,$
$\displaystyle\mathcal{M},w\models\Box_{i}\psi$ $\displaystyle\text{\quad iff
\quad}\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 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 I})$
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.

Given a class of frames $\mathcal{C}$, by the
_$\smash{\mathit{ML}^{n}_{\mathcal{ALC}}}$ formula satisfiability problem on_
(_varying_ or _constant domain_ , respectively) _neighbourhood models based on
a frame in $\mathcal{C}$_ we mean the problem of deciding whether an
$\smash{\mathit{ML}^{n}_{\mathcal{ALC}}}$ formula is satisfied in a (varying
or constant domain, respectively) neighbourhood model based on a frame in
$\mathcal{C}$. In the following, let
$\mathsf{Log}=\\{\mathbf{E},\mathbf{M},\mathbf{C},\mathbf{N}\\}$. Given
$\mathbf{L}\in\mathsf{Log}$, the _$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$
formula satisfiability problem on_ (_varying_ or _constant domain_ ,
respectively) _neighbourhood models_ is the
$\smash{\mathit{ML}^{n}_{\mathcal{ALC}}}$ formula satisfiability problem on
(varying or constant domain, respectively) neighbourhood models based on a
frame in the class of:

  * •

all neighbourhood frames, for $\mathbf{L}=\mathbf{E}$;

  * •

supplemented neighbourhood frames, for $\mathbf{L}=\mathbf{M}$;

  * •

neighbourhood frames closed under intersection, for $\mathbf{L}=\mathbf{C}$;
and

  * •

neighbourhood frames containing the unit, for $\mathbf{L}=\mathbf{N}$.

##  3 Tableaux for Non-normal Modal Description Logics

In this section, 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 Gabbay et al. [27], while the model
construction in the soundness proof is based on the strategy of Dalmonte et
al. [28].

We require the following preliminary notions. For a concept or formula
$\gamma$, we denote by $\dot{\lnot}\gamma$ the negation of $\gamma$ put in
_negation normal form_ (_NNF_), defined as usual. Given an
$\smash{\mathit{ML}^{n}_{\mathcal{ALC}}}$ formula $\varphi$, we assume without
loss of generality that $\varphi$ is in NNF, it contains CIs only of the form
$\top\sqsubseteq C$, and every concept occurring in $\varphi$ is also in NNF.
We define the _weight_ $|C|$ of a concept $C$ in NNF as follows: $|A|=|\lnot
A|=0$; $|\exists r.D|=|\forall r.D|=|\Diamond_{i}D|=|\Box_{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\sqsubseteq D)|=|\lnot(C\sqsubseteq
D)|=0$; $\Box_{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|$. 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)\\}$ and
$\mathsf{for}_{\dot{\lnot}}(\varphi)=\mathsf{for}(\varphi)\cup\\{\dot{\lnot}\psi\mid\psi\in\mathsf{for}(\varphi)\\}$.
The set $\mathsf{rol}(\varphi)$ is the set of role names occurring in
$\varphi$. Let
$\mathsf{Fg}(\varphi)=\mathsf{for}_{\dot{\lnot}}(\varphi)\cup\mathsf{con}_{\dot{\lnot}}(\varphi)\cup\mathsf{rol}(\varphi)$.
Note that, by our assumption on the form of CIs in $\varphi$, we have
$\top\in\mathsf{con}_{\dot{\lnot}}(\varphi)$.

Moreover, let ${\sf N_{V}}$ be a countable set of _variables_ , well-ordered
by the relation $<$, and let $\mathsf{N_{L}}$ be a countable set of _labels_.
Given an $\smash{\mathit{ML}^{n}_{\mathcal{ALC}}}$ formula $\varphi$, an _$n$
-labelled constraint for $\varphi$_ takes the form $n:\psi$, or $n:C(x)$, or
$n:r(x,y)$, where $n\in\mathsf{N_{L}}$,
$\psi\in\mathsf{for}_{\dot{\lnot}}(\varphi)$, $x\in{\sf N_{V}}$,
$C\in\mathsf{con}_{\dot{\lnot}}(\varphi)$, and $r\in\mathsf{rol}(\varphi)$. 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_ $\mathbf{T}$ is a non-empty union of labelled constraint system for
$\varphi$, and we set $\mathsf{L}_{\mathbf{T}}=\\{n\in\mathsf{N_{L}}\mid
S_{n}\in\mathbf{T}\\}$.

Concerning variables, we adopt the following terminology. A variable $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, $x$ is said to be _fresh for $S_{n}$_
if $x$ does not occur in $S_{n}$ and $x>y$, for every $y$ that occurs in $S$.
(These notions can be used with respect to $\mathbf{T}$, whenever
$S_{n}\subseteq\mathbf{T}$). Without loss of generality, we assume that,
whenever $x$ occurs in $S_{n}$, the $n$-labelled constraint $n:\top(x)$ is in
$S_{n}$ . Also, if $n:r(x,y)\in S_{n}$, we call $y$ an _$r$ -successor of $x$_
with respect to $S_{n}$. Finally, given variables $x,y$ in an $n$-labelled
constraint system $S_{n}$, we say that $x$ is _blocked by $y$ in $S_{n}$_ if
$x>y$ and $\\{C\mid n:C(x)\in S_{n}\\}\subseteq\\{C\mid n:C(y)\in S_{n}\\}$.

A completion set $\mathbf{T}$ contains a _clash_ if
$\\{m:\psi,m:\neg\psi\\}\subseteq\mathbf{T}$, or $\\{m:C(x),m:\lnot
C(x)\\}\subseteq\mathbf{T}$, for some $m\in\mathsf{N_{L}}$, and formula $\psi$
or concept $C$. A completion set with no clash is _clash-free_. Given
$\mathbf{L}\in\mathsf{Log}$, a completion set is
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-_complete_ if no
_$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ -rule_ from Figure 1 is applicable
to $\mathbf{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 following
_application conditions_ associated to each
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-rule:

  * $(\mathsf{R}_{\land})$

$\\{n:\psi,n:\chi\\}\not\subseteq\mathbf{T}$; $(\mathsf{R}_{\sqcap})$
$\\{n:C(x),n:D(x)\\}\not\subseteq\mathbf{T}$;

  * $(\mathsf{R}_{\lor})$

$\\{n:\psi,n:\chi\\}\cap\mathbf{T}=\emptyset$; $(\mathsf{R}_{\sqcup})$
$\\{n:C(x),n:D(x)\\}\cap\mathbf{T}=\emptyset$;

  * $(\mathsf{R}_{\exists})$

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

  * $(\mathsf{R}_{\forall})$

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

  * $(\mathsf{R}_{=})$

$x$ occurs in an $n$-labelled constraint in $\mathbf{T}$ and
$n:C(x)\notin\mathbf{T}$;

  * $(\mathsf{R}_{\neq})$

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

  * $(\mathsf{R}_{\mathbf{L}})$

$m$ is fresh for $\mathbf{T}$, and there is no $o\in\mathsf{N_{L}}$ such that
$\\{o:\gamma_{1},\ldots,o:\gamma_{k},o:\delta\\}\subseteq\mathbf{T}$, or
$\\{o:\dot{\lnot}\gamma_{j},o:\dot{\lnot}\delta\\}\subseteq\mathbf{T}$, for
some $j\leq l$, where $k$ and $l$ are as in Figure 1.

$\begin{array}[]{l l}\hbox{\forest for tree={ calign=center, grow'=east,
parent anchor=east, child anchor=west, } [($\mathsf{R}_{\land}$) \ \
\framebox{ \minipage{433.62pt}$n:\psi\land\chi$ \endminipage} [ \framebox{
\minipage{433.62pt}$n:\psi$ {,} $n:\chi$ \endminipage}] ] }&\hbox{\forest for
tree={ calign=center, grow'=east, parent anchor=east, child anchor=west, }
[($\mathsf{R}_{\sqcap}$) \ \ \framebox{ \minipage{433.62pt}$n:C\sqcap
D(x)$\endminipage} [ \framebox{ \minipage{433.62pt}$n:C(x)$ {,}
$n:D(x)$\endminipage}] ] }\\\ \hbox{\forest for tree={ calign=center,
grow'=east, parent anchor=east, child anchor=west, } [($\mathsf{R}_{\lor}$) \
\ \framebox{ \minipage{433.62pt}$n:\psi\lor\chi$ \endminipage} [\framebox{
\minipage{433.62pt}$n:\psi$\endminipage}] [\framebox{
\minipage{433.62pt}$n:\chi$\endminipage}] ] }&\hbox{\forest for tree={
calign=center, grow'=east, parent anchor=east, child anchor=west, }
[($\mathsf{R}_{\sqcup}$) \ \ \framebox{ \minipage{433.62pt}$n:C\sqcup D(x)$
\endminipage} [\framebox{ \minipage{433.62pt}$n:C(x)$\endminipage}]
[\framebox{ \minipage{433.62pt}$n:D(x)$\endminipage}] ] }\\\ \hbox{\forest for
tree={ calign=center, grow'=east, parent anchor=east, child anchor=west, }
[($\mathsf{R}_{\exists}$) \ \ \framebox{ \minipage{433.62pt}$n:\exists r.C(x)$
\endminipage} [ \framebox{ \minipage{433.62pt}{$n:r(x,y)$} {,}
$n:C(y)$\endminipage} ] ] }&\hbox{\forest for tree={ calign=center,
grow'=east, parent anchor=east, child anchor=west, } [($\mathsf{R}_{\forall}$)
\ \ \framebox{ \minipage{433.62pt}$n:\forall r.C(x)$ {,} { $n:r(x,y)$ }
\endminipage} [ \framebox{ \minipage{433.62pt}$n:C(y)$ \endminipage}] ] }\\\
\hbox{\forest for tree={ calign=center, grow'=east, parent anchor=east, child
anchor=west, } [($\mathsf{R}_{=}$) \ \ \framebox{
\minipage{433.62pt}$n:\top\sqsubseteq C$ \endminipage} [\framebox{
\minipage{433.62pt}$n:C(x)$ \endminipage}] ] }&\hbox{\forest for tree={
calign=center, grow'=east, parent anchor=east, child anchor=west, }
[($\mathsf{R}_{\neq}$) \ \ \framebox{
\minipage{433.62pt}$n:\lnot(\top\sqsubseteq C)$ \endminipage} [\framebox{
\minipage{433.62pt}$n:\dot{\lnot}C(x)$ \endminipage}] ] }\\\ \end{array}$

for tree= calign=center, grow’=east, parent anchor=east, child anchor=west,
[($\mathsf{R}_{\mathbf{L}}$)
$n:\Box_{i}\gamma_{1},\ldots,n:\Box_{i}\gamma_{k},n:\Diamond_{i}\delta$ [
$m:\gamma_{1},\ldots,m:\gamma_{k},m:\delta$ $(0)$] [
$m:\dot{\lnot}\gamma_{1},m:\dot{\lnot}\delta$ $(1)$] [ $\vdots$ ] [
$m:\dot{\lnot}\gamma_{k},m:\dot{\lnot}\delta$ $(l)$] ]

Figure 1:  $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-rules, where: for
$\mathbf{L}=\mathbf{E}$, $k=l=1$; for $\mathbf{L}=\mathbf{M}$, $k=1$ and
$l=0$; for $\mathbf{L}=\mathbf{C}$, $k\geq 1$ and $l=k$; for
$\mathbf{L}=\mathbf{N}$, $k=l=1$ or $k=l=0$;

The $\mathbf{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 expansion of the
completion set. For each $\mathbf{L}\in\mathsf{Log}$, we now define an
algorithm based on $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-rules for checking
the $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ formula satisfiability. We then
prove that the algorithm terminates for every formula $\varphi$, and that it
is sound and complete with respect to $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$
satisfiability.

######  Definition 1 ($\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau
algorithm for $\varphi$).

Given an $\smash{\mathit{ML}^{n}_{\mathcal{ALC}}}$ formula $\varphi$, the
_$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm for $\varphi$_
runs as follows: set the initial completion set
$\mathbf{T}_{\varphi}=\\{0:\varphi,0:\top(x)\\}$, and expand it by means of
the $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-rules until a clash or an
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-complete completion set is obtained.

In the rest of this section, we prove termination, soundness and completeness
of the tableau algorithms given above. We start by showing that the
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm terminates.

######  Theorem 1 (Termination).

Having started on the initial completion set
$\mathbf{T}_{\varphi}=\\{0:\varphi,0:\top(x)\\}$, the
$\mathbf{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 1.1.

Let $\mathbf{T}$ be a completion set obtained by applying the
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm for $\varphi$. For
each $n\in\mathsf{L}_{\mathbf{T}}$, the number of $n$-labelled constraints for
$\varphi$ in $\mathbf{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\mathbf{T}$, the
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableaux algorithm behaves exactly
like a standard (non-modal) $\smash{\mathcal{ALC}}$ tableaux algorithm (cf.
e.g. [27, Theorem 15.4], noting also that in our case we do not have to deal
with individual names). ∎

######  Claim 1.2.

Let $\mathbf{T}$ be a completion set obtained by applying the
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm for $\varphi$. For
$\mathbf{L}\in\\{\mathbf{E},\mathbf{M},\mathbf{N}\\}$,
$|\mathsf{L}_{\mathbf{T}}|\leq|\mathsf{Fg}(\varphi)|^{2}$. For
$\mathbf{L}=\mathbf{C}$, $|\mathsf{L}_{\mathbf{T}}|\leq
2^{|\mathsf{Fg}(\varphi)|}\cdot|\mathsf{Fg}(\varphi)|$.

###### Proof of Claim.

Labels $n$ are generated in $\mathbf{T}$ by means of the application of the
rule $\mathsf{R}_{\mathbf{L}}$. For
$\mathbf{L}\in\\{\mathbf{E},\mathbf{M},\mathbf{N}\\}$, this rule is applied to
two $n$-labelled contraints $n:\Box_{i}\gamma,n:\Diamond_{i}\delta$ (for
$\mathbf{L}=\mathbf{N}$ possibly also to a single constraint
$n:\Diamond_{i}\delta$), while for $\mathbf{L}=\mathbf{C}$ it is applied to
$k+1$ $n$-labelled contraints
$n:\Box_{i}\gamma_{1},...n:\Box_{i}\gamma_{k},n:\Diamond_{i}\delta$. By the
application condition of $\mathsf{R}_{\mathbf{L}}$, each such combination of
constraints generates at most one label $m$. Therefore, the number of labels
that can be generated in $\mathbf{T}$ is bounded by the number of possible
such combinations, which is at most $|\mathsf{Fg}(\varphi)|^{2}$, for
$\mathbf{L}\in\\{\mathbf{E},\mathbf{M},\mathbf{N}\\}$, and at most
$2^{|\mathsf{Fg}(\varphi)|}\cdot|\mathsf{Fg}(\varphi)|$, for
$\mathbf{L}=\mathbf{C}$. ∎

The theorem is then a consequence of the following observations. Given a
completion set $\mathbf{T}$ constructed by the
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm, we have by Claim
1.2 that the number of applications of rule $\mathsf{R}_{\mathbf{L}}$ is
bounded by $|\mathsf{L}_{\mathbf{T}}|$, which is at most
$|\mathsf{Fg}(\varphi)|^{2}$, for
$\mathbf{L}\in\\{\mathbf{E},\mathbf{M},\mathbf{N}\\}$, and at most
$2^{|\mathsf{Fg}(\varphi)|}\cdot|\mathsf{Fg}(\varphi)|$, for
$\mathbf{L}=\mathbf{C}$. Moreover, since every application of the rules
$\mathsf{R}_{\land}$ and $\mathsf{R}_{\lor}$ introduces a new formula to an
$n$-labelled constraint, the total number of such rule applications is bounded
by $|\mathsf{L}_{\mathbf{T}}|\cdot|\mathsf{Fg}(\varphi)|$. Finally, by Claim
1.1, the number of applications of rules
$\mathsf{R}_{\sqcap},\mathsf{R}_{\sqcup},\mathsf{R}_{\forall},\mathsf{R}_{\exists},\mathsf{R}_{=},\mathsf{R}_{\neq}$
per label $n$ is bounded by $2^{q(|\mathsf{Fg}(\varphi)|)}$, where $q$ is a
polynomial function, since these rules add a new constraint to an $n$-labelled
constraint system. Thus, the overall number of such rule applications is
bounded by $|\mathsf{L}_{\mathbf{T}}|\cdot 2^{q(|\mathsf{Fg}(\varphi)|)}$. ∎

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

######  Theorem 2 (Soundness).

If, having started on the initial completion set $\mathbf{T}_{\varphi}$, the
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm constructs an
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-complete and clash-free completion
set for $\varphi$, then $\varphi$ is $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$
satisfiable.

###### Proof.

Given an $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-complete and clash-free
completion set $\mathbf{T}$ for $\varphi$, define, for
$n\in\mathsf{L}_{\mathbf{T}}$, $\psi\in\mathsf{for}_{\dot{\lnot}}(\varphi)$,
$C\in\mathsf{con}_{\dot{\lnot}}(\varphi)$, and $x$ occurring in $\mathbf{T}$,

$\lfloor C\rfloor_{x}$ = $\\{n\in\mathsf{L}_{\mathbf{T}}\mid n:C(x)\in S_{n}\\}$, |  |  $\lfloor\psi\rfloor$ = $\\{n\in\mathsf{L}_{\mathbf{T}}\mid n:\psi\in S_{n}\\}$,
---|---|---
$\lceil C\rceil_{x}$ = $\mathsf{L}_{\mathbf{T}}\setminus\\{n\in\mathsf{L}_{\mathbf{T}}\mid n:\dot{\lnot}C(x)\in S_{n}\\}$, |  |  $\lceil\psi\rceil$ = $\mathsf{L}_{\mathbf{T}}\setminus\\{n\in\mathsf{L}_{\mathbf{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{\mathit{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 I})$ and
$\mathcal{I}_{n}=(\Delta_{n},\cdot^{\mathcal{I}_{n}})$, for $n\in\mathcal{W}$,
defined as follows:

  * •

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

  * •

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

– for $\mathbf{L}=\mathbf{E}$: |  $\mathcal{N}_{i}(n)=\big{\\{}\alpha\mid\textnormal{for some}\ \Box_{i}\gamma\in\Gamma^{x}_{n}\colon\lfloor\gamma\rfloor_{x}\subseteq\alpha\subseteq\lceil\gamma\rceil_{x}\big{\\}}$;
---|---
– for $\mathbf{L}=\mathbf{M}$: |  $\mathcal{N}_{i}(n)=\big{\\{}\alpha\mid\textnormal{for some}\ \Box_{i}\gamma\in\Gamma^{x}_{n}\colon\lfloor\gamma\rfloor_{x}\subseteq\alpha\big{\\}}$;
– for $\mathbf{L}=\mathbf{C}$: | $\mathcal{N}_{i}(n)=\big{\\{}\alpha\mid\textnormal{for some}\ \Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{{x}_{k}}_{n}\colon$
|  $\mathcal{N}_{i}(n)=\\{\alpha\mid\,$
$\bigcap^{k}_{j=1}\lfloor\gamma_{j}\rfloor_{{{x}_{j}}}\subseteq\alpha\subseteq\bigcap^{k}_{j=1}\lceil\gamma_{j}\rceil_{{{x}_{j}}}\big{\\}}$;
– for $\mathbf{L}=\mathbf{N}$: |  $\mathcal{N}_{i}(n)=\big{\\{}\alpha\mid\textnormal{for some}\ \Box_{i}\gamma\in\Gamma^{x}_{n}\colon\lfloor\gamma\rfloor_{x}\subseteq\alpha\subseteq\lceil\gamma\rceil_{x}\big{\\}}\cup\mathcal{W}$;

  * •

$\Delta_{n}=\\{x\in\mathsf{N_{V}}\mid x\ \text{occurs in}\ S_{n}\\}$;

  * •

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

  * •

$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}$ }.

First, we observe the following.

  * •

For $\mathbf{L}=\mathbf{M}$, we have that
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ is such that
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in I})$ is supplemented.
Indeed, for all $n\in\mathcal{W}$, $\alpha,\beta\subseteq\mathcal{W}$, suppose
that $\alpha\in\mathcal{N}_{i}(n)$ and $\alpha\subseteq\beta$. By definition,
this implies that: for some $\Box_{i}\gamma\in\Gamma^{x}_{n}$,
$\lfloor\gamma\rfloor_{x}\subseteq\alpha\subseteq\beta$. Hence,
$\beta\in\mathcal{N}_{i}(n)$.

  * •

For $\mathbf{L}=\mathbf{C}$, we have that
$\mathcal{M}=(\mathcal{F},\mathcal{I})$ is such that
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in I})$ is closed under
intersection. Indeed, for all $n\in\mathcal{W}$,
$\alpha,\beta\subseteq\mathcal{W}$, suppose that $\alpha\in\mathcal{N}_{i}(n)$
and $\beta\in\mathcal{N}_{i}(n)$. Now suppose that, for some
$\Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{{x}_{k}}_{n}\colon\bigcap^{k}_{j=1}\lfloor\gamma_{j}\rfloor_{{x}_{j}}\subseteq\alpha\subseteq\bigcap^{k}_{j=1}\lceil\gamma_{j}\rceil_{{x}_{j}}$
and, for some
$\Box_{i}\delta_{1}\in\Gamma^{y_{1}}_{n},\ldots,\Box_{i}\delta_{h}\in\Gamma^{y_{h}}_{n}\colon\bigcap^{h}_{j=1}\lfloor\delta_{j}\rfloor_{y_{j}}\subseteq\beta\subseteq\bigcap^{h}_{j=1}\lceil\delta_{j}\rceil_{y_{j}}$.
Then for some
$\Box_{i}\gamma_{1}\in\Gamma^{{x}_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{{x}_{k}}_{n}$
and some
$\Box_{i}\delta_{1}\in\Gamma^{y_{1}}_{n},\ldots,\Box_{i}\delta_{h}\in\Gamma^{y_{h}}_{n}$
the following holds, which in turn implies that
$\alpha\cap\beta\in\mathcal{N}_{i}(n)$:

$\bigcap^{k}_{j=1}\lfloor\gamma_{j}\rfloor_{{x}_{j}}\cap\bigcap^{h}_{j=1}\lfloor\delta_{j}\rfloor_{y_{j}}\subseteq\alpha\cap\beta\subseteq\bigcap^{k}_{j=1}\lceil\gamma_{j}\rceil_{{x}_{j}}\cap\bigcap^{h}_{j=1}\lceil\delta_{j}\rceil_{y_{j}}$

  * •

For $\mathbf{L}=\mathbf{N}$, we have that
$\mathcal{M}=(\mathcal{F},\mathcal{I})$, with
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in I})$, is such that
$\mathcal{F}$ contains the unit. Indeed, by construction, for all
$n\in\mathcal{W}$, $\mathcal{W}\in\mathcal{N}_{i}(n)$.

We then require the following claims.

######  Claim 2.1.

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 $\mathbf{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 [27, Claim 15.2]).

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

  * •

$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}}$.

  * •

$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(x)\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}}$.

$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}}$.

$C=\Box_{i}D$. Let $n:\Box_{i}D(x)\in S_{n}$, meaning that
$\Box_{i}D\in\Gamma^{x}_{n}$. Consider $\mathbf{L}\in\mathsf{Log}$.

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

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.

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

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}$. Thus, we have $\Box_{i}D\in\Gamma^{x}_{n}$
such that $\lfloor D\rfloor_{x}\subseteq\llbracket
D\rrbracket^{\mathcal{M}}_{x}$. By definition, this means $\llbracket
D\rrbracket^{\mathcal{M}}_{x}\in\mathcal{N}_{i}(n)$, as required.

  3. $\mathbf{L}\in\\{\mathbf{C},\mathbf{N}\\}$.

This cases are analogous to the case for $\mathbf{L}=\mathbf{E}$.

$C=\Diamond_{i}D$. Let $n:\Diamond_{i}D(x)\in S_{n}$. Consider
$\mathbf{L}\in\mathsf{Log}$.

  1. $\mathbf{L}\in\\{\mathbf{E},\mathbf{M}\\}$.

We distinguish two cases. $(i)$ There exists no
$\Box_{i}\gamma\in\Gamma^{y}_{n}$. This means that
$\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}}$. $(ii)$ There exists
$\Box_{i}\gamma\in\Gamma^{y}_{n}$. We then reason similarly to the case for
$\mathbf{L}=\mathbf{C}$.

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

We distinguish two cases. $(i)$ There exist no
$\Box_{i}\gamma_{1}\in\Gamma^{y_{1}}_{n},\ldots,\Box_{i}\gamma_{k}\in\Gamma^{y_{k}}_{n}$.
As for $\mathbf{L}=\mathbf{E}$, we obtain
$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 $\mathbf{T}$ is $\mathbf{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$. Equivalently, it
is not the case that, for every $v\in\mathcal{W}$:
$\gamma_{1}\in\Gamma^{y_{1}}_{m},\ldots,\gamma_{k}\in\Gamma^{y_{k}}_{m}$
implies $x\not\in D^{\mathcal{I}_{m}}$; and for all $j\leq k$,
$x\in\dot{\lnot}D^{\mathcal{I}_{m}}$ implies
$\dot{\lnot}\gamma_{j}\not\in\Gamma^{y_{j}}_{m}$. In other words, it is not
the case that:
$\bigcap_{j=1}^{k}\lfloor\gamma_{j}\rfloor_{y_{j}}\subseteq\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}$; and $\mathcal{W}\setminus\llbracket
D\rrbracket^{\mathcal{M}}_{x}\subseteq\bigcap_{j=1}^{k}\lceil\gamma_{l}\rceil_{y_{l}}$.
Thus, $\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.

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

We distinguish two cases. $(i)$ There exists no
$\Box_{i}\gamma\in\Gamma^{y}_{n}$. This means that
$\mathcal{N}_{i}(n)=\mathcal{W}$. Since $\mathbf{T}$ is
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-complete, there exists
$m\in\mathcal{W}$ such that $D\in\Gamma^{x}_{m}$, i.e., $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$. This holds iff
$\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 exists
$\Box_{i}\gamma\in\Gamma^{y}_{n}$. We then reason similarly to the case for
$\mathbf{L}=\mathbf{C}$. ∎

######  Claim 2.2.

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

###### Proof of Claim.

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

$\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}_{=})$ and $x$
occurs in $S_{n}$, we have that $n:C(x)\in S_{n}$. By Claim 2.1, we have that
$x\in C^{\mathcal{I}_{n}}$. Given that $x$ is arbitrary, we conclude that
$\mathcal{M},n\models\top\sqsubseteq C$.

$\psi=\lnot(\top\sqsubseteq C)$. Let $n:\lnot(\top\sqsubseteq C)\in S_{n}$.
Since $S_{n}$ is closed under $(\mathsf{R}_{\neq})$, there exists $x$
occurring in $S_{n}$ such that $n:\dot{\lnot}C(x)\in S_{n}$. By Claim 2.1, 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 2.1. ∎

Since, by definition, we have $0:\varphi\in S_{0}\subseteq\mathbf{T}$, thanks
to Claim 2.2 we obtain $\mathcal{M},0\models\varphi$. ∎

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

######  Theorem 3 (Completeness).

If $\varphi$ is $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ satisfiable, then,
having started on the initial completion set $\mathbf{T}_{\varphi}$, the
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm constructs an
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-complete and clash-free completion
set for $\varphi$.

###### Proof.

Let $\mathcal{M}=(\mathcal{F},\mathcal{I})$ be an
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-model satisfying $\varphi$, with
$\mathcal{F}=(\mathcal{W},\\{\mathcal{N}\\}_{i\in I})$, 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{\mathit{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}$. We now show that the following holds.

######  Claim 3.1.

For every $w\in\mathcal{W}$ and every
$d_{1},\ldots,d_{k},e\in\bigcup_{v\in\mathcal{W}}\Delta_{v}$: if
$\Box_{i}\gamma_{1}\in\Phi^{d_{1}}_{w},\ldots,\Box_{i}\gamma_{k}\in\Phi^{d_{k}}_{w}$
and $\Diamond_{i}\delta\in\Phi^{e}_{w}$, then there exists $v\in\mathcal{W}$
such that:

  1. $(0)$

$\gamma_{1}\in\Phi^{d_{1}}_{v},\ldots,\gamma_{k}\in\Phi^{d_{k}}_{v}$ and
$\delta\in\Phi^{e}_{v}$; or

  2. $(1)$

$\dot{\lnot}\gamma_{1}\in\Phi^{d_{1}}_{v}$ and
$\dot{\lnot}\delta\in\Phi^{e}_{v}$; or

  3. $\vdots$

  4. $(l)$

$\dot{\lnot}\gamma_{l}\in\Phi^{d_{k}}_{v}$ and
$\dot{\lnot}\delta\in\Phi^{e}_{v}$;

where: for $\mathbf{L}=\mathbf{E}$, $k=l=1$; for $\mathbf{L}=\mathbf{M}$,
$k=1$ and $l=0$; for $\mathbf{L}=\mathbf{C}$, $k\geq 1$ and $l=k$; for
$\mathbf{L}=\mathbf{N}$, $k=l=1$ or $k=l=0$.

###### Proof.

We consider each $\mathbf{L}\in\mathsf{Log}$.

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

Assume $\Box_{i}\gamma\in\Phi^{d}_{w},\Diamond_{i}\delta\in\Phi^{e}_{w}$,
meaning that
$\llbracket\gamma\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)$ and
$\mathcal{W}\setminus\llbracket\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(w)$,
i.e.,
$\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(w)$.
Towards a contradiction, suppose that, for every $v\in\mathcal{W}$, the
following holds: ($\gamma\not\in\Phi^{d}_{v}$ or $\delta\not\in\Phi^{e}_{v}$)
and ($\dot{\lnot}\gamma\not\in\Phi^{d}_{v}$ or
$\dot{\lnot}\delta\not\in\Phi^{e}_{v}$). Equivalently, for every
$v\in\mathcal{W}$: ($\gamma\in\Phi^{d}_{v}$ implies
$\delta\not\in\Phi^{e}_{v}$) and ($\dot{\lnot}\delta\in\Phi^{e}_{v}$ implies
$\dot{\lnot}\gamma\not\in\Phi^{d}_{v}$). By definition, we have that
$\gamma\in\Phi^{d}_{v}$ iff $\dot{\lnot}\gamma\not\in\Phi^{d}_{v}$ and
$\delta\not\in\Phi^{e}_{v}$ iff $\dot{\lnot}\delta\in\Phi^{e}_{v}$. Thus, the
previous step means:
($\llbracket\gamma\rrbracket^{\mathcal{M}}_{d}\subseteq\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}$)
and
($\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\subseteq\llbracket\gamma\rrbracket^{\mathcal{M}}_{d}$),
i.e.,
$\llbracket\gamma\rrbracket^{\mathcal{M}}_{d}=\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}$,
contradicting the assumption that
$\llbracket\gamma\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)$ and
$\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(w)$.

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

Assume $\Box_{i}\gamma\in\Phi^{d}_{w},\Diamond_{i}\delta\in\Phi^{e}_{w}$,
meaning that
$\llbracket\gamma\rrbracket^{\mathcal{M}}_{d}\in\mathcal{N}_{i}(w)$ and
$\mathcal{W}\setminus\llbracket\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(w)$,
i.e.,
$\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(w)$.
Towards a contradiction, suppose that, for every $v\in\mathcal{W}$, the
following holds: $\gamma\not\in\Phi^{d}_{v}$ or $\delta\not\in\Phi^{e}_{v}$.
Equivalently, for every $v\in\mathcal{W}$: $\gamma\in\Phi^{d}_{v}$ implies
$\delta\not\in\Phi^{e}_{v}$. By definition, the previous step means
$\llbracket\gamma\rrbracket^{\mathcal{M}}_{d}\subseteq\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}$.
Since $\mathcal{M}$ is supplemented, we have that
$\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\in\mathcal{N}_{i}(w)$,
which is impossible.

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

Assume
$\Box_{i}\gamma_{1}\in\Phi^{d_{1}}_{w},\ldots,\Box_{i}\gamma_{k}\in\Phi^{d_{k}}_{w},\Diamond_{i}\delta\in\Phi^{e}_{w}$,
meaning that
$\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\in\mathcal{N}_{i}(w)$,
for $j=1,\ldots,k$, and
$\mathcal{W}\setminus\llbracket\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(w)$,
i.e.,
$\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(w)$.
Towards a contradiction, suppose that, for every $v\in\mathcal{W}$, none of
the following holds: $(0)$
$\gamma_{1}\in\Phi^{d_{1}}_{v},\ldots,\gamma_{k}\in\Phi^{d_{k}}_{v}$ and
$\delta\in\Phi^{e}_{v}$; $(1)$ $\dot{\lnot}\gamma_{1}\in\Phi^{d_{1}}_{v}$ and
$\dot{\lnot}\delta\in\Phi^{e}_{v}$; …; $(k)$
$\dot{\lnot}\gamma_{k}\in\Phi^{d_{k}}_{v}$ and
$\dot{\lnot}\delta\in\Phi^{e}_{v}$. Equivalently, for every $v\in\mathcal{W}$,
it holds that $(0)$
$\gamma_{1}\in\Phi^{d_{1}}_{v},\ldots,\gamma_{k}\in\Phi^{d_{k}}_{v}$ implies
$\delta\not\in\Phi^{e}_{v}$; and $(1)$ $\dot{\lnot}\delta\in\Phi^{e}_{v}$
implies $\dot{\lnot}\gamma_{1}\not\in\Phi^{d_{1}}_{v}$; … and $(k)$
$\dot{\lnot}\delta\in\Phi^{e}_{v}$ implies
$\dot{\lnot}\gamma_{k}\not\in\Phi^{d_{k}}_{v}$. By definition, from the
previous step we obtain $(0)$
$\bigcap_{j=1}^{k}\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}\subseteq\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}$;
and $(1)$
$\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\subseteq\llbracket\gamma_{1}\rrbracket^{\mathcal{M}}_{d_{1}}$;
… and $(k)$
$\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\subseteq\llbracket\gamma_{k}\rrbracket^{\mathcal{M}}_{d_{k}}$.
Hence
$\bigcap_{j=1}^{k}\llbracket\gamma_{j}\rrbracket^{\mathcal{M}}_{d_{j}}=\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}$.
Since $\mathcal{M}$ is closed under intersection, we obtain
$\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}\in\mathcal{N}_{i}(w)$,
a contradiction.

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

We distinguish two cases: $(i)$ Let $k=l=0$. That is, there exists no
$\Box_{i}\gamma\in\Phi^{d}_{w}$, while $\Diamond_{i}\delta\in\Phi^{e}_{w}$,
meaning that
$\mathcal{W}\setminus\llbracket\delta\rrbracket^{\mathcal{M}}_{e}\not\in\mathcal{N}_{i}(w)$.
Towards a contradiction, suppose that, for every $v\in\mathcal{W}$,
$\delta\not\in\Phi^{e}_{v}$. Since, by definition, we have
$\delta\not\in\Phi^{e}_{v}$ iff $\dot{\lnot}\delta\in\Phi^{e}_{v}$, the
previous step means that
$\mathcal{W}\subseteq\llbracket\dot{\lnot}\delta\rrbracket^{\mathcal{M}}_{e}$,
and hence $\llbracket\delta\rrbracket^{\mathcal{M}}_{e}=\emptyset$. Thus,
$\mathcal{W}\not\in\mathcal{N}_{i}(w)$, contradicting the fact that
$\mathcal{M}$ contains the unit. $(ii)$ Let $k=l=1$. Hence, there exists
$\Box_{i}\gamma\in\Phi^{e}_{w}$ and $\Diamond_{i}\delta\in\Phi^{e}_{w}$. We
then reason similarly to the case for $\mathbf{L}=\mathbf{E}$. ∎

Given a completion set $\mathbf{T}$ for $\varphi$ and
$S_{n}\subseteq\mathbf{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
$\mathbf{T}$ for $\varphi$ is _$\mathcal{M}$ -compatible_ if there exists a
function $\pi$ from $\mathsf{L}_{\mathbf{T}}$ to $\mathcal{W}$, and, for every
$n\in\mathsf{L}_{\mathbf{T}}$, there exists a function $\pi_{n}$ from the set
of variables 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
then require the following claim.

######  Claim 3.2.

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

###### Proof.

Given an $\mathcal{M}$-compatible completion set $\mathbf{T}$ for $\varphi$
and a label $n\in\mathsf{L}_{\mathbf{T}}$, let $\pi$ and $\pi_{n}$ be the
functions provided by the definition of $\mathcal{M}$-compatibility. We need
to consider each $\mathbf{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}_{=},\mathsf{R}_{\neq}\\}$,
we proceed similarly to [27, Claim 15.14]. Here we consider the case of
$\mathsf{R}_{\mathbf{L}}$: Suppose that $\mathsf{R}_{\mathbf{L}}$ is
applicable to $\mathbf{T}$. Let
$\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 $\mathbf{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)}$. Thus, by Claim 3.1,
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 l$; where: for
$\mathbf{L}=\mathbf{E}$, $k=l=1$; for $\mathbf{L}=\mathbf{M}$, $k=1$ and
$l=0$; for $\mathbf{L}=\mathbf{C}$, $k\geq 1$ and $l=k$; for
$\mathbf{L}=\mathbf{N}$, $k=l=1$ or $k=l=0$. By applying the rule
$\mathsf{R}_{\mathbf{L}}$ accordingly, one can obtain $\mathbf{T}^{\prime}$ by
adding $m:\gamma_{1},\ldots,m:\gamma_{k},m:\delta$, or
$m:\dot{\lnot}\gamma_{j},m:\dot{\lnot}\delta$, for some $j\leq l$, to
$\mathbf{T}$ (recall that $m$ is fresh for $\mathbf{T}$ and $\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)$). By extending $\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)$, we obtain that
$\mathbf{T}^{\prime}$ is $\mathcal{M}$-compatible. ∎

To conclude, let $\mathbf{T}_{\varphi}=\\{0:\varphi,0:\top(x)\\}$ be the
initial completion set for $\varphi$. Define $\pi(0)=w_{\varphi}$ (where
$\mathcal{M},w_{\varphi}\models\varphi$) and $\pi_{0}(x)=d$, for an arbitrary
$d\in\Delta_{w_{\varphi}}$. Clearly, these functions ensure that
$\mathbf{T}_{\varphi}$ is $\mathcal{M}$-compatible. By Claim 3.2, we can apply
the $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-rules so that the obtained
completion sets are $\mathcal{M}$-compatible as well. From Theorem 1, we have
that the $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm eventually
terminates, returning an $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-complete
completion set for $\varphi$ that is clash-free by construction. ∎

By Theorem 1, we have that the non-deterministic
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ tableau algorithm terminates after
exponentially many steps in the size of the input formula. By Theorems 2 and
3, such algorithm is sound and complete with respect to satisfiability in
varying domain neighbourhood models. Thus, we obtain the following result.

######  Theorem 4.

The $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ formula satisfiability problem on
varying domain neighbourhood models is decidable in NExpTime.

To conclude this section, we observe that as an immediate consequence of the
above results we also obtain a (constructive) proof of the following kind of
_exponential model property_.

######  Corollary 5.

For $\mathbf{L}\in\\{\mathbf{E},\mathbf{M},\mathbf{N}\\}$ (respectively,
$\mathbf{L}=\mathbf{C}$), every $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$
satisfiable formula $\varphi$ has a model with at most
$p(|\mathsf{Fg}(\varphi)|)$ (respectively, at most
$2^{p(|\mathsf{Fg}(\varphi)|)}$) worlds, each of them having a domain with at
most $2^{q(|\mathsf{Fg}(\varphi)|)}$ elements, where $p$ and $q$ are
polynomial functions.

###### Proof.

By Theorem 3, if $\varphi$ is $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$
satisfiable, then there is a $\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$-complete
and clash-free completion set $\mathbf{T}$ for it. Then by Theorem 2, there
exists a model $\mathcal{M}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in
I},\mathcal{I})$ for $\varphi$ where $\mathcal{W}=\mathsf{L}_{\mathbf{T}}$ and
for each $n\in\mathcal{W}$, $\Delta_{n}=\\{x\in\mathsf{N_{V}}\mid x\
\text{occurs in}\ S_{n}\\}$. By Theorem 1, Claim 1.2, it follows
$|\mathcal{W}|\leq|\mathsf{Fg}(\varphi)|^{2}$ for
$\mathbf{L}\in\\{\mathbf{E},\mathbf{M},\mathbf{N}\\}$, and $|\mathcal{W}|\leq
2^{|\mathsf{Fg}(\varphi)|}\cdot|\mathsf{Fg}(\varphi)|$ for
$\mathbf{L}=\mathbf{C}$, finally by Theorem 1, Claim 1.1, for each
$n\in\mathcal{W}$, $|\Delta_{n}|$ does not exceed
$2^{q(|\mathsf{Fg}(\varphi)|)}$, where $p$ and $q$ are polynomial functions. ∎

##  4 Reasoning in Fragments without Modalised Concepts

An _$\smash{\mathit{ML}^{n\mid{\sf g}}_{\mathcal{ALC}}}$ formula_ is defined
similarly to the $\smash{\mathit{ML}^{n}_{\mathcal{ALC}}}$ case, by
disallowing modalised concepts. Given $\mathbf{L}\in\mathsf{Log}$, the
_$\mathbf{L}^{n\mid{\sf g}}_{\smash{\mathcal{ALC}}}$ formula satisfiability
problem on constant domain neighbourhood models_ is the
$\smash{\mathit{ML}^{n\mid{\sf g}}_{\mathcal{ALC}}}$ formula satisfiability
problem on constant domain neighbourhood models based on neighbourhood frames
in the respective class for $\mathbf{L}$ (cf. Section 2). An
_$\smash{\mathit{ML}^{n}}$ formula_, instead, is defined analogously to
$\smash{\mathit{ML}^{n\mid{\sf g}}_{\mathcal{ALC}}}$, except that we built it
from the standard propositional (rather than $\smash{\mathcal{ALC}}$) language
over a countable set of _propositional letters_ $\mathsf{N_{P}}$. The
semantics of $\smash{\mathit{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 I},\mathcal{V})$, where
$(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in I})$ is a neighbourhood frame, with
$I=\\{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 [20, 30]). The _$\smash{\mathbf{L}^{n}}$ formula satisfiability problem_,
is the $\smash{\mathit{ML}^{n}}$ formula satisfiability problem on
propositional neighbourhood models based on neighbourhood frames in the
respective class for $\mathbf{L}$. A propositional neighbourhood model based
on a neighbourhood frame in the respective class for $\mathbf{L}$ is called
_$\mathbf{L}^{n}$ model_.

In Dalmonte et al. [24], it is shown that $\smash{\mathbf{E}^{n\mid{\sf
g}}_{\mathcal{ALC}}}$ and $\smash{\mathbf{M}^{n\mid{\sf g}}_{\mathcal{ALC}}}$
formula satisfiability problems on constant domain neighbourhood models are
ExpTime-complete. We now show tight complexity results for
$\smash{\mathbf{C}^{n\mid{\sf g}}_{\mathcal{ALC}}}$ and
$\smash{\mathbf{N}^{n\mid{\sf g}}_{\mathcal{ALC}}}$, using again the notion of
a propositional abstraction of a formula (as in, e.g., [29]). Here, one can
separate the satisfiability test into two parts, one for the description logic
dimension and one for the modal dimension. The _propositional abstraction_
$\varphi_{\sf prop}$ of an $\smash{\mathit{ML}^{n\mid{\sf
g}}_{\mathcal{ALC}}}$ formula $\varphi$ is the result of replacing each
$\smash{\mathcal{ALC}}$ CI in $\varphi$ by a propositional letter $p$, so that
there is a $1:1$ relationship between the $\smash{\mathcal{ALC}}$ CI $\pi$
occurring in $\varphi$ and the propositional letters $p_{\pi}$ used for the
abstraction. We set ${\sf N_{P}}(\varphi)=\\{p_{\pi}\in{\sf
N_{P}}\mid\pi\text{ is an $\smash{\mathcal{ALC}}$ CI in }\varphi\\}$. Given an
$\smash{\mathit{ML}^{n\mid{\sf g}}_{\mathcal{ALC}}}$ formula $\varphi$, we say
that a propositional neighbourhood model $\mathcal{M}^{\sf
P}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in I},\mathcal{V})$ of $\varphi_{\sf
prop}$ is _$\varphi\text{-consistent}$_ if, for all $w\in\mathcal{W}$, the
following $\smash{\mathcal{ALC}}$ formula is satisfiable

$\textstyle\bigwedge_{p_{\pi}\in{\sf N_{P}}(w)}\ {\pi}\ \wedge\
\bigwedge_{p_{\pi}\in\overline{{\sf N_{P}}(w)}}\ \neg{\pi},$

where ${\sf N_{P}}(w)=\\{p_{\pi}\in{\sf N_{P}}(\varphi)\mid
w\in\mathcal{V}(p_{\pi})\\}$ and $\overline{{\sf N_{P}}(w)}={\sf
N_{P}}(\varphi)\setminus{\sf N_{P}}(w)$. We now formalise the connection
between $\smash{\mathit{ML}^{n\mid{\sf g}}_{\mathcal{ALC}}}$ formulas and
their propositional abstractions with the following lemma, where
$\mathbf{L}\in\\{\mathbf{C},\mathbf{N}\\}$, obtained by adapting the proof of
Dalmonte et al. [24, Lemma 1].

######  Lemma 6.

A formula $\varphi$ is $\mathbf{L}^{n\mid{\sf g}}_{\smash{\mathcal{ALC}}}$
satisfiable on constant domain neighbourhood models iff $\varphi_{\sf prop}$
is satisfied in a $\varphi$-consistent $\mathbf{L}^{n}$ model.

We assume that the primitive connectives used to build propositional formulas
are $\neg$ and $\wedge$ ($\vee$ is expressed using $\neg$ and $\wedge$), and
we denote by ${\sf sub}(\varphi_{\sf prop})$ the set of subformulas of
$\varphi_{\sf prop}$ closed under single negation. A _valuation_ for a
propositional $\smash{\mathit{ML}^{n}}$ formula $\varphi_{\sf prop}$ is a
function $\nu:{\sf sub}(\varphi_{\sf prop})\rightarrow\\{0,1\\}$ that
satisfies the following conditions: (1) for all $\neg\psi\in{\sf
sub}(\varphi_{\sf prop})$, $\nu(\psi)=1$ iff $\nu(\neg\psi)=0$; (2) for all
$\psi_{1}\wedge\psi_{2}\in{\sf sub}(\varphi_{\sf prop})$,
$\nu(\psi_{1}\wedge\psi_{2})=1$ iff $\nu(\psi_{1})=1$ and $\nu(\psi_{2})=1$;
and (3) $\nu(\varphi_{\sf prop})=1$. We say that a valuation for $\varphi_{\sf
prop}$ is _$\varphi$ -consistent_ if any propositional neighbourhood model of
the form $(\\{w\\},\\{\mathcal{N}_{i}\\}_{i\in I},\mathcal{V})$ satisfying
$w\in\mathcal{V}(p_{\pi})$ iff $\nu(p_{\pi})=1$, for all $p_{\pi}\in{\sf
N_{P}}(\varphi)$, is $\varphi$-consistent. We now establish that
satisfiability of $\varphi_{\sf prop}$ in a $\varphi$-consistent
$\smash{\mathbf{C}}^{n}$ (respectively, $\smash{\mathbf{N}^{n}}$) model is
characterized by the existence of a $\varphi$-consistent valuation satisfying
the property described in Lemma 7 (respectively, Lemma 8).

######  Lemma 7.

A formula $\varphi_{\sf prop}$ is satisfied in a $\varphi$-consistent
$\smash{\mathbf{C}}^{n}$ model iff there is a $\varphi$-consistent valuation
$\nu$ for $\varphi_{\sf prop}$ such that if
$\Box_{i}\psi_{1},\dots,\Box_{i}\psi_{k}$ are in ${\sf sub}(\varphi_{\sf
prop})$, $\nu(\Box_{i}\psi_{j})=1$ for all $1\leq j<k$, and
$\nu(\Box_{i}\psi_{k})=0$, then either
$(\bigwedge^{k-1}_{j=1}\psi_{j}\wedge\neg\psi_{k})$ or
$(\neg\psi_{j}\wedge\psi_{k})$ for some $1\leq j<k$ is satisfied in a
$\varphi$-consistent $\smash{\mathbf{C}}^{n}$ model.

###### Proof.

($\Rightarrow$) Suppose that $\varphi_{\sf prop}$ is satisfied in a world $w$
of a $\varphi$-consistent $\smash{\mathbf{C}}^{n}$ model $\mathcal{M}^{\sf
P}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in I},\mathcal{V})$. That is,
$\mathcal{M}^{\sf P},w\models\varphi_{\sf prop}$. We define a
$\varphi$-consistent valuation for $\varphi_{\sf prop}$ by setting
$\nu(\psi)=1$ if $\mathcal{M}^{\sf P},w\models\psi$ and $\nu(\psi)=0$ if
$\mathcal{M}^{\sf P},w\not\models\psi$. It is easy to check that $\nu$ is
indeed a $\varphi$-consistent valuation (given that $\mathcal{M}^{\sf P}$ is a
$\varphi$-consistent $\smash{\mathbf{C}}^{n}$ model). Assume
$\Box_{i}\psi_{1},\dots,\Box_{i}\psi_{k}$ are in ${\sf sub}(\varphi_{\sf
prop})$, $\nu(\Box_{i}\psi_{j})=1$ for all $1\leq j<k$, and
$\nu(\Box_{i}\psi_{k})=0$. Then $\mathcal{M}^{\sf P},w\models\Box_{i}\psi_{j}$
for all $1\leq j<k$, and $\mathcal{M}^{\sf P},w\not\models\Box_{i}\psi_{k}$.
By definition,
$(\Box_{i}\psi_{1}\wedge\ldots\wedge\Box_{i}\psi_{k-1})\rightarrow\Box_{i}(\psi_{1}\wedge\ldots\wedge\psi_{k-1})$
holds in $\smash{\mathbf{C}}^{n}$ models. So $\mathcal{M}^{\sf
P},w\models\Box_{i}(\psi_{1}\wedge\ldots\wedge\psi_{k-1})$ and
$\mathcal{M}^{\sf P},w\not\models\Box_{i}\psi_{k}$. This means that
$\nu(\Box_{i}(\bigwedge^{k-1}_{j=1}\psi_{j}))=1$ while
$\nu(\Box_{i}\psi_{k})=0$. By definition,
$\mathcal{V}(\bigwedge^{k-1}_{j=1}\psi_{j})\in\mathcal{N}_{i}(w)$ and
$\mathcal{V}(\psi_{k})\not\in\mathcal{N}_{i}(w)$. So,
$\mathcal{V}(\bigwedge^{k-1}_{j=1}\psi_{j})\neq\mathcal{V}(\psi_{k})$. Then,
there is a world $u$ in the symmetrical difference of these sets such that
$\mathcal{M}^{\sf
P},u\models(\bigwedge^{k-1}_{j=1}\psi_{j}\wedge\neg\psi_{k})\vee(\neg(\bigwedge^{k-1}_{j=1}\psi_{j})\wedge\psi_{k})$.

($\Leftarrow$) Suppose there is a $\varphi$-consistent valuation $\nu$ for
$\varphi_{\sf prop}$ such that if $\Box_{i}\psi_{1},\dots,\Box_{i}\psi_{k}$
are in ${\sf sub}(\varphi_{\sf prop})$, $\nu(\Box_{i}\psi_{j})=1$ for all
$1\leq j<k$, and $\nu(\Box_{i}\psi_{k})=0$, then there is a
$\varphi$-consistent $\smash{\mathbf{C}}^{n}$ model

$\mathcal{M}^{\sf
P}_{\bigwedge^{k-1}_{j=1}\psi_{j},\psi_{k}}=(\mathcal{W}_{\bigwedge^{k-1}_{j=1}\psi_{j},\psi_{k}},\\{\mathcal{N}_{{\bigwedge^{k-1}_{j=1}\psi_{j},\psi_{k}}_{i}}\\}_{i\in
I},\mathcal{V}_{\bigwedge^{k-1}_{j=1}\psi_{j},\psi_{k}})$

and a world
$w_{\bigwedge^{k-1}_{j=1}\psi_{j},\psi_{k}}\in\mathcal{W}_{\bigwedge^{k-1}_{j=1}\psi_{j},\psi_{k}}$
such that

$\mathcal{M}^{\sf
P}_{\bigwedge^{k-1}_{j=1}\psi_{j},\psi_{k}},w_{\bigwedge^{k-1}_{j=1}\psi_{j},\psi_{k}}\models((\bigwedge^{k-1}_{j=1}\psi_{j})\wedge\neg\psi_{k})\vee(\neg(\bigwedge^{k-1}_{j=1}\psi_{j})\wedge\psi_{k}).$

Let $\mathcal{M}^{\sf P}_{1},\ldots,\mathcal{M}^{\sf P}_{m}$ be an enumeration
of the models $\mathcal{M}^{\sf P}_{\bigwedge^{k-1}_{j=1}\psi_{j},\psi_{k}}$,
as above. That is, we take one model $\mathcal{M}^{\sf
P}_{\bigwedge^{k-1}_{l=1}\psi_{l},\psi_{k}}$ for each pair
$j=\bigwedge^{k-1}_{l=1}\psi_{l},\psi_{k}$ where $\mathcal{M}^{\sf
P}_{j}=(\mathcal{W}_{j},\\{\mathcal{N}_{j_{i}}\\}_{i\in I},\mathcal{V}_{j})$,
and let $w_{1},\ldots,w_{m}$ be an enumeration of the worlds
$w_{\bigwedge^{k-1}_{l=1}\psi_{l},\psi_{k}}$, with
$j=\bigwedge^{k-1}_{l=1}\psi_{l},\psi_{k}$ and $w_{j}\in\mathcal{W}_{j}$. We
assume without loss of generality that
$\mathcal{W}_{j}\cap\mathcal{W}_{k}=\emptyset$ for $j\neq k$.

In the following, we define a $\varphi$-consistent $\smash{\mathbf{C}}^{n}$
model $\mathcal{M}^{\sf P}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in
I},\mathcal{V})$ for $\varphi_{\sf prop}$. Intuitively, we construct
$\mathcal{M}^{\sf P}$ by taking the union of each $\mathcal{M}^{\sf P}_{j}$
with the addition of a new world $w$ that will satisfy $\varphi_{\sf prop}$.
We define $\mathcal{W}$ as $\bigcup_{1\leq j\leq
n}\mathcal{W}_{j}\cup\\{w\\}$, where $w$ is fresh. Before defining
$\mathcal{N}_{i}$ and $\mathcal{V}$, we define the function $J:{\sf
sub}(\varphi_{\sf prop})\rightarrow 2^{\mathcal{W}}$ with
$J(\psi)=\bigcup_{0\leq j\leq m}\mathcal{V}_{j}(\psi)$ for all $\psi\in{\sf
sub}(\varphi_{\sf prop})$, where $\mathcal{V}_{0}:{\sf
sub}(\varphi)\rightarrow 2^{\\{w\\}}$ is the function that assigns $\psi$ to
$\\{w\\}$, if $\nu(\psi)=1$, and to $\emptyset$, otherwise ($\mathcal{V}_{j}$,
for $1\leq j\leq m$, is as above). By construction, we have that
$J(\neg\psi)=\mathcal{W}\setminus J(\psi)$ and
$J(\psi_{1}\wedge\psi_{2})=J(\psi_{1})\cap J(\psi_{2})$. We define the
assignment $\mathcal{V}$ as the function $\mathcal{V}:{\sf
N_{P}}(\varphi)\rightarrow 2^{\mathcal{W}}$ satisfying
$\mathcal{V}(p_{\pi})=J(p_{\pi})$ for all $p_{\pi}\in{\sf N_{P}}(\varphi)$.

It remains to define $\mathcal{N}_{i}$, for $i\in I$. For
$u\in\mathcal{W}_{j}$ we first put $\alpha\subseteq W$ in $\mathcal{N}_{i}(u)$
precisely when $\mathcal{M}^{\sf P}_{j},u\models\Box_{i}\psi_{\alpha}$ and
$\alpha=J(\psi_{\alpha})$ for some $\Box_{i}\psi_{\alpha}\in{\sf
sub}(\varphi)$. Then, we close $\mathcal{N}_{i}$ under intersection so that
$\mathcal{M}^{\sf P}$ is a $\smash{\mathbf{C}}^{n}$ model. The next two claims
establish that $\mathcal{N}_{i}$ is as expected.

######  Claim 7.1.

If $\beta\in\mathcal{N}_{i}(u)$ and $\beta=J(\psi)$ for some
$\Box_{i}\psi\in{\sf sub}(\varphi_{\sf prop})$, then $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}\psi$.

Indeed, since $\beta=J(\psi)\in\mathcal{N}_{i}(u)$, we must have that
$\mathcal{M}^{\sf P}_{j},u\models\Box_{i}\psi_{1,\beta}$, …, $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}\psi_{m,\beta}$ and
$\beta=\bigcap^{m}_{l=1}J(\psi_{l,\beta})$ for some
$\Box_{i}\psi_{1,\beta},\ldots,\Box_{i}\psi_{m,\beta}\in{\sf sub}(\varphi_{\sf
prop})$. Since $\mathcal{N}_{i}$ is closed under intersection, in fact, we
have that $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}(\bigwedge^{m}_{l=1}\psi_{l,\beta})$. But since
$J(\psi)=\bigcap^{m}_{i=1}J(\psi_{i,\beta})$, we also have
$\mathcal{V}_{j}(\psi)=\bigcap^{m}_{l=1}\mathcal{V}_{j}(\psi_{l,\beta})$
(recall that $\mathcal{W}_{j}\cap\mathcal{W}_{k}=\emptyset$ for $k\neq j$), so
$\mathcal{M}^{\sf P}_{j},u\models\Box_{i}\psi$ iff $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}(\bigwedge^{m}_{l=1}\psi_{l,\beta})$. It follows that
$\mathcal{M}^{\sf P}_{j},u\models\Box_{i}\psi$.

Regarding the fresh world $w$ introduced above in $\mathcal{W}$, we first put
$\alpha\subseteq\mathcal{W}$ in $\mathcal{N}_{i}(w)$ precisely when
$\nu(\Box_{i}\psi_{\alpha})=1$ and $\alpha=J(\psi_{\alpha})$ for some
$\Box_{i}\psi_{\alpha}\in{\sf sub}(\varphi_{\sf prop})$. Then, we again close
$\mathcal{N}_{i}$ under intersection so that $\mathcal{M}^{\sf P}$ is a
$\smash{\mathbf{C}}^{n}$ model.

######  Claim 7.2.

If $\beta\in\mathcal{N}_{i}(w)$ and $\beta=J(\bigwedge^{k-1}_{l=1}\psi_{l})$
for some $\Box_{i}\psi_{1},\ldots,\Box_{i}\psi_{k-1}\in{\sf sub}(\varphi_{\sf
prop})$ then $\nu(\Box_{i}\psi_{l})=1$ for all $1\leq l<k$.

Indeed, since $\beta=J(\bigwedge^{k-1}_{l=1}\psi_{l})\in\mathcal{N}_{i}(w)$ we
must have that
$\nu(\Box_{i}\psi_{1,\beta})=1,\ldots,\nu(\Box_{i}\psi_{m,\beta})=1$ and
$\beta=\bigcap^{m}_{i=1}J(\psi_{i,\beta})$ for some
$\Box_{i}\psi_{1,\beta},\ldots,\Box_{i}\psi_{m,\beta}\in{\sf sub}(\varphi_{\sf
prop})$. Suppose now that $\nu(\bigwedge^{k-1}_{l=1}\psi_{l})=0$. Then, by
assumption, there exists a structure $\mathcal{M}^{\sf
P}_{j}=(\mathcal{W}_{j},\\{\mathcal{N}_{j_{i}}\\}_{i\in I},\mathcal{V}_{j})$
and a world $w_{j}\in\mathcal{W}_{j}$ such that $\mathcal{M}^{\sf
P}_{j},w_{j}\models(\bigwedge^{k-1}_{l=1}\psi_{l,\beta}\wedge\neg(\bigwedge^{k-1}_{l=1}\psi_{l}))\vee(\neg(\bigwedge^{k-1}_{l=1}\psi_{l,\beta})\wedge(\bigwedge^{k-1}_{l=1}\psi_{l}))$.
It follows that
$\mathcal{V}_{j}(\bigwedge^{k-1}_{l=1}\psi_{l,\beta})\neq\mathcal{V}_{j}(\bigwedge^{k-1}_{l=1}\psi_{l})$.
Consequently $J(\bigwedge^{k-1}_{l=1}\psi_{l,\beta})\neq
J(\bigwedge^{k-1}_{l=1}\psi_{l})$, which is a contradiction.

We now show by induction on the structure of formulas that $\mathcal{V}$ and
$J$ agree on ${\sf sub}(\varphi_{\sf prop})$. This holds by construction for
atomic propositions. It is easy to deal with propositional connectives, since
we know that $J(\neg\psi)=\mathcal{W}\setminus J(\neg\psi)$ and
$J(\psi_{1}\wedge\psi_{2})=J(\psi_{1})\cap J(\psi_{2})$ and similarly for
$\mathcal{V}$. Assume inductively that $\mathcal{V}(\psi)=J(\psi)$. Suppose
first that $u\in J(\Box_{i}\psi)$. Then, either $u=w$ and
$\nu(\Box_{i}\psi)=1$ or $u\in\mathcal{W}_{j}$ and $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}\psi$. In either case we have that
$J(\psi)\in\mathcal{N}_{i}(u)$. Since $\mathcal{V}(\psi)=J(\psi)$, it follows
that $\mathcal{M}^{\sf P},u\models\Box_{i}\psi$, that is,
$u\in\mathcal{V}(\Box_{i}\psi)$. Suppose now that
$u\in\mathcal{V}(\Box_{i}\psi)$, that is, $\mathcal{M}^{\sf
P},u\models\Box_{i}\psi$, or, equivalently,
$\mathcal{V}(\psi)\in\mathcal{N}_{i}(u)$. Since $\mathcal{V}(\psi)=J(\psi)$ it
follows that either $u=w$ and $\nu(\Box_{i}\psi)=1$ or $u\in\mathcal{W}_{j}$
and $\mathcal{M}^{\sf P}_{j},u\models\Box_{i}\psi$. In either case we have
that $u\in J(\Box_{i}\psi)$.

Since $\nu(\varphi_{\sf prop})=1$, we have that $w\in J(\varphi_{\sf prop})$,
and consequently $w\in\mathcal{V}(\varphi_{\sf prop})$. That is,
$\mathcal{M}^{\sf P},w\models\varphi_{\sf prop}$. The fact that
$\mathcal{M}^{\sf P}$ is a $\smash{\mathbf{C}}^{n}$ model follows from the
definition of $\mathcal{N}_{i}$. The fact that $\mathcal{M}^{\sf P}$ is a
$\varphi$-consistent model follows from the fact that $\nu$, used to construct
the assignment related to $w$, is $\varphi$-consistent and the models
$\mathcal{M}^{\sf P}_{1},\ldots,\mathcal{M}^{\sf P}_{m}$, used to define the
remaining worlds in $\mathcal{W}$, are all $\varphi$-consistent models. ∎

######  Lemma 8.

A formula $\varphi_{\sf prop}$ is satisfied in a $\varphi$-consistent
$\smash{\mathbf{N}^{n}}$ model iff there is a $\varphi$-consistent valuation
$\nu$ for $\varphi_{\sf prop}$ such that

  1. 1.

if $\Box_{i}\psi$ is in ${\sf sub}(\varphi_{\sf prop})$ and
$\nu(\Box_{i}\psi)=0$, then $\neg\psi$ is satisfied in a $\varphi$-consistent
$\smash{\mathbf{N}^{n}}$ model;

  2. 2.

if $\Box_{i}\psi_{1}$ and $\Box_{i}\psi_{2}$ are in ${\sf sub}(\varphi_{\sf
prop})$, $\nu(\Box_{i}\psi_{1})=1$, and $\nu(\Box_{i}\psi_{2})=0$, then
$(\psi_{1}\wedge\neg\psi_{2})\vee(\neg\psi_{1}\wedge\psi_{2})$ is satisfied in
a $\varphi$-consistent $\smash{\mathbf{N}^{n}}$ model.

###### Proof.

We start with proving ($\Rightarrow$). Suppose that $\varphi_{\sf prop}$ is
satisfied in a world $w$ of a $\varphi$-consistent $\smash{\mathbf{N}^{n}}$
model $\mathcal{M}^{\sf P}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in
I},\mathcal{V})$. That is, $\mathcal{M}^{\sf P},w\models\varphi_{\sf prop}$.
We define a $\varphi$-consistent valuation for $\varphi_{\sf prop}$ by setting
$\nu(\psi)=1$ if $\mathcal{M}^{\sf P},w\models\psi$ and $\nu(\psi)=0$ if
$\mathcal{M}^{\sf P},w\not\models\psi$. It is easy to check that $\nu$ is
indeed a $\varphi$-consistent valuation (given that $\mathcal{M}^{\sf P}$ is a
$\varphi$-consistent $\smash{\mathbf{N}^{n}}$ model).

Point 1. By definition, $\Box_{i}{\sf true}$ holds in $\smash{\mathbf{N}^{n}}$
models. Since there is a valuation $\nu$ such that $\nu(\Box_{i}\psi)=0$ we
have that $\psi$ cannot be true in all valuations (otherwise $\psi\equiv{\sf
true}$ would hold and $\nu$ would violate $\Box_{i}{\sf true}$ in
$\smash{\mathbf{N}^{n}}$ models). This means that $\neg\psi$ is
$\smash{\mathbf{N}^{n}}$ satisfiable.

Point 2. Assume that $\Box_{i}\psi_{1}$ and $\Box_{i}\psi_{2}$ are in ${\sf
sub}(\varphi_{\sf prop})$, $\nu(\Box_{i}\psi_{1})=1$ and
$\nu(\Box_{i}\psi_{2})=0$. Then $\mathcal{M}^{\sf P},w\models\Box_{i}\psi_{1}$
and $\mathcal{M}^{\sf P},w\not\models\Box_{i}\psi_{2}$. Thus, by definition,
$\mathcal{V}(\psi_{1})\in\mathcal{N}_{i}(w)$ and
$\mathcal{V}(\psi_{2})\not\in\mathcal{N}_{i}(w)$. So,
$\mathcal{V}(\psi_{1})\neq\mathcal{V}(\psi_{2})$. Then, there is a world $u$
in the symmetrical difference of these sets such that $\mathcal{M}^{\sf
P},u\models(\psi_{1}\wedge\neg\psi_{2})\vee(\neg\psi_{1}\wedge\psi_{2})$.

The proof of the converse ($\Leftarrow$) is as follows. Suppose there is a
$\varphi$-consistent valuation $\nu$ for $\varphi_{\sf prop}$ such that Point
1 and Point 2 hold. That is,

  * •

if $\Box_{i}\psi$ is in ${\sf sub}(\varphi_{\sf prop})$ and
$\nu(\Box_{i}\psi)=0$ then there is a $\varphi$-consistent
$\smash{\mathbf{N}^{n}}$ model $\mathcal{M}^{\sf
P}_{\psi}=(\mathcal{W}_{\psi},\\{\mathcal{N}_{{\psi}_{i}}\\}_{i\in
I},\mathcal{V}_{\psi})$ and a world $w_{\psi}\in\mathcal{W}_{\psi}$ such that
$\mathcal{M}^{\sf P}_{\psi},w_{\psi}\models\neg\psi$; and

  * •

if $\Box_{i}\psi_{1}$ and $\Box_{i}\psi_{2}$ are in ${\sf sub}(\varphi_{\sf
prop})$, $\nu(\Box_{i}\psi_{1})=1$, and $\nu(\Box_{i}\psi_{2})=0$, then there
is a $\varphi$-consistent $\smash{\mathbf{N}^{n}}$ model $\mathcal{M}^{\sf
P}_{\psi_{1},\psi_{2}}=(\mathcal{W}_{\psi_{1},\psi_{2}},\\{\mathcal{N}_{{\psi_{1},\psi_{2}}_{i}}\\}_{i\in
I},\mathcal{V}_{\psi_{1},\psi_{2}})$ and a world
$w_{\psi_{1},\psi_{2}}\in\mathcal{W}_{\psi_{1},\psi_{2}}$ such that
$\mathcal{M}^{\sf
P}_{\psi_{1},\psi_{2}},w_{\psi_{1},\psi_{2}}\models(\psi_{1}\wedge\neg\psi_{2})\vee(\neg\psi_{1}\wedge\psi_{2})$.

Let $\mathcal{M}^{\sf P}_{1},\ldots,\mathcal{M}^{\sf P}_{m}$ be an enumeration
of $\smash{\mathbf{N}^{n}}$ models $\mathcal{M}^{\sf P}_{\psi}$ and
$\mathcal{M}^{\sf P}_{\psi_{1},\psi_{2}}$, as above. That is, we take one
model $\mathcal{M}^{\sf P}_{\psi}$ and one model $\mathcal{M}^{\sf
P}_{\psi_{1},\psi_{2}}$ for each such subformula $j=\psi$ and pair of
subformulas $j=\psi_{1},\psi_{2}$ where $\mathcal{M}^{\sf
P}_{j}=(\mathcal{W}_{j},\\{\mathcal{N}_{j_{i}}\\}_{i\in I},\mathcal{V}_{j})$,
and let $w_{1},\ldots,w_{m}$ be an enumeration of the worlds $w_{\psi}$ and
$w_{\psi_{1},\psi_{2}}$, with $w_{j}\in\mathcal{W}_{j}$. Assume without loss
of generality that $\mathcal{W}_{j}\cap\mathcal{W}_{k}=\emptyset$ for $j\neq
k$. In the following, we define a $\varphi$-consistent
$\smash{\mathbf{N}^{n}}$ model $\mathcal{M}^{\sf
P}=(\mathcal{W},\\{\mathcal{N}_{i}\\}_{i\in I},\mathcal{V})$ for $\varphi_{\sf
prop}$.

Intuitively, we construct $\mathcal{M}^{\sf P}$ by taking the union of each
$\mathcal{M}^{\sf P}_{j}$ with the addition of a new world $w$ that will
satisfy $\varphi_{\sf prop}$. We define $\mathcal{W}$ as $\bigcup_{1\leq j\leq
n}\mathcal{W}_{j}\cup\\{w\\}$, where $w$ is fresh. Before defining
$\mathcal{N}_{i}$ and $\mathcal{V}$, we define the function $J:{\sf
sub}(\varphi_{\sf prop})\rightarrow 2^{\mathcal{W}}$ with
$J(\psi)=\bigcup_{0\leq j\leq m}\mathcal{V}_{j}(\psi)$ for all $\psi\in{\sf
sub}(\varphi_{\sf prop})$, where $\mathcal{V}_{0}:{\sf sub}(\varphi_{\sf
prop})\rightarrow 2^{\\{w\\}}$ is the function that assigns $\psi$ to
$\\{w\\}$, if $\nu(\psi)=1$, and to $\emptyset$, otherwise ($\mathcal{V}_{j}$,
for $1\leq j\leq m$, is as above). By construction, we have that
$J(\neg\psi)=\mathcal{W}\setminus J(\psi)$ and
$J(\psi_{1}\wedge\psi_{2})=J(\psi_{1})\cap J(\psi_{2})$. We define the
assignment $\mathcal{V}$ as the function $\mathcal{V}:{\sf
N_{P}}(\varphi)\rightarrow 2^{\mathcal{W}}$ satisfying
$\mathcal{V}(p_{\pi})=J(p_{\pi})$ for all $p_{\pi}\in{\sf N_{P}}(\varphi)$.

It remains to define $\mathcal{N}_{i}$, for $i\in I$. For
$u\in\mathcal{W}_{j}$ we put $\alpha\subseteq\mathcal{W}$ in
$\mathcal{N}_{i}(u)$ precisely when $\alpha=\mathcal{W}$, or,
$\alpha=J(\psi_{\alpha})$ and $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}\psi_{\alpha}$, for some $\Box_{i}\psi_{\alpha}\in{\sf
sub}(\varphi_{\sf prop})$. The next two claims establish that
$\mathcal{N}_{i}$ is as expected.

######  Claim 8.1.

If $\beta\in\mathcal{N}_{i}(u)$ and $\beta=J(\psi)$ for some
$\Box_{i}\psi\in{\sf sub}(\varphi_{\sf prop})$, then $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}\psi$.

###### Proof of Claim.

Indeed, since $\beta=J(\psi)\in\mathcal{N}_{i}(u)$, we must have that either
$\beta=\mathcal{W}$ or $\mathcal{M}^{\sf P}_{j},u\models\Box_{i}\psi_{\beta}$
and $\beta=J(\psi_{\beta})$ for some $\Box_{i}\psi_{\beta}\in{\sf
sub}(\varphi_{\sf prop})$. In the former case, as all $\mathcal{M}^{\sf
P}_{j}$ models are $\smash{\mathbf{N}^{n}}$ models, we have that
$\mathcal{M}^{\sf P}_{j},u\models\Box_{i}\psi$. In the latter, since
$J(\psi)=J(\psi_{\beta})$, we also have
$\mathcal{V}_{j}(\psi)=\mathcal{V}_{j}(\psi_{\beta})$ (recall that
$\mathcal{W}_{j}\cap\mathcal{W}_{k}=\emptyset$ for $k\neq j$), so
$\mathcal{M}^{\sf P}_{j},u\models\Box_{i}\psi$ iff $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}\psi_{\beta}$. It follows that $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}\psi$. ∎

Also, we put $\alpha\subseteq\mathcal{W}$ in $\mathcal{N}_{i}(w)$ (recall $w$
is the fresh world introduced above in $\mathcal{W}$) precisely when
$\alpha=\mathcal{W}$ or $\nu(\Box_{i}\psi_{\alpha})=1$ and
$\alpha=J(\psi_{\alpha})$ for some $\Box_{i}\psi_{\alpha}\in{\sf
sub}(\varphi_{\sf prop})$.

######  Claim 8.2.

If $\beta\in\mathcal{N}_{i}(w)$ and $\beta=J(\psi)$ for some
$\Box_{i}\psi\in{\sf sub}(\varphi_{\sf prop})$ then $\nu(\Box_{i}\psi)=1$.

###### Proof of Claim.

Indeed, since $\beta=J(\psi)\in\mathcal{N}_{i}(w)$ we must have that either
$\beta=\mathcal{W}$ or $\nu(\Box_{i}\psi_{\beta})=1$ and
$\beta=J(\psi_{\beta})$ for some $\Box_{i}\psi_{\beta}\in{\sf
sub}(\varphi_{\sf prop})$. Suppose that $\nu(\Box_{i}\psi)=0$ and
$\beta\neq\mathcal{W}$. Then, by assumption, there exists a
$\varphi$-consistent $\smash{\mathbf{N}^{n}}$ model $\mathcal{M}^{\sf
P}_{j}=(\mathcal{W}_{j},\\{\mathcal{N}_{j_{i}}\\}_{i\in I},\mathcal{V}_{j})$
and a world $w_{j}\in\mathcal{W}_{j}$ such that $\mathcal{M}^{\sf
P}_{j},w_{j}\models(\psi_{\beta}\wedge\neg\psi)\vee(\neg\psi_{\beta}\wedge\psi)$.
It follows that $\mathcal{V}_{j}(\psi_{\beta})\neq\mathcal{V}_{j}(\psi)$.
Consequently $J(\psi_{\beta})\neq J(\psi)$, which is a contradiction. Now,
suppose that $\nu(\Box_{i}\psi)=0$ and $\beta=\mathcal{W}$. By assumption,
there exists a $\varphi$-consistent $\smash{\mathbf{N}^{n}}$ model
$\mathcal{M}^{\sf P}_{j}=(\mathcal{W}_{j},\\{\mathcal{N}_{j_{i}}\\}_{i\in
I},\mathcal{V}_{j})$ and a world $w_{j}\in\mathcal{W}_{j}$ such that
$\mathcal{M}^{\sf P}_{j},w_{j}\models\neg\psi$. It follows that
$\mathcal{V}_{j}(\psi)\neq\mathcal{W}$. Consequently
$\beta=J(\psi)\neq\mathcal{W}$, which is a contradiction. Then,
$\nu(\Box_{i}\psi)=1$, as required. ∎

We now show by induction on the structure of formulas that $\mathcal{V}$ and
$J$ agree on ${\sf sub}(\varphi_{\sf prop})$. This holds by construction for
atomic propositions. It is easy to deal with propositional connectives, since
we know that $J(\neg\psi)=\mathcal{W}\setminus J(\neg\psi)$ and
$J(\psi_{1}\wedge\psi_{2})=J(\psi_{1})\cap J(\psi_{2})$ and similarly for
$\mathcal{V}$. Assume inductively that $\mathcal{V}(\psi)=J(\psi)$. Suppose
first that $u\in J(\Box_{i}\psi)$. Then, either $u=w$ and
$\nu(\Box_{i}\psi)=1$ or $u\in\mathcal{W}_{j}$ and $\mathcal{M}^{\sf
P}_{j},u\models\Box_{i}\psi$. In either case we have that
$J(\psi)\in\mathcal{N}_{i}(u)$. Since $\mathcal{V}(\psi)=J(\psi)$, it follows
that $\mathcal{M}^{\sf P},u\models\Box_{i}\psi$, that is,
$u\in\mathcal{V}(\Box_{i}\psi)$. Suppose now that
$u\in\mathcal{V}(\Box_{i}\psi)$, that is, $\mathcal{M}^{\sf
P},u\models\Box_{i}\psi$, or, equivalently,
$\mathcal{V}(\psi)\in\mathcal{N}_{i}(u)$. Since $\mathcal{V}(\psi)=J(\psi)$ it
follows that either $u=w$ and $\nu(\Box_{i}\psi)=1$ or $u\in\mathcal{W}_{j}$
and $\mathcal{M}^{\sf P}_{j},u\models\Box_{i}\psi$. In either case we have
that $u\in J(\Box_{i}\psi)$.

Since $\nu(\varphi_{\sf prop})=1$, we have that $w\in J(\varphi_{\sf prop})$,
and consequently $w\in\mathcal{V}(\varphi_{\sf prop})$. That is,
$\mathcal{M}^{\sf P},w\models\varphi_{\sf prop}$. The fact that
$\mathcal{M}^{\sf P}$ is $\varphi$-consistent follows from the fact that
$\nu$, used to construct the assignment related to $w$, is
$\varphi$-consistent and the models $\mathcal{M}^{\sf
P}_{1},\ldots,\mathcal{M}^{\sf P}_{m}$, used to define the remaining worlds in
$\mathcal{W}$, are all $\varphi$-consistent. The fact that $\mathcal{M}^{\sf
P}$ contains the unit is by construction, that is, we defined
$\mathcal{M}^{\sf P}$ so that for all $i\in[1,n]$ and all $w\in\mathcal{W}$,
we have that $\mathcal{W}\in\mathcal{N}_{i}(w)$. Thus, $\mathcal{M}^{\sf P}$
is a $\varphi$-consistent $\smash{\mathbf{N}^{n}}$ model that satisfies
$\varphi_{\sf prop}$, as required. ∎

To determine satisfiability of $\varphi_{\sf prop}$ in a $\varphi$-consistent
model, we use Lemma 6 and the characterizations above. To establish complexity
results, we use the fact that there are only quadratically many subformulas in
$\varphi_{\sf prop}$. Satisfiability in $\smash{\mathcal{ALC}}$ is ExpTime-
complete and so, one can determine in exponential time whether a valuation is
$\varphi$-consistent. For an ExpTime upper bound, one can deterministically
compute all possible $\varphi$-consistent valuations for
$(\bigwedge^{k-1}_{j=1}\psi_{j}\wedge\neg\psi_{k})$ (or
$(\psi_{1}\wedge\neg\psi_{2})$) and decide satisfiability of $\varphi_{\sf
prop}$ by a $\varphi$-consistent model using a bottom-up strategy (as in
[29]). Since satisfiability in $\smash{\mathcal{ALC}}$ is ExpTime-hard, our
upper bound is tight.

######  Theorem 9.

The $\smash{\mathbf{C}^{n\mid{\sf g}}_{\mathcal{ALC}}}$ and
$\smash{\mathbf{N}^{n\mid{\sf g}}_{\mathcal{ALC}}}$ formula satisfiability
problems on constant domain neighbourhood models are ExpTime-complete.

##  5 Discussion and Future Work

In this paper, we have presented first results on reasoning in non-normal
modal description logics. After providing motivations and preliminaries for
these logics, we have focused on the following two aspects. First, we have
introduced terminating, sound and complete tableaux algorithms for checking
satisfiability of multi-modal description logics formulas in varying domain
neighbourhood models based on classes of frames that characterise different
non-normal systems, that is, $\mathbf{E}^{n}$, $\mathbf{M}^{n}$,
$\mathbf{C}^{n}$, and $\mathbf{N}^{n}$. We have then studied the complexity of
the satisfiability problem restricted to fragments where modal operators can
be applied to formulas only (thus without modalised concepts) and interpreted
on neighbourhood models with constant domains. As future work, we plan to
investigate along the following directions.

First, we are interested in adapting our tableau algorithms to check
satisfiability of formulas on neighbourhood models with constant domains. This
requires to address the introduction of fresh 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 obtain 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 us to directly extract a model with
constant domain, since there would be no object in the domain of the world
associated with $S_{n}$ capable of representing $y$ correctly.

A possible solution could be to define a suitable notion of _quasimodel_ [27],
to equivalently characterise satisfiability on constant domain neighbourhood
models in terms of structures representing “abstractions” of the actual models
of a formula. The representation of domain objects across worlds would be
given in terms of suitably defined functions, called _runs_ , to guarantee
that they are well-behaved with respect to their modal properties, and that
they do not violate the constant domain assumption. A similar approach is
followed by Seylan and Erdur [23] and Seylan and Jamroga [25, 26], with
suitable “copies” of worlds introduced to address the problem of the
definition of runs. In these works, however, it is not made explicit how such
a definition should be carried out in detail. We conjecture that an approach
based on _marked variables_ , as illustrated in Gabbay et al. [27], can be
fruitfully adopted together with quasimodels to solve the issue of a constant
domain model extraction from a complete and clash-free completion set for a
formula.

In addition, we are interested in tight complexity results for
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ formula satisfiability, with respect
to varying and constant domain neighbourhood models. It is known that
$\smash{\mathcal{ALC}}$ formula satisfiability is ExpTime-complete. However,
we do not know whether the upper bound for
$\mathbf{L}^{n}_{\smash{\mathcal{ALC}}}$ formula satisfiability problem on
varying or constant domain neighbourhood models can be improved to ExpTime-
membership, for any
$\mathbf{L}\in\\{\mathbf{E},\mathbf{M},\mathbf{C},\mathbf{N}\\}$. It has to be
noted that, at the propositional level, the formula satisfiability problem for
the systems $\mathbf{E}$, $\mathbf{M}$, and $\mathbf{N}$ is known to be NP-
complete, with a rise to PSpace-completeness for systems containing
$\mathbf{C}$ [30].

Finally, we plan to consider satisfiability in other combinations and
extensions of non-normal modal description logics. This would naturally lead
us to consider both the straightforward cases of $\mathbf{MC}$, $\mathbf{MN}$
and $\mathbf{CN}$ of the classical cube [31], as well as other logics tailored
to applications in knowledge representation contexts. In particular, we intend
to investigate non-normal modal description logics in epistemic, coalitional,
and deontic settings.

## References

  * Ågotnes and Wáng [2021] T. Ågotnes, Y. N. Wáng,  Somebody knows,  in: KR, volume 18, 2021, pp. 2–11.
  * Balbiani et al. [2019] P. Balbiani, D. Fernández-Duque, E. Lorini,  The dynamics of epistemic attitudes in resource-bounded agents,  Studia Logica 107 (2019) 457–488.
  * Vardi [1986] M. Y. Vardi,  On epistemic logic and logical omniscience,  in: TARK, 1986, pp. 293–305.
  * Brown [1988] M. A. Brown,  On the logic of ability,  Journal of philosophical logic (1988) 1–26.
  * Elgesem [1997] D. Elgesem,  The modal logic of agency,  Nordic Journal of Philosophical Logic (1997).
  * Pauly [2002] M. Pauly,  A modal logic for coalitional power in games,  Journal of logic and computation 12 (2002) 149–166.
  * Troquard [2014] N. Troquard,  Reasoning about coalitional agency and ability in the logics of “bringing-it-about”,  Autonomous Agents and Multi-Agent Systems 28 (2014) 381–407.
  * Anglberger et al. [2015] A. J. Anglberger, N. Gratzl, O. Roy,  Obligation, free choice, and the logic of weakest permissions,  Rev. Symb. Logic 8 (2015) 807–827.
  * Goble [2013] L. Goble,  Prima facie norms, normative conflicts, and dilemmas,  Handbook of deontic logic and normative systems 1 (2013) 241–351.
  * Von Wright [1951] G. H. Von Wright,  Deontic logic,  Mind 60 (1951) 1–15.
  * Ross [1944] A. Ross,  Imperatives and logic,  Philosophy of Science 11 (1944) 30–46.
  * Åqvist [1967] L. Åqvist,  Good samaritans, contrary-to-duty imperatives, and epistemic obligations,  Noûs 1 (1967) 361–379.
  * Forrester [1984] J. W. Forrester,  Gentle murder, or the adverbial samaritan,  The Journal of Philosophy 81 (1984) 193–197.
  * Lewis et al. [1959] C. I. Lewis, C. H. Langford, P. Lamprecht, Symbolic logic, volume 170, Dover Publications New York, 1959\.
  * Lemmon and Scott [1977] E. J. Lemmon, D. Scott, An Introduction to Modal logic, Blackwell, 1977\.
  * Kripke [2014] S. A. Kripke,  Semantical analysis of modal logic II: Non-normal modal propositional calculi,  in: The theory of models, Elsevier, 2014, pp. 206–220.
  * Scott [1970] D. Scott,  Advice on modal logic,  in: Philosophical problems in logic, Springer, 1970, pp. 143–173.
  * Montague [1970] R. Montague,  Universal grammar,  Theoria 36 (1970) 373–398.
  * Segerberg [1971] K. Segerberg,  An essay in classical modal logic (1971).
  * Chellas [1980] B. F. Chellas, Modal logic: an introduction, Cambridge University Press, 1980\.
  * Arló-Costa [2002] H. L. Arló-Costa,  First Order Extensions of Classical Systems of Modal Logic; The role of the Barcan schemas,  Stud. Logica 71 (2002) 87–118.
  * Arló-Costa and Pacuit [2006] H. L. Arló-Costa, E. Pacuit,  First-order classical modal logic,  Stud. Logica 84 (2006) 171–210.
  * Seylan and Erdur [2009] I. Seylan, R. C. Erdur,  A tableau decision procedure for $\mathcal{ALC}$ with monotonic modal operators and constant domains,  ENTCS 231 (2009) 113–130.
  * Dalmonte et al. [2019] T. Dalmonte, A. Mazzullo, A. Ozaki,  On non-normal modal description logics,  in: DL, 2019.
  * Seylan and Jamroga [2009] I. Seylan, W. Jamroga,  Description logic for coalitions,  in: AAMAS, 2009, pp. 425–432.
  * Seylan and Jamroga [2010] I. Seylan, W. Jamroga,  Coalition description logic with individuals,  ENTCS 262 (2010) 231–248.
  * Gabbay et al. [2003] D. M. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Many-dimensional Modal Logics: Theory and Applications, Elsevier, 2003.
  * Dalmonte et al. [2021] T. Dalmonte, B. Lellmann, N. Olivetti, E. Pimentel,  Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity,  Journal of Logic and Computation 31 (2021) 67–111.
  * Baader et al. [2012] F. Baader, S. Ghilardi, C. Lutz,  LTL over description logic axioms,  ACM T. Comput. Logic 13 (2012) 21:1–21:32.
  * Vardi [1989] M. Y. Vardi,  On the complexity of epistemic reasoning,  in: LICS, 1989, pp. 243–252.
  * Lellmann and Pimentel [2019] B. Lellmann, E. Pimentel,  Modularisation of sequent calculi for normal and non-normal modalities,  ACM Trans. Comput. Log. 20 (2019) 7:1–7:46.