# Reasoning in SHIQ with axiom- and concept-level standpoint modalities

Lucía Gómez Álvarez, Sebastian Rudolph

► To cite this version:

Lucía Gómez Álvarez, Sebastian Rudolph. Reasoning in SHIQ with axiom- and concept-level standpoint modalities. KR 2024 - 21st International Conference on Principles of Knowledge Representation and Reasoning, Nov 2024, Hanoi, Vietnam. pp.383-393, 10.24963/kr.2024/36. hal-04884917

HAL Id: hal-04884917

https://hal.science/hal-04884917v1

Submitted on 13 Jan 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Reasoning in SHIQ with Axiom- and Concept-Level Standpoint Modalities

Lucía Gómez Álvarez<fnref n="1" />, Sebastian Rudolph<fnref n="2" />,³

¹Université Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, France

²Computational Logic Group, TU Dresden, Germany

³Center for Scalable Data Analytics and Artificial Intelligence Dresden/Leipzig, Germany

lucia.gomez-alvarez@inria.fr, sebastian.rudolph@tu-dresden.de

## Abstract

Standpoint logic is a recently proposed modal logic framework that is well-suited for multiperspective reasoning and ontology integration. For this reason, combinations of standpoint logic with description logics (DLs), a popular family of logic-based ontology languages, are of special interest.

Prior work has shown that it is possible to add standpoints to numerous decidable fragments of first-order logics – including very expressive DLs up to $SROIQb_s$ – while preserving their reasoning complexity, so long as standpoint modalities are limited to the axiom level. A more expressive tighter modal integration, where standpoint modalities are also allowed to occur in concept expressions, has so far only been investigated for the much less expressive DL $EL^+$.

In this paper, we push this line of research showing that the DL SHIQ allows for a tight modal integration with standpoints without compromising its EXPTIME reasoning complexity. The core insight toward this result is that any satisfiable knowledge base admits a model with only polynomially many worlds, an argument which requires a rather elaborate model-theoretic construction. This allows us to establish a polynomially satisfiable translation into plain SHIQ which, beyond showing the theoretical result, enables us to use highly optimised OWL reasoners to provide practical reasoning support for ontology languages extended by standpoint modelling. We complement our findings with the observation that our techniques would fail upon adding the modeling feature of nominals to the underlying DL.

## 1 Introduction

Within the knowledge representation community, a key objective has been to develop methods for integrating and effectively using various knowledge sources relevant to specific tasks. A common challenge in this area arises when dealing with multiple ontologies that overlap in content since they frequently differ in perspective and modelling principles. For example, in the medical domain, the concept of Allergy might be defined in one ontology as a reaction to exposure to a substance, while another ontology might define it as a chronic predisposition to such reactions. Similarly, the term Tumour can be used to refer either to a process or to an abnormal piece of tissue. These issues pose well-known challenges in the area of knowledge integration.

Standpoint logic is a recently proposed modal logic framework intended for multi-perspective reasoning and on-

tology integration. In a similar vein to epistemic logic, propositions with labelled modal operators $\Box_s\phi$ and $\Diamond_s\phi$ express information relative to the standpoint $s$ and read, respectively: “according to $s$, it is unequivocal/conceivable that $\phi$”. For instance, consider the following axioms formalising knowledge about Allergies and showcasing the different interpretations of a general practitioner (GP) and an emergency department (ED), with the former describing a sensitivity to a particular Substance, and the latter denoting a specific reaction to it.

$$ \Box_{GP}[\text{Allergy} \sqsubseteq \text{1 SensitivityTo.Substance}] \quad (\text{F1}) $$

$$ \Box_{ED}[\text{Allergy} \sqsubseteq \text{AntibodyRelease}] \quad (\text{F2}) $$

In the above example, axiom (F1) expresses that according to the GP every Allergy is a sensitivity to one specific Substance<fnref n="1" /> and axiom (F2) expresses that according to the ED it is unequivocal that an Allegy is a bodily release of antibodies (AntibodyRelease) in response to an event. In addition, one may want to relate those standpoints, for instance by means of the additional axiom

$$ \Box_{ED}[\text{Allergy} \sqsubseteq \exists \text{TriggeredBy.} \diamond_{GP}[\text{Allergy}]] \quad (\text{F3}) $$

expressing that according to the ED, allergies are always triggered by a certain kind of sensitivity to a substance that is in turn conceivably an Allergy according to the GP. Finally, we can establish hierarchies of standpoints via sharpening statements like ED $\preceq$ SNOMED, which indicates that the ED ontology is more precise than the SNOMED<fnref n="2" /> and thus the former standpoint inherits all the axioms of the latter. With this, the logic allows for the integrated representation of domain knowledge relative to diverse, possibly conflicting standpoints, which can be hierarchically organised, combined, and related.

Description logics (DLs) (Baader et al. 2017; Rudolph 2011) are one of the most prominent and successful families of logic-based knowledge representation formalisms and provide the formal basis for the Web Ontology Language OWL DL (Bao et al. 2009). Since supporting the interoperability of independently developed knowledge specifications or ontologies is a fundamental application scenario

<footnote n="1">¹In (F1), = is a shortcut for $\ge$ and $\le$; the complete axiom is $\Box_{GP}[\text{Allergy} \sqsubseteq (\ge 1 \text{ SensitivityTo.Substance} \wedge 1 \le 1 \text{ SensitivityTo.Substance})]$</footnote>

<footnote n="2">²The SNOMED CT (Donnelly 2006) is the largest healthcare ontology, with a broad user base of clinicians, researchers, ...</footnote>
for standpoint logic, the study of combinations of stand-
point logic with DLs is of particular interest. This goes in
line with previous work enhancing DLs to support different
forms of contextuality, for instance C-OWL (Bouquet et al.
2003), Distributed ontologies (Borgida and Serafini 2003)
and the Contextualised Knowledge Repository (Serafini and
Homola 2012; Bozzato, Eiter, and Serafini 2018).
Modal extensions of DLs in the spirit of what we propose
in this paper have been studied for years (Baader, Küsters,
and Wolter 2003). It is known that the interplay between
DL constructs and modalities is generally not well-behaved,
often endangering the decidability of reasoning tasks of ex-
tensions allowing for full modal integration (that is, for
modalised axioms, concepts and roles) or increasing their
complexity (Baader and Ohlbach 1995; Mosurović 1999;
Wolter and Zakharyaschev 1999) with high modal integra-
tion (that is, allowing for modalised axioms and concepts<fnref n="3" />).
Examples of the latter are the NEXPTIME-completeness of
the multi-modal description logic $K_{ALC}$ (Lutz et al. 2002)
and the 2EXPTIME-completeness of $ALC_{ALC}$ (Klarman
and Gutiérrez-Basulto 2013), also conceived as a contextual
logic framework (McCarthy and Buvac 1998).
We are especially interested in cases where one can ex-
tend a DL with the standpoint framework while preserving
the complexity of the standpoint-free DL. When choosing
such DLs as base languages, joint reasoning over the integ-
rated combination of possibly many ontologies is not funda-
mentally harder than reasoning with the ontologies in sep-
aration (beyond the difference in size) and there are prom-
ising paths toward efficient reasoning algorithms. In re-
cent work (Gómez Álvarez, Rudolph, and Strass 2023a), it
has been shown for the lightweight description logic $\mathcal{EL}+$,
that standpoint-$\mathcal{EL}+$ still exhibits $\mathcal{EL}$'s favourable PTIME
standard reasoning while having high modal integration,
which is necessary to exploit the full modelling features of
standpoint logic.<fnref n="4" /> For the much more expressive side of
DLs up to $SROIQb_s$, however, the results obtained so far
only consider sentential fragments, that is, the easier case
where the modal integration is limited to the axiom-level
(Gómez Álvarez, Rudolph, and Strass 2022).
In this paper, we push this line of research to show that
Standpoint-$\mathcal{SHIQ}$ stays in EXPTIME with high modal in-
tegration. Notice that the previous results for $\mathcal{EL}$ were shown
using a tableau algorithm and a saturation calculus, both
of which have the potential to be implemented into dedic-
ated “standpoint $\mathcal{EL}$” solvers. Here we follow a different
approach, which consists of first showing that Standpoint
$\mathcal{SHIQ}$ has a small-model property, and then exploiting the
higher expressivity of the base language to establish a poly-
nomial equisatisfiable translation from Standpoint $\mathcal{SHIQ}$
into plain $\mathcal{SHIQ}$ knowledge bases. Beyond establishing the
worst-case complexity, this technique paves the way for the
use of highly optimised OWL reasoners to provide reason-
ing support for Standpoint $\mathcal{SHIQ}$ ontologies.

Modal extensions of DLs in the spirit of what we propose
in this paper have been studied for years (Baader, Küsters,
and Wolter 2003). It is known that the interplay between
DL constructs and modalities is generally not well-behaved,
often endangering the decidability of reasoning tasks of ex-
tensions allowing for full modal integration (that is, for
modalised axioms, concepts and roles) or increasing their
complexity (Baader and Ohlbach 1995; Mosurović 1999;
Wolter and Zakharyaschev 1999) with high modal integra-
tion (that is, allowing for modalised axioms and concepts<fnref n="3" />).
Examples of the latter are the NEXPTIME-completeness of
the multi-modal description logic $K_{ALC}$ (Lutz et al. 2002)
and the 2EXPTIME-completeness of $ALC_{ALC}$ (Klarman
and Gutiérrez-Basulto 2013), also conceived as a contextual
logic framework (McCarthy and Buvac 1998).
We are especially interested in cases where one can ex-
tend a DL with the standpoint framework while preserving
the complexity of the standpoint-free DL. When choosing
such DLs as base languages, joint reasoning over the integ-
rated combination of possibly many ontologies is not funda-
mentally harder than reasoning with the ontologies in sep-
aration (beyond the difference in size) and there are prom-
ising paths toward efficient reasoning algorithms. In re-
cent work (Gómez Álvarez, Rudolph, and Strass 2023a), it
has been shown for the lightweight description logic $\mathcal{EL}+$,
that standpoint-$\mathcal{EL}+$ still exhibits $\mathcal{EL}$'s favourable PTIME
standard reasoning while having high modal integration,
which is necessary to exploit the full modelling features of
standpoint logic.<fnref n="4" /> For the much more expressive side of
DLs up to $SROIQb_s$, however, the results obtained so far
only consider sentential fragments, that is, the easier case
where the modal integration is limited to the axiom-level
(Gómez Álvarez, Rudolph, and Strass 2022).
In this paper, we push this line of research to show that
Standpoint-$\mathcal{SHIQ}$ stays in EXPTIME with high modal in-
tegration. Notice that the previous results for $\mathcal{EL}$ were shown
using a tableau algorithm and a saturation calculus, both
of which have the potential to be implemented into dedic-
ated “standpoint $\mathcal{EL}$” solvers. Here we follow a different
approach, which consists of first showing that Standpoint
$\mathcal{SHIQ}$ has a small-model property, and then exploiting the
higher expressivity of the base language to establish a poly-
nomial equisatisfiable translation from Standpoint $\mathcal{SHIQ}$
into plain $\mathcal{SHIQ}$ knowledge bases. Beyond establishing the
worst-case complexity, this technique paves the way for the
use of highly optimised OWL reasoners to provide reason-
ing support for Standpoint $\mathcal{SHIQ}$ ontologies.

We are especially interested in cases where one can ex-
tend a DL with the standpoint framework while preserving
the complexity of the standpoint-free DL. When choosing
such DLs as base languages, joint reasoning over the integ-
rated combination of possibly many ontologies is not funda-
mentally harder than reasoning with the ontologies in sep-
aration (beyond the difference in size) and there are prom-
ising paths toward efficient reasoning algorithms. In re-
cent work (Gómez Álvarez, Rudolph, and Strass 2023a), it
has been shown for the lightweight description logic $\mathcal{EL}+$,
that standpoint-$\mathcal{EL}+$ still exhibits $\mathcal{EL}$'s favourable PTIME
standard reasoning while having high modal integration,
which is necessary to exploit the full modelling features of
standpoint logic.<fnref n="4" /> For the much more expressive side of
DLs up to $SROIQb_s$, however, the results obtained so far
only consider sentential fragments, that is, the easier case
where the modal integration is limited to the axiom-level
(Gómez Álvarez, Rudolph, and Strass 2022).

In this paper, we push this line of research to show that Standpoint-$\mathcal{SHIQ}$ stays in EXPTIME with high modal integration. Notice that the previous results for $\mathcal{EL}$ were shown using a tableau algorithm and a saturation calculus, both of which have the potential to be implemented into dedicated “standpoint $\mathcal{EL}$” solvers. Here we follow a different approach, which consists of first showing that Standpoint $\mathcal{SHIQ}$ has a small-model property, and then exploiting the higher expressivity of the base language to establish a polynomial equisatisfiable translation from Standpoint $\mathcal{SHIQ}$ into plain $\mathcal{SHIQ}$ knowledge bases. Beyond establishing the worst-case complexity, this technique paves the way for the use of highly optimised OWL reasoners to provide reasoning support for Standpoint $\mathcal{SHIQ}$ ontologies.

The rest of the paper is organised as follows. After intro-
ducing the syntax and semantics of Standpoint SHIQ and a
suitable normal form (Section 2), we establish our main res-
ult: that satisfiability of Standpoint SHIQ knowledge bases
implies the existence of small models of a particular form,
which we call *tidy* models (Section 3). Subsequently, we
provide a polynomial equisatisfiable translation from Stand-
point SHIQ into SHIQ by virtue of which we establish
the complexity result (Section 4). We then show how nom-
inals break this small model property (Section 5) and we
finish the paper with concluding remarks and a discussion
of future work (Section 6).

## 2 Syntax and Semantics

We expect the reader to be familiar with the basics of de-
scription logics and in particular the popular description lo-
gic SHIQ. We start by introducing syntax and semantics
of Standpoint SHIQ (referred to as $\mathfrak{S}_{SHIQ}$) and propose a
normal form that is useful for the subsequent treatise.

### 2.1 Syntax

A Standpoint DL vocabulary contains a set $N_S$ of standpoint names with $* \in N_S$ the universal standpoint, together with a traditional DL vocabulary consisting of sets $N_1$ of individual names, $N_C$ of concept names, and $N_R^s$ and $N_R^{ns}$ of simple and nonsimple role names, respectively. All these sets are pairwise disjoint. The sets $R^s$ and $R^{ns}$ of simple/non-simple roles consist of all simple/non-simple role names $R$ and their inverted versions $R^-$. A standpoint operator is of the form $\diamond_s$ ("diamond") or $\Box_s$ ("box") with $s \in N_S$; we use $\odot_s$ to refer to either, and may delimit their scope by brackets [...].

* Concept terms are defined via

$$C ::= \top | \bot | A | \neg C | C_1 \sqcap C_2 | C_1 \sqcup C_2 \\ | \exists R.C | \forall R.C | \leq n.S.C | \geq n.S.C | \odot_s C, \\ \text{where } A \in N_C, R \in R^s \cup R^{ns}, S \in R^s, \text{ and } n \in \mathbb{N}.$$

* A general concept inclusion (GCI) is of the form $C \subseteq D$, where $C$ and $D$ are concept terms.

* A role inclusion (RI) is of the form $S \subseteq R$ where $S, R \in N_R^s \cup N_R^{ns}$ satisfying $S \in N_R^s$ or $R \in N_R^{ns}$.

* A transitivity axiom is of the form $Tra(R)$ with $R \in N_R^{ns}$.

* A concept assertion is of the form $C(a)$, where $C$ is a concept term and $a \in N_1$. A role assertion is of the form $R(a, b)$, with $a, b \in N_1$ and $R \in N_R$.

* An axiom $\xi$ is a GCI, RI, transitivity axiom, or assertion.

* A literal $\lambda$ is an axiom $\xi$ or a negated axiom $\neg\xi$.

* A monomial $\mu$ is a conjunction $\lambda_1 \wedge \dots \wedge \lambda_m$ of literals.

* A formula $\varphi$ is of the form $\odot_s\mu$ for a monomial $\mu$ and $s \in N_S$.

* A sharpening statement is of the form $s_1 \cap \dots \cap s_n \preceq s$ where $n \ge 1$ and $s_1, \dots, s_n, s \in N_S \cup \{0\}$.<fnref n="5" />

Note that monomials can be used to express any (finite)
$\mathcal{SHIQ}$ knowledge base, but even allow for the occurrence
of *negated* axioms. Still they do not cover arbitrary Boolean
combinations of axioms – a necessary restriction for our
complexity results.

<footnote n="3">³These are sometimes referred to in the literature as *monodic* fragments (Wolter and Zakharyaschev 2001).</footnote>

<footnote n="4">⁴Axioms like (F3), which allow us to establish alignments between different standpoints require this higher modal integration</footnote>

<footnote n="5">⁵$0$ is used to express standpoint disjointness as in $s \cap s' \preceq 0$.</footnote>
A $\mathbb{S}_{SHIQ}$ knowledge base (KB) is a finite set of formulae and possibly negated sharpening statements. We refer to arbitrary elements of $\mathcal{K}$ as statements. Note that all statements except sharpening statements are preceded by modal operators ("modalised" for short).

## 2.2 Semantics

The semantics of $\mathbb{S}_{SHIQ}$ is defined via (description logic) standpoint structures. Given a Standpoint DL vocabulary $\langle \mathbf{N}_S, \mathbf{N}_I, \mathbf{N}_C, \mathbf{N}_R, \mathbf{N}_R^{\text{ns}} \rangle$, a description logic standpoint structure is a tuple $\mathfrak{D} = \langle \Delta, \Pi, \sigma, \gamma \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 standpoint names to nonempty subsets of $\Pi$ while we set $\sigma(\emptyset) = \emptyset$ and $\sigma(*) = \Pi$;

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

- any concept name $A \in \mathbf{N}_C$ to a set $A^{\mathcal{I}} \subseteq \Delta$,

- any role name $R \in \mathbf{N}_R$ to a binary relation $R^{\mathcal{I}} \subseteq \Delta \times \Delta$,

- any individual name $a \in \mathbf{N}_I$ to an element $a^{\mathcal{I}} \in \Delta$,

requiring $\dot{a}^{\gamma(\pi)} = \dot{a}^{\gamma(\pi')}$ for all $\pi, \pi' \in \Pi$ and $a \in \mathbf{N}_I$.

By this definition, individual names (also called 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 all $\pi \in \Pi$, we extend the interpretation function $\mathcal{I} = \gamma(\pi)$ to inverted role names by $R^{-\mathcal{I}} := \{\langle \varepsilon, \delta \rangle \mid \langle \delta, \varepsilon \rangle \in R^{\mathcal{I}}\}$ and – inductively – to all concept terms as follows:

$$ 
\begin{align*}
\top^{\mathcal{I}} &:= \Delta & (C_1 \sqcap C_2)^{\mathcal{I}} &:= C_1^{\mathcal{I}} \sqcap C_2^{\mathcal{I}} \\
\bot^{\mathcal{I}} &:= \emptyset & (C_1 \sqcup C_2)^{\mathcal{I}} &:= C_1^{\mathcal{I}} \cup C_2^{\mathcal{I}} \\
(\neg C)^{\mathcal{I}} &:= \Delta \setminus C^{\mathcal{I}} \\
(\exists R.C)^{\mathcal{I}} &:= \{\delta \in \Delta \mid \langle \delta, \varepsilon \rangle \in R^{\mathcal{I}} \text{ for some } \varepsilon \in C^{\mathcal{I}}\} \\
(\forall R.C)^{\mathcal{I}} &:= \{\delta \in \Delta \mid \langle \delta, \varepsilon \rangle \in R^{\mathcal{I}} \text{ implies } \varepsilon \in C^{\mathcal{I}}\} \\
(\leq n.S.C)^{\mathcal{I}} &:= \{\delta \in \Delta \mid |\{\varepsilon \in C^{\mathcal{I}} \mid \langle \delta, \varepsilon \rangle \in S^{\mathcal{I}}\}| \leq n\} \\
(\geq n.S.C)^{\mathcal{I}} &:= \{\delta \in \Delta \mid |\{\varepsilon \in C^{\mathcal{I}} \mid \langle \delta, \varepsilon \rangle \in S^{\mathcal{I}}\}| \geq n\} \\
(\diamond_s C)^{\mathcal{I}} &:= \bigcup_{\pi' \in \sigma(s)} C^{\gamma(\pi')} \\
(\Box_s C)^{\mathcal{I}} &:= \bigcap_{\pi' \in \sigma(s)} C^{\gamma(\pi')}
\end{align*}
$$

We observe that precisifications are akin to worlds or points in Kripke models<fnref n="6" />, and that modalised concepts $\odot_s C$ are interpreted uniformly across all precisifications $\pi \in \Pi$, which allows us to denote their extensions with $(\odot_s C)^{\mathfrak{D}}$. For technical reasons, we will also make use of the concept constructor $\llcorner$, where $\llcorner n.S.C$ is a shorthand for $\llcorner n.S.\neg C$ and can be read as "all but (maximally) $n$ S-neighbours satisfy $C$". By means of the usual concept equivalences as well as the observation $(\neg\diamond_s C)^{\mathcal{I}} = (\Box_s\neg C)^{\mathcal{I}}$, it is easy to show

that every concept term $C$ can be easily transformed into an equivalent concept term $NNF(C)$ in negation normal form, where all subterms using $\llcorner$ have been rewritten into subterms using $\llcorner$ and negation is allowed to occur only in front of concept names.

Satisfaction of a statement by a DL standpoint structure $\mathfrak{D}$ (and precisification $\pi$) is then defined as follows:

$$ 
\begin{align*}
\mathfrak{D}, \pi \models C \sqsubseteq D &::= C^{\gamma(\pi)} \sqsubseteq D^{\gamma(\pi)} \\
\mathfrak{D}, \pi \models S \sqsubseteq R &::= S^{\gamma(\pi)} \sqsubseteq R^{\gamma(\pi)} \\
\mathfrak{D}, \pi \models \text{Tra}(R) &::= R^{\gamma(\pi)} \text{ is transitive} \\
\mathfrak{D}, \pi \models C(a) &::= a^{\mathfrak{D}} \models C^{\gamma(\pi)} \\
\mathfrak{D}, \pi \models R(a, b) &::= \langle a^{\mathfrak{D}}, b^{\mathfrak{D}} \rangle \models R^{\gamma(\pi)} \\
\mathfrak{D}, \pi \models \neg \xi &::= \mathfrak{D}, \pi \not\models \xi \\
\mathfrak{D}, \pi \models \lambda_1 \wedge \dots \wedge \lambda_n &::= \mathfrak{D}, \pi \models \lambda_i \text{ for all } 1 \le i \le n \\
\mathfrak{D} \models \Box_s \mu &::= \mathfrak{D}, \pi \models \mu \text{ for each } \pi \in \sigma(s) \\
\mathfrak{D} \models \diamond_s \mu &::= \mathfrak{D}, \pi \models \mu \text{ for some } \pi \in \sigma(s) \\
\mathfrak{D} \models s_1 \cap \dots \cap s_n \preceq s &::= \sigma(s_1) \cap \dots \cap \sigma(s_n) \subseteq \sigma(s)
\end{align*}
$$

Finally, $\mathfrak{D}$ is a model of a $\mathbb{S}_{SHIQ}$ knowledge base $\mathcal{K}$ (written $\mathfrak{D} \models \mathcal{K}$) iff it satisfies every statement in $\mathcal{K}$. As usual, we call $\mathcal{K}$ satisfiable iff some $\mathfrak{D}$ with $\mathfrak{D} \models \mathcal{K}$ exists. A $\mathbb{S}_{SHIQ}$ statement $\psi$ is entailed by $\mathcal{K}$ (written $\mathcal{K} \models \psi$) iff $\mathfrak{D} \models \psi$ holds for every model $\mathfrak{D}$ of $\mathcal{K}$.

For the sake of illustration, Figure 2 (1) depicts a model of the $\mathbb{S}_{SHIQ}$ knowledge base consisting of the axioms (F1-3), with each point denoting the interpretation of a domain element $\delta$ at a precisification $\pi$. The blue labels at the top left of points represent the concepts to which $\delta$ belongs and the green arrows represent the roles it participates in at $\pi$.

For our subsequent treatise, we will presume that the sets $\Delta$ and $\Pi$ of all considered structures are countable. This assumption can be made without loss of generality since $\mathbb{S}_{SHIQ}$ could be reformulated as a fragment of (two-sorted) first-order logic, so that the downward Löwenheim-Skolem Theorem can be applied (Skolem 1929).

## 2.3 Normalisation

It will be convenient to work with $\mathbb{S}_{SHIQ}$ knowledge bases in normal form, as specified in the following.

**Definition 1 (Normal Form of $\mathbb{S}_{SHIQ}$ Knowledge Bases).** A KB $\mathcal{K}$ is in normal form iff it only contains statements of the following shapes:

* sharpening statements not using 0,

* modalised GCIs of the shape $\Box_s[\top \sqsubseteq C]$ with $s \in \mathbf{N}_S$ and $C$ a concept term in negation normal form.

* modalised axioms of the form $\Box_s \xi$ where $\xi$ is any RI, transitivity axiom, role assertion, or concept assertion $C(a)$ with $C$ in negation normal form. $\triangleright$

For a given $\mathbb{S}_{SHIQ}$ KB $\mathcal{K}$, we can compute its normal form by exhaustively applying the transformation rules depicted in Figure 1, where "rule application" means that the statement on the left-hand side is replaced with the set of statements on the right-hand side. This eliminates most statements preceded by diamonds, modalised axiom sets, and negated axioms.

<footnote n="6">⁶The term *precisification*, which comes from the supervaluationist theory of natural language, is used when one models precise interpretations of the language rather than possible states of affairs (Gómez Álvarez and Rudolph 2021).</footnote>
<figure><img src="image_2.png" /><figcaption>Figure 1: Normalisation rules for $\mathbb{S}_{SHIQ}$ knowledge bases. Therein, $s_1, \dots, s_n, u \in \mathbb{N}_S \cup \{0\}$, the $A, A_a, A_b$ denote fresh concept names, $R'$ a fresh role name, and $v$ a fresh standpoint name. The last rule is only applied if $C$ is not $\top$ or $D$ is not in negation normal form.</figcaption></figure>

**Lemma 1.** Any $\mathbb{S}_{SHIQ}$ KB $\mathcal{K}$ can be transformed into a $\mathbb{S}_{SHIQ}$ KB $\mathcal{K}'$ in normal form such that:

* $\mathcal{K}'$ and $\mathcal{K}$ are equisatisfiable,

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

* the transformation can be computed in PTIME.

## 2.4 Reasoning Problems and Reducibility

Now we briefly recap the two central reasoning tasks (knowledge base) satisfiability and statement entailment, which we will investigate in this paper.

**Problem:** $\mathbb{S}_{SHIQ}$ KNOWLEDGE BASE SATISFIABILITY

**Input:** $\mathbb{S}_{SHIQ}$ knowledge base $\mathcal{K}$.

**Output:** YES, if $\mathcal{K}$ has a model, NO otherwise.

This reasoning task is useful in itself, e.g. for knowledge engineers to check for grave modelling errors that turn the specified knowledge base globally inconsistent. From a user's perspective, however, a more application-relevant problem is that of statement entailment, allowing for determining consequences following from the specified knowledge:

**Problem:** $\mathbb{S}_{SHIQ}$ STATEMENT ENTAILMENT

**Input:** $\mathbb{S}_{SHIQ}$ knowledge base $\mathcal{K}$, $\mathbb{S}_{SHIQ}$ statement $\phi$.

**Output:** YES, if $\mathcal{K} \models \phi$, NO otherwise.

Using the same techniques as described in our prior work (Gómez Álvarez, Rudolph, and Strass 2023a), we can establish reducibility of statement entailment to KB satisfiability.

**Theorem 2.** There exists a PTIME Turing reduction from $\mathbb{S}_{SHIQ}$ STATEMENT ENTAILMENT to $\mathbb{S}_{SHIQ}$ KNOWLEDGE BASE SATISFIABILITY.

## 3 Small Models for Standpoint SHIQ

We now proceed to show that any satisfiable $\mathbb{S}_{SHIQ}$ KB $\mathcal{K}$ has a model of a very specific shape, having only polynomially many precisifications with respect to the size of $\mathcal{K}$. Due to Lemma 1, we will assume without loss of generality that $\mathcal{K}$ is in normal form. We let $ST(\mathcal{K})$ denote

all the concept terms (including subterms) occurring inside $\mathcal{K}$. For any $t \in \mathbb{N}_S$, we let $t^K$ denote the smallest set of standpoint names that (i) contains $t$ and $*$ and (ii) for any sharpening statement $s_1 \cap \dots \cap s_n \preceq s$ from $\mathcal{K}$ we have that $\{s_1, \dots, s_n\} \subseteq t^K$ implies $s \in t^K$.

**Definition 2.** Given a $\mathbb{S}_{SHIQ}$ KB $\mathcal{K}$ in normal form, a model $\mathcal{D} = (\Delta, \Pi, \sigma, \gamma)$ of $\mathcal{K}$ is *tidy*, if $\Pi$ consists of the following distinct elements:

* for all $s \in \mathbb{N}_S(\mathcal{K})$ a precisification $\pi_s \in \sigma(s)$,

* for all $\diamond_s C \in ST(\mathcal{K})$ two precisifications $\pi_{s,C}^0, \pi_{s,C}^1 \in \sigma(s)$,

* for all $\diamond_s C \in ST(\mathcal{K})$ and $a \in \mathbb{N}_I(\mathcal{K})$ a precisification $\pi_{s,C}^a \in \sigma(s)$.

Given $\mathcal{K}$, let $\Pi_{\mathcal{K}}$ denote the specific set $\Pi$ described above. $\diamond$

In and by itself, the definition of tidiness just fixes the set of precisifications and assigned standpoints. While the names used for the precisifications may seem arbitrary, they will be instantiated in the subsequent construction by worlds witnessing (i) standpoint non-emptiness, (ii) diamond concept memberships of anonymous individuals, and (iii) diamond concept membership of named individuals. In particular, we will make sure that our tidy model requires just two s-precisifications – namely $\pi_{s,C}^0$ and $\pi_{s,C}^1$ – to jointly witness local satisfaction of $C$ simultaneously for all anonymous individuals from $(\diamond_s C)^\mathcal{D}$. This requirement is crucial to keep the total number of precisifications polynomial in the size of $\mathcal{K}$ in order to establish our wanted complexity result. However, this requirement is not to be taken for granted nor easily achieved. To see this, consider the statement $\Box_*[\top \sqsubseteq \diamond_s A]$, establishing that every domain individual is in $A$ in some s-precisification. In the worst case, a model of this statement could be such that every domain element satisfies $A$ in a different precisification. Then, each of these – numerous or even infinitely many – “witnessing” precisifications would be essential to satisfy the above statement, i.e., removing any of them would destroy modelhood.

We will proceed to show that, despite these hindrances, every satisfiable normalized $\mathbb{S}_{SHIQ}$ KB has a model that is tidy. To this end, we use the common strategy for such pur-
<figure><img src="image_3.png" /><figcaption>Figure 2: (1) illustrates a model $\mathcal{D}^o$ of the axioms (F1-3), which we refer to as $\mathcal{K}$. Each row denotes a precisification in the model, which is associated to a standard-DL interpretation of the shared domain, in columns. (2) illustrates a $\mathcal{K}$-pruning $\mathcal{D}$ of $\mathcal{D}^o$, for which the values of the functions $f$ and $g$ are specified in Table 1. Notice that $\Delta$ is an infinite sequence and the roles pointing to the outside of the figure are associated to some domain element $\langle\delta, k\rangle$ with $k > 3$.</figcaption></figure>

poses: given an arbitrary model $\mathcal{D}^o$, we describe how to use it to construct a tidy model $\mathcal{D}$. For the reasons just discussed, however, the tidy model can not be obtained by simply eliminating enough precisifications. Rather, we describe an elaborate construction that allows to “squeeze” all the witnessing precisifications into just two. In doing so, we greatly benefit from the well-known fact that in the description logistic SHIQ, the disjoint union of two or more models will be a model again (Rudolph 2011). This observation makes sure that several precisifications can actually “co-exist” side by side inside one precisification without mutual interference. What remains to be taken care of is the alignment across precisifications, which we will have to arrange in a “pedestrian”, stepwise fashion. For cardinality reasons, “squeezing” many witnessing precisifications into two in a bijective fashion requires the domain $\Delta$ of our to-be-constructed tidy model to be infinite. Moreover, for alignment reasons, the domain also needs to contain many “look-alike” elements. Both of these requirements are achieved by letting $\Delta$ consist of countably many copies of the domain $\Delta^o$ of the originally provided model $\mathcal{D}^o$. This intuition should make it easier to grasp the formal definition of our model construction.

**Definition 3.** Let $\mathcal{K}$ be a $\mathcal{S}_{SHIQ}$ KB in normal form and let $\mathcal{D}^o = \langle\Delta^o, \Pi^o, \sigma^o, \gamma^o\rangle$ be a model of $\mathcal{K}$. Then, a structure $\mathcal{D} = \langle\Delta, \Pi, \sigma, \gamma\rangle$ is a $\mathcal{K}$-pruning of $\mathcal{D}^o$ if it can be constructed in the following way:

* Let $\Delta = \Delta^o \times \mathbb{N}$ and $\Pi = \Pi_{\mathcal{K}}$.

* Let $\sigma(s') = \{\pi_s, \pi_{s,C}^0, \pi_{s,C}^1, \pi_{s,C}^a \in \Pi_{\mathcal{K}} \mid s' \in s^{\mathcal{K}}, s \in \mathbb{N}_s\}$,

* $a^{\mathcal{D}} = \langle a^{\mathcal{D}^o}, 0 \rangle$ for all $a \in \mathbb{N}_1(\mathcal{K})$

* $A^{\gamma(\pi)} = \{\langle\delta, k\rangle \mid \delta \in A^{\gamma^o(f(\pi, \delta, k))}\}$

* $R^{\gamma(\pi)}$ contains every pair $\langle\langle\delta, k\rangle, \langle\epsilon, \ell\rangle\rangle \in \Delta \times \Delta$ for which $f(\pi, \delta, k) = f(\pi, \epsilon, \ell)$ and $g(\pi, \delta, k) = g(\pi, \epsilon, \ell)$ and $\langle\delta, \epsilon\rangle \in R^{\gamma^o(f(\pi, \delta, k))}$.

Where $f: \Pi \times \Delta^o \times \mathbb{N} \to \Pi^o$ and $g: \Pi \times \Delta^o \times \mathbb{N} \to \mathbb{N}$ are functions obtained as follows:

(C1) For any $\pi_s \in \Pi$ pick some $\pi \in \Pi^o$ with $\pi \in \sigma^o(s)$, and let $f(\pi_s, \delta, k) = \pi$ and $g(\pi_s, \delta, k) = k$.

(C2) For any $\pi_{s,C}^a \in \Pi$ pick some $\pi \in \Pi^o$ with $\pi \in \sigma^o(s)$,

and let $f(\pi_{s,C}^a, \delta, k) = \pi$ and $g(\pi_{s,C}^a, \delta, k) = k$. In the case where $\mathcal{D}^o \models \Diamond_s(C(a))$, pick $\pi$ such that it also satisfies $a^{\mathcal{D}^o} \in C^{\gamma^o(\pi)}$.

(C3) For $\pi_{s,C}^i$ with $i \in \{0, 1\}$, let $\Pi' = \sigma^o(s)$ and let $\trianglelefteq$ be some order over $\Pi' \times \mathbb{N}$ induced by an enumeration$^7$ of this set (thus, in particular, $\trianglelefteq$ is a linear discrete well-order). Let $\pi'$ be an arbitrary element of $\Pi'$. For any fixed $\delta \in \Delta^o$, we now define the unary functions $f(\pi_{s,C}^i, \delta, \cdot)$ and $g(\pi_{s,C}^i, \delta, \cdot)$ step by step, incrementing the last argument. In case $k = 0$ and $\delta$ is named in $\mathcal{D}^o$, we let $f(\pi_{s,C}^i, \delta, 0) = \pi'$ and $g(\pi_{s,C}^i, \delta, 0) = 0$. Otherwise, we distinguish two cases:

(C3.1) Whenever $\delta \in (\Diamond_s C)^{\mathcal{D}^o}$ and $k + i$ is even, we let $\langle\pi, m\rangle$ be the $\trianglelefteq$-smallest element of $\Pi' \times \mathbb{N}$ that (first) satisfies $\delta \in C^{\gamma^o(\pi)}$ and (second) is not in $\{\langle f(\pi_{s,C}^i, \delta, \ell), g(\pi_{s,C}^i, \delta, \ell)\rangle \mid \ell < k\}$. Then let $f(\pi_{s,C}^i, \delta, k) = \pi$ and $g(\pi_{s,C}^i, \delta, k) = m$.

(C3.2) If the above is not the case, let $\langle\pi, m\rangle$ simply be the $\trianglelefteq$-smallest element of $\Pi' \times \mathbb{N}$ not contained in $\{\langle f(\pi_{s,C}^i, \delta, \ell), g(\pi_{s,C}^i, \delta, \ell)\rangle \mid \ell < k\}$. Then let $f(\pi_{s,C}^i, \delta, k) = \pi$ and $g(\pi_{s,C}^i, \delta, k) = m$. $\Diamond$

Let us discuss Definition 3 in some more detail. First, each precisification of the form $\pi_s$ ensures that the standpoint $s$ is non-empty. For this, in (C1) it is sufficient to pick any precisification $\pi$ in $\sigma^o(s)$ and obtain $\pi_s$ as the $\mathbb{N}$-fold disjoint union of $\pi$ (that is, every $\langle\delta, k\rangle$ at $\pi_s$ “looks like” $\delta$ at $\pi$). Mark that thanks to our normal form, diamonds will only occur at the concept level and notice that any precisification $\pi$ will satisfy any boxed expression both at the concept and axiom levels.

The purpose of the rest of the precisifications in the $\mathcal{K}$-pruning is to witness diamond concept memberships of named and unnamed individuals. For the named case, we have precisifications of the form $\pi_{s,C}^a$ which are meant

<footnote>$^7$Recall that an enumeration of a countably infinite set $S$ is a bijection from $\mathbb{N}$ to $S$ and that for every countably infinite set, such an enumeration exists.</footnote>
<table><caption>Table 1: Values of the functions $f(\pi, \delta, k)$ and $g(\pi, \delta, k)$ for each $\pi \in \Pi$, $\delta \in \Delta^o$ and $k \in \mathbb{N}$, for the $\mathcal{K}$-pruning in Example 1. The table shows values up to $k = 9$, with the cases (C1), (C3.1) and (C3.2) from Definition 3 coloured in blue, purple and green respectively.</caption><thead><tr><th rowspan="2">Π</th><th rowspan="2">Δ</th><th colspan="10">f(π, δ, k), g(π, δ, k)</th></tr><tr><th>k = 0</th><th>k = 1</th><th>k = 2</th><th>k = 3</th><th>k = 4</th><th>k = 5</th><th>k = 6</th><th>k = 7</th><th>k = 8</th><th>k = 9</th><th>...</th></tr></thead><tbody><tr><td rowspan="3">π<sub>ED</sub></td><td>δ<sub>1</sub></td><td>π<sub>1</sub>, 0</td><td>π<sub>1</sub>, 1</td><td>π<sub>1</sub>, 2</td><td>π<sub>1</sub>, 3</td><td>π<sub>1</sub>, 4</td><td>π<sub>1</sub>, 5</td><td>π<sub>1</sub>, 6</td><td>π<sub>1</sub>, 7</td><td>π<sub>1</sub>, 8</td><td>π<sub>1</sub>, 9</td><td></td></tr><tr><td>δ<sub>2</sub></td><td>π<sub>1</sub>, 0</td><td>π<sub>1</sub>, 1</td><td>π<sub>1</sub>, 2</td><td>π<sub>1</sub>, 3</td><td>π<sub>1</sub>, 4</td><td>π<sub>1</sub>, 5</td><td>π<sub>1</sub>, 6</td><td>π<sub>1</sub>, 7</td><td>π<sub>1</sub>, 8</td><td>π<sub>1</sub>, 9</td><td></td></tr><tr><td>δ<sub>3</sub></td><td>π<sub>1</sub>, 0</td><td>π<sub>1</sub>, 1</td><td>π<sub>1</sub>, 2</td><td>π<sub>1</sub>, 3</td><td>π<sub>1</sub>, 4</td><td>π<sub>1</sub>, 5</td><td>π<sub>1</sub>, 6</td><td>π<sub>1</sub>, 7</td><td>π<sub>1</sub>, 8</td><td>π<sub>1</sub>, 9</td><td></td></tr><tr><td rowspan="3">π<sub>GP</sub></td><td>δ<sub>1</sub></td><td>π<sub>4</sub>, 0</td><td>π<sub>4</sub>, 1</td><td>π<sub>4</sub>, 2</td><td>π<sub>4</sub>, 3</td><td>π<sub>4</sub>, 4</td><td>π<sub>4</sub>, 5</td><td>π<sub>4</sub>, 6</td><td>π<sub>4</sub>, 7</td><td>π<sub>4</sub>, 8</td><td>π<sub>4</sub>, 9</td><td></td></tr><tr><td>δ<sub>2</sub></td><td>π<sub>4</sub>, 0</td><td>π<sub>4</sub>, 1</td><td>π<sub>4</sub>, 2</td><td>π<sub>4</sub>, 3</td><td>π<sub>4</sub>, 4</td><td>π<sub>4</sub>, 5</td><td>π<sub>4</sub>, 6</td><td>π<sub>4</sub>, 7</td><td>π<sub>4</sub>, 8</td><td>π<sub>4</sub>, 9</td><td></td></tr><tr><td>δ<sub>3</sub></td><td>π<sub>4</sub>, 0</td><td>π<sub>4</sub>, 1</td><td>π<sub>4</sub>, 2</td><td>π<sub>4</sub>, 3</td><td>π<sub>4</sub>, 4</td><td>π<sub>4</sub>, 5</td><td>π<sub>4</sub>, 6</td><td>π<sub>4</sub>, 7</td><td>π<sub>4</sub>, 8</td><td>π<sub>4</sub>, 9</td><td></td></tr><tr><td rowspan="3">π<sup>0</sup><sub>GP,Allergy</sub></td><td>δ<sub>1</sub></td><td>π<sub>3</sub>, 0</td><td>π<sub>4</sub>, 0</td><td>π<sub>5</sub>, 0</td><td>π<sub>3</sub>, 1</td><td>π<sub>4</sub>, 1</td><td>π<sub>5</sub>, 1</td><td>π<sub>3</sub>, 2</td><td>π<sub>4</sub>, 2</td><td>π<sub>5</sub>, 2</td><td>π<sub>3</sub>, 3</td><td></td></tr><tr><td>δ<sub>2</sub></td><td>π<sub>3</sub>, 0</td><td>π<sub>5</sub>, 0</td><td>π<sub>4</sub>, 0</td><td>π<sub>5</sub>, 1</td><td>π<sub>3</sub>, 1</td><td>π<sub>5</sub>, 2</td><td>π<sub>4</sub>, 1</td><td>π<sub>5</sub>, 3</td><td>π<sub>3</sub>, 2</td><td>π<sub>5</sub>, 4</td><td></td></tr><tr><td>δ<sub>3</sub></td><td>π<sub>3</sub>, 0</td><td>π<sub>4</sub>, 0</td><td>π<sub>5</sub>, 0</td><td>π<sub>3</sub>, 1</td><td>π<sub>4</sub>, 1</td><td>π<sub>5</sub>, 1</td><td>π<sub>3</sub>, 2</td><td>π<sub>4</sub>, 2</td><td>π<sub>5</sub>, 2</td><td>π<sub>3</sub>, 3</td><td></td></tr><tr><td rowspan="3">π<sup>1</sup><sub>GP,Allergy</sub></td><td>δ<sub>1</sub></td><td>π<sub>3</sub>, 0</td><td>π<sub>4</sub>, 0</td><td>π<sub>5</sub>, 0</td><td>π<sub>3</sub>, 1</td><td>π<sub>4</sub>, 1</td><td>π<sub>5</sub>, 1</td><td>π<sub>3</sub>, 2</td><td>π<sub>4</sub>, 2</td><td>π<sub>5</sub>, 2</td><td>π<sub>3</sub>, 3</td><td></td></tr><tr><td>δ<sub>2</sub></td><td>π<sub>5</sub>, 0</td><td>π<sub>3</sub>, 0</td><td>π<sub>5</sub>, 1</td><td>π<sub>4</sub>, 0</td><td>π<sub>5</sub>, 2</td><td>π<sub>3</sub>, 1</td><td>π<sub>5</sub>, 3</td><td>π<sub>4</sub>, 1</td><td>π<sub>5</sub>, 4</td><td>π<sub>3</sub>, 2</td><td></td></tr><tr><td>δ<sub>3</sub></td><td>π<sub>3</sub>, 0</td><td>π<sub>4</sub>, 0</td><td>π<sub>5</sub>, 0</td><td>π<sub>3</sub>, 1</td><td>π<sub>4</sub>, 1</td><td>π<sub>5</sub>, 1</td><td>π<sub>3</sub>, 2</td><td>π<sub>4</sub>, 2</td><td>π<sub>5</sub>, 2</td><td>π<sub>3</sub>, 3</td><td></td></tr></tbody></table>

to witness the $\mathcal{C}$-membership of named individuals $a$, whenever the latter satisfy some $\diamond_s C$. In order to form such a $\pi_{s,C}^a$, in (C2) we pick from $\sigma^o(s)$ any $\pi$ with $a^{\mathcal{D}^o} \in C^{\gamma^o(\pi)}$, and again obtain $\pi_{s,C}^a$ as the $\mathbb{N}$-fold disjoint union of $\pi$, where we stipulate $a^{\mathcal{D}^o} = \langle\delta, 0\rangle$ (when taking disjoint unions of precisifications, constants must not be duplicated, so we always place them in the first copy).

For the much more intricate unnamed case, our goal is to let the two precisifications $\pi_{s,C}^0$ and $\pi_{s,C}^1$ together witness all the $\mathcal{C}$-memberships of all unnamed $\diamond_s C$-instances of $\Delta$ at once. To achieve this, in (C3) we make use of all precisifications from $\sigma^o(s)$ for the creation of $\pi_{s,C}^0$ and $\pi_{s,C}^1$. More specifically, each $\pi_{s,C}^i$ is composed of infinitely many copies of each $\pi \in \sigma^o(s)$, and the alignment with the other precisifications is arranged in such a way that if $\delta \in (\diamond_s C)^{\mathcal{D}^o}$ then we have $\langle\delta, k\rangle \in C^{\gamma(\pi_{s,C}^0)}$ for even $k$ and $\langle\delta, k\rangle \in C^{\gamma(\pi_{s,C}^1)}$ for odd $k$ (that is $\pi_{s,C}^0$ and $\pi_{s,C}^1$ take turns at “witness duty”), thus clearly achieving $\langle\delta, k\rangle \in (\diamond_s C)^{\mathcal{D}}$ for any $k$. Thereby, the two auxiliary functions $f$ and $g$ serve as “coordinates” relating each $\langle\delta, k\rangle \in \Delta$ at some $\pi \in \Pi$ to the very copy of the $\pi' \in \Pi^o$ which we choose to serve as “blueprint” for $\langle\delta, k\rangle$ in terms of concept and role memberships. So for $f(\pi_{s,C}^i, \delta, k) = \pi$ and $g(\pi_{s,C}^i, \delta, k) = m$, the interpretation of the element $\langle\delta, k\rangle$ at the precisification $\pi_{s,C}^i$ is the $m$th copy of the interpretation of $\delta$ at $\pi$. Notice that we keep track of $m$ to ensure that roles are copied correctly, so $\langle\langle\langle\delta, k\rangle, \langle\epsilon, \ell\rangle\rangle \in R^{\gamma(\pi_{s,C}^i)}$ only if $\langle\delta, k\rangle$ and $\langle\epsilon, \ell\rangle$ correspond to the same copy of the same precisification.

**Example 1.** Consider a knowledge base $\mathcal{K}$ consisting of the set of axioms (F1-3), and its model $\mathcal{D}^o$ in Figure 2 (1). We show how to produce its $\mathcal{K}$-pruning $\mathcal{D}$. First, we have,

* $\Pi' = \{\pi_1\}$ for $\pi_{ED}$,

* $\Pi' = \{\pi_4\}$ for $\pi_{GP}$,

* $\Pi' = \{\pi_3, \pi_4, \pi_5\}$ for $\pi_{GP,Allergy}^0$ and $\pi_{GP,Allergy}^1$.

Also, let $\sqsubseteq$ give rise to the enumeration $\langle\pi_3, 0\rangle$, $\langle\pi_4, 0\rangle$, $\langle\pi_5, 0\rangle$, $\langle\pi_3, 1\rangle$, $\langle\pi_4, 1\rangle$, $\langle\pi_5, 1\rangle$, $\langle\pi_3, 2\rangle$, ..., for $\pi_{GP,Allergy}^0$ and $\pi_{GP,Allergy}^1$. With this, we have everything in place to assign the values for each $f(\pi, \delta, k)$ and $g(\pi, \delta, k)$ in the way specified in Definition 3, which we can see in Table 1. The resulting pruning is illustrated in Figure 2 (2). $\diamond$

In the rest of the section we introduce some intermediate lemmas and we finish with Theorem 7, which establishes that every satisfiable standpoint SHIQ knowledge base $\mathcal{K}$ has a tidy model. The proof-sketches contain the most interesting cases and the full proofs are provided in the supplementary material.

First, we show that for every precisification $\pi$ in $\mathcal{D}$, there is a bijective mapping between every element in $\Delta$ and its origin in $\mathcal{D}^o$. This is given by the precisification in $\Pi'$, the associated element in $\Delta^o$, and the specific copy (in $\mathbb{N}$).

**Lemma 3.** Let $\mathcal{K}$, $\mathcal{D}^o$, and $\mathcal{D}$ as well as $f$ and $g$ be as in the above definition. Let $\pi \in \Pi$ and let $\Pi' = \{f(\pi, \epsilon, \ell) \mid \epsilon \in \Delta^o, \ell \in \mathbb{N}\}$. Then, for every $\delta \in \Delta^o$, the mapping

$$k \mapsto \langle f(\pi, \delta, k), g(\pi, \delta, k) \rangle$$

is a bijection from $\mathbb{N}$ to $\Pi' \times \mathbb{N}$. Consequently, the mapping

$$\langle\delta, k\rangle \mapsto \langle f(\pi, \delta, k), \delta, g(\pi, \delta, k) \rangle$$

is a bijection from $\Delta$ to $\Pi' \times \Delta^o \times \mathbb{N}$.

*Proof.* We prove that for every $\delta \in \Delta^o$, the mapping $k \mapsto \langle f(\pi, \delta, k), g(\pi, \delta, k) \rangle$ is a bijection from $\mathbb{N}$ to $\Pi' \times \mathbb{N}$.

First, we prove that the mapping is injective.

**Case $\pi$ is $\pi_s$ or $\pi_{s,C}^a$**. We recall that $\Pi'$ is a singleton, and $g(\pi, \delta, k) = k$ from Definition 3. Then, it is easy to see that if $\langle f(\pi, \delta, k), g(\pi, \delta, k) \rangle = \langle f(\pi, \delta, k'), g(\pi, \delta, k') \rangle$ then $k = k'$ as desired.
**Case π is π<sup>i</sup><sub>s,C</sub> with i ∈ {0, 1}.** There are two subcases:

* If $k = 0$ and $\delta$ is named in $\mathcal{D}^o$: By Definition 3 we have $f(\pi, \delta, k) = \pi'$ and $g(\pi, \delta, k) = 0$. For the sake of contradiction, assume $\langle f(\pi, \delta, k), g(\pi, \delta, k) \rangle = \langle f(\pi, \delta, k'), g(\pi, \delta, k') \rangle$ but $k' > 0$. Then by the definition of $f$ and $g$ (Definition 3) we have a contradiction because we cannot assign $f(\pi, \delta, k') = \pi'$ and $g(\pi, \delta, k') = 0$ since $\langle \pi', 0 \rangle = \{ \langle f(\pi, \delta, \ell), g(\pi, \delta, \ell) \rangle | \ell < k' \}$.

* Else: assume $f(\pi, \delta, k) = \pi'$, $g(\pi, \delta, k) = m$, $f(\pi, \delta, k') = \pi'$, and $g(\pi, \delta, k') = m$, but $k \neq k'$, with $k > k'$. Then by the definition of $f$ and $g$ (Definition 3) we have a contradiction because we cannot assign $f(\pi, \delta, k) = \pi'$ and $g(\pi, \delta, k) = m$ since $\langle \pi', m \rangle = \{ \langle f(\pi, \delta, \ell), g(\pi, \delta, \ell) \rangle | \ell < k \}$ because $k' < k$.

Then, we prove that the mapping is surjective.

**Case π is π<sub>s</sub> or π<sup>a</sup><sub>s,C</sub>.** By Definition 3, it is easy to see that for all $\langle \pi', k \rangle \in \Pi' \times \mathbb{N}$ there is a mapping from $k \in \mathbb{N}$ to $\langle \pi', k \rangle$, since $g(\pi, \delta, k) = k$.

**Case π is π<sup>i</sup><sub>s,C</sub> with i ∈ {0, 1}.** Assume $\langle \pi', m \rangle \in \Pi' \times \mathbb{N}$ and there is no $k \in \mathbb{N}$ such that $f(\pi, \delta, k) = \pi'$ and $g(\pi, \delta, k) = m$. But from the order $\sqsubseteq$ we know that $\langle \pi', m \rangle$ is the ith element of $\Pi' \times \mathbb{N}$. Then, from the definition of $f$ and $g$ (Definition 3), we can see that the tuple $\langle \pi', m \rangle$ must be assigned to some $k \in \mathbb{N}$ such that $k \le 2i + 1$ because in the worst case, for every $k > 0$ and $k + 1$ odd, $k$ maps to the $\sqsubseteq$-smallest element of $\Pi' \times \mathbb{N}$ that is not contained in $\{ \langle f(\pi, \delta, \ell), g(\pi, \delta, \ell) \rangle | \ell < k \}$. □

It is now easier to show that for an element $\langle \delta, k \rangle \in \Delta$ at some $\pi \in \Pi$, if its origin has a concept membership in $\mathcal{D}^o$ then $\langle \delta, k \rangle$ has this same concept membership in $\pi$, thus "copying" the origin's interpretation.

**Lemma 4.** Let $\mathcal{K}$, $\mathcal{D}^o$, and $\mathcal{D}$ as well as $f$ be as in Definition 3. Then, for any $\pi \in \Pi$, $\langle \delta, k \rangle \in \Delta$, and $C \in \mathcal{ST}(\mathcal{K})$, it holds that

$$ \delta \in C^{\gamma^o(f(\pi, \delta, k))} \implies \langle \delta, k \rangle \in C^{\gamma(\pi)}. $$

*Proof Sketch.* We begin by recalling that $\mathcal{ST}(\mathcal{K})$ denotes all concept terms, including their subterms, occurring inside $\mathcal{K}$. By induction, we show that if $\delta$ belongs to $C^{\gamma^o(f(\pi, \delta, k))}$, then $\langle \delta, k \rangle$ belongs to $C^{\gamma(\pi)}$. We will focus on presenting the most interesting cases.

**Base case A:** By Definition 3, $A^{\gamma(\pi)} = \{\langle \delta, k \rangle \mid \delta \in A^{\gamma^o(f(\pi, \delta, k))}\}$

**Case $\neg A$:** By the semantics and the base case we have $\neg A^{\gamma(\pi)} = \{\langle \delta, k \rangle \mid \langle \delta, k \rangle \notin A^{\gamma(\pi)}\} = \{\langle \delta, k \rangle \mid \delta \notin A^{\gamma^o(f(\pi, \delta, k))}\} = \{\langle \delta, k \rangle \mid \delta \in \neg A^{\gamma^o(f(\pi, \delta, k))}\}$

**Case $\exists R.C$:** We show that $\delta \in \exists R.C^{\gamma^o(f(\pi, \delta, k))} \implies \langle \delta, k \rangle \in \exists R.C^{\gamma(\pi)}$.

(1) Let $f(\pi, \delta, k) = \pi'$ and $g(\pi, \delta, k) = m$.

(2) Assume $\delta \in \exists R.C^{\gamma^o(\pi')}.$

(3) From (2) and the semantics, there is some $\epsilon$ such that $\langle \delta, \epsilon \rangle \in R^{\gamma^o(\pi')}$ and $\epsilon \in C^{\gamma^o(\pi')}.$

(4) By (3) and Lemma 3 there is some $\ell \in \mathbb{N}$ such that $f(\pi, \ell, \ell) = \pi'$ and $g(\pi, \ell, \ell) = m$. Notice that $\pi' \in \Pi'$ since $f(\pi, \delta, k) = \pi'$.

(5) By (3), (4) and the inductive hypothesis, $\langle \epsilon, \ell \rangle \in C^{\gamma(\pi)}$.

(6) Notice that $f(\pi, \epsilon, \ell) = f(\pi, \delta, k)$ and $g(\pi, \epsilon, \ell) = g(\pi, \delta, k)$ from (1) and (4), and $\langle \delta, \epsilon \rangle \in R^{\gamma^o(f(\pi, \delta, k))}$, from (3), hence $\langle \langle \delta, k \rangle, \langle \epsilon, \ell \rangle \rangle \in R^{\gamma(\pi)}$ by Definition 3.

(7) From (5), (6) and the semantics we obtain $\langle \delta, k \rangle \in \exists R.C^{\gamma(\pi)}$ as desired.

**Case $\leqslant n.S.C$:** We show that $\delta \in \leqslant n.S.C^{\gamma^o(f(\pi, \delta, k))} \implies \langle \delta, k \rangle \in \leqslant n.S.C^{\gamma(\pi)}$.

(1) Assume $\delta \in \leqslant n.S.C^{\gamma^o(\pi')}$ and let $f(\pi, \delta, k) = \pi'$ and $g(\pi, \delta, k) = m$.

(2) Also, let $(\neg C)^\delta = \{ \epsilon \notin C^{\gamma^o(\pi')} | \langle \delta, \epsilon \rangle \in S^{\gamma^o(\pi')} \}$ and $C^\delta = \{ \epsilon \in C^{\gamma^o(\pi')} | \langle \delta, \epsilon \rangle \in S^{\gamma^o(\pi')} \}$.

(3) By (1) and the semantics we have $|\neg C)^\delta| \le n$.

(4) By Lemma 3, for each $\epsilon \in (\neg C)^\delta \cup C^\delta$ there is exactly one $\ell \in \mathbb{N}$ such that $f(\pi, \epsilon, \ell) = \pi'$ and $g(\pi, \epsilon, \ell) = m$.

(5) By Definition 3 and (4) we have that $\langle \langle \delta, k \rangle, \langle \epsilon, \ell \rangle \rangle \in S^{\gamma(\pi)}$, and therefore we have exactly $(\neg C)^\delta \cup C^\delta = \{ \langle \langle \delta, k \rangle, \langle \epsilon, \ell \rangle \rangle \in S^{\gamma(\pi)} \}$.

(6) From (4) and by the inductive hypothesis, for all $\epsilon \in C^\delta$ we have that $\langle \epsilon, \ell \rangle \in C^{\gamma(\pi)}$.

(7) Hence, from (5) and (6) we have that $|C^\delta| \le |\{ \langle \epsilon, \ell \rangle \in C^{\gamma(\pi)} | \langle \langle \delta, k \rangle, \langle \epsilon, \ell \rangle \rangle \in S^{\gamma(\pi)} \}|$.

(8) Finally, from (3), (5) and (7) it must be the case that $|\{ \langle \epsilon, \ell \rangle \notin C^{\gamma(\pi)} | \langle \langle \delta, k \rangle, \langle \epsilon, \ell \rangle \rangle \in S^{\gamma(\pi)} \}| \le |(\neg C)^\delta| \le n$, thus $\langle \delta, k \rangle \in \leqslant n.S.C^{\gamma(\pi)}$ as desired.

**Case $\diamond_s C$:** We show that $\delta \in \diamond_s C^{\gamma^o(f(\pi, \delta, k))} \implies \langle \delta, k \rangle \in \diamond_s C^{\gamma(\pi)}$.

**- Case 1** There is a named individual such that $\langle \delta, 0 \rangle = a^{\mathcal{D}}$.

(1) Assume $\delta \in \diamond_s C^{\gamma^o(f(\pi, \delta, 0))}$.

(2) By (1) and Definition 3, for $\pi^a_{s,C}$ we have $g(\pi^a_{s,C}, \delta, 0) = 0$ and $f(\pi^a_{s,C}, \delta, 0) = \pi''$ such that $\delta \in C^{\gamma^o(\pi'')}$.

(3) By (2) and the inductive hypothesis, we obtain that if $\delta \in C^{\gamma^o(f(\pi^a_{s,C}, \delta, 0))}$ then $\langle \delta, 0 \rangle \in C^{\gamma(\pi^a_{s,C})}$.

(4) By (3) and the semantics we obtain $\langle \delta, 0 \rangle \in \diamond_s C^{\gamma(\pi)}$ as desired.

**- Case 2** Otherwise.

(1) Assume $\delta \in \diamond_s C^{\gamma^o(f(\pi, \delta, k))}$ and let $i \in \{0, 1\}$ be such that $k + i$ is even.

(2) From (1) and the semantics, there is a $\pi' \in \sigma^o(s)$ such that $\delta \in C^{\gamma^o(\pi')}.$

(3) By Definition 3, for $\pi^i_{s,C}$ we have $\Pi' = \sigma^o(s)$.

(4) By Lemma 3, there is some $m$ and $\pi''$ such that $f(\pi^i_{s,C}, \delta, k) = \pi''$ and $g(\pi^i_{s,C}, \delta, k) = m$.

(5) By (1) and the construction of $\pi^i_{s,C}$ (Definition 3), $\pi''$ is assigned in such a way that $\delta \in C^{\gamma^o(\pi'')}$, and from (2) and (3) we know that such assignment is possible.

(6) By the inductive hypothesis, (4) and (5), we have that since $\delta \in C^{\gamma^o(f(\pi^i_{s,C}, \delta, k))}$ then $\langle \delta, k \rangle \in C^{\gamma(\pi^i_{s,C})}$.

(7) By (6) and the semantics, $\langle \delta, k \rangle \in \diamond_s C^{\gamma(\pi)}$ as desired. □
We now proceed to show that the construction of a *K*-pruning is possible for any given model.

**Lemma 5.** Let $\mathcal{K}$ be a $\mathcal{S}_{SHIQ}$ KB in normal form. For each model $\mathcal{D}^o = \langle \Delta^o, \Pi^o, \sigma^o, \gamma^o \rangle$ of $\mathcal{K}$ there is a $\mathcal{K}$-pruning $\mathcal{D} = \langle \Delta, \Pi, \sigma, \gamma \rangle$ of $\mathcal{D}^o$.

*Proof.* Let $\mathcal{D}^o = \langle \Delta^o, \Pi^o, \sigma^o, \gamma^o \rangle$ be a model of $\mathcal{K}$. First, observe that from $\mathcal{D}^o$ we can construct $\mathcal{D} = \langle \Delta, \Pi, \sigma, \gamma \rangle$ such that $\Delta = \Delta^o \times \mathbb{N}$, $\Pi = \Pi_{\mathcal{K}}$, $a^\mathcal{D} = \langle a^{\mathcal{D}^o}, 0 \rangle$ for all $a \in \mathbb{N}_{\mathcal{I}}(\mathcal{K})$ and $\sigma(s') = \{\pi_s, \pi_{s,C}^o, \pi_{s,C}^{1}, \pi_{s,C}^a \in \Pi_{\mathcal{K}} \mid s' \in s^{\mathcal{K}}, s \in \mathbb{N}_{\mathcal{S}}\}$.

It is left to establish the interpretation of concepts and roles for all precisifications in $\Pi$, for which we must be able to define the functions $f$ and $g$ as per Definition 3.

For any $\pi_s \in \Pi$ or $\pi_{s,C}^a \in \Pi$, there must be some $\pi \in \Pi^o$ with $\pi \in \sigma^o(s)$ to pick, which is always the case because by the semantics standpoints are non-empty. Moreover, in case $\mathcal{D}^o \models \Diamond_s(C(a))$, we must pick $\pi$ such that it also satisfies $a^{\mathcal{D}^o} \in C^{\gamma^o(\pi)}$. Again by the semantics if $\mathcal{D}^o \models \Diamond_s(C(a))$ then there is some $\pi \in \sigma^o(s)$ such that $\mathcal{D}^o, \pi \models C(a)$ and thus $a^{\mathcal{D}^o} \in C^{\gamma^o(\pi)}$ as required.

For $\pi_{s,C}^i$ with $i \in \{0,1\}$, we let $\Pi' = \sigma^o(s)$, which by the semantics is nonempty. When we assign the values of $f$ and $g$ for some $\delta$, we require a tuple that is not in $\{\langle f(\pi_{s,C}^i, \delta, \ell), g(\pi_{s,C}^i, \delta, \ell) \rangle \mid \ell < k\}$. Moreover, if $\delta \in (\Diamond_s C)^{\mathcal{D}^o}$ and $k$ is such that $k + i$ even, we also require that the assigned tuple $\langle \pi, m \rangle$ satisfies $\delta \in C^{\gamma^o(\pi)}$. But we know by the semantics that if $\delta \in (\Diamond_s C)^{\mathcal{D}^o}$ then there is at least some $\pi \in \sigma^o(s)$ such that $\delta \in C^{\gamma^o(\pi)}$. Then, let $m$ be the largest number such that $\langle \pi, m-1 \rangle \in \{\langle f(\pi_{s,C}^i, \delta, \ell), g(\pi_{s,C}^i, \delta, \ell) \rangle \mid \ell < k\}$ for $f(\pi_{s,C}^i, \delta, \ell) = \pi$ or 0 if the set is empty. Then, the tuple $\langle \pi, m \rangle$ could be chosen. With $f$ and $g$ guaranteed to be definable as specified in Definition 3, we can then complete the construction setting $A^{\gamma(\pi)} = \{\langle \delta, k \rangle \mid \delta \in A^{\gamma^o(f(\pi, \delta, k))}\}$ and $R^{\gamma(\pi)}$ to contain every pair $\langle\langle \delta, k \rangle, \langle \epsilon, \ell \rangle\rangle \in \Delta \times \Delta$ for which $f(\pi, \delta, k) = f(\pi, \epsilon, \ell)$ and $g(\pi, \delta, k) = g(\pi, \epsilon, \ell)$ and $\langle \delta, \epsilon \rangle \in R^{\gamma^o(f(\pi, \delta, k))}$ as required. $\square$

Finally, we show that if $\mathcal{D}^o$ was a model of $\mathcal{K}$ then the constructed pruning $\mathcal{D}$ is also a model.

**Lemma 6.** Let $\mathcal{K}$ be a $\mathcal{S}_{SHIQ}$ KB in normal form and let $\mathcal{D}^o = \langle \Delta^o, \Pi^o, \sigma^o, \gamma^o \rangle$ be a model of $\mathcal{K}$. If a structure $\mathcal{D} = \langle \Delta, \Pi, \sigma, \gamma \rangle$ is a $\mathcal{K}$-pruning of $\mathcal{D}^o$, then $\mathcal{D}$ is a model of $\mathcal{K}$.

*Proof Sketch.* Assume that $\mathcal{D}^o$ is a model of $\mathcal{K}$ and recall that $\mathcal{D}$ is also a model $\mathcal{K}$ iff it satisfies every statement in $\mathcal{K}$. Statements in $\mathcal{K}$ can be sharpening statements or modalised axioms $\Box_s \xi$. We focus on presenting some of the most interesting cases of the latter.

First, recall that $\mathcal{D} \models \Box_s \xi$ iff for all $\pi \in \sigma(s)$ we have $\mathcal{D}, \pi \models \xi$. In what follows, we show (for some axiom types) that if we have $\mathcal{D}^o, \pi^o \models \xi$ for all $\pi^o \in \sigma^o(s)$, then $\mathcal{D}, \pi \models \xi$ for all $\pi \in \sigma(s)$.

**Case** $\top \sqsubseteq C$. Let $\Pi' = \{f(\pi, \epsilon, \ell) \mid \epsilon \in \Delta^o, \ell \in \mathbb{N}\}$ and $\pi \in \sigma(s)$, noticing that $\Pi' \subseteq \sigma^o(s)$ by Definition 3.

(1) By assumption, we have $\mathcal{D}^o, \pi^o \models \top \sqsubseteq C$ for all $\pi^o \in \sigma^o(s)$, thus $\delta \in C^{\gamma^o(\pi^o)}$ for all $\delta \in \Delta^o$.

(2) By Lemma 3, for each $\pi$ and $\langle \delta, k \rangle$ there is some $m$ such that $f(\pi, \delta, k) = \pi^o$ with $\pi^o \in \Pi'$ and $g(\pi, \delta, k) = m$.

(3) From (1), (2) and Lemma 4, we have that since $\delta \in C^{\gamma^o(f(\pi, \delta, k))}$, then $\langle \delta, k \rangle \in C^{\gamma(\pi)}$.

(4) Thus, from (3) we obtain that $\mathcal{D}, \pi \models \top \sqsubseteq C$ as desired. **Case** $S \sqsubseteq R$. Let $\Pi' = \{f(\pi, \epsilon, \ell) \mid \epsilon \in \Delta^o, \ell \in \mathbb{N}\}$ and $\pi \in \sigma(s)$, noticing that $\Pi' \subseteq \sigma^o(s)$ by Definition 3.

(1) By assumption we have $\mathcal{D}^o, \pi^o \models S \sqsubseteq R$ for all $\pi^o \in \sigma^o(s)$, thus if $\langle \delta, \epsilon \rangle \in S^{\gamma^o(\pi^o)}$ then $\langle \delta, \epsilon \rangle \in R^{\gamma^o(\pi^o)}$ for all $\delta, \epsilon \in \Delta^o$.

(2) Assume $\langle\langle \delta, k \rangle, \langle \epsilon, \ell \rangle\rangle \in S^{\gamma(\pi)}$.

(3) Then, from (2) and Definition 3, we obtain $f(\pi, \delta, k) = f(\pi, \epsilon, \ell)$, $g(\pi, \delta, k) = g(\pi, \epsilon, \ell)$ and $\langle \delta, \epsilon \rangle \in S^{\gamma^o(f(\pi, \delta, k))}$.

(4) From (1) and (3) we have that $\langle \delta, \epsilon \rangle \in R^{\gamma^o(f(\pi, \delta, k))}$.

(5) From (4) and Definition 3 we have $\langle\langle \delta, k \rangle, \langle \epsilon, \ell \rangle\rangle \in R^{\gamma(\pi)}$ and thus $\mathcal{D}, \pi \models S \sqsubseteq R$ as desired.

**Case** $C(a)$. Let $\Pi' = \{f(\pi, \epsilon, \ell) \mid \epsilon \in \Delta^o, \ell \in \mathbb{N}\}$, $\pi \in \sigma(s)$ and $\delta = a^{\mathcal{D}^o}$, noticing that $\Pi' \subseteq \sigma^o(s)$ by Definition 3.

(1) By assumption we have $\mathcal{D}^o, \pi^o \models C(a)$ for all $\pi^o \in \sigma^o(s)$, thus $\delta \in C^{\gamma^o(\pi^o)}$.

(2) By Definition 3 we have $\langle \delta, 0 \rangle = a^{\mathcal{D}}$.

(3) By Definition 3 and Lemma 3, there is some $\pi^o \in \Pi'$ such that $f(\pi, \delta, 0) = \pi^o$ and $g(\pi, \delta, 0) = 0$.

(4) From (1), (3) and Lemma 4, we have that since $\delta \in C^{\gamma^o(f(\pi, \delta, 0))}$, then $\langle \delta, 0 \rangle \in C^{\gamma(\pi)}$.

(5) Last, from (2) and (4) we have $\mathcal{D}, \pi \models C(a)$ as desired.

So far we have shown that $\mathcal{D}$ is a model of $\mathcal{K}$, thus it remains to show that it is tidy. It is clear from Definition 2 and Definition 3 that $\Pi = \Pi_{\mathcal{K}}$, therefore it consists of a precisification $\pi_s \in \sigma(s)$ for all $s \in \mathbb{N}_{\mathcal{S}}(\mathcal{K})$, a precisification $\pi_{s,C}^a \in \sigma(s)$ for all $\Diamond_s C \in ST(\mathcal{K})$ and $a \in \mathbb{N}_{\mathcal{I}}(\mathcal{K})$ and two precisifications $\pi_{s,C}^o, \pi_{s,C}^{1} \in \sigma(s)$ for all $\Diamond_s C \in ST(\mathcal{K})$. Hence, $\mathcal{D}$ is a tidy model as required. $\square$

With all the lemmas in place, we are in a position to establish the main theorem.

**Theorem 7.** Any satisfiable $\mathcal{S}_{SHIQ}$ knowledge base in negation normal form has a tidy model.

*Proof.* Let $\mathcal{K}$ be a $\mathcal{S}_{SHIQ}$ knowledge base in negation normal form. If $\mathcal{K}$ is satisfiable then it has a model $\mathcal{D}^o$. By Lemma 5, then there is a $\mathcal{K}$-pruning $\mathcal{D}$ of $\mathcal{D}^o$, which by Lemma 6 is a tidy model of $\mathcal{K}$ as desired. $\square$

## 4 Translation from $\mathcal{S}_{SHIQ}$ to SHIQ

The fact that in $\mathcal{S}_{SHIQ}$ satisfiability coincides with satisfiability in a tidy model, which has a polynomially bounded number of precisifications, allows us to develop a polytime satisfiability-preserving translation from $\mathcal{S}_{SHIQ}$ to SHIQ knowledge bases. The underlying idea, which has been introduced earlier for the more general setting of first-order standpoint logic (Gómez Álvarez, Rudolph, and Strass 2022), is to “simulate” the $n$ precisifications of the considered structure by means of a plain DL interpretation with the same domain, but the vocabulary of concepts and roles
copied n-fold. Then, for instance, the fact that the element $\delta$ carries the concept A in the kth precisification of the DL standpoint structure would be encoded in the corresponding DL interpretation by $\delta$ carrying the kth copy of A.

We now assume a given $\mathbb{S}_{SHIQ}$ knowledge base $\mathcal{K}$ in NNF, and provide the formal definition of the translation. To this end, we fix $\Pi_{\mathcal{K}}$ as before and, for any $s \in \mathbf{N}_S$ let $\Pi_{\mathcal{K}}^s$ denote the subset $\{\pi_t, \pi_{t,C}^0, \pi_{t,C}^1, \pi_{t,C}^a \in \Pi_{\mathcal{K}} | s \in t^{\mathcal{K}}\}$. Our translation's vocabulary consists of all individual names inside $\mathcal{K}$, plus, for each $\pi \in \Pi_{\mathcal{K}}$, the following symbols:

* a concept name $A^\pi$ for each $A \in \mathbf{N}_C(\mathcal{K})$;

* a simple role name $S^\pi$ for each $S \in \mathbf{N}_R^s(\mathcal{K})$;

* a non-simple role name $R^\pi$ for each $R \in \mathbf{N}_R^{ns}(\mathcal{K})$;

* a concept name $A_C^\pi$ for each $\odot_S C$ occurring in $\mathcal{K}$;

We first inductively specify a function trans, taking some $\pi \in \Pi_{\mathcal{K}}$ and a $\mathbb{S}_{SHIQ}$ concept term $C$ in NNF as input and producing a $SHIQ$ concept term:

$$
\begin{align*}
\text{trans}(\pi, \top) &= \top \\
\text{trans}(\pi, \bot) &= \bot \\
\text{trans}(\pi, A) &= A^\pi \\
\text{trans}(\pi, \neg A) &= \neg A^\pi \\
\text{trans}(\pi, C \sqcap D) &= \text{trans}(\pi, C) \sqcap \text{trans}(\pi, D) \\
\text{trans}(\pi, C \sqcup D) &= \text{trans}(\pi, C) \sqcup \text{trans}(\pi, D) \\
\text{trans}(\pi, \exists R.C) &= \exists R^\pi.\text{trans}(\pi, C) \\
\text{trans}(\pi, \forall R.C) &= \forall R^\pi.\text{trans}(\pi, C) \\
\text{trans}(\pi, \leq n S.C) &= \leq n S^\pi.\text{trans}(\pi, C) \\
\text{trans}(\pi, \geq n S.C) &= \geq n S^\pi.\text{trans}(\pi, C) \\
\text{trans}(\pi, \Box_s C) &= \bigcap_{\pi' \in \Pi_{\mathcal{K}}^s} A_C^{\pi'} \\
\text{trans}(\pi, \Diamond_s C) &= \bigsqcup_{\pi' \in \Pi_{\mathcal{K}}^s} A_C^{\pi'}
\end{align*}
$$

Now, we let $\text{Trans}(\mathcal{K})$ denote the $SHIQ$ knowledge base consisting of the following axioms:

* $A_C^\pi \sqsubseteq \text{trans}(\pi, C)$ for every new concept name $A_C^\pi$ and $\pi \in \Pi_{\mathcal{K}}$.

* $\top \sqsubseteq \text{trans}(\pi, C)$ for each $\Box_s[\top \sqsubseteq C]$ from $\mathcal{K}$ and every $\pi \in \Pi_{\mathcal{K}}^s$.

* $S^\pi \sqsubseteq R^\pi$ for every $\Box_s[R^\pi]$ from $\mathcal{K}$ and every $\pi \in \Pi_{\mathcal{K}}^s$.

* $\text{Tra}(R^\pi)$ for every $\Box_s[\text{Tra}(R)]$ from $\mathcal{K}$ and every $\pi \in \Pi_{\mathcal{K}}^s$.

* $\text{trans}(\pi, C)(a)$ for each $\Box_s[C(a)]$ from $\mathcal{K}$ and every $\pi \in \Pi_{\mathcal{K}}^s$.

* $R^\pi(a, b)$ for each $\Box_s[R(a, b)]$ from $\mathcal{K}$ and every $\pi \in \Pi_{\mathcal{K}}^s$. With all definitions in place, we obtain the desired result.

**Theorem 8.** Given a $\mathbb{S}_{SHIQ}$ knowledge base $\mathcal{K}$ in NNF, the $SHIQ$ knowledge base $\text{Trans}(\mathcal{K})$

(i) is equisatisfiable with $\mathcal{K}$,

(ii) is of polynomial size wrt. $\mathcal{K}$, and

(iii) can be computed in polynomial time.

**Proof Sketch.** PTIME computability and the polynomial size of the result are straightforward consequences of the given definition, where we note that the introduction of the

concept names of the type $A_C^\pi$ is necessary to avoid an exponential blow-up that might otherwise occur through the nesting of modal operators.

Equisatisfiability will be shown by arguing that (a) every model of $\text{Trans}(\mathcal{K})$ gives rise to a model of $\mathcal{K}$ and (b) every tidy model of $\mathcal{K}$ gives rise to a model of $\text{Trans}(\mathcal{K})$ (which is sufficient in the light of Theorem 7).

For part (a), consider any model $\mathcal{I} = \langle \Delta, \mathcal{I} \rangle$ of $\text{Trans}(\mathcal{K})$. Then we can construct a model $\mathfrak{D}(\Delta, \Pi_{\mathcal{K}}, \sigma, \gamma)$ by letting $\sigma(s) = \Pi_{\mathcal{K}}^s$ as well as $a^{\gamma(\pi)} = a^{\mathcal{I}}$, $A^{\gamma(\pi)} = (A^\pi)^{\mathcal{I}}$, and $R^{\gamma(\pi)} = (R^\pi)^{\mathcal{I}}$. Then it can be readily checked that modelhood of $\mathcal{I}$ implies modelhood of $\mathfrak{D}$.

For part (b), consider a tidy model $\mathfrak{D}(\Delta, \Pi_{\mathcal{K}}, \sigma, \gamma)$ of $\mathcal{K}$. Then we can construct a model $\mathcal{I} = \langle \Delta, \mathcal{I} \rangle$ of $\text{Trans}(\mathcal{K})$ by letting $a^{\mathcal{I}} = a^{\mathfrak{D}}$, $(A^\pi)^{\mathcal{I}} = A^{\gamma(\pi)}$, $(R^\pi)^{\mathcal{I}} = R^{\gamma(\pi)}$, and $(A_C^\pi)^{\mathcal{I}} = C^{\gamma(\pi)}$. Then it can be checked that modelhood of $\mathfrak{D}$ implies modelhood of $\mathcal{I}$. $\square$

**Corollary 9.** Satisfiability and statement entailment in $\mathbb{S}_{SHIQ}$ are EXPTIME-complete.

*Proof.* The two reasoning tasks are PTIME-interreducible: By Theorem 2, statement entailment can be PTIME-reduced to satisfiability; the reduction in the other direction is trivial (one can check unsatisfiability by checking entailment of the statement $\Box_*[\top \sqsubseteq \bot]$). To show EXPTIME-membership of satisfiability, we first note that any given $\mathbb{S}_{SHIQ}$ knowledge base can be normalized in polynomial time with only polynomial blow-up (Lemma 1). This normalized knowledge base can then be translated into an equisatisfiable $SHIQ$ knowledge base, again in polytime and with only polynomial blowup (Theorem 8). Checking satisfiability of $SHIQ$ knowledge bases is known to be EXPTIME-complete (Toby 2001), which finishes the membership argument. Hardness follows from the fact that satisfiability of any $SHIQ$ knowledge base $\mathcal{K}$ coincides with satisfiability of the $\mathbb{S}_{SHIQ}$ knowledge base $\{\Diamond_* \wedge_{\xi \in \mathcal{K}} \xi\}$. $\square$

# 5 Nominals Destroy the Small Model Property

Nominals constitute an important mainstream modeling feature, present in many of today's ontology languages. For any individual name $a$, the nominal concept $\{a\}$ refers to the singleton set $\{a^\mathcal{I}\}$.

Alas, we will now show that, if we extended $\mathbb{S}_{SHIQ}$ by nominals, the “small model property” would cease to hold. In fact, it would be violated in the strongest way possible, as there exist satisfiable knowledge bases all of whose models have infinitely many precisifications. This is even the case in the absence of any role inclusion and transitivity statements and using only the universal standpoint $\ast$.

Consider the knowledge base with the following axioms:

$$ \Box_*[\{a\} \sqsubseteq \forall R^- \sqcup \bot] \qquad (12) $$

$$ \Box_*[\top \sqsubseteq \exists R.\top \sqcap \leq 1 R^- \sqcup \top \sqcap \leq 1 S^- \sqcup \top] \qquad (13) $$

$$ \Box_*[\top \sqsubseteq \Diamond_* \exists S.\{a\}] \qquad (14) $$

The first statement ensures that in any precisification, the individual named $a$ has no incoming $R$-relations. The
second statement stipulates that, in any precisification, every
individual has at least one outgoing *R*-relation, at most one
incoming *R*, and at most one incoming *S*. Note that the first
two statements together can only be satisfied in a standpoint
structure where $\Delta$ is an infinite set. The third statement en-
forces that for any element $\delta \in \Delta$ there is some precisifica-
tion in which $\delta$ is *S*-related to the individual *a*. On the other
hand, just as any other individual, *a* can have at most one in-
coming *S*-relation (per precisification). Consequently, each
of the infinitely many $\delta \in \Delta$ must be *S*-connected to *a* in a
distinct precisification, which forces $\Pi$ to be infinite.

Note that this finding does not rule out the possibility that
a polynomial equisatisfiable translation from Standpoint DL
with nominals to the standpoint-free version exists. It just
would have to be established based on different principles.

6 Conclusion and Future Work

In this paper, we introduced Standpoint SHIQ, a standpoint
DL that supports the tight modal integration of knowledge
bases of higher expressivity than in previously considered
Standpoint DL extensions. We subsequently established a
small model property for Standpoint SHIQ KBs, showing
that satisfiability coincides with the existence of tidy models,
which have a polynomially bounded number of precisifica-
tions. Exploiting this result, we provided a polytime equisat-
isfiable translation from S<sub>SHIQ</sub> to SHIQ, which not only
shows that the satisfiability of S<sub>SHIQ</sub> KBs is in EXPTIME,
but also provides us with a decision procedure for standard
reasoning tasks. Finally, we demonstrated that, while sup-
porting nominals would be desirable from an expressivity
point of view, this would destroy the small model property.

As avenues for future work, we see both practical and the-
oretical contributions. On the practical side, we plan to use
the translation described in Section 4, possibly with some
optimisations, to implement reasoning in S<sub>SHIQ</sub> harness-
ing existing OWL reasoners. Despite the PTIME transla-
tion, it remains to be seen if this approach performs well in
practical cases. An alternative would be to devise a quasi-
model-based tableau algorithm along the lines of (Wolter
and Zakharyaschev 1998; Gómez Álvarez, Rudolph, and
Strass 2023b), yet this would be a challenging endeavour
since it requires the implementation of a tailored reasoner.

On the theoretical side, it seems worthwhile to investig-
ate, which modelling features can be added to S<sub>SHIQ</sub> while
maintaining the small model property, which warrants the
translation-based approach. As per Section 5, nominals do
not qualify as “well-behaved” in this sense. With a similar
argument, it should be possible to disqualify the universal
role. On the other hand, we expect several popular DL mod-
elling features to be well-behaved, including the Self con-
struct, safe boolean role constructors, and regular RBoxes.

Finally, as discussed before, expressive DLs that do use
“non well-behaved” modelling features such as SHOIQ or
SROIQ might still allow for the complexity-neutral addi-
tion of standpoints on formal grounds other than the small
model property. We consider it an important question for
future research to find out if this is the case, or if the com-
plexity increases in such cases.

References

Baader, F., and Ohlbach, H. J. 1995. A multi-dimensional
terminological knowledge representation language. *Journal
of Applied Non-Classical Logics* 5(2):153–197.

Baader, F.; Horrocks, I.; Lutz, C.; and Sattler, U. 2017. *An
Introduction to Description Logic*. Cambridge University
Press.

Baader, F.; Küsters, R.; and Wolter, F. 2003. Extensions to description logics. In Baader, F.; Calvanese, D.; McGuinness, D. L.; Nardi, D.; and Patel-Schneider, P. F., eds., *The Description Logic Handbook: Theory, Implementation, and Applications*. Cambridge University Press. 219–261.

Bao, J.; Calvanese, D.; Grau, B. C.; Dzbor, M.; Fokoue, A.; Golbreich, C.; Hawke, S.; Herman, I.; Hoekstra, R.; Horrocks, I.; Kendall, E.; Krötzsch, M.; Lutz, C.; McGuinness, D. L.; Motik, B.; Pan, J.; Parsia, B.; Patel-Schneider, P. F.; Rudolph, S.; Ruttenberg, A.; Sattler, U.; Schneider, M.; Smith, M.; Wallace, E.; Wu, Z.; and Zimmermann, A. 2009. OWL 2 Web Ontology Language: Document Overview. W3C Recommendation. http://www.w3.org/TR/owl2-overview/. Accessed: 2023-01-01.

Borgida, A., and Serafini, L. 2003. Distributed Descrip-
tion Logics: Assimilating information from peer sources.
*Journal on Data Semantics* 2800:153–184.

Bouquet, P.; Giunchiglia, F.; van Harmelen, F.; Serafini, L.; and Stuckenschmidt, H. 2003. C-OWL: contextualizing ontologies. In Fensel, D.; Sycara, K. P.; and Mylopoulos, J., eds., *Proceedings of the 2nd International Semantic Web Conference*, volume 2870 of LNCS, 164–179. Springer.

Bozzato, L.; Eiter, T.; and Serafini, L. 2018. Enhancing
context knowledge repositories with justifiable exceptions.
*Artificial Intelligence* 257:72–126.

Donnelly, K. 2006. SNOMED-CT: The advanced terminol-
ogy and coding system for eHealth. *Studies in health tech-
nology and informatics* 121:279.

Gómez Álvarez, L., and Rudolph, S. 2021. Standpoint logic: Multi-perspective knowledge representation. In Neuhaus, F., and Brodaric, B., eds., *Proceedings of the 12th International Conference on Formal Ontology in Information Systems*, volume 344 of *FAIA*, 3–17. IOS Press.

Gómez Álvarez, L.; Rudolph, S.; and Strass, H. 2022. How to Agree to Disagree: Managing Ontological Perspectives using Standpoint Logic. In Sattler, U.; Hogan, A.; Keet, C. M.; Presutti, V.; Almeida, J. P. A.; Takeda, H.; Monnin, P.; Pirrò, G.; and d’Amato, C., eds., *Proceedings of the 21st International Semantic Web Conference*, 125–141. Springer.

Gómez Álvarez, L.; Rudolph, S.; and Strass, H. 2023a. Pushing the boundaries of tractable multiperspective reasoning: A deduction calculus for standpoint EL+. In Marquis, P.; Son, T. C.; and Kern-Isberner, G., eds., *Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning*, 333–343. IJCAI Organization.

Gómez Álvarez, L.; Rudolph, S.; and Strass, H. 2023b. Tractable diversity: Scalable multiperspective ontology management via standpoint EL. In *Proceedings of the*
32nd International Joint Conference on Artificial Intelligence, 3258–3267. IJCAI Organization.

Klarman, S., and Gutiérrez-Basulto, V. 2013. Description logics of context. *Journal of Logic and Computation* 26(3):817–854.

Lutz, C.; Sturm, H.; Wolter, F.; and Zakharyaschev, M. 2002. A tableau decision algorithm for modalized ALC with constant domains. *Studia Logica* 72(2):199–232.

McCarthy, J., and Buvac, S. 1998. Formalizing context (expanded notes). *CSLI Lecture Notes* 81:13–50.

Mosurović, M. 1999. *On the complexity of description logics with modal operators*. PhD thesis, University of Belgrade. In Serbian.

Rudolph, S. 2011. Foundations of description logics. In Polleres, A.; d'Amato, C.; Arenas, M.; Handschuh, S.; Kroner, P.; Ossowski, S.; and Patel-Schneider, P. F., eds., *Lecture Notes of the 7th International Reasoning Web Summer School*, volume 6848 of LNCS, 76–136. Springer.

Serafini, L., and Homola, M. 2012. Contextualized knowledge repositories for the semantic web. *Journal of Web Semantics* 12-13:64–87.

Skolem, T. 1929. Über einige Grundlagenfragen der Mathematik. *Skrifter utgitt av det Norske Videnskaps-Akademi i Oslo, I. Matematisk-naturvidenskabelig Klasse* 7:1–49.

Tobies, S. 2001. *Complexity results and practical algorithms for logics in knowledge representation*. Ph.D. Dissertation, RWTH Aachen University, Germany.

Wolter, F., and Zakharyaschev, M. 1998. Satisfiability problem in description logics with modal operators. In Cohn, A. G.; Schubert, L. K.; and Shapiro, S. C., eds., *Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning*, 512–523. Morgan Kaufmann.

Wolter, F., and Zakharyaschev, M. 1999. Multi-dimensional description logics. In Dean, T., ed., *Proceedings of the 16th International Joint Conference on Artificial Intelligence, volume 1, 104–109*. Morgan Kaufmann.

Wolter, F., and Zakharyaschev, M. 2001. Decidable fragments of first-order modal logics. *Journal of Symbolic Logic* 66(3):1415–1438.