$(x^{\prime}{\hskip 1.5pt:\hskip 2.0pt}\Phi)\notin S$,
then set $S\mathrel{\,:=\,}S\cup\\{x^{\prime}{\hskip 1.5pt:\hskip
2.0pt}\Phi\\}$. $\mathbf{R}_{g}$ If $(x{\hskip 1.5pt:\hskip
2.0pt}\mathbf{G})\in S$ but $(x^{\prime}{\hskip 1.5pt:\hskip
2.0pt}\mathbf{G})\notin S$,
then set $S\mathrel{\,:=\,}S\cup\\{x^{\prime}{\hskip 1.5pt:\hskip
2.0pt}\mathbf{G}\\}$. $\mathbf{R}_{a}$ If $\\{x{\hskip 1.5pt:\hskip 2.0pt}a,\
x{\hskip 1.5pt:\hskip 2.0pt}C(a)\\}\subseteq S$ but $(x{\hskip 1.5pt:\hskip
2.0pt}C)\notin S$,
then set $S\mathrel{\,:=\,}S\cup\\{x{\hskip 1.5pt:\hskip 2.0pt}C\\}$.
$\mathbf{R}_{\mathop{\lozenge}}$ If $(x{\hskip 1.5pt:\hskip
2.0pt}\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}C)\in S$ and
$\\{x^{\prime}{\hskip 1.5pt:\hskip 2.0pt}\hbox{$\mathsf{s}$},\
x^{\prime}{\hskip 1.5pt:\hskip 2.0pt}C\\}\nsubseteq S$ for all $x^{\prime}$ in
$S$, then create a fresh variable $x^{\prime}$ and set
$S\mathrel{\,:=\,}S\cup\\{x^{\prime}{\hskip 1.5pt:\hskip 2.0pt}C,\
x^{\prime}{\hskip 1.5pt:\hskip 2.0pt}\hbox{$\mathsf{s}$},\ x^{\prime}{\hskip
1.5pt:\hskip 2.0pt}*,\ x^{\prime}{\hskip 1.5pt:\hskip 2.0pt}\top\\}$. Global
non-generating (GN) rules: $\mathbf{R}_{\downarrow}$ If $(x{\hskip
1.5pt:\hskip 2.0pt}C){\,\in\,}\mathscr{S}(\varepsilon)$,
$\langle\varepsilon^{\prime}\\!,x^{\prime}\\!,\varepsilon,x,R\rangle{\,\in\,}\mathscr{R}$,
and $\exists R.C{\,\in\,}\mathsf{C}_{\mathcal{K}}$, but $(x^{\prime}\\!{\hskip
1.5pt:\hskip 2.0pt}\exists R.C){\,\notin\,}\mathscr{S}(\varepsilon^{\prime})$,
then set
$\mathscr{S}(\varepsilon^{\prime})\mathrel{\,:=\,}\mathscr{S}(\varepsilon^{\prime})\cup\\{x^{\prime}{\hskip
1.5pt:\hskip 2.0pt}\exists R.C\\}$. $\mathbf{R}_{r}$ If $\\{x{\hskip
1.5pt:\hskip 2.0pt}a,\ x{\hskip 1.5pt:\hskip
2.0pt}R(a,b)\\}\subseteq\mathscr{S}(\varepsilon)$ and $(x^{\prime}{\hskip
1.5pt:\hskip 2.0pt}b)\in\mathscr{S}(\varepsilon^{\prime})$, but
$\langle\varepsilon,x,\varepsilon^{\prime},x,R\rangle\notin\mathscr{R}$, then
set
$\mathscr{S}(\varepsilon^{\prime})\mathrel{\,:=\,}\mathscr{S}(\varepsilon^{\prime}){\,\cup\,}\\{x{\hskip
1.5pt:\hskip 2.0pt}\top\\}{\,\cup\,}\\{x{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$}\mid\hbox{$\mathsf{s}$}\in\mathsf{st}_{\varepsilon}(x)\\}$
and
$\mathscr{R}\mathrel{\,:=\,}\mathscr{R}{\,\cup\,}\\{\langle\varepsilon,x,\varepsilon^{\prime}\\!,x,R\rangle\\}$.
$\mathbf{R}_{r^{\prime}}\\!$ If $\\{x{\hskip 1.5pt:\hskip 2.0pt}b,\ x{\hskip
1.5pt:\hskip 2.0pt}R(a,b)\\}\subseteq\mathscr{S}(\varepsilon)$ and
$(x^{\prime}{\hskip 1.5pt:\hskip
2.0pt}a)\in\mathscr{S}(\varepsilon^{\prime})$, but
$\langle\varepsilon^{\prime},x,\varepsilon,x,R\rangle\notin\mathscr{R}$, then
set
$\mathscr{S}(\varepsilon^{\prime})\mathrel{\,:=\,}\mathscr{S}(\varepsilon^{\prime})\cup\\{x{\hskip
1.5pt:\hskip 2.0pt}\top\\}\cup\\{x{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$}\mid\hbox{$\mathsf{s}$}\in\mathsf{st}_{\varepsilon}(x)\\}$
and
$\mathscr{R}\mathrel{\,:=\,}\mathscr{R}\cup\\{\langle\varepsilon^{\prime},x,\varepsilon,x,R\rangle\\}$.
$\mathbf{R}_{\exists^{\prime}}\\!$ If $(x{\hskip 1.5pt:\hskip 2.0pt}\exists
R.C)\in\mathscr{S}(\varepsilon)$,
$(C,\mathsf{st}_{\varepsilon}(x),x^{\prime})\in\mathscr{L}(\varepsilon^{\prime})$
with $\varepsilon\neq\varepsilon^{\prime}$ or $x=x^{\prime}$, but
$\langle\varepsilon,x,\varepsilon^{\prime\prime}\\!,x^{\prime\prime}\\!,R\rangle\notin\mathscr{R}$
whenever
$(C,\mathsf{st}_{\varepsilon}(x),x^{\prime\prime})\in\mathscr{L}(\varepsilon^{\prime\prime})$
and $\varepsilon{\,\neq\,}\varepsilon^{\prime\prime}$ or
$x{\,=\,}x^{\prime\prime}$, then set
$\mathscr{R}\mathrel{\,:=\,}\mathscr{R}\cup\\{\langle\varepsilon,x,\varepsilon^{\prime},x^{\prime},R\rangle\\}$.
Global generating (GG) rule: $\mathbf{R}_{\exists}$ If$(x{\hskip 1.5pt:\hskip
2.0pt}\exists R.C)\in\mathscr{S}(\varepsilon)$, but
$\langle\varepsilon,x,\varepsilon^{\prime\prime}\\!,x^{\prime\prime}\\!,R\rangle\notin\mathscr{R}$
whenever
$(C,\mathsf{st}_{\varepsilon}(x),x^{\prime\prime})\in\mathscr{L}(\varepsilon^{\prime\prime})$
and $\varepsilon{\,\neq\,}\varepsilon^{\prime\prime}$ or
$x{\,=\,}x^{\prime\prime}$,
then create $\varepsilon^{\prime}$ and a fresh variable $x^{\prime}$, and then
set
$\mathscr{L}(\varepsilon^{\prime})\mathrel{\,:=\,}\\{(C,\mathsf{st}_{\varepsilon}(x),x^{\prime})\\}$,
$\mathscr{S}(\varepsilon^{\prime}){\mathrel{\,:=\,}}S_{0}^{\mathcal{K}}{\,\cup\,}\\{x^{\prime}\\!{\hskip
1.5pt:\hskip 2.0pt}C,\,x^{\prime}\\!{\hskip 1.5pt:\hskip
2.0pt}\\!\top\\}{\,\cup\,}\\{x^{\prime}\\!{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$}\mid\hbox{$\mathsf{s}$}{\,\in\,}\mathsf{st}_{\varepsilon}(x)\\}$,
$\mathscr{R}{\mathrel{\,:=\,}}\mathscr{R}{\,\cup\,}\\{\langle\varepsilon,x,\varepsilon^{\prime}\\!\\!,x^{\prime}\\!\\!,R\rangle\\}$.

Figure 1: The tableau completion rules. $\mathbf{G}$ can be of the form $a$,
$(\hbox{$\mathsf{s}$}\preceq\hbox{$\mathsf{s^{\prime}}$})$, or
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}\phi$. $\Phi$ may denote any
element of $\mathsf{SF}_{\mathcal{K}}\cup\mathsf{C}_{\mathcal{K}}$.

For convenience of presentation, we use the shortcut
$\mathsf{st}_{\varepsilon}(v)$ for $\mathsf{st}_{\mathscr{S}(\varepsilon)}(v)$
and for any
$\mathbf{CG}=\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R}\right\rangle$}$,
we will refer to all $\varepsilon\in\Delta$ simply as elements of
$\mathbf{CG}$.

$\mathbf{CG}$ is said to be _locally complete_ iff for every element
$\varepsilon$ in $\mathbf{CG}$, $\mathscr{S}(\varepsilon)$ is complete, and we
call $\mathbf{CG}$ _globally complete_ iff it is locally complete and no
global completion rule (see Figure 1) is applicable to $\mathbf{CG}$ as a
whole.

Intuitively, the next definition poses some global requirements for
$\mathbf{CG}$ to warrant its eligibility as a model-substitute.

######  Definition 5 (Coherence).

Let
$\mathbf{CG}=\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R}\right\rangle$}$
be a completion graph for $\mathcal{K}$. $\mathbf{CG}$ is called _coherent_
iff

  * •

for each $a\in\mathsf{IN}_{\mathcal{K}}$ there is a unique element
$\varepsilon_{a}\in\Delta$ such that $(v{\hskip 1.5pt:\hskip
2.0pt}a)\in\mathscr{S}(\varepsilon_{a})$ for all variables $v$ in
$\mathscr{S}(\varepsilon_{a})$,

  * •

for each $\varepsilon,\varepsilon^{\prime}\in\Delta$ and each variable $v$
contained in $\mathscr{S}(\varepsilon)$, $\mathscr{S}(\varepsilon^{\prime})$
contains some $v^{\prime}$ such that
$\mathsf{st}_{\varepsilon}(v)=\mathsf{st}_{\varepsilon^{\prime}}(v^{\prime})$,
and

  * •

if $(v{\hskip 1.5pt:\hskip 2.0pt}\phi){\in}\mathscr{S}(\varepsilon)$ and
$\mathsf{st}_{\varepsilon}(v){=}\mathsf{st}_{\varepsilon^{\prime}}(v^{\prime})$,
then $(v^{\prime}\\!{\hskip 1.5pt:\hskip
2.0pt}\phi){\in}\mathscr{S}(\varepsilon^{\prime})$.

❑

As usual in tableaux, inconsistencies emerge as clashes.

######  Definition 6 (Clash).

A _clash_ is a constraint of the form $(x{\hskip 1.5pt:\hskip 2.0pt}\bot)$. A
completion graph $\mathbf{CG}$ is said to _contain a clash_ iff
$\mathscr{S}(\varepsilon)$ does for some $\varepsilon$ in $\mathbf{CG}$.
Constraint systems or completion graphs not containing clashes are called
_clash-free_.  ❑

###  3.0.1 The Algorithm

To decide whether a given $\mathbb{S}_{\mathcal{E\\!L}}$ knowledge base
$\mathcal{K}$ in normal form is satisfiable, we form the initial completion
graph $\mathbf{CG}_{I}$ with $\mathscr{R}=\emptyset$ and $\Delta$ consisting
of an element $\varepsilon_{\top}$ with
$\mathscr{L}(\varepsilon_{\top})=\emptyset$ and
$\mathscr{S}(\varepsilon_{\top})=S_{0}^{\mathcal{K}}$, and for every
$a\in\mathsf{IN}_{\mathcal{K}}$ an element $\varepsilon_{a}$ with
$\mathscr{L}(\varepsilon_{a})=\emptyset$ and
$\mathscr{S}(\varepsilon_{a})=S_{0}^{\mathcal{K}}\cup\\{(x_{\hbox{$\mathsf{s}$}}{\hskip
1.5pt:\hskip 2.0pt}a)\mid(x_{\hbox{$\mathsf{s}$}}{\hskip 1.5pt:\hskip
2.0pt}\top)\in S_{0}^{\mathcal{K}}\\}$.

After that, we repeatedly apply the local and global completion rules from
Figure 1, where LL rules have the highest priority, followed by LC, GN, and GG
rules, in that order. After each rule application, we check if $\mathbf{CG}$
contains a clash and terminate with answer “unsatisfiable” should this be the
case. If we arrive at a clash-free $\mathbf{CG}$ with no more rules
applicable, the algorithm terminates and returns “satisfiable”.

###  3.0.2 Quasi-Models and Quasi-Satisfiability

This section sketches how special structures, called (dual) quasi-models can
serve as proxies for proper $\mathbb{S}_{\mathcal{E\\!L}}$ models.

######  Definition 7 (Run, Quasi-model).

Let
$\mathbf{CG}{\,=\,}\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\\!\mathscr{R}\right\rangle$}$
be a completion graph. A _run_ $r$ in $\mathbf{CG}$ is a function mapping each
element $\varepsilon\in\Delta$ to a variable of $\mathscr{S}(\varepsilon)$,
such that

  1. C1

if $(r(\varepsilon){\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$})\in\mathscr{S}(\varepsilon)$, then
$(r(\varepsilon^{\prime}){\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$})\in\mathscr{S}(\varepsilon^{\prime})$
for all $\varepsilon,\varepsilon^{\prime}\in\Delta$ and
$\hbox{$\mathsf{s}$}\in\mathsf{ST}_{\mathcal{K}}$,

  2. C2

if
$\mbox{$\left\langle\varepsilon,v,\varepsilon^{\prime}\\!,v^{\prime}\\!,R\right\rangle$}\in\mathscr{R}$
and $r(\varepsilon)=v$, then $r(\varepsilon^{\prime})=v^{\prime}\\!$, and

  3. C3

if $(r(\varepsilon){\hskip 1.5pt:\hskip 2.0pt}\exists
R.C)\in\mathscr{S}(\varepsilon)$, there exists some
$\varepsilon^{\prime}\in\Delta$ with
$\mbox{$\left\langle\varepsilon,r(\varepsilon),\varepsilon^{\prime}\\!,r(\varepsilon^{\prime}),R\right\rangle$}\in\mathscr{R}$
and $(r(\varepsilon^{\prime}){\hskip 1.5pt:\hskip
2.0pt}C)\in\mathscr{S}(\varepsilon^{\prime})$.

A _quasi-model_ of $\mathcal{K}$ is a tuple
$\mathcal{Q}=\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R},\Upgamma\right\rangle$}$
where $\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R}\right\rangle$ is
a globally complete, coherent and clash-free completion graph for
$\mathcal{K}$, and $\Upgamma$ a set of runs in
$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R}\right\rangle$ such
that for every $\varepsilon\in\Delta$ and variable $v$ in
$\mathscr{S}(\varepsilon)$, there is a run $r$ in $\Upgamma$ such that
$r(\varepsilon)=v$. $\mathcal{K}$ is called _quasi-satisfiable_ iff
$\mathcal{K}$ has a quasi-model.  ❑

In a nutshell, runs serve the purpose of lining up “compatible” variables, one
from each individual constraint system, in such a way that precisifications
can be constructed. With these notions in place, we can establish the desired
result.

######  Theorem 2.

A $\mathbb{S}_{\mathcal{E\\!L}}$ knowledge base $\mathcal{K}$ is satisfiable
iff it is quasi-satisfiable.

###### Proof.

_(sketch)_ We prove the correspondence by showing that every quasi-model gives
rise to a model and vice versa.
($\Leftarrow$) Given a quasi-model
$\mathcal{Q}=\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R},\Upgamma\right\rangle$}$
of $\mathcal{K}$, we obtain a model
$\mathfrak{D}=\mbox{$\left\langle\Delta,\Pi,\sigma,\gamma\right\rangle$}$ by
letting $\Pi=\Upgamma$,
$\sigma(\hbox{$\mathsf{s}$})=\\{r\mid(r(\varepsilon){\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$})\in\mathscr{S}(\varepsilon)\\}$,
$C^{\gamma(r)}=\\{\varepsilon\mid(r(\varepsilon){\hskip 1.5pt:\hskip
2.0pt}C)\in\mathscr{S}(\varepsilon)\\}$ for $C\in\mathsf{BC}_{\mathcal{K}}$,
$R^{\gamma(r)}=\\{(\varepsilon,\varepsilon^{\prime})\mid\langle\varepsilon,r(\varepsilon),\varepsilon^{\prime},r(\varepsilon^{\prime}),R\rangle\in\mathscr{R}\\}$
and $a^{\gamma(r)}=\varepsilon_{a}$ for all $a\in\mathsf{IN}_{\mathcal{K}}$.
($\Rightarrow$) Given a model
$\mathfrak{D}=\mbox{$\left\langle\Delta,\Pi,\sigma,\gamma\right\rangle$}$ of
$\mathcal{K}$, we obtain a quasi-model
$\mathcal{Q}=\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R},\Upgamma\right\rangle$}$
as follows: Let $P\mathrel{\,:=\,}\Pi\cup\mathsf{ST}_{\mathcal{K}}$ and for
$p\in P$, let $\bar{p}$ denote some arbitrary but fixed $\pi\in\sigma(p)$ if
$p\in\mathsf{ST}_{\mathcal{K}}$, and otherwise $\bar{p}=p$. Finally, let

$\displaystyle\mathscr{S}(\varepsilon)\mathrel{\,:=\,}$
$\displaystyle\\{v_{p}{\hskip 1.5pt:\hskip 2.0pt}C\mid\varepsilon\in
C^{\gamma(\bar{p})},p\in P\\}\cup\\{v_{p}{\hskip 1.5pt:\hskip
2.0pt}a\mid\varepsilon=a^{\gamma(\bar{p})},p\in P\\}$
$\displaystyle\cup\\{v_{p}{\hskip 1.5pt:\hskip
2.0pt}\phi\mid\mathfrak{D},\bar{p}\models\phi,\
\phi\in\mathsf{SF}_{\mathcal{K}}\\}\cup\\{v_{p}{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$}\mid\bar{p}\in\sigma(\hbox{$\mathsf{s}$})\\}$
$\displaystyle\mathscr{L}(\varepsilon)\mathrel{\,:=\,}$
$\displaystyle\\{(C,\\!\\{\hbox{$\mathsf{s}$}\mid\bar{p}{\in}\sigma(\hbox{$\mathsf{s}$})\\}\\!,\\!v_{p})\mid\exists
R.C{\in}\mathsf{C}_{\mathcal{K}},(\varepsilon^{\prime}\\!\\!,\varepsilon){\in}R^{\gamma(\bar{p})}\\!\\!,\varepsilon{\in}C^{\gamma(\bar{p})}\\}$
$\displaystyle\mathscr{R}\mathrel{\,:=\,}$
$\displaystyle\\{\mbox{$\left\langle\varepsilon,v_{p},\varepsilon^{\prime},v_{p},R\right\rangle$}\mid(\varepsilon,\varepsilon^{\prime})\in
R^{\gamma(\bar{p})}\\}$ $\displaystyle\Upgamma\mathrel{\,:=\,}$
$\displaystyle\\{\\{\varepsilon\mapsto v_{p}\mid\varepsilon\in\Delta\\}\mid
p\in P\\}.$

###  3.0.3 Polytime Termination and Correctness

Next, we give an overview of our argument why our algorithm runs in polynomial
time with respect to $\left\lVert\mathcal{K}\right\rVert$, the size of its
input $\mathcal{K}$. We observe that the number $|\Delta|$ of domain elements
of any completion graph $\mathbf{CG}$ constructed by our algorithm is bounded
by $3\left\lVert\mathcal{K}\right\rVert^{2}$ (${\dagger}$). We also find that
the number of variables used in any single $\mathscr{S}(\varepsilon)$ is
bounded by $2\left\lVert\mathcal{K}\right\rVert^{2}$ and the number of
constraints in $\mathscr{S}(\varepsilon)$ by
$2\left\lVert\mathcal{K}\right\rVert^{3}$ (${\ddagger}$). Now, the number of
applications of $\mathbf{R}_{\exists}$ is bounded by the number of elements in
each completion graph, i.e. at most $3\left\lVert\mathcal{K}\right\rVert^{2}$
in view of (${\dagger}$). Since the rules $\mathbf{R}_{\preceq}$,
$\mathbf{R}_{\sqcap}$, $\mathbf{R}_{\sqsubseteq}$,
$\mathbf{R}_{\mathop{\square}}$, $\mathbf{R}_{\mathop{\lozenge}}$,
$\mathbf{R}_{g}$, $\mathbf{R}_{a}$, $\mathbf{R}_{r}$,
$\mathbf{R}_{r^{\prime}}$ and $\mathbf{R}_{\downarrow}$ produce one or more
new constraints in an element, the number of applications of such rules per
element is bounded by $2\left\lVert\mathcal{K}\right\rVert^{3}$ due to
(${\ddagger}$). $\mathbf{R}_{\exists^{\prime}}$ can add, for each
$\varepsilon$ with $(C,s,x)\in\mathscr{L}(\varepsilon)$, at most one quasi-
role from every variable in every element, thus we have at most
$6\left\lVert\mathcal{K}\right\rVert^{4}$ rule applications. The total number
of rule applications is bounded by the rule applications per element
multiplied by the bound on elements, together with the bound on
$\mathbf{R}_{\exists}$, which gives us

$(6\\!\left\lVert\mathcal{K}\right\rVert^{4})(3\\!\left\lVert\mathcal{K}\right\rVert^{2})+(2\\!\left\lVert\mathcal{K}\right\rVert^{3})(3\\!\left\lVert\mathcal{K}\right\rVert^{2})+3\\!\left\lVert\mathcal{K}\right\rVert^{2}\leq(27\\!\left\lVert\mathcal{K}\right\rVert^{6}).$

######  Theorem 3.

The completion algorithm terminates after at most
$c\left\lVert\mathcal{K}\right\rVert^{6}$ steps, where $c$ is a constant.

As every single rule application can be clearly executed in polynomial time
with respect to $\mathcal{K}$, we can conclude that our algorithm runs in
polynomial time.

We are now ready to establish correctness of our decision algorithm, by
showing its soundness and completeness. For both directions, Theorem 2 will
come in handy. As usual, the soundness part of our argument is the easier one.

######  Theorem 4 (Soundness).

If there is a globally complete, coherent and clash-free completion graph
$\mathbf{CG}$ for a knowledge base $\mathcal{K}$, then $\mathcal{K}$ is
satisfiable.

###### Proof.

_(sketch)_ Given
$\mathbf{CG}=\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R}\right\rangle$}$,
let $\Upgamma$ consist of all runs on $\mathbf{CG}$. Then we can show that
$\mathcal{Q}=\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R},\Upgamma\right\rangle$}$
constitutes a quasi-model for $\mathcal{K}$, so we can conclude by Theorem 2
that $\mathcal{K}$ is satisfiable.

Proving completeness requires significantly more work. We make use of a notion
that, intuitively, formalizes the idea that a completion graph $\mathbf{CG}$
under development is “in sync” with a quasi-model $\mathcal{Q}$ of the same
knowledge base, where $\mathcal{Q}$ can be conceived as a model-theoretic
“upper bound” of $\mathbf{CG}$.

######  Definition 8 ($\mathcal{Q}$-compatibility).

Let $\mathcal{K}$ be a $\mathbb{S}_{\mathcal{E\\!L}}$ knowledge base and
$\mathcal{Q}=\mbox{$\left\langle\Delta^{q},\mathscr{S}^{q},\mathscr{L}^{q},\mathscr{R}^{q},\Upgamma^{q}\right\rangle$}$
be a quasimodel for $\mathcal{K}$. A completion graph
$\mathbf{CG}=\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R}\right\rangle$}$
for $\mathcal{K}$ is called _$\mathcal{Q}$ -compatible_ iff there is a left-
total relation $\mu\subseteq\Delta\times\Delta^{q}$ where

  * •

for all $g\in\Delta$ and $\varepsilon\in\Delta^{q}$, if both
$\mathscr{L}(g)\subseteq\mathscr{L}^{q}(\varepsilon)$ and $\\{a\mid(x{\hskip
1.5pt:\hskip
2.0pt}a){\,\in\,}\mathscr{S}(g)\\}{\,\subseteq\,}\\{a\mid(v{\hskip
1.5pt:\hskip 2.0pt}a){\,\in\,}{\mathscr{S}^{q}}(\varepsilon)\\}$, then
$(g,\\!\varepsilon){\,\in\,}\mu$,

  * •

for each $(g,\varepsilon)\in\mu$ there is a surjective function
$\mu_{g,\varepsilon}$ from the variables in ${\mathscr{S}^{q}}(\varepsilon)$
to the variables in $\mathscr{S}(g)$ such that

    * –

$(\mu_{g,\varepsilon}(v){\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$})\in\mathscr{S}(g)$ implies $(v{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$})\in{\mathscr{S}^{q}}(\varepsilon)$,

    * –

$(\mu_{g,\varepsilon}(v){\hskip 1.5pt:\hskip 2.0pt}\Phi)\in\mathscr{S}(g)$
implies $(v{\hskip 1.5pt:\hskip 2.0pt}\Phi)\in{\mathscr{S}^{q}}(\varepsilon)$,

    * –

if $\mbox{$\left\langle
g,x,g^{\prime},x^{\prime},R\right\rangle$}\in\mathscr{R}$ then
$\mbox{$\left\langle\varepsilon,\\!y,\\!\varepsilon^{\prime},\\!y^{\prime},\\!R\right\rangle$}\\!\in\\!\mathscr{R}^{q}$
for some $(g,\varepsilon),(g^{\prime}\\!,\varepsilon^{\prime})\in\mu$ with
$\mu_{g,\varepsilon}(y){=}x$ and
$\mu_{g^{\prime},\varepsilon^{\prime}}(y^{\prime}){=}x^{\prime}$.

❑

With this definition, we can establish two important insights:

  * •

The tableau algorithm’s initial completion graph $\mathbf{CG}_{I}$ is
$\mathcal{Q}$-compatible for any quasimodel $\mathcal{Q}$ of $\mathcal{K}$.

  * •

Applications of tableau rules preserve $\mathcal{Q}$-compatiblility.

This entails that the completion graph maintained in the algorithm will be
$\mathcal{Q}$-compatible at all times, thus also upon termination. We exploit
this insight to show completeness.

######  Theorem 5 (Completeness).

If a $\mathbb{S}_{\mathcal{E\\!L}}$ knowledge base $\mathcal{K}$ is
satisfiable, the tableau algorithm will construct a globally complete,
coherent, and clash-free completion graph for $\mathcal{K}$.

###### Proof.

If $\mathcal{K}$ is satisfiable then by Theorem 2, there is a quasi-model
$\mathcal{Q}$ for $\mathcal{K}$. According to Theorem 3, we can obtain a
globally complete completion graph $\mathbf{CG}$ after polynomially many
applications of the tableau rules, which, as just discussed, is
$\mathcal{Q}$-compatible. It must thus also be clash-free, because otherwise
there were an element $g$ and variable $x$, with $(x{\hskip 1.5pt:\hskip
2.0pt}\bot)\in\mathscr{S}(g)$, and thus there is $(g,\varepsilon)\in\mu$ and
$\mu_{g,\varepsilon}$ such that $(\mu_{g,\varepsilon}(x){\hskip 1.5pt:\hskip
2.0pt}\bot)\in{\mathscr{S}^{q}}(\varepsilon)$, which is a contradiction
because $\mathcal{Q}$ is a quasi-model. It is not hard to show that
$\mathbf{CG}$ is also coherent, whence we can conclude that $\mathbf{CG}$ is a
globally complete, coherent, and clash-free completion graph for
$\mathcal{K}$.

Together with the well-known PTime-hardness of the satisfiability problem in
(standpoint-free) $\mathcal{E\\!L}$, we have therefore established PTime-
completeness of $\mathbb{S}_{\mathcal{E\\!L}}$ and exhibited a worst-case
optimal algorithm for it.

##  4 Intractable Extensions

While the shown tractability of reasoning in $\mathbb{S}_{\mathcal{E\\!L}}$ is
good news, one might ask if one could include more modelling features or relax
certain side conditions and still preserve tractability. This section shows
that tractability can be easily lost (at least under standard complexity-
theoretic assumptions).

###  4.0.1 Empty standpoints

While it may make sense on a philosophical level, one might wonder whether the
constraint that $\sigma(\hbox{$\mathsf{s}$})$ needs to be nonempty for every
$\hbox{$\mathsf{s}$}\in\mathsf{ST}_{\mathcal{K}}$ has an impact on
tractability. In fact, dropping this constraint, obtaining a logic
$\mathbb{S}_{\mathcal{E\\!L}}^{\emptyset}$ with the same syntax but modified
semantics, would increase expressivity (standpoint non-emptiness could still
be enforced in $\mathbb{S}_{\mathcal{E\\!L}}^{\smash{\emptyset}}$ by asserting
$\top\sqsubseteq\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}\\!\top$ for
every $\hbox{$\mathsf{s}$}\in\mathsf{ST}_{\mathcal{K}}$). However,
satisfiability in $\mathbb{S}_{\mathcal{E\\!L}}^{\smash{\emptyset}}$ turns out
to be NP-hard, even when disallowing usage of concept and role names entirely.
The key insight that both
$\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}\\!\top$ and its negation
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}\bot$ can be expressed as
$\mathbb{S}_{\mathcal{E\\!L}}^{\smash{\emptyset}}$ concepts gives rise to the
following reduction from 3SAT: Assume an instance
$\phi=\bigvee\\!\mathbf{C}_{1}\mathrel{\wedge}\ldots\mathrel{\wedge}\bigvee\\!\mathbf{C}_{n}$
of 3SAT containing $n$ clauses (i.e., disjunctions of literals)
$\bigvee\\!\mathbf{C}_{j}$ over the propositional variables
$P=\left\\{p_{1},\ldots,p_{k}\right\\}$. We note that $\phi$ is equivalent to
$(\bigwedge\\!\overline{\mathbf{C}}_{1}\to\mathbf{false})\wedge\ldots\wedge(\bigwedge\\!\overline{\mathbf{C}}_{k}\to\mathbf{false})$,
where $\overline{\mathbf{C}}_{j}$ is obtained from ${\mathbf{C}}_{j}$ by
replacing every literal by its negated version. Let now
$\\{\hbox{$\mathsf{s}$}_{1},\ldots,\hbox{$\mathsf{s}$}_{k}\\}$ be a set of
standpoint names and, for any literal $\ell$ over $P$, define

$L_{\ell}=\begin{cases}\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s_{i}}}}\\!\top&\text{
if }\ell=p_{i},\\\
\mathord{\mathop{\square}\nolimits_{\mathsf{s_{i}}}}\bot&\text{ if }\ell=\neg
p_{i}.\\\ \end{cases}$

Then, $\phi$ is satisfiable iff the following
$\mathbb{S}_{\mathcal{E\\!L}}^{\emptyset}$ knowledge base is:

$\text{$\mathcal{K}$}_{\phi}=\big{\\{}L_{\ell}\sqcap L_{\ell^{\prime}}\sqcap
L_{\ell^{\prime\prime}}\sqsubseteq\bot\mid\\{\ell,\ell^{\prime},\ell^{\prime\prime}\\}=\overline{\mathbf{C}}_{j},1\leq
j\leq n\big{\\}}.$

###  4.0.2 Rigid roles

$\mathbb{S}_{\mathcal{E\\!L}}$ allows to globally enforce rigidity of specific
concepts through axioms of the shape
$A\sqsubseteq\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A$. (This is in
contrast to e.g. $\mathbf{K}_{n}\mathcal{ALC}$, where rigidity of concepts can
only be expressed _relative_ to a given formula.) In a similar manner,
rigidity of roles (i.e., the interpretation of certain distinguished roles
being the same throughout all precisifications) would represent a desirable
modelling feature. Other modal extensions of DLs have easily been shown to
even become undecidable when this feature is permitted, but as
$\mathbb{S}_{\mathcal{E\\!L}}$ uses a much simplified semantics on the modal
dimension, these results do not carry over to $\mathbb{S}_{\mathcal{E\\!L}}$.
Yet, we will show that just the presence of _one_ distinguished rigid role
$\dot{R}$ causes $\mathbb{S}_{\mathcal{E\\!L}}$ to become intractable as
satisfiability turns coNP-hard. To demonstrate this, we reduce 3SAT to KB
unsatisfiability. As above, assume an instance
$\phi=\bigvee\\!\mathbf{C}_{1}\mathrel{\wedge}\ldots\mathrel{\wedge}\bigvee\\!\mathbf{C}_{n}$
of 3SAT over propositional variables $P=\left\\{p_{1},\ldots,p_{k}\right\\}$.
Then $\phi$ is satisfiable iff the following $\mathbb{S}_{\mathcal{E\\!L}}$
TBox is unsatisfiable (with all axioms instantiated for $1\leq i\leq k$):

$\begin{array}[]{@{}r@{\ }l@{}r@{\ }l}\top&\sqsubseteq\exists
T.L_{0}&L_{k}&\sqsubseteq\mathord{\mathop{\lozenge}\nolimits_{\mathsf{*}}}\mathit{S}\\\
L_{i-1}&\sqsubseteq\exists\dot{R}.\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}(L_{i}\sqcap
T_{p_{i}})&\exists\dot{R}.(T_{p_{i}}\sqcap\mathit{S})&\sqsubseteq(T_{p_{i}}\sqcap\mathit{S})\\\
L_{i-1}&\sqsubseteq\exists\dot{R}.\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}(L_{i}\sqcap
T_{\neg p_{i}})&\exists\dot{R}.(T_{\neg
p_{i}}\sqcap\mathit{S})&\sqsubseteq(T_{\neg p_{i}}\sqcap\mathit{S})\\\
T_{\ell}&\sqsubseteq T_{\mathbf{C}_{j}}\text{\ \ for all
}\ell\in\mathbf{C}_{j}&T_{\mathbf{C}_{1}}\\!\sqcap\ldots\sqcap
T_{\mathbf{C}_{n}}\\!&\sqsubseteq\bot\end{array}$

###  4.0.3 Nominal Concepts

Nominal concepts are a modelling feature widely used in ontology languages.
For an individual $o$, the nominal concept $\\{o\\}$ refers to the singleton
set $\\{o^{\mathcal{I}}\\}$. Let $\mathcal{ELO}$ denote $\mathcal{E\\!L}$
extended by nominal concepts. Several formalisms subsuming $\mathcal{ELO}$,
including OWL 2 EL, are known to allow for tractable reasoning Baader et al.
(2005); Krötzsch (2010). However, in the presence of standpoints, nominals
prove to be detrimental for the reasoning complexity: satisfiability of
$\mathbb{S}_{\mathcal{ELO}}$ TBoxes using just one nominal concept $\\{o\\}$
turns out to be ExpTime-hard and thus definitely harder than for
$\mathbb{S}_{\mathcal{E\\!L}}$. This can be shown by a PTime reduction of
satisfiability for Horn-$\mathcal{ALC}$ TBoxes (which is known to be ExpTime-
complete Krötzsch et al. (2013)) to satisfiability of
$\mathbb{S}_{\mathcal{ELO}}$ TBoxes with just one standpoint (the global one)
and one nominal concept $\\{o\\}$. To this end, recall that any
Horn-$\mathcal{ALC}$ TBox can be normalised in PTime to consist of only axioms
of the following shapes:

$A\sqsubseteq B\quad\\!A\sqcap B\sqsubseteq C\quad\\!\exists R.A\sqsubseteq
B\quad\\!A\sqsubseteq\exists R.B\quad\\!A\sqsubseteq\forall R.B$

where $A$ and $B$ can be concept names, $\top$, or $\bot$. From a normalised
Horn-$\mathcal{ALC}$ TBox $\mathcal{T}$, we obtain the target
$\mathbb{S}_{\mathcal{ELO}}$ TBox $\mathcal{T}^{\prime}$ by (i) declaring
every original concept name as rigid via the axiom
$A\sqsubseteq\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A$ as well as
(ii) replacing every axiom of the shape $A\sqsubseteq\exists R.B$ by the axiom

$A\sqsubseteq\mathord{\mathop{\lozenge}\nolimits_{\mathsf{*}}}((\exists\mathit{Src}.\\{o\\})\sqcap(\exists
R.(B\sqcap\exists\mathit{Tgt}.\\{o\\})))$

(introducing two fresh role names $\mathit{Src}$ and $\mathit{Tgt}$), and
replacing every axiom of the shape $A\sqsubseteq\forall r.B$ by the two axioms

$A\sqcap\exists
R.\top\sqsubseteq(\exists\mathit{Src}.(\\{o\\}\sqcap\tilde{B}))\quad\text{and}\quad\exists\mathit{Tgt}.\tilde{B}\sqsubseteq
B,$

introducing a copy $\tilde{A}$ for every original concept name $A$. With this
polytime translation, satisfiability of the Horn-$\mathcal{ALC}$ TBox
$\mathcal{T}$ and the $\mathbb{S}_{\mathcal{ELO}}$ TBox $\mathcal{T}^{\prime}$
coincide.

######  Proposition 6.

$\mathcal{T}$ and $\mathcal{T}^{\prime}$ are equisatisfiable.

###### Proof.

We show equisatisfiability of $\mathcal{T}$ and $\mathcal{T}^{\prime}$ by
providing constructions to obtain a model of $\mathcal{T}$ from a model of
$\mathcal{T}^{\prime}$ and vice versa. Let
$\mathcal{I}=(\Delta,\cdot^{\mathcal{I}})$ be a model of $\mathcal{T}$. Then
we construct a model
$\mathfrak{D}=\mbox{$\left\langle\Delta,\Pi,\sigma,\gamma\right\rangle$}$ of
$\mathcal{T}^{\prime}$ as follows:

  * •

$\Pi=N_{\mathsf{R}}\times\Delta\times\Delta$ with $\sigma(*)=\Pi$,

  * •

pick one arbitrary but fixed $\delta_{o}\in\Delta$ and let
$o^{\gamma(\pi)}=\delta_{o}$ for all $\pi\in\Pi$,

  * •

$A^{\gamma(\pi)}=A^{\mathcal{I}}$ for all $\pi\in\Pi$, whereas
$\tilde{A}^{\gamma((r,\delta_{1},\delta_{2}))}=\\{\delta_{o}\mid\delta_{2}\in
A^{\mathcal{I}}\\}$ for $A\in N_{\mathsf{C}}$,

  * •

$r^{\gamma((r,\delta_{1},\delta_{2}))}=\\{(\delta_{1},\delta_{2})\\}\cap
r^{\mathcal{I}}$, while
$src^{\gamma((r,\delta_{1},\delta_{2}))}=\\{(\delta_{1},\delta_{o})\\}$ and
$tgt^{\gamma((r,\delta_{1},\delta_{2}))}=\\{(\delta_{2},\delta_{o})\\}$.

For the other direction, let
$\mathfrak{D}=\mbox{$\left\langle\Delta,\Pi,\sigma,\gamma\right\rangle$}$ be a
model of $\mathcal{T}^{\prime}$. Then we construct a model
$\mathcal{I}=(\Delta,\cdot^{\mathcal{I}})$ of $\mathcal{T}$ as follows:

  * •

$A^{\mathcal{I}}=A^{\gamma(\pi)}$ for any $\pi\in\Pi$ (the choice is
irrelevant because all $A$ are rigid)

  * •

$r^{\mathcal{I}}=\bigcup_{\pi\in\Pi}\\{(\delta_{1},\delta_{2})\in
r^{\gamma(\pi)}\mid(\delta_{1},o^{\gamma(\pi)})\in src^{\gamma(\pi)},\
(\delta_{2},o^{\gamma(\pi)})\in tgt^{\gamma(\pi)}\\}$

##  5 Conclusion and Future Work

In this paper we introduced Standpoint $\mathcal{E\\!L}$, a new, lightweight
member of the emerging family of standpoint logics. We described the new
modelling and reasoning capabilities it brings to large-scale ontology
management and established a PTime (and thus worst-case optimal) tableau-based
decision procedure for standard reasoning tasks. We also demonstrated that
certain extensions of $\mathbb{S}_{\mathcal{E\\!L}}$, which would be desirable
from a expressivity point of view, inevitably come with a loss of tractability
(sometimes under the assumption $\textsc{P}\neq\textsc{NP}$).

Yet several modelling features can be accommodated into
$\mathbb{S}_{\mathcal{E\\!L}}$ without endangering tractability. For instance,
from a usability perspective, it would seem very advantageous if not just
single axioms, but whole axiom sets (up to whole knowledge bases) could be
preceded by standpoint modalities. By definition, an axiom of the type
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}\mathcal{K}$ can be
equivalently rewritten into the axiom set
$\\{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}\phi\mid\phi\in\mathcal{K}\\}$.
While something alike is not immediately possible for axioms of the type
$\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}\mathcal{K}$, our
normalization rule for diamond-preceded axioms can be lifted and thus
$\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}\mathcal{K}$ can be
rewritten to
$\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}\mathcal{K}$ (and
further to
$\\{\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}\phi\mid\phi\in\mathcal{K}\\}$)
upon introducing a fresh standpoint name $\mathsf{s^{\prime}}$ and asserting
$\hbox{$\mathsf{s^{\prime}}$}\preceq\hbox{$\mathsf{s}$}$. Thus standpoint-
modality-annotated knowledge bases come essentially for free in
$\mathbb{S}_{\mathcal{E\\!L}}$. In fact, we already made use of this modelling
feature in Axiom 9 and Axiom 10 of our initial example.

Moreover, we are confident that, as opposed to nominal concepts, other
modelling features of OWL 2 EL can be added to $\mathbb{S}_{\mathcal{E\\!L}}$
without harming tractability. These include complex role inclusions (also
called role-chain axioms) such as
$\mbox{\small\tt{FindingSite}}\circ\mbox{\small\tt{PartOf}}\sqsubseteq\mbox{\small\tt{FindingSite}}$,
and the self-concept as in
$\mbox{\small\tt{ApoptoticCell}}\sqsubseteq\exists\mbox{\small\tt{Destroys}}.\mathsf{Self}$.
It also seems plausible that the sharpening statements can be extended to
incorporate intersection and disjointness of standpoints.

Beyond exploring the tractability boundaries, next endeavours include to
investigate feasible strategies for developing a
$\mathbb{S}_{\mathcal{E\\!L}}$ reasoner. Options include

  * •

to implement our tableau algorithm from scratch or by modifying existing open-
source tableaux systems,

  * •

to design a deduction calculus over normalised axioms that can be translated
into a datalog program, akin to the approach of Krötzsch [2010], then
utilizing a state-of-the-art datalog engine like VLog Urbani et al. (2016), or

  * •

to find a reduction to reasoning in standpoint-free (PTime extensions of)
$\mathcal{E\\!L}$ that is supported by existing reasoners (such as ELK Kazakov
et al. (2014) or Snorocket Metke-Jimenez and Lawley (2013)).

With one or several reasoners in place, appropriate experiments will be
designed and conducted to assess practical feasibility and scalability.

Beyond the $\mathcal{E\\!L}$ family, further popular and computationally
lightweight formalisms exist, such as the tractable profiles OWL 2 RL and OWL
2 QL Motik et al. (2009a). It would be interesting to investigate options to
extend these by standpoint reasoning without sacrificing tractability. More
generally, we intend to research the effect of adding standpoints to KR
languages – light- or heavyweight – in terms of computational properties and
expressivity as well as avenues for implementing efficient reasoners for them.

## References

  * Baader and Ohlbach [1995] Franz Baader and Hans Jürgen Ohlbach.  A multi-dimensional terminological knowledge representation language.  Journal of Applied Non-Classical Logics, 5(2):153–197, 1995.
  * Baader et al. [2005] Franz Baader, Sebastian Brandt, and Carsten Lutz.  Pushing the EL envelope.  In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, 2005, pages 364–369. Professional Book Center, 2005\.
  * Baader et al. [2017] Franz Baader, Ian Horrocks, Carsten Lutz, and Uli Sattler.  An Introduction to Description Logic.  Cambridge University Press, 2017.
  * Borgida and Serafini [2003] Alex Borgida and Luciano Serafini.  Distributed Description Logics: Assimilating information from peer sources.  Journal on Data Semantics, 2800:153–184, 2003.
  * Bouquet et al. [2003] Paolo Bouquet, Fausto Giunchiglia, Frank Van Harmelen, Luciano Serafini, and Heiner Stuckenschmidt.  C-OWL: Contextualizing ontologies.  Lecture Notes in Computer Science, 2870:164–179, 10 2003.
  * Bozzato et al. [2018] Loris Bozzato, Thomas Eiter, and Luciano Serafini.  Enhancing context knowledge repositories with justifiable exceptions.  Artificial Intelligence, 257:72–126, 2018.
  * Carral et al. [2014] David Carral, Adila Krisnadhi, Sebastian Rudolph, and Pascal Hitzler.  All but not nothing: Left-hand side universals for tractable OWL profiles.  In C. Maria Keet and Valentina A. M. Tamma, editors, Proceedings of the 11th International Workshop on OWL: Experiences and Directions (OWLED 2014) co-located with 13th International Semantic Web Conference on (ISWC 2014), volume 1265, pages 97–108. CEUR Workshop Proceedings, 2014.
  * Donnelly [2006] Kevin Donnelly.  SNOMED-CT: The advanced terminology and coding system for eHealth.  Studies in health technology and informatics, 121:279, 2006.
  * Fine [1975] Kit Fine.  Vagueness, truth and logic.  Synthese, 30(3-4):265–300, 1975.
  * Gómez Álvarez and Rudolph [2021] Lucía Gómez Álvarez and Sebastian Rudolph.  Standpoint logic: Multi-perspective knowledge representation.  In Fabian Neuhaus and Boyan Brodaric, editors, Proceedings of the 12th International Conference on Formal Ontology in Information Systems, volume 344 of FAIA, pages 3–17. IOS Press, 2021.
  * Gómez Álvarez et al. [2022] Lucía Gómez Álvarez, Sebastian Rudolph, and Hannes Strass.  How to Agree to Disagree: Managing Ontological Perspectives using Standpoint Logic.  In Proceedings of the 21st International Semantic Web Conference, pages 125–141. Springer, 2022.
  * Hemam and Boufaïda [2011] Mounir Hemam and Zizette Boufaïda.  MVP-OWL: A multi-viewpoints ontology language for the Semantic Web.  International Journal of Reasoning-based Intelligent Systems, 3(3-4):147–155, 2011.
  * Hemam [2018] Mounir Hemam.  An extension of the ontology web language with multi-viewpoints and probabilistic reasoning.  International Journal of Advanced Intelligence Paradigms, 10(3):247–265, 2018.
  * Kazakov et al. [2014] Yevgeny Kazakov, Markus Krötzsch, and Frantisek Simancik.  The incredible ELK - from polynomial procedures to efficient reasoning with $\mathcal{EL}$ ontologies.  J. Autom. Reason., 53(1):1–61, 2014.
  * Klarman and Gutiérrez-Basulto [2013] Szymon Klarman and Víctor Gutiérrez-Basulto.  Description logics of context.  Journal of Logic and Computation, 26(3):817–854, 2013.
  * Krötzsch et al. [2013] Markus Krötzsch, Sebastian Rudolph, and Pascal Hitzler.  Complexities of Horn description logics.  ACM Trans. Comput. Log., 14(1):2:1–2:36, 2013.
  * Krötzsch [2010] Markus Krötzsch.  Efficient inferencing for OWL EL.  In Tomi Janhunen and Ilkka Niemelä, editors, Proceedings of the 12th European Conference on Logics in Artificial Intelligence JELIA 2010., volume 6341 of Lecture Notes in Computer Science, pages 234–246. Springer, 2010.
  * Lutz et al. [2002] Carsten Lutz, Holger Sturm, Frank Wolter, and Michael Zakharyaschev.  A tableau decision algorithm for modalized ALC with constant domains.  Studia Logica, 72(2):199–232, 2002.
  * McCarthy and Buvac [1998] John McCarthy and Sasa Buvac.  Formalizing context (expanded notes).  CSLI Lecture Notes, 81:13–50, 1998.
  * Metke-Jimenez and Lawley [2013] Alejandro Metke-Jimenez and Michael Lawley.  Snorocket 2.0: Concrete domains and concurrent classification.  In Samantha Bail, Birte Glimm, Rafael S. Gonçalves, Ernesto Jiménez-Ruiz, Yevgeny Kazakov, Nicolas Matentzoglu, and Bijan Parsia, editors, Informal Proceedings of the 2nd International Workshop on OWL Reasoner Evaluation (ORE-2013), Ulm, Germany, July 22, 2013, volume 1015 of CEUR Workshop Proceedings, pages 32–38. CEUR-WS.org, 2013.
  * Mosurović [1999] Milenko Mosurović.  On the complexity of description logics with modal operators.  1999\.
  * Motik et al. [2009a] Boris Motik, Bernardo Cuenca Grau, Ian Horrocks, Zhe Wu, Achille Fokoue, and Carsten Lutz, editors.  OWL 2 Web Ontology Language: Profiles.  W3C Recommendation, 27 October 2009.  Available at http://www.w3.org/TR/owl2-profiles/.
  * Motik et al. [2009b] Boris Motik, Peter F. Patel-Schneider, and Bernardo Cuenca Grau, editors.  OWL 2 Web Ontology Language: Direct Semantics.  W3C Recommendation, 27 October 2009.  Available at http://www.w3.org/TR/owl2-direct-semantics/.
  * Osman et al. [2021] Inès Osman, Sadok Ben Yahia, and Gayo Diallo.  Ontology Integration: Approaches and Challenging Issues.  Information Fusion, 71:38–63, 2021.
  * OWL Working Group [2009] W3C OWL Working Group.  OWL 2 Web Ontology Language: Document Overview.  W3C Recommendation, 27 October 2009.  Available at http://www.w3.org/TR/owl2-overview/.
  * Rudolph [2011] Sebastian Rudolph.  Foundations of description logics.  In Axel Polleres, Claudia d’Amato, Marcelo Arenas, Siegfried Handschuh, Paula Kroner, Sascha Ossowski, and Peter F. Patel-Schneider, editors, Lecture Notes of the 7th International Reasoning Web Summer School (RW’11), volume 6848 of LNCS, pages 76–136. Springer, 2011.
  * Schulz et al. [2017] Stefan Schulz, Catalina Martínez-Costa, and Jose Antonio Miñarro-Giménez.  Lexical ambiguity in SNOMED CT.  In JOWO, 2017.
  * Serafini and Homola [2012] Luciano Serafini and Martin Homola.  Contextualized knowledge repositories for the semantic web.  Journal of Web Semantics, 12-13:64–87, 2012.  Reasoning with context in the Semantic Web.
  * Urbani et al. [2016] Jacopo Urbani, Ceriel J. H. Jacobs, and Markus Krötzsch.  Column-oriented datalog materialization for large knowledge graphs.  In Dale Schuurmans and Michael P. Wellman, editors, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA, pages 258–264. AAAI Press, 2016.
  * Wolter and Zakharyaschev [1998] Frank Wolter and Michael Zakharyaschev.  Satisfiability problem in description logics with modal operators.  In Anthony G. Cohn, Lenhart K. Schubert, and Stuart C. Shapiro, editors, Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning, pages 512–523. Morgan Kaufmann, 1998\.
  * Wolter and Zakharyaschev [1999] Frank Wolter and Michael Zakharyaschev.  Multi-dimensional description logics.  In Proceedings of the 16th International Joint Conference on Artifical Intelligence - Volume 1, IJCAI’99, page 104–109. Morgan Kaufmann Publishers Inc., 1999.