shortproof

###### Proof.

shortproofsketch

######  Proof sketch.

$\Box$

longproof[1][] supplementary shortonly longonly

# Tractable Diversity:
Scalable Multiperspective Ontology Management via Standpoint $\mathcal{E\\!L}$

Lucía Gómez Álvarez and Sebastian Rudolph and Hannes Strass Computational
Logic Group, TU Dresden, Germany{lucia.gomez_alvarez, sebastian.rudolph,
<EMAIL_ADDRESS>
###### Abstract

The tractability of the lightweight description logic $\mathcal{E\\!L}$ has
allowed for the construction of large and widely used ontologies that support
semantic interoperability. However, comprehensive domains with a broad user
base are often at odds with strong axiomatisations otherwise useful for
inferencing, since these are usually context dependent and subject to
diverging perspectives.

In this paper we introduce _Standpoint $\mathcal{E\\!L}$_, a multi-modal
extension of $\mathcal{E\\!L}$ that allows for the integrated representation
of domain knowledge relative to diverse, possibly conflicting _standpoints_
(or contexts), which can be hierarchically organised and put in relation with
each other. We establish that _Standpoint $\mathcal{E\\!L}$_ still exhibits
$\mathcal{E\\!L}$’s favourable PTime standard reasoning, whereas introducing
additional features like empty standpoints, rigid roles, and no-
minals makes standard reasoning tasks intractable.

##  1 Introduction

In many subfields of artificial intelligence, ontologies are used to provide a
formal representation of a shared vocabulary, give meaning to its terms, and
describe the relations between them. To this end, one of the most prominent
and successful class of logic-based knowledge representation formalisms are
_description logics_ (DLs) Baader et al. (2017); Rudolph (2011), which provide
the formal basis for most recent version of the Web Ontology Language OWL 2
OWL Working Group (2009).

Among the most widely used families of DLs used today is $\mathcal{E\\!L}$
Baader et al. (2005), which is the formal basis of OWL 2 EL Motik et al.
(2009a), a popular tractable profile of OWL 2. One of the main appeals of
$\mathcal{E\\!L}$ is that basic reasoning tasks can be performed in polynomial
time with respect to the size of the ontology, enabling reasoning-supported
creation and maintenance of very large ontologies. An example of this is the
healthcare ontology SNOMED CT Donnelly (2006), with worldwide adoption and a
broad user base comprising clinicians, patients, and researchers.

However, when modelling comprehensive ontologies like SNOMED CT, one is
usually facing issues related to context or perspective-dependent knowledge as
well as ambiguity of language Schulz et al. (2017). For instance, the concept
Tumour might denote a process or a piece of tissue; Allergy may denote an
allergic reaction or just an allergic disposition.

In a similar vein, the decentralised nature of the Semantic Web has led to the
generation of various ontologies of overlapping knowledge that inevitably
reflect different points of view. For instance, an initiative has attempted to
integrate the FMA1140 (Foundational Model of Anatomy), SNOMED-CT, and the NCI
(National Cancer Institute Thesaurus) into a single combined version called
LargeBio and reported ensuing challenges Osman et al. (2021). In this context,
frameworks supporting the integrated representation of multiple perspectives
seem preferable to recording the distinct views in a detached way, but also to
entirely merging them at the risk of causing inconsistencies or unintended
consequences.

To this end, Gómez Álvarez and Rudolph [2021] proposed _standpoint logic_ , a
formalism inspired by the theory of supervaluationism Fine (1975) and rooted
in modal logic, which allows for the simultaneous representation of multiple,
potentially contradictory, viewpoints in a unified way and the establishment
of alignments between them. This is achieved by extending the base language
with labelled modal operators, where propositions
$\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{S}}}}\phi$ and
$\mathord{\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{S}}}}\phi$
express information relative to the _standpoint_ $\mathsf{S}$ and read,
respectively: “according to $\mathsf{S}$, it is _unequivocal/conceivable_ that
$\phi$”. Semantically, standpoints are represented by sets of
_precisifications_ ,111Precisifications are analogous to the _worlds_ of
modal-logic frameworks with possible-worlds semantics. such that
$\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{S}}}}\phi$ and
$\mathord{\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{S}}}}\phi$ hold
if $\phi$ is true in all/some of the precisifications associated with
$\mathsf{S}$. Consider the following example.

######  Example 1 (Tumour Disambiguation).

Two derivatives of the SNOMED CT ontology $(\mathsf{SN})$ model tumours
differently. According to $\mathsf{TP}$, a Tumour is a process by which
abnormal or damaged cells grow and multiply (1), yet according to
$\mathsf{TT}$, a Tumour is a lump of tissue (2).

$\displaystyle\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TP}}}}[\mbox{\small\tt{Tumour}}$
$\displaystyle\sqsubseteq\mbox{\small\tt{AbnormalGrowthProcess}}]$ (1)
$\displaystyle\small\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TT}}}}[\mbox{\small\tt{Tumour}}$
$\displaystyle\sqsubseteq\mbox{\small\tt{Tissue}}]$ (2)

Both interpretations inherit the axioms of the original SNOMED CT (3) and are
such that if according to $\mathsf{SN}$ something is arguably both a Tumour
and a Tissue, then it (unequivocally) is a Tumour according to $\mathsf{TT}$
(4). The respective assertion is made for $\mathsf{TP}$ (5). But Tissue and
Process are disjoint categories according to $\mathsf{SN}$ (6).

$\displaystyle(\mathsf{TP}\preceq\mathsf{SN})\quad$
$\displaystyle\quad(\mathsf{TT}\preceq\mathsf{SN})$ (3)
$\displaystyle\mathord{\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{SN}}}}[\mbox{\small\tt{Tumour}}\sqcap\mbox{\small\tt{PhysicalObject}}]$
$\displaystyle\sqsubseteq\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TT}}}}[\mbox{\small\tt{Tumour}}]$
(4)
$\displaystyle\mathord{\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{SN}}}}[\mbox{\small\tt{Tumour}}\sqcap\mbox{\small\tt{Process}}]$
$\displaystyle\sqsubseteq\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TP}}}}[\mbox{\small\tt{Tumour}}]$
(5)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{SN}}}}[\mbox{\small\tt{Tissue}}\sqcap\mbox{\small\tt{Process}}$
$\displaystyle\sqsubseteq\bot]$ (6)

While clearly incompatible, both perspectives are semantically close and we
can establish relations between them. For instance, we might assert that
something is unequivocally the product of a Tumour (process) according to
$\mathsf{TP}$ if and only if it is arguably a Tumour (tissue) according to
$\mathsf{TT}$ (7). Or we may want to specify a subsumption between the classes
of unequivocal instances of Tissue according to $\mathsf{TT}$ and to
$\mathsf{TP}$ (8).

$\displaystyle\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TP}}}}[\exists\mbox{\small\tt{ProductOf.Tumour}}]\equiv\mathord{\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{TT}}}}[\mbox{\small\tt{Tumour}}]$
(7)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TT}}}}[\mbox{\small\tt{Tissue}}]\sqsubseteq\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TP}}}}[\mbox{\small\tt{Tissue}}]$
(8)

When recording clinical findings, clinicians may use ambiguous language, so an
automated knowledge extraction service may obtain the following from text and
annotated scans:

$\displaystyle\small\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{SN}}}}\\!$
$\displaystyle\small\left\\{\mbox{\small\tt{Patient}}(p1),\,\mbox{\small\tt{HasPart}}(p1,a),\,\mbox{\small\tt{Colon}}(a)\right\\}$
(9)
$\displaystyle\small\mathord{\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{SN}}}}\\!$
$\displaystyle\small\left\\{\mbox{\small\tt{HasPart}}(a,b),\,\mbox{\small\tt{Tumour}}(b),\,\mbox{\small\tt{PhysicalObject}}(b)\right\\}$
(10)

❑

The logical statements (1)–(10), which formalise Example 1 by means of a
standpoint-enhanced $\mathcal{E\\!L}$ description logic, are not inconsistent,
so all axioms can be jointly represented. Let us now illustrate the use of
standpoint logic for reasoning with and across individual perspectives.

######  Example 2 (Continued from Example 1).

In this case, we can disambiguate the information given by Axiom (10) using
Axiom (3) and Axiom (4), which entail that according to $\small\mathsf{TT}$,
$b$ is unequivocally a tumour,
$\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TT}}}}\mbox{\small\tt{Tumour}}(b)$,
and with Axiom (2) also a tissue,
$\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TT}}}}\mbox{\small\tt{Tissue}}(b)$.
Moreover, we can use the “bridges” to switch to another perspective. From
Axiom (8), it is clear that according to $\small\mathsf{TP}$, $b$ is also a
tissue,
$\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TP}}}}\mbox{\small\tt{Tissue}}(b)$,
and from Axiom (7) $b$ is the product of a tumour,
$\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TP}}}}\exists\mbox{\small\tt{ProductOf.Tumour}}(b)$.
Then Axiom (1) yields

$\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{TP}}}}\exists\mbox{\small\tt{ProductOf}}.(\mbox{\small\tt{Tumour}}\sqcap\mbox{\small\tt{AbnormalGrowthProcess}})(b).$

The statement
$\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{SN}}}}[\mbox{\small\tt{Tumour}}\sqcap\mbox{\small\tt{Process}}](d)$,
in contrast, will trigger an inconsistency thanks to Axiom (6), which prevents
the evaluation of Tumour simultaneously as a Tissue and a Process and Axiom
(2), which states that according to some interpretations, a Tumour is a
Tissue. Finally, a user (e.g. a specific clinic, $\small\mathsf{CL}$) may
inherit the SNOMED CT $(\small\mathsf{CL}\preceq\mathsf{SN})$ and establish
further axioms, e.g,

$\displaystyle\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{CL}}}}[\mbox{\small\tt{Patient}}\sqcap\exists\mbox{\small\tt{HasPart.}}(\mbox{\small\tt{Colon}}\sqcap\mathord{\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{SN}}}}\exists\mbox{\small\tt{HasPart.}}\mbox{\small\tt{Tumour}})\sqsubseteq$
$\displaystyle\exists\mbox{\small\tt{AssociatedWith.ColonCancerRisk}}],$

to identify patients with cancer risk. Here, one can infer with Ax. (9) that
$\mathord{\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{CL}}}}\exists\mbox{\small\tt{AssociatedWith.ColonCancerRisk}}(p1)$.
❑

The need of handling multiple perspectives in the Semantic Web has led to
several (non-modal) logic-based proposals. The closest regarding goals are
multi-viewpoint ontologies Hemam and Boufaïda (2011); Hemam (2018), which
model the intuition of viewpoints in a tailored extension of OWL for which no
complexity bounds are given. Similar problems are also addressed in the more
extensive work on contextuality (e.g. C-OWL and Distributed ontologies Bouquet
et al. (2003); Borgida and Serafini (2003) and the Contextualised Knowledge
Repository (CKR) Serafini and Homola (2012)). These frameworks focus on
contextual and distributed reasoning and range between different levels of
expressivity for modelling the structure of contexts and the bridges between
them. In the context of scalable reasoning, one should highlight the
implementations that provide support for OWL2-RL based CKR defeasible
reasoning Bozzato et al. (2018).

As for modal logics, their suitability to model perspectives and contexts in a
natural way is obvious Klarman and Gutiérrez-Basulto (2013); Gómez Álvarez and
Rudolph (2021), they are well-known in the community and their semantics is
well-understood. Yet, the interplay between DL constructs and modalities is
often not well-behaved and can easily endanger the decidability of reasoning
tasks or increase their complexity Baader and Ohlbach (1995); Mosurović
(1999); Wolter and Zakharyaschev (1999). Notable examples are NExpTime-
completeness of the multi-modal description logic $\mathbf{K}_{\mathcal{ALC}}$
Lutz et al. (2002) and 2ExpTime-completeness of
$\mathcal{ALC}_{\mathcal{ALC}}$ Klarman and Gutiérrez-Basulto (2013), a modal
contextual logic framework in the style proposed by McCarthy McCarthy and
Buvac (1998).

In this work, we focus on the framework of _standpoint logics_ Gómez Álvarez
and Rudolph (2021), which are modal logics, too, but come with a simplified
Kripke semantics. Recently, Gómez Álvarez et al. [2022] introduced _First-
Order_ Standpoint Logic (FOSL) and showed favourable complexity results for
its _sentential_ fragments,222This includes the sentential standpoint variant
of the expressive DL $\mathcal{SROIQ}b_{s}$, a logical basis of OWL 2 DL Motik
et al. (2009b). which disallow modal operators being applied to formulas with
free variables. In particular, adding sentential standpoints does not increase
the complexity for fragments that are _NP -hard_. Yet, a fine-grained
terminological alignment between different perspectives requires concepts
preceded by modal operators, as in Axiom (7), leading to non-sentential
fragments of FOSL.

Our paper is structured as follows. After introducing the syntax and semantics
of Standpoint $\mathcal{E\\!L}$ ($\mathbb{S}_{\mathcal{E\\!L}}$) and a
suitable normal form (Section 2), we establish our main result: satisfiability
checking in $\mathbb{S}_{\mathcal{E\\!L}}$ is PTime. We show this by providing
a worst-case optimal tableau-based algorithm (Section 3) that takes
inspiration in the _quasi-model_ based methods Wolter and Zakharyaschev (1998)
as used for $K_{\mathcal{ALC}}$ Lutz et al. (2002), but differs in its
specifics. Our approach builds a _quasi-model_ from a graph of _(quasi) domain
elements_ , which are annotated with various constraints, to then reconstruct
the worlds or, in our case, precisifications. We also show that introducing
additional features such as empty standpoints, rigid roles, and nominals make
standard reasoning tasks intractable (Section 4). In Section 5, we conclude
the paper with a discussion of future work, including efficient approaches for
reasoner implementations. Altogether, this paper provides a clear pathway for
making scalable multiperspective ontology management possible.

An extended version of the paper with proofs of all results is available as a
technical appendix.

##  2 Syntax, Semantics, and Normalisation

We now introduce syntax and semantics of Standpoint $\mathcal{E\\!L}$
(referred to as $\mathbb{S}_{\mathcal{E\\!L}}$) and propose a normal form that
is useful for subsequent algorithmic considerations.

###  2.0.1 Syntax

A _Standpoint DL vocabulary_ is a traditional DL vocabulary consisting of sets
$N_{\mathsf{C}}$ of _concept names_ , $N_{\mathsf{R}}$ of _role names_ , and
$N_{\mathsf{I}}$ of _individual names_ , extended it by an additional set
$N_{\mathsf{S}}$ of _standpoint names_ with $\hbox{$*$}\in N_{\mathsf{S}}$. A
_standpoint operator_ is of the form
$\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}$ (“diamond”) or
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}$ (“box”) with $\mathsf{s}\in
N_{\mathsf{S}}$; we use $\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}$ to
refer to either. A _concept term_ is defined via

$C\mathrel{::=}\top\mathrel{\;\mid\;}\bot\mathrel{\;\mid\;}A\mathrel{\;\mid\;}C_{1}\sqcap
C_{2}\mathrel{\;\mid\;}\exists
R.C\mathrel{\;\mid\;}\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}[C]$

where $A\in N_{\mathsf{C}}$ and $R\in N_{\mathsf{R}}$. A _general concept
inclusion (GCI)_ is of the form
$\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}[C\sqsubseteq D]$, where $C$
and $D$ are concept terms.333The square brackets $[\ldots]$ indicate the scope
of the modality, as the same modalities may be used inside concept terms. A
_concept assertion_ is of of the form
$\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}[C(a)]$ while a _role
assertion_ is of the form
$\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}[R(a,b)]$, where $a,b\in
N_{\mathsf{I}}$, $C$ is a concept term, and $R\in N_{\mathsf{R}}$. A
_sharpening statement_ is of the form $\mathsf{s}\preceq\mathsf{s}^{\prime}$
where $\mathsf{s},\mathsf{s}^{\prime}\in N_{\mathsf{S}}$.

A _$\mathbb{S}_{\mathcal{E\\!L}}$ knowledge base_ is a tuple
$\mathcal{K}=\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}$,
where $\mathcal{T}$ is a set of GCIs, called _TBox_ ; $\mathcal{A}$ is a set
of (concept or role) assertions, called _ABox_ ; and $\mathcal{S}$ is a set of
sharpening statements, called _SBox_. We refer to arbitrary statements from
$\mathcal{K}$ as _axioms_. Since the axiom types in $\mathcal{S}$,
$\mathcal{T}$, and $\mathcal{A}$ are syntactically well-distinguished, we
sometimes identify $\mathcal{K}$ as
$\mathcal{S}\cup\mathcal{T}\cup\mathcal{A}$. Note that all axioms except
sharpening statements are preceded by modal operators (_“modalised”_ for
short). In case the preceding operator happens to be
$\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}$, we may omit it.

###  2.0.2 Semantics

The semantics of standpoint $\mathcal{E\\!L}$ is defined via standpoint
structures. Given a Standpoint DL vocabulary $\left\langle
N_{\mathsf{C}},N_{\mathsf{R}},N_{\mathsf{I}},N_{\mathsf{S}}\right\rangle$, a
_description logic standpoint structure_ is a tuple
$\mathfrak{D}=\mbox{$\left\langle\Delta,\Pi,\sigma,\gamma\right\rangle$}$
where:

  * •

$\Delta$ is a non-empty set, the _domain_ of $\mathfrak{D}$;

  * •

$\Pi$ is a set, called the _precisifications_ of $\mathfrak{D}$;

  * •

$\sigma$ is a function mapping each standpoint symbol to a non-empty subset of
$\Pi$;444As shown in Section 4, allowing for “empty standpoints” immediately
incurs intractability, even for an otherwise empty vocabulary.

  * •

$\gamma$ is a function mapping each precisification from $\Pi$ to an
“ordinary” DL interpretation
$\mathcal{I}=\mbox{$\langle\Delta,\cdot^{\mathcal{I}}\rangle$}$ over the
domain $\Delta$, where the interpretation function $\cdot^{\mathcal{I}}$ maps:

    * –

each concept name $A\in N_{\mathsf{C}}$ to a set
$A^{\mathcal{I}}\subseteq\Delta$,

    * –

each role name $R{\,\in\,}N_{\mathsf{R}}$ to a binary relation
$R^{\mathcal{I}}{\,\subseteq\,}\Delta{\times}\Delta$,

    * –

each individual name $a\in N_{\mathsf{I}}$ to an element
$a^{\mathcal{I}}\in\Delta$,

and we require $a^{\gamma(\pi)}=a^{\gamma(\pi^{\prime})}$ for all
$\pi,\pi^{\prime}\in\Pi$ and $a\in N_{\mathsf{I}}$.

Note that by this definition, individual names (also referred to as constants)
are interpreted rigidly, i.e., each individual name $a$ is assigned the same
$a^{\gamma(\pi)}\in\Delta$ across all precisifications $\pi\in\Pi$. We will
refer to this uniform $a^{\gamma(\pi)}$ by $a^{\mathfrak{D}}$.

For each $\pi\in\Pi$, the interpretation mapping $\mathcal{I}=\gamma(\pi)$ is
extended to concept terms via structural induction as follows:

$\displaystyle\top^{\mathcal{I}}$
$\displaystyle\mathrel{\,:=\,}\Delta\qquad\qquad\quad(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}C)^{\mathcal{I}}\mathrel{\,:=\,}\textstyle\bigcup_{\pi^{\prime}\in\sigma(\mathsf{s})}C^{\gamma(\pi^{\prime})}$
$\displaystyle\bot^{\mathcal{I}}$ $\displaystyle\mathrel{\,:=\,}\emptyset\
\qquad\qquad\quad(\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}C)^{\mathcal{I}}\mathrel{\,:=\,}\textstyle\bigcap_{\pi^{\prime}\in\sigma(\mathsf{s})}C^{\gamma(\pi^{\prime})}$
$\displaystyle(C_{1}\sqcap C_{2})^{\mathcal{I}}$
$\displaystyle\mathrel{\,:=\,}C_{1}^{\mathcal{I}}\cap C_{2}^{\mathcal{I}}$
$\displaystyle(\exists R.C)^{\mathcal{I}}$
$\displaystyle\mathrel{\,:=\,}\left\\{\delta\in\Delta\;\middle|\;\mbox{$\left\langle\delta,\varepsilon\right\rangle$}\in
R^{\mathcal{I}}\text{ for some }\varepsilon\in C^{\mathcal{I}}\right\\}$

We observe that modalised concepts
$\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}C$ are interpreted uniformly
across all precisifications $\pi\in\Pi$, which allows us to denote their
extensions with
$(\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}C)^{\mathfrak{D}}$.

A DL standpoint structure $\mathfrak{D}$ _satisfies a sharpening statement_
$\mathsf{s}\preceq\mathsf{s^{\prime}}$, written as
$\mathfrak{D}\models\mathsf{s}\preceq\mathsf{s^{\prime}}$, iff
$\sigma(\mathsf{s})\subseteq\sigma(\mathsf{s^{\prime}})$. For the other axiom
types, satisfaction by $\mathfrak{D}$ is defined as follows:

$\displaystyle\mathfrak{D}$
$\displaystyle\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C{\,\sqsubseteq\,}D]$
$\displaystyle\mathrel{\;:\mathrel{\mkern-6.0mu}{\Longleftrightarrow}\;}$
$\displaystyle C^{\gamma(\pi)}\subseteq D^{\gamma(\pi)}\text{ for each
}\pi\in\sigma(\mathsf{s})$ $\displaystyle\mathfrak{D}$
$\displaystyle\models\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C{\,\sqsubseteq\,}D]$
$\displaystyle\mathrel{\;:\mathrel{\mkern-6.0mu}{\Longleftrightarrow}\;}$
$\displaystyle C^{\gamma(\pi)}\subseteq D^{\gamma(\pi)}\text{ for some
}\pi\in\sigma(\mathsf{s})$ $\displaystyle\mathfrak{D}$
$\displaystyle\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C(a)]$
$\displaystyle\mathrel{\;:\mathrel{\mkern-6.0mu}{\Longleftrightarrow}\;}$
$\displaystyle
a^{\mathfrak{D}}\in\textstyle\bigcap_{\pi\in\sigma(\mathsf{s})}C^{\gamma(\pi)}\
{\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color@gray@fill{.75}\left(=(\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}C)^{\mathfrak{D}}\right)}$
$\displaystyle\mathfrak{D}$
$\displaystyle\models\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C(a)]$
$\displaystyle\mathrel{\;:\mathrel{\mkern-6.0mu}{\Longleftrightarrow}\;}$
$\displaystyle
a^{\mathfrak{D}}\in\textstyle\bigcup_{\pi\in\sigma(\mathsf{s})}C^{\gamma(\pi)}\
{\color[rgb]{.75,.75,.75}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.75,.75}\pgfsys@color@gray@stroke{.75}\pgfsys@color@gray@fill{.75}\left(=(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}C)^{\mathfrak{D}}\right)}$
$\displaystyle\mathfrak{D}$
$\displaystyle\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[R(a,\\!b)]$
$\displaystyle\mathrel{\;:\mathrel{\mkern-6.0mu}{\Longleftrightarrow}\;}$
$\displaystyle\mbox{$\langle
a^{\mathfrak{D}}\\!\\!,b^{\mathfrak{D}}\rangle$}\in\textstyle\bigcap_{\pi\in\sigma(\mathsf{s})}R^{\gamma(\pi)}$
$\displaystyle\mathfrak{D}$
$\displaystyle\models\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[R(a,\\!b)]$
$\displaystyle\mathrel{\;:\mathrel{\mkern-6.0mu}{\Longleftrightarrow}\;}$
$\displaystyle\mbox{$\langle
a^{\mathfrak{D}}\\!\\!,b^{\mathfrak{D}}\rangle$}\in\textstyle\bigcup_{\pi\in\sigma(\mathsf{s})}R^{\gamma(\pi)}$

As usual, $\mathfrak{D}$ is a _model of $\mathcal{S}$_ iff it satisfies every
sharpening statement in $\mathcal{S}$; it is a _model of $\mathcal{T}$_ iff it
satisfies every GCI $\tau\in\mathcal{T}$; it is a _model of $\mathcal{A}$_ iff
it satisfies every assertion $\alpha\in\mathcal{A}$; it is a _model of
$\mathcal{K}=\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}$_
(written $\mathfrak{D}\models\mathcal{K}$) iff it is a model of $\mathcal{S}$
and a model of $\mathcal{T}$ and a model of $\mathcal{A}$.

Our investigations regarding reasoning in $\mathbb{S}_{\mathcal{E\\!L}}$ will
focus on standpoint versions of the well-known standard reasoning tasks, and
we will make use of variations of established techniques to (directly or
indirectly) reduce all of them to the first.

Knowledge base satisfiability:

Given a knowledge base $\mathcal{K}$, is there a DL standpoint structure
$\mathfrak{D}$ such that $\mathfrak{D}\models\mathcal{K}$?

Axiom entailment:

Given $\mathcal{K}$ and some SBox, TBox, or ABox axiom $\phi$, does
$\mathcal{K}\models\phi$ hold, that is, is it the case that for every model
$\mathfrak{D}$ of $\mathcal{K}$ we have $\mathfrak{D}\models\phi$?
To show that axiom entailment can be polynomially reduced to knowledge base
unsatisfiability, we exhibit for every axiom type $\phi$ a knowledge base
$\mathcal{K}_{\neg\phi}$ such that $\mathcal{K}\models\phi$ coincides with
unsatisfiability of $\mathcal{K}\cup\mathcal{K}_{\neg\phi}$:

$\displaystyle\mathcal{K}_{\hbox{$\mathsf{s}$}\preceq\hbox{$\mathsf{s^{\prime}}$}}$
$\displaystyle\mathrel{\,:=\,}\\{\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[\top\sqsubseteq\tilde{A}],\
\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}[\tilde{A}\sqsubseteq\bot]\\}$
$\displaystyle\mathcal{K}_{\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]}$ $\displaystyle\mathrel{\,:=\,}\\{\tilde{A}\sqsubseteq C,\ \tilde{A}\sqcap
D\sqsubseteq\bot,\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}^{\\!\\!d}[\top\sqsubseteq\exists\tilde{R}.\tilde{A}]\\}$
$\displaystyle\mathcal{K}_{\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}[C(a)]}$
$\displaystyle\mathrel{\,:=\,}\\{\tilde{A}\sqcap C\sqsubseteq\bot,\
\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}^{\\!\\!d}[\tilde{A}(a)]\\}$
$\displaystyle\mathcal{K}_{\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}[R(a,b)]}$
$\displaystyle\mathrel{\,:=\,}\\{\tilde{B}(b),\ \tilde{A}\sqcap\exists
R.\tilde{B}\sqsubseteq\bot,\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}^{\\!\\!d}[\tilde{A}(a)]\\}$

Thereby,
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}^{\\!\\!d}\mathrel{\,:=\,}\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}$
and
$\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}^{\\!\\!d}\mathrel{\,:=\,}\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}$,
and $\tilde{A},\tilde{B}$ denote fresh concept names and $\tilde{R}$ a fresh
role name.

Concept satisfiability (w.r.t. $\mathcal{K}$):

Given $\mathcal{K}$ and a modalised concept term $C$, is there a model
$\mathfrak{D}$ of $\mathcal{K}$ with $C^{\mathfrak{D}}\neq\emptyset$?
This task can be solved by checking the axiom entailment
$\mathcal{K}\models\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}[C\sqsubseteq\bot]$.
If the entailment holds, then $C$ is unsatisfiable w.r.t. $\mathcal{K}$,
otherwise it is satisfiable.

Instance retrieval:

Given $\mathcal{K}$ and a modalised concept term $C$, obtain all $a\in
N_{\mathsf{I}}$ with $a^{\mathfrak{D}}\in C^{\mathfrak{D}}$ for every model
$\mathfrak{D}$ of $\mathcal{K}$.
This task can be solved by checking, for all individuals $a$, if the
entailment
$\mathcal{K}\models\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}[C(a)]$
holds and returning all such $a$.

For boxed GCIs, the latter problem can be reduced to the former as follows:

$\displaystyle\mathrel{\phantom{\iff}}\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}\not\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]$ $\displaystyle\iff\text{for some
}\mathfrak{D}\models\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}\text{
we have
}\mathfrak{D}\not\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]$ $\displaystyle\iff\text{for some
}\mathfrak{D}\models\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}\text{
there is a }\pi\in\sigma(\mathsf{s})\text{ such that
}C^{\gamma(\pi)}\not\subseteq D^{\gamma(\pi)}$ $\displaystyle\iff\text{for
some
}\mathfrak{D}\models\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}\text{
there is a }\pi\in\sigma(\mathsf{s})\text{ and a }\delta\in\Delta\text{ with
}\delta\in C^{\gamma(\pi)}\text{ but }\delta\notin D^{\gamma(\pi)}$
$\displaystyle\iff\mbox{$\left\langle\mathcal{C}\cup\left\\{\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C_{a}\sqcap
D\sqsubseteq\bot]\right\\},\mathcal{A}\cup\left\\{a:C,a:C_{a}\right\\}\right\rangle$}\text{
is satisfiable}$

where $a\in N_{\mathsf{I}}$ and $C_{a}\in N_{\mathsf{C}}$ are fresh symbols
not occurring in $\mathcal{K}$.

Dually, for “diamonded” GCIs we can use the following:

$\displaystyle\mathrel{\phantom{\iff}}\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}\not\models\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]$ $\displaystyle\iff\text{for some
}\mathfrak{D}\models\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}\text{
we have
}\mathfrak{D}\not\models\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]$ $\displaystyle\iff\text{for some
}\mathfrak{D}\models\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}\text{
we find that }\pi\in\sigma(\mathsf{s})\text{ implies
}C^{\gamma(\pi)}\not\subseteq D^{\gamma(\pi)}$ $\displaystyle\iff\text{for
some
}\mathfrak{D}\models\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}\text{
we find that for each }\pi\in\sigma(\mathsf{s})\text{ there is a }\delta\in
C^{\gamma(\pi)}\setminus D^{\gamma(\pi)}$
$\displaystyle\iff\mbox{$\left\langle\mathcal{C}\cup\left\\{\top\sqsubseteq\exists
R.C^{\prime},\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C^{\prime}\sqsubseteq
C],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C^{\prime}\sqcap
D\sqsubseteq\bot]\right\\},\mathcal{A}\right\rangle$}\text{ is satisfiable}$

where $C^{\prime}\in N_{\mathsf{C}}$ and $R\in N_{\mathsf{R}}$ are fresh
symbols not occurring in $\mathcal{K}$.

###  2.0.3 Normalisation

Before we can describe a PTime algorithm for checking satisfiability of
$\mathbb{S}_{\mathcal{E\\!L}}$ knowledge bases, we need to introduce an
appropriate normal form.

######  Definition 1 (Normal Form of $\mathbb{S}_{\mathcal{E\\!L}}$ Knowledge
Bases).

A TBox $\mathcal{T}$ is in _normal form_ iff, for all its GCIs
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq D],$$C$ is of
the form $A$, $\exists R.A$ or $A\sqcap A^{\prime}$ with
$A,\\!A^{\prime}{\,\in\,}N_{\mathsf{C}}{\,\cup\,}\\{\top\\}$ and $D$ is of the
form $B$, $\exists R.B$,
$\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B$ or
$\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B$ with
$B{\,\in\,}N_{\mathsf{C}}{\,\cup\,}\\{\bot\\}$, where $R\in N_{\mathsf{R}}$,
and $\hbox{$\mathsf{s}$},\hbox{$\mathsf{s^{\prime}}$}\in N_{\mathsf{S}}$.
An ABox $\mathcal{A}$ is in _normal form_ iff all assertions have the form
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A(a)]$ or
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[R(a,b)]$ for
$a,\\!b{\,\in\,}N_{\mathsf{I}}$, $A{\,\in\,}N_{\mathsf{C}}$, and
$R{\,\in\,}N_{\mathsf{R}}$.
$\mathcal{K}=\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}$
is in _normal form_ whenever $\mathcal{T}$ and $\mathcal{A}$ are.  ❑

For a given $\mathbb{S}_{\mathcal{E\\!L}}$ knowledge base
$\mathcal{K}=\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}$,
we can compute its normal form by exhaustively applying the following
transformation rules (where “rule application” means that the axiom on the
left-hand side is replaced with the set of axioms on the right-hand side):

$\displaystyle\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C(a)]$
$\displaystyle\rightarrow\left\\{\mathsf{v}\preceq\mathsf{s},\mathord{\mathop{\square}\nolimits_{\mathsf{v}}}[C(a)]\right\\}$
(11) $\displaystyle\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[R(a,b)]$
$\displaystyle\rightarrow\left\\{\mathsf{v}\preceq\mathsf{s},\mathord{\mathop{\square}\nolimits_{\mathsf{v}}}[R(a,b)]\right\\}$
(12)
$\displaystyle\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]$
$\displaystyle\rightarrow\left\\{\mathsf{v}\preceq\mathsf{s},\mathord{\mathop{\square}\nolimits_{\mathsf{v}}}[C\sqsubseteq
D]\right\\}$ (13)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}(a)]$
$\displaystyle\rightarrow\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A(a)],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq\bar{C}]\right\\}$
(14)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq\exists
R.\bar{C}]$
$\displaystyle\rightarrow\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq\exists
R.A],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq\bar{C}]\right\\}$
(15)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq
C\sqcap D]$
$\displaystyle\rightarrow\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq
A],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
C],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq D]\right\\}$
(16)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq\mathord{\mathop{\odot}\nolimits_{\mathsf{u}}}\bar{D}]$
$\displaystyle\rightarrow\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq\mathord{\mathop{\odot}\nolimits_{\mathsf{u}}}A],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq\bar{D}]\right\\}$
(17)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq\top]$
$\displaystyle\rightarrow\emptyset\quad\text{and}\quad\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bot\sqsubseteq
D]\rightarrow\emptyset$ (18)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\exists
R.\bar{C}\sqsubseteq D]$
$\displaystyle\rightarrow\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqsubseteq
A],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\exists R.A\sqsubseteq
D]\right\\}$ (19)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqcap
D\sqsubseteq E]$
$\displaystyle\rightarrow\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqsubseteq
A],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqcap D\sqsubseteq
E]\right\\}$ (20)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{u}}}C\sqsubseteq
D]$
$\displaystyle\rightarrow\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[C\sqsubseteq\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
D]\right\\}$ (21)
$\displaystyle\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}C\sqsubseteq
D]$
$\displaystyle\rightarrow\\{\mathsf{v}_{0}\preceq\mathsf{u},\mathsf{v}_{1}\preceq\mathsf{u},\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[C\sqsubseteq
A],$
$\displaystyle\qquad\qquad\quad\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A\sqsubseteq
D]\\}$ (22)

Therein, $\bar{C}$ and $\bar{D}$ stand for complex concept terms not contained
in $N_{\mathsf{C}}{\,\cup\,}\\{\top\\}$, and each occurrence of $A$ on a
right-hand side denotes the introduction of a fresh concept name; likewise,
$\mathsf{v}$, $\mathsf{v}_{0}$, and $\mathsf{v}_{1}$ denote of a fresh
standpoint name. Rule (20) is applied modulo commutativity of $\sqcap$. Most
of the transformation rules should be intuitive (keep in mind that standpoints
must be nonempty). A notable exception is Rule (22), which is crucial to
remove boxes occurring with negative polarity. It draws some high-level
inspiration from existing work on non-vacuous left-hand-side universal
quantifiers in Horn DLs Carral et al. (2014), yet the argument for its
correctness requires a more intricate model-theoretic construction and hinges
on “Hornness” of $\mathcal{K}$ and nonemptiness of standpoints. A careful
analysis yields that the transformation has the desired semantic and
computational properties.

######  Lemma 1.

Every $\mathbb{S}_{\mathcal{E\\!L}}$ knowledge base $\mathcal{K}$ can be
transformed into a $\mathbb{S}_{\mathcal{E\\!L}}$ knowledge base
$\mathcal{K}^{\prime}$ in normal form such that:

  * •

$\mathcal{K}^{\prime}$ is a $\mathbb{S}_{\mathcal{E\\!L}}$-conservative
extension of $\mathcal{K}$,

  * •

the size of $\mathcal{K}^{\prime}$ is at most linear in the size of
$\mathcal{K}$, and

  * •

the transformation can be computed in PTime.

While $\mathcal{K}^{\prime}$ being a
$\mathbb{S}_{\mathcal{E\\!L}}$-conservative extension of $\mathcal{K}$ brings
about various valuable properties, what matters for our purposes is that this
implies equisatisfiability of $\mathcal{K}$ and $\mathcal{K}^{\prime}$, thus
we will not go into details about conservative extensions.

We will next show Lemma 1, where we will concentrate on normalising TBoxes. By
introducing new standpoint, concept, and role names, any TBox $\mathcal{T}$
can be turned into a normalised TBox $\mathcal{T}^{\prime}$ that is a
conservative extension of $\mathcal{T}$, i.e., every model of
$\mathcal{T}^{\prime}$ is also a model of $\mathcal{T}$, and every model of
$\mathcal{T}$ can be extended to a model of $\mathcal{T}^{\prime}$ by
appropriately choosing the interpretations of the additional standpoint,
concept, and role names.

To show that this transformation can be done in polynomial time, yielding a
normalised TBox $\mathcal{T}^{\prime}$ whose size is linear in the size of
$\mathcal{T}$, we next define the size $\left\lVert\mathcal{K}\right\rVert$ of
a knowledge base $\mathcal{K}$ roughly as the number of symbols needed to
write down $\mathcal{K}$, and define it formally as follows.

######  Definition 2.

Let
$\mathcal{K}=\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}$
be a Standpoint DL knowledge base. The _size_ of $\mathcal{K}$, denoted
$\left\lVert\mathcal{K}\right\rVert$, and its various constituents is defined
inductively as follows:

$\displaystyle\left\lVert\mathsf{s}\preceq\mathsf{u}\right\rVert$
$\displaystyle\mathrel{\,:=\,}2$
$\displaystyle\left\lVert\mathcal{S}\right\rVert$
$\displaystyle\mathrel{\,:=\,}\sum_{\zeta\in\mathcal{S}}\left\lVert\zeta\right\rVert$
$\displaystyle\left\lVert\top\right\rVert$ $\displaystyle\mathrel{\,:=\,}1$
$\displaystyle\left\lVert\bot\right\rVert$ $\displaystyle\mathrel{\,:=\,}1$
$\displaystyle\left\lVert A\right\rVert$ $\displaystyle\mathrel{\,:=\,}1$
$\displaystyle\text{ for }A\in N_{\mathsf{C}}$ $\displaystyle\left\lVert
C\sqcap D\right\rVert$ $\displaystyle\mathrel{\,:=\,}1+\left\lVert
C\right\rVert+\left\lVert D\right\rVert$ $\displaystyle\left\lVert\exists
R.C\right\rVert$ $\displaystyle\mathrel{\,:=\,}1+\left\lVert C\right\rVert$
$\displaystyle\left\lVert\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}C\right\rVert$
$\displaystyle\mathrel{\,:=\,}1+\left\lVert C\right\rVert$
$\displaystyle\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}C\right\rVert$
$\displaystyle\mathrel{\,:=\,}1+\left\lVert C\right\rVert$
$\displaystyle\left\lVert C\sqsubseteq D\right\rVert$
$\displaystyle\mathrel{\,:=\,}1+\left\lVert C\right\rVert+\left\lVert
D\right\rVert$
$\displaystyle\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]\right\rVert$ $\displaystyle\mathrel{\,:=\,}1+\left\lVert C\sqsubseteq
D\right\rVert$
$\displaystyle\left\lVert\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]\right\rVert$ $\displaystyle\mathrel{\,:=\,}1+\left\lVert C\sqsubseteq
D\right\rVert$ $\displaystyle\left\lVert\mathcal{T}\right\rVert$
$\displaystyle\mathrel{\,:=\,}\sum_{\tau\in\mathcal{T}}\left\lVert\tau\right\rVert$
$\displaystyle\left\lVert C(a)\right\rVert$
$\displaystyle\mathrel{\,:=\,}1+\left\lVert C\right\rVert$
$\displaystyle\left\lVert R(a_{1},a_{2})\right\rVert$
$\displaystyle\mathrel{\,:=\,}3$
$\displaystyle\left\lVert\mathcal{A}\right\rVert$
$\displaystyle\mathrel{\,:=\,}\sum_{\alpha\in\mathcal{A}}\left\lVert\alpha\right\rVert$
$\displaystyle\left\lVert\mathcal{K}\right\rVert$
$\displaystyle\mathrel{\,:=\,}\left\lVert\mathcal{S}\right\rVert+\left\lVert\mathcal{T}\right\rVert+\left\lVert\mathcal{A}\right\rVert$

❑

[Proof of Lemma 1] Let
$\mathcal{K}=\mbox{$\left\langle\mathcal{S},\mathcal{T},\mathcal{A}\right\rangle$}$
be a Standpoint $\mathcal{E\\!L}$ knowledge base where w.l.o.g. $\mathcal{A}$
is in normal form. The rest of $\mathcal{K}$ (that is, $\mathcal{T}$, since
there is only one form of sharpening statements) can be converted into normal
form by exhaustively applying the replacement rules shown on page 2.0.3. In
what follows, let $\mathcal{T}$ be an arbitrary TBox and let
$\mathcal{T}^{\prime}$ result from exhaustive rule application to
$\mathcal{T}$. To prove the lemma, we proceed to show the following:

  1. 1.

Polynomial runtime and linear output size: Application of the normalisation
rules terminates after at most a polynomial (in the size of $\mathcal{T}$)
number of steps, and the size of the resulting TBox $\mathcal{T}^{\prime}$ is
at most linear in the size of $\mathcal{T}$.

  2. 2.

Syntactic Correctness: $\mathcal{T}^{\prime}$ is in normal form according to
Definition 1.

  3. 3.

Semantic Correctness:
$\mathcal{K}^{\prime}=\mbox{$\left\langle\mathcal{S}^{\prime},\mathcal{T}^{\prime},\mathcal{A}\right\rangle$}$
is a conservative extension of $\mathcal{K}$, more specifically:

(a)

For every model $\mathfrak{D}$ of $\mathcal{K}$ there exists a DL standpoint
structure $\mathfrak{D}^{\prime}$ that extends $\mathfrak{D}$ (agrees with
$\mathfrak{D}$ on the vocabulary of $\mathcal{K}$) and that is a model of
$\mathcal{K}^{\prime}$.

(b)

Every model $\mathfrak{D}^{\prime}$ of $\mathcal{K}^{\prime}$ is also a model
of $\mathcal{K}$.

In most of the cases, we can however restrict our attention to
$\mathcal{T}^{\prime}$.

  1. 1.

We first show that normalisation must terminate after at most
$\left\lVert\mathcal{T}\right\rVert$ normalisation rule applications. The
proof plan is as follows: We define the multiset
$\mathcal{C}_{\mathcal{T}}:\mathsf{SC}_{\mathcal{T}}\to\mathbb{N}$ that
contains one copy for each occurence of a concept term occurring in
$\mathcal{T}$. We observe that for each complex concept $\bar{C}$ causing some
GCI not to be in normal form, a constant number of normalisation rule
applications can be used to strictly decrease the cardinality of $\bar{C}$ in
$\mathcal{C}_{\mathcal{T}}$. Together with the fact that
$\sum_{D\in\mathsf{SC}_{\mathcal{T}}}\mathcal{C}_{\mathcal{T}}(D)\leq\left\lVert\mathcal{T}\right\rVert$,
the claim then follows.

First of all, rules (11)–(14) and in particular rule (13) are only applied
once per axiom type, so in what follows we may safely assume that
$\mathcal{T}$ contains only GCIs of the form
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq D]$. Define the
set $\mathsf{SC}_{\mathcal{T}}$ as the least set such that:

     * •

If $\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]\in\mathcal{T}$, then $C,D\in\mathsf{SC}_{\mathcal{T}}$;

     * •

if $C\in\mathsf{SC}_{\mathcal{T}}$, then for all subconcepts $C^{\prime}$ of
$C$ (written $C^{\prime}\in\mathsf{sub}(C)$) we have
$C^{\prime}\in\mathsf{SC}_{\mathcal{T}}$.

Now for any TBox $\mathcal{T}^{\prime}$ (typically obtained from $\mathcal{T}$
by applying zero or more normalisation rules), the multiset
$\mathcal{C}_{\mathcal{T}^{\prime}}\colon\mathsf{SC}_{\mathcal{T}}\to\mathbb{N}$
is then as follows:

$\displaystyle C$
$\displaystyle\mapsto\sum_{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D\sqsubseteq
E]\in\mathcal{T}^{\prime}}\left(c(C,D)+c(C,E)\right)$ where we define the
concept-counting function
$c\colon\mathsf{SC}_{\mathcal{T}}\times\mathsf{SC}_{\mathcal{T}}\to\mathbb{N}$
inductively: $\displaystyle c(C,D)$
$\displaystyle\mathrel{\,:=\,}\begin{cases}1&\text{ if }C=D,\\\ c(C,E)&\text{
if }C\neq D\text{ and }[D=\exists R.E\text{ or
}D=\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}E]\\\
c(C,E_{1})+c(C,E_{2})&\text{ if }C\neq D\text{ and }D=E_{1}\sqcap E_{2}\\\
0&\text{ if }C\neq D\text{ and }D\in
N_{\mathsf{C}}\cup\left\\{\top,\bot\right\\}\end{cases}$

For example if
$D=\top\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}(\top\sqcap\exists
R.(\top\sqcap\top))$, then $c(\top,D)=4$ while $c(\top\sqcap\top,D)=1$.

We next relate the overall cardinality (sum of number of occurrences) of
$\mathcal{C}_{\mathcal{T}}$ to the size $\left\lVert\mathcal{T}\right\rVert$
on the basis that both can be represented as disjoint unions and we can
therefore sum up the individual cardinalities.

######  Claim 1.

We have
$\sum_{C\in\mathsf{SC}_{\mathcal{T}}}\mathcal{C}_{\mathcal{T}}(C)\leq\left\lVert\mathcal{T}\right\rVert$.

######  Proof of the claim.

As
$\left\lVert\mathcal{T}\right\rVert=\sum_{\tau\in\mathcal{T}}\left\lVert\tau\right\rVert$
and

$\sum_{C\in\mathsf{SC}_{\mathcal{T}}}\mathcal{C}_{\mathcal{T}}(C)=\sum_{C\in\mathsf{SC}_{\mathcal{T}}}\sum_{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D\sqsubseteq
E]\in\mathcal{T}}\left(c(C,D)+c(C,E)\right)=\sum_{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D\sqsubseteq
E]\in\mathcal{T}}\sum_{C\in\mathsf{SC}_{\mathcal{T}}}\left(c(C,D)+c(C,E)\right)$

it suffices to look at a single
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D\sqsubseteq
E]\in\mathcal{T}$ and show

$\sum_{C\in\mathsf{SC}_{\mathcal{T}}}\left(c(C,D)+c(C,E)\right)\leq\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D\sqsubseteq
E]\right\rVert$

which by

$\sum_{C\in\mathsf{SC}_{\mathcal{T}}}\left(c(C,D)+c(C,E)\right)=\sum_{D^{\prime}\in\mathsf{sub}(D)}c(D^{\prime},D)+\sum_{E^{\prime}\in\mathsf{sub}(E)}c(E^{\prime},E)$

develops into

$\sum_{D^{\prime}\in\mathsf{sub}(D)}c(D^{\prime},D)+\sum_{E^{\prime}\in\mathsf{sub}(E)}c(E^{\prime},E)\leq\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D\sqsubseteq
E]\right\rVert=1+1+\left\lVert D\right\rVert+\left\lVert E\right\rVert$

for which it suffices to show that for any concept
$C\in\mathsf{SC}_{\mathcal{T}}$, we have
$\sum_{C^{\prime}\in\mathsf{sub}(C)}c(C^{\prime},C)\leq\left\lVert
C\right\rVert$, which we show by induction.

     * •

The base case is clear, as
$\sum_{C^{\prime}\in\mathsf{sub}(C)}c(C^{\prime},C)=c(C,C)=1\leq 1=\left\lVert
C\right\rVert$ for any $C\in N_{\mathsf{C}}\cup\left\\{\top,\bot\right\\}$.

     * •

$C=\exists R.D$:

$\displaystyle\mathrel{\phantom{=}}\sum_{C^{\prime}\in\mathsf{sub}(\exists
R.D)}c(C^{\prime},\exists R.D)$ $\displaystyle=c(\exists R.D,\exists
R.D)+\sum_{C^{\prime}\in\mathsf{sub}(D)}c(C^{\prime},D)$
$\displaystyle\stackrel{{\scriptstyle\text{(IH)}}}{{\leq}}=c(\exists
R.D,\exists R.D)+\left\lVert D\right\rVert$ $\displaystyle=1+\left\lVert
D\right\rVert$ $\displaystyle=\left\lVert\exists R.D\right\rVert$

     * •

$C=\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}D$: Similar.

     * •

$C=C_{1}\sqcap C_{2}$:

$\displaystyle\mathrel{\phantom{=}}\sum_{C^{\prime}\in\mathsf{sub}(C_{1}\sqcap
C_{2})}c(C^{\prime},C_{1}\sqcap C_{2})$ $\displaystyle=c(C_{1}\sqcap
C_{2},C_{1}\sqcap
C_{2})+\sum_{C^{\prime}\in\mathsf{sub}(C_{1})}c(C^{\prime},C_{1})+\sum_{C^{\prime}\in\mathsf{sub}(C_{2})}c(C^{\prime},C_{2})$
$\displaystyle\stackrel{{\scriptstyle\text{(IH)}}}{{\leq}}c(C_{1}\sqcap
C_{2},C_{1}\sqcap C_{2})+\left\lVert C_{1}\right\rVert+\left\lVert
C_{2}\right\rVert$ $\displaystyle=1+\left\lVert C_{1}\right\rVert+\left\lVert
C_{2}\right\rVert$ $\displaystyle=\left\lVert C_{1}\sqcap C_{2}\right\rVert$

This concludes the proof of 1.  ❑

To prove an overall linear number of rule applications, we next show that for
each complex concept $\bar{C}$ whose occurence in a GCI
$\tau\in\mathcal{T}^{\prime}$ causes $\tau$ not to be in normal form, there is
a constant number of rule applications (that is, constant for all TBoxes) such
that after rule application, the number of overall occurrences of $\bar{C}$
has strictly decreased and additionally, any intermediate complex concepts
introduced by the rule have been normalised in turn. To this end, we need to
define some more notions. Let $\mathcal{T}$ be a TBox and
$\mathcal{T}^{\prime}$ be obtained by application of an arbitrary number of
normalisation rules. We say that a complex concept $\bar{C}$ occurring in a
GCI $\tau\in\mathcal{T}^{\prime}$ is a _culprit for $\tau$_ iff $\tau$ is not
in normal form because of $\bar{C}$; a culprit $\bar{C}$ is _top-level_ for
$\tau=\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D\sqsubseteq E]$ iff
$\bar{C}=D$ or $\bar{C}=E$. We say that $\mathcal{T}^{\prime}$ is _faithful to
$\mathcal{T}$_ iff every culprit occurring in $\mathcal{T}^{\prime}$ already
occurs in $\mathcal{T}$. In the proof below, we show that although
normalisation rules sometimes introduce new culprits, those culprits will not
lead to problems because each one can only cause a constant overhead.

######  Claim 2.

Let $\mathcal{T}$ be a TBox and let $\mathcal{T}^{\prime}$ be obtained from
$\mathcal{T}$ by applying any number of rules from (15)–(22). Let $\bar{C}$ be
a top-level culprit for $\tau\in\mathcal{T}^{\prime}$. Then there is a
constant number of rule applications leading to a TBox
$\mathcal{T}^{\prime\prime}$ that is faithful to $\mathcal{T}$ and where
$\mathcal{C}_{\mathcal{T}^{\prime}}(\bar{C})>\mathcal{C}_{\mathcal{T}^{\prime\prime}}(\bar{C})$.

######  Proof of the claim.

We do a case distinction on the occurrence (left-hand vs. right-hand side) and
form of $\bar{C}$. In every case, we will explicitly give the (constantly
many) rules to apply to decrease the cardinality of $\bar{C}$. In most cases,
it is easy to see that only one rule is needed, we show this exemplarily for
one case and then concentrate on the two non-trivial cases.

     * •

$\bar{C}=\exists R.\bar{D}$ occurs on the right-hand side: Then we apply rule
(15), removing one occurrence of $\bar{C}$. The resulting
$\mathcal{T}^{\prime\prime}$ is faithful because the only newly introduced
concept terms are $\exists R.A$ on a right-hand side and $A$ on a left-hand
side, and neither of these is a culprit.

     * •

$\bar{C}=D_{1}\sqcap D_{2}$ or
$\bar{C}=\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}D$ and $\bar{C}$ occurs
on the right-hand side: Similar.

     * •

$\bar{C}=\exists R.\bar{D}$ or
$\bar{C}=\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}D$ and $\bar{C}$
occurs on the left-hand side: Exercise.

     * •

$\bar{C}=D_{1}\sqcap D_{2}$ occurs on the left-hand side: Denote
$\tau=\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqsubseteq
E]=\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D_{1}\sqcap
D_{2}\sqsubseteq E]$. We apply rule (20) and obtain
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D_{1}\sqsubseteq A]$ and
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqcap D_{2}\sqsubseteq
E]$, thus removing once occurence of $\bar{C}$. The latter rule contains the
(new) culprit $A\sqcap D_{2}$ to which we can apply the same rule again
(modulo commutativity) to obtain
$\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[D_{2}\sqsubseteq
A^{\prime}]$ and $\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqcap
A^{\prime}\sqsubseteq E]$. The only remaining (potential) culprits are
$D_{1}$, $D_{2}$, and $E$, whence the resulting $\mathcal{T}^{\prime\prime}$
is faithful to $\mathcal{T}$.

     * •

$\bar{C}=\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}D$ occurs on the
left-hand side: Denote
$\tau=\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}D\sqsubseteq
E]$. We apply rules (to underlined GCIs) as follows:

$\displaystyle\mathrel{\phantom{\leadsto}}\left\\{\underline{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}D\sqsubseteq
E]}\right\\}$ $\displaystyle\stackrel{{\scriptstyle\text{(\ref{norm:box-
left})}}}{{\leadsto}}\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[D\sqsubseteq
A_{1}],\underline{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A_{1}\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A_{1}\sqsubseteq
E]}\right\\}$
$\displaystyle\stackrel{{\scriptstyle\text{(\ref{norm:conjunction-
left})}}}{{\leadsto}}\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[D\sqsubseteq
A_{1}],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A_{1}\sqsubseteq
A_{2}],\underline{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A_{2}\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A_{1}\sqsubseteq
E]}\right\\}$
$\displaystyle\stackrel{{\scriptstyle\text{(\ref{norm:conjunction-
left})}}}{{\leadsto}}\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[D\sqsubseteq
A_{1}],\underline{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A_{1}\sqsubseteq
A_{2}]},\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A_{1}\sqsubseteq
A_{3}],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A_{2}\sqcap
A_{3}\sqsubseteq E]\right\\}$
$\displaystyle\stackrel{{\scriptstyle\text{(\ref{norm:diamond-
left})}}}{{\leadsto}}\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[D\sqsubseteq
A_{1}],\mathord{\mathop{\square}\nolimits_{\mathsf{\mathsf{v}_{0}}}}[A_{1}\sqsubseteq\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A_{4}],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A_{4}\sqsubseteq
A_{2}],\underline{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A_{1}\sqsubseteq
A_{3}]},\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A_{2}\sqcap
A_{3}\sqsubseteq E]\right\\}$
$\displaystyle\stackrel{{\scriptstyle\text{(\ref{norm:diamond-
left})}}}{{\leadsto}}\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[D\sqsubseteq
A_{1}],\mathord{\mathop{\square}\nolimits_{\mathsf{\mathsf{v}_{0}}}}[A_{1}\sqsubseteq\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A_{4}],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A_{4}\sqsubseteq
A_{2}],\mathord{\mathop{\square}\nolimits_{\mathsf{\mathsf{v}_{1}}}}[A_{1}\sqsubseteq\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A_{5}],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A_{5}\sqsubseteq
A_{3}],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A_{2}\sqcap
A_{3}\sqsubseteq E]\right\\}$

It is easy to see that $D$ and $E$ are the only remaining (potential)
culprits, and that one occurence of
$\bar{C}=\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}D$ has been removed.

❑

Thus each culprit will be not only be removed eventually, but removing each
single occurrence will take only a constant number of steps. Therefore, the
number of rule applications is linear in
$\sum_{C\in\mathsf{SC}_{\mathcal{T}}}\mathcal{C}_{\mathcal{T}}(C)$. By 1, the
number of rule applications is linear in $\left\lVert\mathcal{T}\right\rVert$,
thus linear in $\left\lVert\mathcal{K}\right\rVert$.

It remains to show that the overall increase in size is at most linear. We do
this by showing that for each single rule, the size increase caused by its
application is constant. Together with the overall linear number of rule
applications, it follows that the size of the resulting normalised TBox
$\mathcal{T}^{\prime}$ is at most linear in the size of the original TBox
$\mathcal{T}$.

Rule (13):

$\displaystyle\mathrel{\phantom{=}}\left\lVert\mathsf{v}\preceq\mathsf{s}\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{v}}}[C\sqsubseteq
D]\right\rVert-\left\lVert\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]\right\rVert$ $\displaystyle=2+1+1+\left\lVert C\right\rVert+\left\lVert
D\right\rVert-\left(1+1+\left\lVert C\right\rVert+\left\lVert
D\right\rVert\right)$ $\displaystyle=2$

Rule (15):

$\displaystyle\mathrel{\phantom{=}}\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq\exists
R.A]\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq\bar{C}]\right\rVert-\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq\exists
R.\bar{C}]\right\rVert$ $\displaystyle=1+1+\left\lVert
B\right\rVert+2+1+1+1+\left\lVert\bar{C}\right\rVert-\left(1+1+\left\lVert
B\right\rVert+1+\left\lVert\bar{C}\right\rVert\right)$ $\displaystyle=4$

Rule (16):

$\displaystyle\mathrel{\phantom{=}}\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq
A]\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
C]\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
D]\right\rVert-\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq
C\sqcap D]\right\rVert$ $\displaystyle=(1+1+\left\lVert
B\right\rVert+1)+(1+1+1+\left\lVert C\right\rVert)+(1+1+1+\left\lVert
D\right\rVert)-\left(1+1+\left\lVert B\right\rVert+1+\left\lVert
C\right\rVert+\left\lVert D\right\rVert\right)$ $\displaystyle=6$

Rule (17):

$\displaystyle\mathrel{\phantom{=}}\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq\mathord{\mathop{\odot}\nolimits_{\mathsf{u}}}A]\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq\bar{D}]\right\rVert-\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq\mathord{\mathop{\odot}\nolimits_{\mathsf{u}}}\bar{D}]\right\rVert$
$\displaystyle=1+1+\left\lVert
C\right\rVert+2+1+1+1+\left\lVert\bar{D}\right\rVert-\left(1+1+\left\lVert
C\right\rVert+1+\left\lVert\bar{D}\right\rVert\right)$ $\displaystyle=4$

Rule (18):

Clear.

Rule (19):

$\displaystyle\mathrel{\phantom{=}}\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqsubseteq
A]\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\exists
R.A\sqsubseteq D]\right\rVert-\left\lVert\exists R.\bar{C}\sqsubseteq
D\right\rVert$
$\displaystyle=1+1+\left\lVert\bar{C}\right\rVert+1+1+1+2+\left\lVert
D\right\rVert-\left(1+1+\left\lVert\bar{C}\right\rVert+\left\lVert
D\right\rVert\right)$ $\displaystyle=5$

Rule (20):

$\displaystyle\mathrel{\phantom{=}}\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqsubseteq
A]\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqcap
D\sqsubseteq
E]\right\rVert-\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqcap
D\sqsubseteq E]\right\rVert$
$\displaystyle=1+1+\left\lVert\bar{C}\right\rVert+1+1+1+1+1+\left\lVert
D\right\rVert+\left\lVert
E\right\rVert-\left(1+1+1+\left\lVert\bar{C}\right\rVert+\left\lVert
D\right\rVert+\left\lVert E\right\rVert\right)$ $\displaystyle=4$

Rule (21):

$\displaystyle\mathrel{\phantom{=}}\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[C\sqsubseteq\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A]\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
D]\right\rVert-\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{u}}}C\sqsubseteq
D]\right\rVert$ $\displaystyle=1+1+\left\lVert
C\right\rVert+2+1+1+1+\left\lVert D\right\rVert-(1+1+1+\left\lVert
C\right\rVert+\left\lVert D\right\rVert)$ $\displaystyle=4$

Rule (22):

$\displaystyle\mathrel{\phantom{=}}\left\lVert\mathsf{v}_{0}\preceq\mathsf{u}\right\rVert+\left\lVert\mathsf{v}_{1}\preceq\mathsf{u}\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[C\sqsubseteq
A]\right\rVert+\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A\sqsubseteq
D]\right\rVert-\left\lVert\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}C\sqsubseteq
D]\right\rVert$ $\displaystyle=2+2+1+1+\left\lVert
C\right\rVert+1+1+1+2+2+\left\lVert D\right\rVert-(1+1+1+\left\lVert
C\right\rVert+\left\lVert D\right\rVert)$ $\displaystyle=10$

  2. 2.

Assume that $\mathcal{T}^{\prime}$ is the result of exhaustively applying the
normalisation rules (13)–(17) to $\mathcal{T}$. The proof is by contradiction.
Assume that a GCI $\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]$ is not in normal form; we do a case distinction on the possible reasons
for this where in each case it will turn out that at least one of the rules is
applicable in contradiction to the presumption.

     * •

$\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}\neq\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}$:
Then
$\mathord{\mathop{\odot}\nolimits_{\mathsf{s}}}=\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}$
and Rule (13) is applicable.

     * •

$D$ is of the form $\exists R.E$ with
$E\notin\mathsf{BC}_{\mathcal{K}}\cup\left\\{\bot\right\\}$: Then Rule (15) is
applicable.

     * •

$D$ is of the form $E_{1}\sqcap E_{2}$: Then Rule (16) is applicable.

     * •

$D$ is of the form $\mathord{\mathop{\odot}\nolimits_{\mathsf{s^{\prime}}}}E$
with $E\notin\mathsf{BC}_{\mathcal{K}}\cup\left\\{\bot\right\\}$: Then Rule
(17) is applicable.

     * •

$D=\top$ or $C=\bot$: Then Rule (18) is applicable.

     * •

$C$ is of the form $\exists R.B$ with $B\notin\mathsf{BC}_{\mathcal{K}}$: Then
Rule (19) is applicable.

     * •

$C$ is of the form $B_{1}\sqcap B_{2}$ with
$\left\\{B_{1},B_{2}\right\\}\not\subseteq\mathsf{BC}_{\mathcal{K}}$: Then
Rule (20) is applicable.

     * •

$C$ is of the form
$\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B$ with
$B\notin\mathsf{BC}_{\mathcal{K}}$: Then Rule (22) is applicable.

     * •

$C$ is of the form
$\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B$ with
$B\notin\mathsf{BC}_{\mathcal{K}}$: Then Rule (21) is applicable.

  3. 3.

We show correctness of each rule. Correctness of the overall normalisation
process follows by induction on the number of rule applications. We slightly
adapt the notation to denote by
$\mathcal{K}^{\prime}=\mbox{$\left\langle\mathcal{S},\mathcal{T}^{\prime},\mathcal{A}\right\rangle$}$
the KB that results from application _of a single rule_ and do a case
distinction on the rules. In each case, assume
$\mathfrak{D}=\mbox{$\left\langle\Delta,\Pi,\gamma,\sigma\right\rangle$}$ with
$\mathfrak{D}\models\mathcal{K}$ and denote
$\mathfrak{D}^{\prime}=\mbox{$\left\langle\Delta^{\prime},\Pi^{\prime},\gamma^{\prime},\sigma^{\prime}\right\rangle$}$
in case the components differ from those of $\mathfrak{D}$. (In most cases, we
only need to show $\mathfrak{D}^{\prime}\models\mathcal{T}^{\prime}$ and
therefore do not mention the other KB components.)

Rule (13):

(a) Let
$\mathfrak{D}\models\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]$. Then there is a $\pi\in\sigma(\mathsf{s})$ such that
$C^{\gamma(\pi)}\subseteq D^{\gamma(\pi)}$. Define $\mathfrak{D}^{\prime}$
from $\mathfrak{D}$ by
$\sigma^{\prime}(\mathsf{v})\mathrel{\,:=\,}\left\\{\pi\right\\}$. It follows
that $\mathfrak{D}^{\prime}\models\mathsf{v}\preceq\mathsf{s}$ and
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{v}}}[C\sqsubseteq
D]$.

(b) Let $\mathfrak{D}^{\prime}\models\mathcal{T}^{\prime}$ and consider any
$\pi\in\sigma^{\prime}(\mathsf{v})$ (which exists due to standpoint-non-
emptiness). Clearly $\mathfrak{D}^{\prime}\models\mathcal{S}^{\prime}$ shows
$\pi\in\sigma^{\prime}(\mathsf{v})\subseteq\sigma^{\prime}(\mathsf{s})$,
whence $C^{\gamma(\pi)}\subseteq D^{\gamma(\pi)}$ witnesses that
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s}}}[C\sqsubseteq
D]$.

Rule (15):

(a) Let
$\mathfrak{D}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq\exists
R.\bar{C}]$. Define $\mathfrak{D}^{\prime}$ from $\mathfrak{D}$ as follows:
For any $\pi\in\sigma(\mathsf{s})$, set
$A^{\gamma^{\prime}(\pi)}\mathrel{\,:=\,}\bar{C}^{\gamma(\pi)}$. It follows by
definition that
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq\exists
R.A]$ and
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq\bar{C}]$.

(b) Let $\mathfrak{D}^{\prime}\models\mathcal{T}^{\prime}$ and consider any
$\pi\in\sigma^{\prime}(\mathsf{s})$ and $\delta\in B^{\gamma^{\prime}(\pi)}$.
By
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq\exists
R.A]$ we get $\delta\in(\exists R.A)^{\gamma^{\prime}(\pi)}$, whence there is
an $\varepsilon\in\Delta^{\prime}$ with
$\mbox{$\left\langle\delta,\varepsilon\right\rangle$}\in
r^{\gamma^{\prime}(\pi)}$ and $\varepsilon\in A^{\gamma^{\prime}(\pi)}$. By
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq\bar{C}]$,
we get $\varepsilon\in\bar{C}^{\gamma^{\prime}(\pi)}$ and ultimately
$\delta\in(\exists R.\bar{C})^{\gamma^{\prime}(\pi)}$.

Rule (16):

(a) Let
$\mathfrak{D}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq
C\sqcap D]$ and define $\mathfrak{D}^{\prime}$ from $\mathfrak{D}$ by setting,
for each $\pi\in\sigma(\mathsf{s})$,
$A^{\gamma^{\prime}(\pi)}\mathrel{\,:=\,}B^{\gamma(\pi)}$. Then by definition
we get
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq
A]$, as well as
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
C]$ and
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
D]$.

(b) Let $\mathfrak{D}^{\prime}\models\mathcal{T}^{\prime}$ and consider any
$\pi\in\sigma^{\prime}(\mathsf{s})$ and $\delta\in B^{\gamma^{\prime}(\pi)}$.
By
$\mathcal{T}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[B\sqsubseteq
A]$ we get $\delta\in A^{\gamma^{\prime}(\pi)}$. By
$\mathcal{T}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
C]$ and
$\mathcal{T}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
D]$ we get $\delta\in C^{\gamma^{\prime}(\pi)}$ and $\delta\in
D^{\gamma^{\prime}(\pi)}$, respectively. In combination, $\delta\in(C\sqcap
D)^{\gamma^{\prime}(\pi)}$.

Rule (17):

(a) Let
$\mathfrak{D}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq\mathord{\mathop{\odot}\nolimits_{\mathsf{u}}}\bar{D}]$
and define $\mathfrak{D}^{\prime}$ from $\mathfrak{D}$ by setting, for each
$\pi\in\sigma(\mathsf{s})$,
$A^{\gamma^{\prime}(\pi)}\mathrel{\,:=\,}\bar{D}^{\gamma(\pi)}$. It follows
directly that
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq\mathord{\mathop{\odot}\nolimits_{\mathsf{u}}}A]$
and
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq\bar{D}]$.

(b) Let $\mathfrak{D}^{\prime}\models\mathcal{T}^{\prime}$ and consider any
$\pi\in\sigma^{\prime}(\mathsf{s})$ and $\delta\in C^{\gamma^{\prime}(\pi)}$.
From
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq\mathord{\mathop{\odot}\nolimits_{\mathsf{u}}}A]$
we get
$\delta\in(\mathord{\mathop{\odot}\nolimits_{\mathsf{u}}}A)^{\gamma^{\prime}(\pi)}$.
Thus, for some (all) $\pi^{\prime}\in\sigma^{\prime}(\mathsf{u})$, we get
$\delta\in A^{\gamma^{\prime}(\pi^{\prime})}$; and in turn, by
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq\bar{D}]$,
for some (all) $\pi^{\prime}\in\sigma^{\prime}(\mathsf{u})$, we get
$\delta\in\bar{D}^{\gamma^{\prime}(\pi^{\prime})}$.

Rule (18):

Clear, as any DL interpretation satisfies $C\sqsubseteq\top$ and
$\bot\sqsubseteq D$.

Rule (19):

(a) Let
$\mathfrak{D}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\exists
R.\bar{C}\sqsubseteq D]$. Define $\mathfrak{D}^{\prime}$ from $\mathfrak{D}$
as follows: For any $\pi\in\sigma(\mathsf{s})$, set
$A^{\gamma^{\prime}(\pi)}\mathrel{\,:=\,}\bar{C}^{\gamma(\pi)}$. It follows
from this definition that
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqsubseteq
A]$ and
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\exists
R.A\sqsubseteq D]$.

(b) Let $\mathfrak{D}^{\prime}\models\mathcal{T}^{\prime}$ and consider
$\pi\in\sigma^{\prime}(\mathsf{s})$ and any $\delta\in\exists
R.\bar{C}^{\gamma^{\prime}(\pi)}$. There is thus a $\varepsilon\in\Delta$ with
$\mbox{$\left\langle\delta,\varepsilon\right\rangle$}\in
r^{\gamma^{\prime}(\pi)}$ and $\varepsilon\in\bar{C}^{\gamma^{\prime}(\pi)}$.
By
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqsubseteq
A]$ we get $\varepsilon\in A^{\gamma^{\prime}(\pi)}$, and in turn
$\delta\in(\exists R.A)^{\gamma^{\prime}(\pi)}$. By
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\exists
R.A\sqsubseteq D]$, we get $\delta\in D^{\gamma^{\prime}(\pi)}$.

Rule (20):

(a) Let
$\mathfrak{D}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqcap
D\sqsubseteq E]$. Define $\mathfrak{D}^{\prime}$ from $\mathfrak{D}$ as
follows: For any $\pi\in\sigma(\mathsf{s})$, set
$A^{\gamma^{\prime}(\pi)}\mathrel{\,:=\,}\bar{C}^{\gamma(\pi)}$. It follows
from this definition that
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqsubseteq
A]$ and
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqcap
D\sqsubseteq E]$.

(b) Let $\mathfrak{D}^{\prime}\models\mathcal{T}^{\prime}$ and consider
$\pi\in\sigma^{\prime}(\mathsf{s})$ and
$\delta\in\bar{C}^{\gamma^{\prime}(\pi)}\cap D^{\gamma^{\prime}(\pi)}$. By
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\bar{C}\sqsubseteq
A]$ we get $\delta\in A^{\gamma^{\prime}(\pi)}$, and by
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqcap
D\sqsubseteq E]$ and $\delta\in D^{\gamma^{\prime}(\pi)}$ we get $\delta\in
E^{\gamma^{\prime}(\pi)}$.

Rule (21):

(a) Let
$\mathfrak{D}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{u}}}C\sqsubseteq
D]$ and define $\mathfrak{D}^{\prime}$ from $\mathfrak{D}$ by setting
$A^{\gamma^{\prime}(\pi)}\mathrel{\,:=\,}(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{u}}}C)^{\gamma(\pi)}$
for every $\pi\in\Pi$.

     * •

$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[C\sqsubseteq\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A]$:
Let $\pi\in\sigma^{\prime}(\mathsf{u})=\sigma(\mathsf{u})$ and $\delta\in
C^{\gamma^{\prime}(\pi)}=C^{\gamma(\pi)}$. Then by definition, we have
$\delta\in A^{\gamma^{\prime}(\pi)}$ for all $\pi\in\Pi$, whence
$\delta\in(\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A)^{\gamma^{\prime}(\pi)}$.

     * •

$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
D]$: Let $\pi\in\sigma^{\prime}(\mathsf{s})=\sigma(\mathsf{s})$ and $\delta\in
A^{\gamma^{\prime}(\pi)}$. Then by definition,
$\delta\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{u}}}C)^{\gamma(\pi)}$
and by the presumption that
$\mathfrak{D}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{u}}}C\sqsubseteq
D]$ we get $\delta\in D^{\gamma(\pi)}=D^{\gamma^{\prime}(\pi)}$.

(b) Let $\mathfrak{D}^{\prime}\models\mathcal{T}^{\prime}$ and consider
$\pi\in\sigma^{\prime}(\mathsf{s})$ and
$\delta\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{u}}}C)^{\gamma^{\prime}(\pi)}$.
Then there is a $\pi^{\prime}\in\sigma^{\prime}(\mathsf{u})$ such that
$\delta\in C^{\gamma^{\prime}(\pi^{\prime})}$. Thus
$\delta\in(\mathord{\mathop{\square}\nolimits_{\mathsf{*}}}A)^{\gamma^{\prime}(\pi^{\prime})}$,
that is,
$\delta\in\bigcap_{\pi^{\prime\prime}\in\Pi}A^{\gamma^{\prime}(\pi^{\prime\prime})}$.
Thus in particular for $\pi\in\sigma^{\prime}(\mathsf{s})$, we get $\delta\in
A^{\gamma^{\prime}(\pi)}$ and by
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[A\sqsubseteq
D]$ we obtain $\delta\in D^{\gamma^{\prime}(\pi)}$.

Rule (22):

(a) Let
$\mathfrak{D}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}C\sqsubseteq
D]$. We define
$\mathfrak{D}^{\prime}=\mbox{$\left\langle\Delta^{\prime},\Pi^{\prime},\sigma^{\prime},\gamma^{\prime}\right\rangle$}$
as follows:

     * •

$\Delta^{\prime}$ consists of two copies
$\delta^{\prime}_{0},\delta^{\prime}_{1}$ of every function
$\delta^{\prime}\colon\sigma(\mathsf{u})\times\Delta\to\Delta$.

     * •

$\Pi^{\prime}$ consists of all functions
$\pi^{\prime}\colon\sigma(\mathsf{u})\times\Delta\to\Pi$ plus two extra,
distinct copies of the particular function
$\pi^{\prime}_{\mathrm{diag}}\mathrel{\,:=\,}\left\\{(\pi,\delta)\mapsto\pi\right\\}$,
denoted $\pi^{\prime}_{\mathsf{v}_{0}}$ and $\pi^{\prime}_{\mathsf{v}_{1}}$.

     * •

$\sigma^{\prime}(\mathsf{v}_{b})\mathrel{\,:=\,}\left\\{\pi^{\prime}_{\mathsf{v}_{b}}\right\\}$
for each $b\in\left\\{0,1\right\\}$ and, for all other $\mathsf{s}$,

$\sigma^{\prime}(\mathsf{s})\mathrel{\,:=\,}\left\\{\pi^{\prime}\in\Pi^{\prime}\;\middle|\;\mathop{\bigcup_{\pi\in\sigma(\mathsf{u}),}}_{\delta\in\Delta}\left\\{\pi^{\prime}(\pi,\delta)\right\\}\subseteq\sigma(\mathsf{s})\right\\}$

For every $\pi^{\prime}\in\Pi^{\prime}$, the DL interpretation
$\gamma^{\prime}(\pi^{\prime})$ over $\Delta^{\prime}$ is such that

$\displaystyle a^{\gamma^{\prime}(\pi^{\prime})}$
$\displaystyle\mathrel{\,:=\,}\left\\{(\pi,\delta)\mapsto\delta_{a}\right\\}_{0}$
$\displaystyle\text{ for }a\in N_{\mathsf{I}}$

where $\delta_{a}\in\Delta$ denotes the domain element for which
$\delta_{a}=a^{\gamma(\pi)}$ for all $\pi\in\Pi$.
Further, for
$\pi^{\prime}\in\Pi^{\prime}\setminus\\{\pi^{\prime}_{\mathsf{v}_{0}},\pi^{\prime}_{\mathsf{v}_{1}}\\}$,
the DL interpretation $\gamma^{\prime}(\pi^{\prime})$ over $\Delta^{\prime}$
is such that

$\displaystyle A^{\gamma^{\prime}(\pi^{\prime})}$
$\displaystyle\mathrel{\,:=\,}\left\\{\delta^{\prime}_{b}\in\Delta^{\prime}\;\middle|\;\delta^{\prime}_{b}(\pi,\delta)\in
A^{\gamma(\pi^{\prime}(\pi,\delta))}\text{ for all
}{\pi\in\sigma(\mathsf{u})},\ {\delta\in\Delta}\right\\}$ $\displaystyle\text{
for }A\in N_{\mathsf{C}}$ $\displaystyle R^{\gamma^{\prime}(\pi^{\prime})}$
$\displaystyle\mathrel{\,:=\,}\left\\{\mbox{$\left\langle\delta^{\prime}_{b},\varepsilon^{\prime}_{b}\right\rangle$}\in\Delta^{\prime}\times\Delta^{\prime}\;\middle|\;\mbox{$\left\langle\delta^{\prime}_{b}(\pi,\delta),\varepsilon^{\prime}_{b}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi^{\prime}(\pi,\delta))}\text{ for all
}{\pi\in\sigma(\mathsf{u})},\ {\delta\in\Delta}\right\\}$ $\displaystyle\text{
for }R\in N_{\mathsf{R}}$

and $\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})$ assigns as follows:

$\displaystyle A^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$
$\displaystyle\mathrel{\,:=\,}\left(\left\\{\delta^{\prime}_{b}\in\Delta^{\prime}\right\\}\cap
A^{\gamma^{\prime}(\pi^{\prime}_{\mathrm{diag}})}\right)\cup\left\\{\delta^{\prime}_{1-b}\in\Delta^{\prime}\;\middle|\;\bigcup_{{\pi\in\sigma(\mathsf{u}),}\atop{\delta\in\Delta}}\left\\{\delta^{\prime}_{1-b}(\pi,\delta)\right\\}\subseteq{\bigcap_{\pi\in\sigma(\mathsf{u})}}A^{\gamma(\pi)}\right\\}$
$\displaystyle\text{ for }A\in N_{\mathsf{C}}$ $\displaystyle
R^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$
$\displaystyle\mathrel{\,:=\,}\left(\left\\{\mbox{$\left\langle\delta^{\prime}_{b},\varepsilon^{\prime}_{b}\right\rangle$}\in\Delta^{\prime}\times\Delta^{\prime}\right\\}\cap
R^{\gamma^{\prime}(\pi^{\prime}_{\mathrm{diag}})}\right)$
$\displaystyle\quad\cup\left\\{\mbox{$\left\langle\delta^{\prime}_{1-b},\varepsilon^{\prime}_{1-b}\right\rangle$}\in\Delta^{\prime}\times\Delta^{\prime}\;\middle|\;\bigcup_{{\pi\in\sigma(\mathsf{u}),}\atop{\delta\in\Delta}}\left\\{\mbox{$\left\langle\delta^{\prime}_{1-b}(\pi,\delta),\varepsilon^{\prime}_{1-b}(\pi,\delta)\right\rangle$}\right\\}\subseteq{\bigcap_{\pi\in\sigma(\mathsf{u})}}R^{\gamma(\pi)}\right\\}$
$\displaystyle\quad\cup\left\\{\mbox{$\left\langle\delta^{\prime}_{1-b},\varepsilon^{\prime}_{b}\right\rangle$}\in\Delta^{\prime}\times\Delta^{\prime}\;\middle|\;\mbox{$\left\langle\zeta^{\prime}_{b},\varepsilon^{\prime}_{b}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime}_{\mathrm{diag}})}\text{ for some
}\zeta^{\prime}_{b}\approx\delta^{\prime}_{1-b}\right\\}$ $\displaystyle\text{
for }R\in N_{\mathsf{R}}$

where $\zeta^{\prime}_{b}\approx\delta^{\prime}_{1-b}$ holds iff for every
$\pi\in\sigma(\mathsf{u})$ we have
$\textstyle\bigcup_{{\delta\in\Delta}}\\{\zeta^{\prime}_{b}(\pi,\delta)\\}=\textstyle\bigcup_{{\pi_{*}\in\sigma(\mathsf{u}),}\atop{\delta_{*}\in\Delta}}\\{\delta^{\prime}_{1-b}(\pi_{*},\delta_{*})\\}$.
Finally for the fresh concept name $A$ introduced by the rule, define
$A^{\gamma^{\prime}(\pi^{\prime})}\mathrel{\,:=\,}C^{\gamma^{\prime}(\pi^{\prime})}$
for all $\pi^{\prime}\in\sigma^{\prime}(\mathsf{u})$.

We now show that $\mathfrak{D}^{\prime}\models\mathcal{K}^{\prime}$. For this,
we start out with some useful observations.

######  Claim 3.

For every concept $E$, $\delta^{\prime}\in\Delta^{\prime}$, and
$\pi^{\prime}\in\Pi^{\prime}\setminus\left\\{\pi^{\prime}_{\mathsf{v}_{0}},\pi^{\prime}_{\mathsf{v}_{1}}\right\\}$:

$\delta^{\prime}\in
E^{\gamma^{\prime}(\pi^{\prime})}\iff\left(\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
E^{\gamma(\pi^{\prime}(\pi,\delta))}\right)$

######  Proof of the claim.

We use structural induction on $E$.

     * •

$E=A\in\mathsf{BC}_{\mathcal{K}}$: By definition.

     * •

$E=E_{1}\sqcap E_{2}$:

$\displaystyle\mathrel{\phantom{\iff}}\delta^{\prime}\in(E_{1}\sqcap
E_{2})^{\gamma^{\prime}(\pi^{\prime})}$ $\displaystyle\iff\delta^{\prime}\in
E_{1}^{\gamma^{\prime}(\pi^{\prime})}\cap
E_{2}^{\gamma^{\prime}(\pi^{\prime})}$ $\displaystyle\iff\delta^{\prime}\in
E_{1}^{\gamma^{\prime}(\pi^{\prime})}\text{ and }\delta^{\prime}\in
E_{2}^{\gamma^{\prime}(\pi^{\prime})}$
$\displaystyle\stackrel{{\scriptstyle\text{(IH)}}}{{\iff}}\left[\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
E_{1}^{\gamma(\pi^{\prime}(\pi,\delta))}\right]\text{ and
}\left[\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
E_{2}^{\gamma(\pi^{\prime}(\pi,\delta))}\right]$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\left[\delta^{\prime}(\pi,\delta)\in
E_{1}^{\gamma(\pi^{\prime}(\pi,\delta))}\text{ and
}\delta^{\prime}(\pi,\delta)\in
E_{2}^{\gamma(\pi^{\prime}(\pi,\delta))}\right]$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
E_{1}^{\gamma(\pi^{\prime}(\pi,\delta))}\cap
E_{2}^{\gamma(\pi^{\prime}(\pi,\delta))}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in(E_{1}\sqcap
E_{2})^{\gamma(\pi^{\prime}(\pi,\delta))}$

     * •

$E=\exists R.B$:

$\displaystyle\mathrel{\phantom{\iff}}\delta^{\prime}\in\exists
R.B^{\gamma^{\prime}(\pi^{\prime})}$
$\displaystyle\iff\exists\varepsilon^{\prime}\in\Delta^{\prime}:\left[\mbox{$\left\langle\delta^{\prime},\varepsilon^{\prime}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime})}\text{ and }\varepsilon^{\prime}\in
B^{\gamma^{\prime}(\pi^{\prime})}\right]$
$\displaystyle\stackrel{{\scriptstyle\text{(IH)}}}{{\iff}}\exists\varepsilon^{\prime}\in\Delta^{\prime}:\left[\mbox{$\left\langle\delta^{\prime},\varepsilon^{\prime}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime})}\text{ and
}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\varepsilon^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime}(\pi,\delta))}\right]$
$\displaystyle\iff\exists\varepsilon^{\prime}\in\Delta^{\prime}:\left[\left[\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\mbox{$\left\langle\delta^{\prime}(\pi,\delta),\varepsilon^{\prime}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi^{\prime}(\pi,\delta))}\right]\text{ and
}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\varepsilon^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime}(\pi,\delta))}\right]$
$\displaystyle\iff\exists\varepsilon^{\prime}\in\Delta^{\prime}:\left[\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\left[\mbox{$\left\langle\delta^{\prime}(\pi,\delta),\varepsilon^{\prime}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi^{\prime}(\pi,\delta))}\text{ and
}\varepsilon^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime}(\pi,\delta))}\right]\right]$
$\displaystyle\stackrel{{\scriptstyle\ddagger}}{{\iff}}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\exists\varepsilon^{\prime}\in\Delta^{\prime}:\left[\mbox{$\left\langle\delta^{\prime}(\pi,\delta),\varepsilon^{\prime}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi^{\prime}(\pi,\delta))}\text{ and
}\varepsilon^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime}(\pi,\delta))}\right]$
$\displaystyle\stackrel{{\scriptstyle\dagger}}{{\iff}}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\exists\varepsilon\in\Delta:\left[\mbox{$\left\langle\delta^{\prime}(\pi,\delta),\varepsilon\right\rangle$}\in
R^{\gamma(\pi^{\prime}(\pi,\delta))}\text{ and }\varepsilon\in
B^{\gamma(\pi^{\prime}(\pi,\delta))}\right]$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in(\exists
R.B)^{\gamma(\pi^{\prime}(\pi,\delta))}$

Note that for the “$\impliedby$” direction, there is always an
$\varepsilon^{\prime}\in\Delta^{\prime}$ such that for all
$\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$ we find
$\varepsilon^{\prime}(\pi,\delta)=\varepsilon$ for the appropriate
$\varepsilon\in\Delta$ (step $\dagger$), and thus this $\varepsilon^{\prime}$
is in this sense independent of concrete $\pi\in\sigma(\mathsf{u})$ and
$\delta\in\Delta$ (step $\ddagger$).

     * •

$E=\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B$:

$\displaystyle\mathrel{\phantom{\iff}}\delta^{\prime}\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma^{\prime}(\pi^{\prime})}$
$\displaystyle\iff\exists\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\delta^{\prime}\in
B^{\gamma^{\prime}(\pi^{\prime\prime})}$
$\displaystyle\stackrel{{\scriptstyle\text{(IH)}}}{{\iff}}\exists\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime\prime}(\pi,\delta))}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\exists\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma^{\prime}(\pi^{\prime\prime}(\pi,\delta))}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\exists\pi_{\mathsf{s^{\prime}}}\in\sigma(\mathsf{s^{\prime}}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi_{\mathsf{s^{\prime}}})}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma(\pi^{\prime}(\pi,\delta))}$

Again, for “$\impliedby$”, we find a
$\pi^{\prime\prime}\in\sigma(\mathsf{s^{\prime}})$ for which always
$\pi^{\prime\prime}(\pi,\delta)=\pi_{\mathsf{s^{\prime}}}$ as desired.

     * •

$E=\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B$:

$\displaystyle\mathrel{\phantom{\iff}}\delta^{\prime}\in(\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma^{\prime}(\pi^{\prime})}$
$\displaystyle\iff\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\delta^{\prime}\in
B^{\gamma^{\prime}(\pi^{\prime})}$
$\displaystyle\stackrel{{\scriptstyle\text{(IH)}}}{{\iff}}\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime\prime}(\pi,\delta))}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma^{\prime}(\pi^{\prime\prime}(\pi,\delta))}$
$\displaystyle\stackrel{{\scriptstyle\dagger}}{{\iff}}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{\mathsf{s^{\prime}}}\in\sigma(\mathsf{s^{\prime}}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi_{\mathsf{s^{\prime}}})}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in(\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma(\pi^{\prime}(\pi,\delta))}$

The equivalence marked $\dagger$ holds because for every
$\pi_{\mathsf{s^{\prime}}}\in\sigma(\mathsf{s^{\prime}})$ we can find a
$\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}})$ such that
$\pi^{\prime\prime}(\pi,\delta)=\pi_{\mathsf{s^{\prime}}}$ for all
$\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$ (e.g. the constant function
$\left\\{(\pi,\delta)\mapsto\pi_{\mathsf{s^{\prime}}}\right\\}$); conversely,
for every $\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}})$,
$\pi\in\sigma(\mathsf{u})$, and $\delta\in\Delta$, we have
$\pi^{\prime\prime}(\pi,\delta)\in\sigma(\mathsf{s^{\prime}})$ by definition.

❑

The claim above does not consider the newly introduced precisifications. They
are however covered by the next claim.

######  Claim 4.

For every concept $E$, $\delta^{\prime}\in\Delta^{\prime}$, and
$\pi^{\prime}\in\left\\{\pi^{\prime}_{\mathsf{v}_{0}},\pi^{\prime}_{\mathsf{v}_{1}}\right\\}$:

    1. (a)

$\delta^{\prime}\in
E^{\gamma^{\prime}(\pi^{\prime})}\implies\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
E^{\gamma(\pi^{\prime}(\pi,\delta))}$

    2. (b)

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}(\pi,\delta)\in
E^{\gamma(\pi^{\prime}(\pi_{*},\delta))}\implies\delta^{\prime}\in
E^{\gamma^{\prime}(\pi^{\prime})}$

######  Proof of the claim.

We use structural induction on $E$.

     * •

$E=A\in\mathsf{BC}_{\mathcal{K}}$: Assume
$\pi^{\prime}=\pi^{\prime}_{\mathsf{v}_{0}}$ (the remaining case is
symmetric). For direction (3a) we have:

$\displaystyle\mathrel{\phantom{\iff}}\delta^{\prime}_{b}\in
A^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}\text{ for some
}b\in\left\\{0,1\right\\}$ $\displaystyle\iff\delta^{\prime}_{0}\in
A^{\gamma^{\prime}(\pi^{\prime}_{\mathrm{diag}})}\text{ or
}\mathop{\bigcup_{\pi\in\sigma(\mathsf{u}),}}_{\delta\in\Delta}\left\\{\delta^{\prime}_{1}(\pi,\delta)\right\\}\subseteq\bigcap_{\pi\in\sigma(\mathsf{u})}A^{\gamma(\pi)}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{0}(\pi,\delta)\in
A^{\gamma(\pi^{\prime}_{\mathrm{diag}}(\pi,\delta))}\text{ or
}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}_{1}(\pi,\delta)\in
A^{\gamma(\pi_{*})}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{0}(\pi,\delta)\in
A^{\gamma(\pi)}\text{ or
}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}_{1}(\pi,\delta)\in
A^{\gamma(\pi_{*})}$
$\displaystyle\implies\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{0}(\pi,\delta)\in
A^{\gamma(\pi)}\text{ or
}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{1}(\pi,\delta)\in
A^{\gamma(\pi)}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{b}(\pi,\delta)\in
A^{\gamma(\pi)}\text{ for some }b\in\left\\{0,1\right\\}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{b}(\pi,\delta)\in
A^{\gamma(\pi^{\prime}_{\mathrm{diag}}(\pi,\delta))}\text{ for some
}b\in\left\\{0,1\right\\}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{b}(\pi,\delta)\in
A^{\gamma(\pi^{\prime}_{\mathsf{v}_{0}}(\pi,\delta))}\text{ for some
}b\in\left\\{0,1\right\\}$

In direction (3b), we have:

$\displaystyle\mathrel{\phantom{\iff}}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}_{b}(\pi,\delta)\in
E^{\gamma(\pi^{\prime}(\pi_{*},\delta))}\text{ for some
}b\in\left\\{0,1\right\\}$
$\displaystyle\iff\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}_{0}(\pi,\delta)\in
E^{\gamma(\pi^{\prime}(\pi_{*},\delta))}\text{ or
}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}_{1}(\pi,\delta)\in
E^{\gamma(\pi^{\prime}(\pi_{*},\delta))}$
$\displaystyle\implies\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{0}(\pi,\delta)\in
A^{\gamma(\pi)}\text{ or
}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}_{1}(\pi,\delta)\in
A^{\gamma(\pi_{*})}$

In the last line, we continue with the equivalences from direction (3a) above
the line with “$\implies\\!$”.

     * •

$E=\exists R.B$: We show the claim for
$\pi^{\prime}=\pi^{\prime}_{\mathsf{v}_{0}}$, as the other case is symmetric.
In direction (3a), let $\delta^{\prime}_{b}\in(\exists
R.B)^{\gamma^{\prime}(\pi^{\prime})}$. By definition of the semantics, there
is a $\varepsilon^{\prime}_{c}\in\Delta^{\prime}$ such that
$\mbox{$\left\langle\delta^{\prime}_{b},\varepsilon^{\prime}_{c}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime})}$ and $\varepsilon^{\prime}_{c}\in
B^{\gamma^{\prime}(\pi^{\prime})}$. Applying the induction hypothesis to
$\varepsilon^{\prime}_{c}\in B^{\gamma^{\prime}(\pi^{\prime})}$ yields that

$\displaystyle\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\varepsilon^{\prime}_{c}(\pi,\delta)\in
B^{\gamma(\pi^{\prime}(\pi,\delta))}=B^{\gamma(\pi)}$ (23)

By definition of $R^{\gamma^{\prime}(\pi^{\prime})}$, we have three cases for
$\mbox{$\left\langle\delta^{\prime}_{b},\varepsilon^{\prime}_{c}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime})}$, in each of which we show the claim.

       1. (a)

$\mbox{$\left\langle\delta^{\prime}_{0},\varepsilon^{\prime}_{0}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime}_{\mathrm{diag}})}$. That is,
$\mbox{$\left\langle\delta^{\prime}_{0}(\pi,\delta),\varepsilon^{\prime}_{0}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi)}$ for all $\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$.
Together with Equation 23, we obtain

$\forall\pi\in\sigma:\forall\delta\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{0}(\pi,\delta),\varepsilon^{\prime}_{0}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi)}\text{ and }\varepsilon^{\prime}_{c}(\pi,\delta)\in
B^{\gamma(\pi)}\right)$

Now since $\varepsilon^{\prime}_{0}$ and $\varepsilon^{\prime}_{1}$ are two
distinct copies of the same function, this means that

$\forall\pi\in\sigma:\forall\delta\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{0}(\pi,\delta),\varepsilon^{\prime}_{0}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi)}\text{ and }\varepsilon^{\prime}_{0}(\pi,\delta)\in
B^{\gamma(\pi)}\right)$

Thus

$\forall\pi\in\sigma:\forall\delta\in\Delta:\exists\varepsilon\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{0}(\pi,\delta),\varepsilon\right\rangle$}\in
R^{\gamma(\pi)}\text{ and }\varepsilon\in B^{\gamma(\pi)}\right)$

namely we set $\varepsilon\mathrel{\,:=\,}\varepsilon^{\prime}(\pi,\delta)$ in
each case. By the definition of the semantics we get

$\forall\pi\in\sigma:\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in(\exists
R.B)^{\gamma(\pi)}$

which, by
$\pi^{\prime}=\pi^{\prime}_{\mathsf{v}_{0}}=\pi^{\prime}_{\mathrm{diag}}$
means

$\forall\pi\in\sigma:\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in(\exists
R.B)^{\gamma(\pi^{\prime}(\pi,\delta))}$

       2. (b)

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\mbox{$\left\langle\delta^{\prime}_{1}(\pi,\delta),\varepsilon^{\prime}_{1}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi_{*})}$. In combination with Equation 23, we get

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\left(\mbox{$\left\langle\delta^{\prime}_{1}(\pi,\delta),\varepsilon^{\prime}_{1}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi_{*})}\text{ and }\varepsilon^{\prime}_{c}(\pi,\delta)\in
B^{\gamma(\pi)}\right)$

which, by virtue of $\varepsilon^{\prime}_{0}$ and $\varepsilon^{\prime}_{1}$
being the same function, means

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\left(\mbox{$\left\langle\delta^{\prime}_{1}(\pi,\delta),\varepsilon^{\prime}_{1}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi_{*})}\text{ and }\varepsilon^{\prime}_{1}(\pi,\delta)\in
B^{\gamma(\pi)}\right)$

which in particular implies

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{1}(\pi,\delta),\varepsilon^{\prime}_{1}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi)}\text{ and }\varepsilon^{\prime}_{1}(\pi,\delta)\in
B^{\gamma(\pi)}\right)$

which implies the claim as in the case above.

       3. (c)

there is some $\zeta^{\prime}_{0}\in\Delta^{\prime}$ with
$\zeta^{\prime}_{0}\approx\delta^{\prime}_{1}$ and
$\mbox{$\left\langle\zeta^{\prime}_{0},\varepsilon^{\prime}_{0}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime}_{\mathrm{diag}})}$. The latter property
implies

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\mbox{$\left\langle\zeta^{\prime}_{0}(\pi,\delta),\varepsilon^{\prime}_{0}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi)}$

In turn, from $\zeta^{\prime}_{0}\approx\delta^{\prime}_{0}$ we obtain

$\forall\pi\in\sigma(\mathsf{u}):\bigcup_{\delta\in\Delta}\left\\{\zeta^{\prime}_{0}(\pi,\delta)\right\\}=\mathop{\bigcup_{\pi_{*}\in\sigma(\mathsf{u}),}}_{\delta_{*}\in\Delta}\left\\{\delta^{\prime}_{1}(\pi_{*},\delta_{*})\right\\}$

This means in particular that

$\forall\pi,\pi_{*}\in\sigma(\mathsf{u}):\forall\delta_{*}\in\Delta:\exists\delta_{+}\in\Delta:\delta^{\prime}_{1}(\pi_{*},\delta_{*})=\zeta^{\prime}_{0}(\pi,\delta_{+})$

Thus

$\forall\pi,\pi_{*}\in\sigma(\mathsf{u}):\forall\delta_{*}\in\Delta:\exists\delta_{+}\in\Delta:\mbox{$\left\langle\delta^{\prime}_{1}(\pi_{*},\delta_{*}),\varepsilon^{\prime}_{0}(\pi,\delta_{+})\right\rangle$}\in
R^{\gamma(\pi)}$

which we combine with Equation 23 as usual to obtain

$\forall\pi,\pi_{*}\in\sigma(\mathsf{u}):\forall\delta_{*}\in\Delta:\exists\delta_{+}\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{1}(\pi_{*},\delta_{*}),\varepsilon^{\prime}_{0}(\pi,\delta_{+})\right\rangle$}\in
R^{\gamma(\pi)}\text{ and }\varepsilon^{\prime}_{c}(\pi,\delta_{+})\in
B^{\gamma(\pi)}\right)$

which in particular implies

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\exists\delta_{+}\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{1}(\pi,\delta),\varepsilon^{\prime}_{0}(\pi,\delta_{+})\right\rangle$}\in
R^{\gamma(\pi)}\text{ and }\varepsilon^{\prime}_{0}(\pi,\delta_{+})\in
B^{\gamma(\pi)}\right)$

whence we get

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{1}(\pi,\delta)\in(\exists
R.B)^{\gamma(\pi)}$

In direction (3b), assume that

$\forall\pi\in\sigma:\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}_{0}(\pi,\delta)\in(\exists
R.B)^{\gamma(\pi^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}},\delta))}$

By the definition of the semantics, we obtain

$\forall\pi\in\sigma:\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\exists\varepsilon\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{0}(\pi,\delta),\varepsilon\right\rangle$}\in
R^{\gamma(\pi^{\prime}(\pi_{*},\delta))}\text{ and
}\varepsilon_{\pi,\delta}\in B^{\gamma(\pi^{\prime}(\pi_{*},\delta))}\right)$

Since
$\pi^{\prime}=\pi^{\prime}_{\mathsf{v}_{0}}=\pi^{\prime}_{\mathrm{diag}}$,
this means that

$\forall\pi\in\sigma:\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\exists\varepsilon_{\pi,\delta}\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}(\pi,\delta),\varepsilon\right\rangle$}\in
R^{\gamma(\pi_{*})}\text{ and }\varepsilon\in B^{\gamma(\pi_{*})}\right)$

Since $\Delta^{\prime}$ contains every function
$\zeta^{\prime}\colon\sigma(\mathsf{u})\times\Delta\to\Delta$, there in
particular exists a function $\varepsilon^{\prime}_{0}\in\Delta^{\prime}$ such
that $\varepsilon^{\prime}_{0}(\pi,\delta)=\varepsilon_{\pi,\delta}$ for all
$\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$. Thus

$\exists\varepsilon^{\prime}_{0}\in\Delta^{\prime}:\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\left(\mbox{$\left\langle\delta^{\prime}_{0}(\pi,\delta),\varepsilon^{\prime}_{0}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi_{*})}\text{ and }\varepsilon^{\prime}_{0}(\pi,\delta)\in
B^{\gamma(\pi_{*})}\right)$

which means

$\left(\exists\varepsilon^{\prime}_{0}\in\Delta^{\prime}:\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\mbox{$\left\langle\delta^{\prime}_{0}(\pi,\delta),\varepsilon^{\prime}_{0}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi_{*})}\right)\text{ and }\\\
\left(\exists\varepsilon^{\prime}_{0}\in\Delta^{\prime}:\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\varepsilon^{\prime}_{0}(\pi,\delta)\in
B^{\gamma(\pi_{*})}\right)$

where we can apply the induction hypothesis to the second line to obtain

$\left(\exists\varepsilon^{\prime}_{0}\in\Delta^{\prime}:\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\mbox{$\left\langle\delta^{\prime}_{0}(\pi,\delta),\varepsilon^{\prime}_{0}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi_{*})}\right)\text{ and }\\\ \varepsilon^{\prime}_{0}\in
B^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}$

which in particular means that

$\exists\varepsilon^{\prime}_{0}\in\Delta^{\prime}:\left(\left(\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\mbox{$\left\langle\delta^{\prime}_{0}(\pi,\delta),\varepsilon^{\prime}_{0}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi)}\right)\text{ and }\varepsilon^{\prime}_{0}\in
B^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}\right)$

which (employing among other things that
$\pi^{\prime}_{\mathsf{v}_{0}}(\pi,\delta)=\pi$ for all
$\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$) implies

$\exists\varepsilon^{\prime}_{0}\in\Delta^{\prime}:\left(\mbox{$\left\langle\delta^{\prime}_{0},\varepsilon^{\prime}_{0}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}\text{ and
}\varepsilon^{\prime}\in
B^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}\right)$

that is, $\delta^{\prime}_{0}\in(\exists
R.B)^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}$.

     * •

$E=\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B$: In direction
(3a), assume
$\delta^{\prime}\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma^{\prime}(\pi^{\prime})}$.
Thus there exists some
$\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}})$ such that
$\delta^{\prime}\in B^{\gamma^{\prime}(\pi^{\prime\prime})}$. The induction
hypothesis yields

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime\prime}(\pi,\delta))}$

Thus for all $\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$ there exists a
$\pi_{\pi,\delta}^{\mathsf{s^{\prime}}}\in\sigma(\mathsf{s^{\prime}})$, namely
$\pi_{\pi,\delta}^{\mathsf{s^{\prime}}}\mathrel{\,:=\,}\pi^{\prime\prime}(\pi,\delta)$,
such that $\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi_{\pi,\delta}^{\mathsf{s^{\prime}}})}$. This directly yields
$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma^{\prime}(\pi^{\prime})}$.

In direction (3b), assume

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}(\pi,\delta)\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma(\pi^{\prime}_{\mathsf{v}_{0}}(\pi_{*},\delta))}$

This means that

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\exists\pi_{\pi_{*},\delta}^{\mathsf{s^{\prime}}}\in\sigma(\mathsf{s^{\prime}}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi_{\pi_{*},\delta}^{\mathsf{s^{\prime}}})}$

Choose
$\pi^{\prime}_{\mathsf{s^{\prime}}}\in\sigma^{\prime}(\mathsf{s^{\prime}})$
such that for all $\pi_{*}\in\sigma(\mathsf{u})$ and $\delta\in\Delta$, we
have
$\pi^{\prime}_{\mathsf{s^{\prime}}}(\pi_{*},\delta)=\pi_{\pi_{*},\delta}^{\mathsf{s^{\prime}}}$.
Thus we obtain

$\exists\pi^{\prime}_{\mathsf{s^{\prime}}}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime}_{\mathsf{s^{\prime}}}(\pi_{*},\delta))}$

We apply the induction hypothesis and get
$\exists\pi^{\prime}_{\mathsf{s^{\prime}}}\in\Delta^{\prime}:\delta^{\prime}\in
B^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{s^{\prime}}})}$, that is,
$\delta^{\prime}\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma^{\prime}(\pi^{\prime})}$.

     * •

$E=\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B$: In direction
(3a), we have

$\displaystyle\mathrel{\phantom{\implies}}\delta^{\prime}\in(\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma^{\prime}(\pi^{\prime})}$
$\displaystyle\implies\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\delta^{\prime}\in
B^{\gamma^{\prime}(\pi^{\prime\prime})}$
$\displaystyle\stackrel{{\scriptstyle\text{(IH)}}}{{\implies}}\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime\prime}(\pi,\delta))}$
$\displaystyle\implies\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime\prime}(\pi,\delta))}$
$\displaystyle\stackrel{{\scriptstyle\dagger}}{{\implies}}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{\mathsf{s^{\prime}}}\in\sigma(\mathsf{s^{\prime}}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi_{\mathsf{s^{\prime}}})}$
$\displaystyle\implies\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in(\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma(\pi)}$

and for the converse direction, (3b), we consider

$\displaystyle\mathrel{\phantom{\implies}}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}(\pi,\delta)\in(\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}B)^{\gamma(\pi^{\prime}(\pi_{*},\delta))}$
$\displaystyle\implies\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\forall\pi_{\mathsf{s^{\prime}}}\in\sigma(\mathsf{s^{\prime}}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi_{\mathsf{s^{\prime}}})}$
$\displaystyle\stackrel{{\scriptstyle\dagger}}{{\implies}}\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime\prime}(\pi,\delta))}$
$\displaystyle\implies\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}(\pi,\delta)\in
B^{\gamma(\pi^{\prime\prime}(\pi,\delta))}$
$\displaystyle\stackrel{{\scriptstyle\text{(IH)}}}{{\implies}}\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\delta^{\prime}\in
B^{\gamma^{\prime}(\pi^{\prime\prime})}$
$\displaystyle\implies\delta^{\prime}\in(\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma^{\prime}(\pi^{\prime})}$

Here, in both directions the implications marked $\dagger$ can be justifed
just like in the proof of 3.

❑

The two previous claims can be combined to obtain the following “global”
property:

######  Claim 5.

For every concept $E$, $\delta^{\prime}\in\Delta^{\prime}$, and
$\pi^{\prime}\in\Pi^{\prime}$:

$\delta^{\prime}\in
E^{\gamma^{\prime}(\pi^{\prime})}\implies\left(\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
E^{\gamma(\pi^{\prime}(\pi,\delta))}\right)$

######  Proof of the claim.

Follows from direction “$\implies\\!$” of 3 and Item 3a of 4.  ❑

For the new precisifications, we sometimes also have to pay attention to which
copy of the functions in $\Delta^{\prime}$ we are currently considering,
especially for the main case we will need below, namely where both copies are
contained in the same concept’s extension in both precisifications.

######  Claim 6.

For every concept $E$, function
$\delta^{\prime}\colon\sigma(\mathsf{u})\times\Delta\to\Delta$, and
$b\in\left\\{0,1\right\\}$:

$\displaystyle\delta^{\prime}_{b}\in E^{\pi^{\prime}_{\mathsf{v}_{b}}}$
$\displaystyle\implies\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in
E^{\gamma(\pi)}$ (24) $\displaystyle\delta^{\prime}_{1-b}\in
E^{\pi^{\prime}_{\mathsf{v}_{b}}}$
$\displaystyle\implies\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}(\pi,\delta)\in
E^{\gamma(\pi_{*})}$ (25)

######  Proof of the claim.

We use structural induction on $E$.

     * •

$E=A\in\mathsf{BC}_{\mathcal{K}}$: By definition.

     * •

$E=\exists R.B$:

(24):

Let $\delta^{\prime}_{b}\in(\exists
R.B)^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$ for some
$b\in\left\\{0,1\right\\}$. By definition of the semantics, there is an
$\varepsilon^{\prime}_{c}\in\Delta^{\prime}$ such that
$\mbox{$\left\langle\delta^{\prime}_{b},\varepsilon^{\prime}_{c}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$ and
$\varepsilon^{\prime}_{c}\in
B^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$. By definition of
$R^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$ the only possible reason
for
$\mbox{$\left\langle\delta^{\prime}_{b},\varepsilon^{\prime}_{c}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$ is that $b=c$ and
$\mbox{$\left\langle\delta^{\prime}_{b},\varepsilon^{\prime}_{c}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime}_{\mathrm{diag}})}$, that is,

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\mbox{$\left\langle\delta^{\prime}_{b}(\pi,\delta),\varepsilon^{\prime}_{c}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi)}$

Due to $b=c$, we can apply the induction hypothesis of (24) to
$\varepsilon^{\prime}_{c}\in
B^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$ and obtain

$\forall\pi\in\mathsf{u}:\forall\delta\in\Delta:\varepsilon^{\prime}_{c}(\pi,\delta)\in
B^{\gamma(\pi)}$

Togher with the above, we obtain

$\forall\pi\in\sigma:\forall\delta\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{b}(\pi,\delta),\varepsilon^{\prime}_{c}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi)}\text{ and }\varepsilon^{\prime}_{c}(\pi,\delta)\in
B^{\gamma(\pi)}\right)$

Thus

$\forall\pi\in\sigma:\forall\delta\in\Delta:\exists\varepsilon_{\pi,\delta}\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{b}(\pi,\delta),\varepsilon_{\pi,\delta}\right\rangle$}\in
R^{\gamma(\pi)}\text{ and }\varepsilon_{\pi,\delta}\in B^{\gamma(\pi)}\right)$

namely we set
$\varepsilon_{\pi,\delta}\mathrel{\,:=\,}\varepsilon^{\prime}_{c}(\pi,\delta)$
in each case. By the definition of the semantics we get

$\forall\pi\in\sigma:\forall\delta\in\Delta:\delta^{\prime}(\pi,\delta)\in(\exists
R.B)^{\gamma(\pi)}$

(25):

Let $\delta^{\prime}_{1-b}\in(\exists
R.B)^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$. By the definition of
the semantics, there exists some $\varepsilon^{\prime}_{c}\in\Delta^{\prime}$
such that
$\mbox{$\left\langle\delta^{\prime}_{1-b},\varepsilon^{\prime}_{c}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$ and
$\varepsilon^{\prime}_{c}\in
B^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$. According to the
definition of $R^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$, there are
two possible cases:

       1. (a)

$c=1-b$ and
$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\mbox{$\left\langle\delta^{\prime}_{1-b}(\pi,\delta),\varepsilon^{\prime}_{c}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi_{*})}$. We can apply the induction hypothesis of (25) to the
fact that $\varepsilon^{\prime}_{c}=\varepsilon^{\prime}_{1-b}\in
B^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$ and obtain

$\forall\pi\in\mathsf{u}:\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\varepsilon^{\prime}_{c}(\pi,\delta)\in
B^{\gamma(\pi_{*})}$

In combination with the presumption of this case, we obtain

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\left(\mbox{$\left\langle\delta^{\prime}_{b}(\pi,\delta),\varepsilon^{\prime}_{c}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi_{*})}\text{ and }\varepsilon^{\prime}_{c}(\pi,\delta)\in
B^{\gamma(\pi_{*})}\right)$

thus proving the claim.

       2. (b)

$c=b$ and there is some $\zeta^{\prime}_{b}\in\Delta^{\prime}$ with
$\zeta^{\prime}_{b}\approx\delta^{\prime}_{1-b}$ and
$\mbox{$\left\langle\zeta^{\prime}_{b},\varepsilon^{\prime}_{c}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime}_{\mathrm{diag}})}$. The latter property
implies

$\forall\pi_{*}\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\mbox{$\left\langle\zeta^{\prime}_{b}(\pi_{*},\delta),\varepsilon^{\prime}_{c}(\pi_{*},\delta)\right\rangle$}\in
R^{\gamma(\pi_{*})}$

In turn, from $\zeta^{\prime}_{b}\approx\delta^{\prime}_{1-b}$ we obtain

$\forall\pi_{*}\in\sigma(\mathsf{u}):\bigcup_{\delta\in\Delta}\left\\{\zeta^{\prime}_{b}(\pi_{*},\delta)\right\\}=\mathop{\bigcup_{\pi\in\sigma(\mathsf{u}),}}_{\delta\in\Delta}\left\\{\delta^{\prime}_{1-b}(\pi,\delta)\right\\}$

This means in particular that

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\exists\delta_{+}\in\Delta:\zeta^{\prime}_{b}(\pi_{*},\delta_{+})=\delta^{\prime}_{1-b}(\pi,\delta)$

whence

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\exists\delta_{+}\in\Delta:\mbox{$\left\langle\delta^{\prime}_{1-b}(\pi,\delta),\varepsilon^{\prime}_{c}(\pi_{*},\delta_{+})\right\rangle$}\in
R^{\gamma(\pi_{*})}$

Now $b=c$ means that we can apply the induction hypothesis of (24) to
$\varepsilon^{\prime}_{c}=\varepsilon^{\prime}_{b}\in
B^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{b}})}$, from which we get

$\forall\pi_{*}\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\varepsilon^{\prime}_{b}(\pi_{*},\delta)\in
B^{\gamma(\pi_{*})}$

which we combine with the line above as usual to obtain

$\forall\pi,\pi_{*}\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\exists\delta_{+}\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{1-b}(\pi,\delta),\varepsilon^{\prime}_{c}(\pi_{*},\delta_{+})\right\rangle$}\in
R^{\gamma(\pi_{*})}\text{ and }\varepsilon^{\prime}_{c}(\pi_{*},\delta_{+})\in
B^{\gamma(\pi_{*})}\right)$

which in particular implies

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\exists\varepsilon\in\Delta:\left(\mbox{$\left\langle\delta^{\prime}_{1-b}(\pi,\delta),\varepsilon\right\rangle$}\in
R^{\gamma(\pi_{*})}\text{ and }\varepsilon\in B^{\gamma(\pi_{*})}\right)$

namely in each case
$\varepsilon\mathrel{\,:=\,}\varepsilon^{\prime}_{c}(\pi_{*},\delta_{+})$,
whence we get

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}_{1-b}(\pi,\delta)\in(\exists
R.B)^{\gamma(\pi_{*})}$

thus proving the claim.

     * •

$E=\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B$: Let
$\pi^{\prime}\in\left\\{\pi^{\prime}_{\mathsf{v}_{0}},\pi^{\prime}_{\mathsf{v}_{1}}\right\\}$
and consider
$\delta^{\prime}_{b}\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma^{\prime}(\pi^{\prime})}$.
Then there is some $\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}})$
such that $\delta^{\prime}_{1-b}\in B^{\gamma^{\prime}(\pi^{\prime\prime})}$.
By 5 we obtain

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{b}(\pi,\delta)\in
B^{\gamma(\pi^{\prime\prime}(\pi,\delta))}$

whence for all $\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$ we can set
$\pi_{\pi,\delta}\mathrel{\,:=\,}\pi^{\prime\prime}(\pi,\delta)$ to rewrite
this into

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\exists\pi_{\pi,\delta}\in\sigma(\mathsf{s^{\prime}}):\delta^{\prime}_{b}(\pi,\delta)\in
B^{\gamma(\pi_{\pi,\delta})}$

and we conclude the claim:

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}_{b}(\pi,\delta)\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma(\pi_{*})}$

     * •

$E=\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B$: Let
$\pi^{\prime}\in\left\\{\pi^{\prime}_{\mathsf{v}_{0}},\pi^{\prime}_{\mathsf{v}_{1}}\right\\}$
and consider
$\delta^{\prime}_{b}\in(\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}B)^{\gamma^{\prime}(\pi^{\prime})}$.
Then for all $\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}})$, we
have $\delta^{\prime}_{b}\in B^{\gamma^{\prime}(\pi^{\prime\prime})}$, which
by 5 means that

$\forall\pi^{\prime\prime}\in\sigma^{\prime}(\mathsf{s^{\prime}}):\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{b}(\pi,\delta)\in
B^{\gamma(\pi^{\prime\prime}(\pi,\delta))}$

Let $\pi_{\mathsf{s^{\prime}}}\in\sigma(\mathsf{s^{\prime}})$ be arbitrary.
Consider the function
$\pi^{\prime}_{\mathsf{s^{\prime}}}=\left\\{(\pi,\delta)\mapsto\pi_{\mathsf{s^{\prime}}}\right\\}$,
for which we have
$\pi^{\prime}_{\mathsf{s^{\prime}}}\in\sigma^{\prime}(\mathsf{s^{\prime}})$ by
definition and thus also

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\delta^{\prime}_{b}(\pi,\delta)\in
B^{\gamma(\pi^{\prime}_{\mathsf{s^{\prime}}}(\pi,\delta))}=B^{\gamma(\pi_{\mathsf{s^{\prime}}})}$

Since $\pi_{\mathsf{s^{\prime}}}$ was arbitrarily chosen, we get

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{\mathsf{s^{\prime}}}\in\sigma(\mathsf{s^{\prime}}):\delta^{\prime}_{b}(\pi,\delta)\in
B^{\gamma(\pi_{\mathsf{s^{\prime}}})}$

which shows the claim.

❑

We now continue the main proof, showing that
$\mathfrak{D}^{\prime}\models\mathcal{K}^{\prime}$.

     * •

$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[C\sqsubseteq
A]$: By definition.

     * •

$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A\sqsubseteq
D]$: Let $\pi^{\prime}\in\sigma^{\prime}(\mathsf{s})$ and
$\delta^{\prime}_{b}\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A)^{\gamma^{\prime}(\pi^{\prime})}$
for some $b\in\left\\{0,1\right\\}$. We have to show $\delta^{\prime}_{b}\in
D^{\gamma^{\prime}(\pi^{\prime})}$. By definition of $\mathfrak{D}^{\prime}$,
we conclude that $\delta^{\prime}_{b}\in
A^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}\cap
A^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{1}})}$; we furthermore have
$\pi^{\prime}_{\mathsf{v}_{0}},\pi^{\prime}_{\mathsf{v}_{1}}\in\sigma^{\prime}(\mathsf{u})$
and
$A^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{y}})}=C^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{y}})}$
for all $y\in\left\\{0,1\right\\}$; thus it follows that
$\delta^{\prime}_{b}\in C^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}\cap
C^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{1}})}$. So in any case we obtain
that $\delta^{\prime}_{b}\in C^{\gamma^{\prime}(\pi_{\mathsf{v}_{1-b}})}$,
whence by 6 we get

$\forall\pi\in\sigma(\mathsf{u}):\forall\delta\in\Delta:\forall\pi_{*}\in\sigma(\mathsf{u}):\delta^{\prime}(\pi,\delta)\in
C^{\gamma(\pi_{*})}$

Hence, for all $\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$ we have
$\delta^{\prime}(\pi,\delta)\in(\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}C)^{\gamma(\pi)}$.
From
$\mathfrak{D}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}C\sqsubseteq
D]$ it therefore follows that $\delta^{\prime}(\pi_{*},\delta)\in
D^{\gamma(\pi)}$ for all $\pi_{*}\in\sigma(\mathsf{u})$, $\delta\in\Delta$,
and $\pi\in\sigma(\mathsf{s})$. Now by
$\pi^{\prime}\in\sigma^{\prime}(\mathsf{s})$ we obtain that for any
$\pi_{*}\in\sigma(\mathsf{u})$ and $\delta\in\Delta$ we get
$\pi^{\prime}(\pi_{*},\delta)\in\sigma(\mathsf{s})$. Thus it follows that
$\delta^{\prime}(\pi,\delta)\in D^{\gamma(\pi^{\prime}(\pi_{*},\delta))}$ for
all $\pi,\pi_{*}\in\sigma(\mathsf{u})$ and $\delta\in\Delta$. By 3/4 above, we
get $\delta^{\prime}\in D^{\gamma^{\prime}(\pi^{\prime})}$.

     * •

$\mathfrak{D}^{\prime}\models\tau$ for all
$\tau\in\mathcal{T}^{\prime}\setminus\left\\{\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[C\sqsubseteq
A],\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A\sqsubseteq
D]\right\\}$: Let w.l.o.g.
$\tau=\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}[E\sqsubseteq
F]$. By presumption $\mathfrak{D}\models\mathcal{T}$ we get that for every
$\pi\in\sigma(\mathsf{s}^{\prime})$ we have $E^{\gamma(\pi)}\subseteq
F^{\gamma(\pi)}$. Let $\pi^{\prime}\in\sigma^{\prime}(\mathsf{s}^{\prime})$
and $\delta^{\prime}\in E^{\gamma^{\prime}(\pi^{\prime})}$. From 5 we get that
$\delta^{\prime}(\pi,\delta)\in E^{\gamma(\pi^{\prime}(\pi,\delta))}$ for all
$\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$. From
$\pi^{\prime}\in\sigma^{\prime}(\mathsf{s}^{\prime})$ we get that
$\pi^{\prime}(\pi_{*},\delta)\in\sigma(\mathsf{s}^{\prime})$ for all
$\pi_{*}\in\sigma(\mathsf{u})$ and $\delta\in\Delta$. It follows that
$E^{\gamma(\pi^{\prime}(\pi_{*},\delta))}\subseteq
F^{\gamma(\pi^{\prime}(\pi_{*},\delta))}$ for all
$\pi_{*}\in\sigma(\mathsf{u})$ and $\delta\in\Delta$. In particular,
$\delta^{\prime}(\pi,\delta)\in F^{\gamma(\pi^{\prime}(\pi_{*},\delta))}$ for
all $\pi,\pi_{*}\in\sigma(\mathsf{u})$ and $\delta\in\Delta$. Therefore, 3/4
yields $\delta^{\prime}\in F^{\gamma^{\prime}(\pi^{\prime})}$.

     * •

$\mathfrak{D}^{\prime}\models\alpha$ for all $\alpha\in\mathcal{A}$: We do a
case distinction on the possible forms of assertions.

       * –

$\alpha=\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}[B(a)]$: It
follows that $B\in\mathsf{BC}_{\mathcal{K}}$ since $\mathcal{A}$ is in normal
form. From $\mathfrak{D}\models\mathcal{A}$ we get that for any
$\pi\in\sigma(\mathsf{s}^{\prime})$ we have $a^{\gamma(\pi)}=\delta_{a}\in
B^{\gamma(\pi)}$. Let $\pi^{\prime}\in\sigma^{\prime}(\mathsf{s}^{\prime})$.
By definition, we get that
$a^{\gamma^{\prime}(\pi^{\prime})}(\pi,\delta)=\delta_{a}$ for all
$\delta\in\Delta$ and all $\pi\in\Pi$ and in particular for all
$\pi\in\sigma(\mathsf{u})$. From
$\pi^{\prime}\in\sigma^{\prime}(\mathsf{s}^{\prime})$ we get that for any
$\pi\in\sigma(\mathsf{u})$ and $\delta\in\Delta$ we find
$\pi^{\prime}(\pi,\delta)\in\sigma(\mathsf{s}^{\prime})$. It thus follows that
$a^{\gamma^{\prime}(\pi^{\prime})}(\pi,\delta)=\delta_{a}\in
B^{\gamma(\pi^{\prime}(\pi,\delta))}$ for all $\pi\in\sigma(\mathsf{u})$ and
$\delta\in\Delta$. Consequently, $a^{\gamma^{\prime}(\pi^{\prime})}\in
B^{\gamma^{\prime}(\pi^{\prime})}$.

       * –

$\alpha=\mathord{\mathop{\square}\nolimits_{\mathsf{s^{\prime}}}}[R(a,c)]$:
From $\mathfrak{D}\models\mathcal{A}$ it follows that for every
$\pi\in\sigma(\mathsf{s}^{\prime})$ we have $\mbox{$\left\langle
a^{\gamma(\pi)},c^{\gamma(\pi)}\right\rangle$}\in R^{\gamma(\pi)}$. Let
$\pi^{\prime}\in\sigma^{\prime}(\mathsf{s}^{\prime})$. As above, we get
$a^{\gamma^{\prime}(\pi^{\prime})}(\pi,\delta)=\delta_{a}$ and
$c^{\gamma^{\prime}(\pi^{\prime})}(\pi,\delta)=\delta_{c}$ for every
$\delta\in\Delta$ and $\pi\in\sigma(\mathsf{u})$. From
$\pi^{\prime}\in\sigma^{\prime}(\mathsf{s}^{\prime})$, we get
$\pi^{\prime}(\pi,\delta)\in\sigma(\mathsf{s}^{\prime})$ for every
$\delta\in\Delta$ and $\pi\in\sigma(\mathsf{u})$. Thus $\mbox{$\left\langle
a^{\gamma^{\prime}(\pi^{\prime})}(\pi,\delta),a^{\gamma^{\prime}(\pi^{\prime})}(\pi,\delta)\right\rangle$}\in
R^{\gamma(\pi^{\prime}(\pi,\delta))}$ for all $\delta\in\Delta$ and
$\pi\in\sigma(\mathsf{u})$ whence $\mbox{$\left\langle
a^{\gamma^{\prime}(\pi^{\prime})},a^{\gamma^{\prime}(\pi^{\prime})}\right\rangle$}\in
R^{\gamma^{\prime}(\pi^{\prime})}$.

     * •

$\mathfrak{D}^{\prime}\models\zeta$ for all $\zeta\in\mathcal{S}$: Let
$\mathsf{s}^{\prime}\preceq\mathsf{s}^{\prime\prime}\in\mathcal{S}$ and
$\pi^{\prime}\in\sigma^{\prime}(\mathsf{s}^{\prime})$. Then by definition of
$\sigma^{\prime}$, we get
$\mathop{\bigcup_{\pi\in\sigma(\mathsf{u}),}}_{\delta\in\Delta}\left\\{\pi^{\prime}(\pi,\delta)\right\\}\subseteq\sigma(\mathsf{s}^{\prime})$.
By $\sigma(\mathsf{s}^{\prime})\subseteq\sigma(\mathsf{s}^{\prime\prime})$ it
follows that $\pi^{\prime}\in\sigma^{\prime}(\mathsf{s}^{\prime\prime})$.

(b) Let $\mathfrak{D}^{\prime}\models\mathcal{T}^{\prime}$ and consider
$\pi^{\prime}\in\sigma^{\prime}(\mathsf{s})$ and
$\delta^{\prime}\in(\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}C)^{\gamma^{\prime}(\pi^{\prime})}$.
Since
$\pi^{\prime}_{\mathsf{v}_{0}},\pi^{\prime}_{\mathsf{v}_{1}}\in\sigma^{\prime}(\mathsf{u})$,
we thus get $\delta^{\prime}\in
C^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}\cap
C^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{1}})}$. By
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{u}}}[C\sqsubseteq
A]$, we obtain that $\delta^{\prime}\in
A^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{0}})}\cap
A^{\gamma^{\prime}(\pi^{\prime}_{\mathsf{v}_{1}})}$; that is,
$\delta^{\prime}\in(\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A)^{\gamma^{\prime}(\pi^{\prime})}$.
Since also
$\mathfrak{D}^{\prime}\models\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}[\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{0}}}A\sqcap\mathord{\mathop{\lozenge}\nolimits_{\mathsf{v}_{1}}}A\sqsubseteq
D]$, it follows that $\delta^{\prime}\in D^{\gamma^{\prime}(\pi^{\prime})}$.

##  3 A Tableau Algorithm for Standpoint $\mathcal{E\\!L}$

We present a PTime tableau decision algorithm for
$\mathbb{S}_{\mathcal{E\\!L}}$. Complexity-optimal tableau algorithms have
been proposed for description logics with modal operators applied to concepts
and axioms such as $\mathbf{K}_{\mathcal{ALC}}$ Lutz et al. (2002), which is
known to be in NExpTime. Our case cannot be treated in the same way, as we
need to take greater care to show tractability in the end. Lutz et al. [2002]
build a “quasi-model” from a tree of “quasi-worlds”, which is not as easily
applicable in our case, so we follow a dual approach: we will build a _quasi-
model_ from a completion graph of _(quasi) domain elements_ , where each of
the latter is associated to a constraint system with assembled information
regarding one individual’s specifics in each precisification. We begin with
some definitions. Given a $\mathbb{S}_{\mathcal{E\\!L}}$ knowledge base
$\mathcal{K}$, denote by

  * •

$\mathsf{ST}_{\mathcal{K}}$ the elements of $N_{\mathsf{S}}$ occurring in
$\mathcal{K}$ together with $*$,

  * •

$\mathsf{IN}_{\mathcal{K}}$ the set of all individual names occurring in
$\mathcal{K}$,

  * •

$\mathsf{BC}_{\mathcal{K}}$ (_basic concepts_) the concept names used in
$\mathcal{K}$, plus $\top$,

  * •

$\mathsf{C}_{\mathcal{K}}$ the set of concept terms used in $\mathcal{K}$
(with $\mathsf{BC}_{\mathcal{K}}\subseteq\mathsf{C}_{\mathcal{K}}$),

  * •

$\mathsf{SF}_{\mathcal{K}}$ the set of _subformulas_ of $\mathcal{K}$,
consisting of all axioms of $\mathcal{K}$ with and without their outer
standpoint modality.

A _constraint_ for $\mathcal{K}$ is of the form $(x{\hskip 1.5pt:\hskip
2.0pt}C)$, $(x{\hskip 1.5pt:\hskip 2.0pt}a)$, $(x{\hskip 1.5pt:\hskip
2.0pt}\phi)$, or $(x{\hskip 1.5pt:\hskip 2.0pt}\hbox{$\mathsf{s}$})$,555For
better legibility, we will sometimes omit the parentheses. where $x$ is a
variable, $C\in\mathsf{C}_{\mathcal{K}}$ a concept,
$a\in\mathsf{IN}_{\mathcal{K}}$ an individual,
$\phi\in\mathsf{SF}_{\mathcal{K}}$ a formula, and
$\hbox{$\mathsf{s}$}\in\mathsf{ST}_{\mathcal{K}}$ a standpoint name.
_Constraint systems_ are finite sets of constraints.

######  Definition 3 ((Initial) Constraint System for $\mathcal{K}$).

The _initial constraint system_ for $\mathcal{K}$, called
$S_{0}^{\mathcal{K}}$, is the set

$\\{x_{\hbox{$\mathsf{s}$}}{\hskip 1.5pt:\hskip 2.0pt}*,\
x_{\hbox{$\mathsf{s}$}}{\hskip 1.5pt:\hskip 2.0pt}\\!\top,\
x_{\hbox{$\mathsf{s}$}}{\hskip 1.5pt:\hskip 2.0pt}\phi,\
x_{\hbox{$\mathsf{s}$}}{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$}\mid\phi\in\mathcal{K},\hbox{$\mathsf{s}$}\in\mathsf{ST}_{\mathcal{K}}\\}$

A _constraint system_ for $\mathcal{K}$ is a finite set $S$ of constraints for
$\mathcal{K}$ such that $S_{0}^{\mathcal{K}}\subseteq S$ and $\\{x{\hskip
1.5pt:\hskip 2.0pt}*,\ x{\hskip 1.5pt:\hskip 2.0pt}\\!\top\\}\subseteq S$ for
each $x$ in $S$. For a variable $x$, let
$\mathsf{st}_{S}(x)=\left\\{\hbox{$\mathsf{s}$}\;\middle|\;(x{\hskip
1.5pt:\hskip 2.0pt}\hbox{$\mathsf{s}$})\in S\right\\}$ be the _standpoint
signature_ of $x$ in $S$.  ❑

Intuitively, each constraint system $S$ produced by the algorithm corresponds
to a domain element $\varepsilon\in\Delta$ and each variable $x$ in $S$
corresponds to some precisification $\pi$. Moreover, each constraint $x{\hskip
1.5pt:\hskip 2.0pt}X$ in $S$ encodes information of $\varepsilon$ in $\pi$.
Namely, $X$ may be an axiom that holds in $\pi$, a standpoint that contains
$\pi$, or a concept expression of which $\varepsilon$ is an instance in $\pi$.
Initialising one variable per standpoint in the initial constraint system
guarantees non-empty standpoints.

A constraint system is _complete_ iff it satisfies every local completion rule
from Figure 1. Local completion rules operate on constraint systems, while
global rules involve more than one constraint system and operate on completion
graphs.

######  Definition 4 (Completion Graph).

An _element label_ is a set $L$ of triples of the form $(C,s,x)$, where
$C\in\mathsf{BC}_{\mathcal{K}}$ is a concept,
$s\subseteq\mathsf{ST}_{\mathcal{K}}$ is a set of standpoints, and $x$ is a
variable.
A _quasi-role_ for a set $\Delta$ is a tuple
$\langle\varepsilon,v,\varepsilon^{\prime},v^{\prime},R\rangle$ where $v$ and
$v^{\prime}$ are variables, $\varepsilon,\varepsilon^{\prime}\in\Delta$, and
$R$ is a role name in $\mathcal{K}$.
A _completion graph_ for $\mathcal{K}$ is a tuple
$\mathbf{CG}=\mbox{$\left\langle\Delta,\mathscr{S},\mathscr{L},\mathscr{R}\right\rangle$}$,
with $\Delta$ a non-empty set of elements; $\mathscr{S}$ a map from $\Delta$
into constraint systems; $\mathscr{L}$ a map from $\Delta$ into element
labels; and $\mathscr{R}$ a set of quasi-roles such that

  * •

for all
$\langle\varepsilon,v,\varepsilon^{\prime}\\!,v^{\prime}\\!,R\rangle\\!\in\\!\mathscr{R}$,
$(v{\hskip 1.5pt:\hskip 2.0pt}\hbox{$\mathsf{s}$})\in\mathscr{S}(\varepsilon)$
iff $(v^{\prime}{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$})\in\mathscr{S}(\varepsilon^{\prime})$;

  * •

if $(C,s,x)\\!\in\\!\mathscr{L}(\varepsilon)$, then $\\{x{\hskip 1.5pt:\hskip
2.0pt}C\\}\\!\cup\\!\\{x{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$}\mid\hbox{$\mathsf{s}$}\in
s\\}\subseteq\mathscr{S}(\varepsilon)$.

❑

  Local labelling (LL) rule: $\mathbf{R}_{\preceq}$ If $\\{x{\hskip
1.5pt:\hskip 2.0pt}\hbox{$\mathsf{s}$},\ x^{\prime}{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s}$}\\!\preceq\\!\hbox{$\mathsf{s^{\prime}}$}\\}\subseteq
S$ but $(x{\hskip 1.5pt:\hskip 2.0pt}\hbox{$\mathsf{s^{\prime}}$})\notin S$,
then set $S\mathrel{\,:=\,}S\cup\\{x{\hskip 1.5pt:\hskip
2.0pt}\hbox{$\mathsf{s^{\prime}}$}\\}$. Local content (LC) rules:
$\mathbf{R}_{\sqcap}$ If $\\{x{\hskip 1.5pt:\hskip 2.0pt}C,\ x{\hskip
1.5pt:\hskip 2.0pt}D\\}\subseteq S$, $(x{\hskip 1.5pt:\hskip 2.0pt}C\sqcap
D)\notin S$ and $C\sqcap D\in\mathsf{C}_{\mathcal{K}}$, then set
$S\mathrel{\,:=\,}S\cup\\{x{\hskip 1.5pt:\hskip 2.0pt}C\sqcap D\\}$.
$\mathbf{R}_{\sqsubseteq}$ If $\\{x{\hskip 1.5pt:\hskip 2.0pt}C,\ x{\hskip
1.5pt:\hskip 2.0pt}C\sqsubseteq D\\}\subseteq S$ but $(x{\hskip 1.5pt:\hskip
2.0pt}D)\notin S$, then set $S\mathrel{\,:=\,}S\cup\\{x{\hskip 1.5pt:\hskip
2.0pt}D\\}$. $\mathbf{R}_{\mathop{\square}}$ If $\\{x{\hskip 1.5pt:\hskip
2.0pt}\\!\mathord{\mathop{\square}\nolimits_{\mathsf{s}}}\Phi,\
x^{\prime}{\hskip 1.5pt:\hskip 2.0pt}\hbox{$\mathsf{s}$}\\}\subseteq S$ but