11institutetext: Computational Logic Group, Faculty of Computer Science, TU
Dresden, Germany
11email: {lucia.gomez_alvarez, sebastian.rudolph<EMAIL_ADDRESS>
# How to Agree to Disagree

Managing Ontological Perspectives using Standpoint Logic

Lucía Gómez Álvarez  0000-0002-2525-8839 Sebastian Rudolph
0000-0002-1609-2080 Hannes Strass  0000-0001-6180-6452

###### Abstract

The importance of taking individual, potentially conflicting perspectives into
account when dealing with knowledge has been widely recognised. Many existing
ontology management approaches fully merge knowledge perspectives, which may
require weakening in order to maintain consistency; others represent the
distinct views in an entirely detached way.

As an alternative, we propose _Standpoint Logic_ , a simple, yet versatile
multi-modal logic “add-on” for existing KR languages intended for the
integrated representation of domain knowledge relative to diverse, possibly
conflicting _standpoints_ , which can be hierarchically organised, combined,
and put in relation with each other.

Starting from the generic framework of _First-Order Standpoint Logic_ (FOSL),
we subsequently focus our attention on the fragment of _sentential_ formulas,
for which we provide a polytime translation into the standpoint-free version.
This result yields decidability and favourable complexities for a variety of
highly expressive decidable fragments of first-order logic. Using some
elaborate encoding tricks, we then establish a similar translation for the
very expressive description logic $\mathcal{SROIQ}b_{s}$ underlying the OWL 2
DL ontology language. By virtue of this result, existing highly optimised OWL
reasoners can be used to provide practical reasoning support for ontology
languages extended by standpoint modelling.

###### Keywords:

knowledge integration ontology alignment conflict management

##  1 Introduction

Artefacts of contemporary knowledge representation (ontologies, knowledge
bases, or knowledge graphs) serve as means to conceptualise specific domains,
with varying degrees of expressivity ranging from simple classifications and
database schemas to fully axiomatised theories. Inevitably, such
specifications reflect the individual points of view of their creators (be it
on a personal or an institutional level) along with other contextual aspects,
and they may also differ in modelling design decisions, such as the choice of
conceptual granularity or specific ways of axiomatising information. This
semantic heterogeneity is bound to pose significant challenges whenever the
interoperability of independently developed knowledge specifications is
required.

This paper proposes a way to address the interoperability challenge while at
the same time preserving the varying perspectives of the original sources.
This is particularly important in scenarios that require the simultaneous
consideration of multiple, potentially contradictory, viewpoints.

###### Example 1

A broad range of conceptualisations and definitions for the notion of _forest_
have been specified for different purposes, giving rise to diverging or even
contradictory statements regarding forest distributions. Consider a knowledge
integration scenario involving two sources adopting a _land cover_
$(\mathsf{LC})$ and a _land use_ $(\mathsf{LU})$ perspective on forestry.
$\mathsf{LC}$ characterises a _forest_ as a “forest ecosystem” with a minimum
area (F1) where a _forest ecosystem_ is specified as an ecosystem with a
certain ratio of tree canopy cover (F2). $\mathsf{LU}$ defines a forest with
regard to the purpose for which an area of land is put to use by humans, i.e.
a forest is a maximally connected area with “forest use” (F3).111“Forest use”
areas may qualify for logging and mining concessions as well as be further
classified into, e.g. agricultural or recreational land use.

Both sources $\mathsf{LC}$ and $\mathsf{LU}$ agree that forests subsume
broadleaf, needleleaf and tropical forests (F4), and they both adhere to the
Basic Formal Ontology ($\mathsf{BFO}$, [1]), an upper-level ontology that
formalises general terms, stipulating for instance that _land_ and _ecosystem_
are disjoint categories (F5). Using standard description logic notation and
providing “perspective annotations” by means of correspondingly labelled box
operators borrowed from multi-modal logic, the above setting might be
formalised as follows:

  1. (F1)

$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}[\small\mbox{\tt
Forest}\equiv\small\mbox{\tt ForestEcosystem}\sqcap\exists\small\mbox{\tt
hasLand}.\small\mbox{\tt Area}_{\geq 0.5\mathrm{ha}}]$

  2. (F2)

$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}[\small\mbox{\tt
ForestEcosystem}\equiv\small\mbox{\tt Ecosystem}\sqcap\small\mbox{\tt
TreeCanopy}_{\geq 20\%}]$

  3. (F3)

$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LU}}}[\small\mbox{\tt
Forest}\equiv\small\mbox{\tt ForestlandUse}\sqcap\small\mbox{\tt
MCON}]\mbox{$\ \wedge\
$}\mathop{\square}\nolimits_{\mathsf{*}}[\small\mbox{\tt
ForestlandUse}\sqsubseteq\small\mbox{\tt Land}]$

  4. (F4)

$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC\cup
LU}}}[(\small\mbox{\tt BroadleafForest}\sqcup\small\mbox{\tt
NeedleleafForest}\sqcup\small\mbox{\tt
TropicalForest})\sqsubseteq\small\mbox{\tt Forest}]$

  5. (F5)

$(\mathsf{LC}\preceq\mathsf{BFO})\mbox{$\ \wedge\
$}(\mathsf{LU}\preceq\mathsf{BFO})\mbox{$\ \wedge\
$}\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{BFO}}}[\small\mbox{\tt
Land}\sqcap\small\mbox{\tt Ecosystem}\sqsubseteq\bot]$

In the case of Example 1, _ecosystem_ and _land_ are disjoint categories
according to the overarching $\mathsf{BFO}$ (F5), yet forests are defined as
ecosystems according to $\mathsf{LC}$ (F1) and as lands according to
${\mathsf{LU}}$ (F3). These kinds of disagreements result in well-reported
challenges in the area of Ontology Integration [6, 21] and make ontology
merging a non-trivial task, often involving a certain knowledge loss or
weakening in order to avoid incoherence and inconsistency [22, 29]. In Example
1, to merge $\mathsf{LU}$ and $\mathsf{LC}$, there are two typical options to
resolve the issue: (Opt-Weak) one may give up on the disjointness axiom (F5),
or (Opt-Dup) one could duplicate all the conflicting predicates [20], in this
case not only Forest (into Forest_LC and Forest_LU), but also the forest
subclasses in (F4): BroadleafForest, NeedleleafForest and TropicalForest. In
contrast, we advocate a multi-perspective approach that can represent and
reason with many – possibly conflicting – standpoints, instead of focusing on
combining and merging different sources into a single conflict-free conceptual
model.

_Standpoint logic_ [8] is a formalism inspired by the theory of
supervaluationism [7] and rooted in modal logic that supports the coexistence
of multiple standpoints and the establishment of alignments between them, by
extending the base language with labelled modal operators. Propositions
$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}\phi$ and
$\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}\phi$ express
information relative to the _standpoint_ $\mathsf{LC}$ and read, respectively:
“according to $\mathsf{LC}$, it is _unequivocal/conceivable_ that $\phi$”. In
the semantics, standpoints are represented by sets of _precisifications_
,222Precisifications are analogous to the _worlds_ of frameworks with
possible-worlds semantics. such that
$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}\phi$ and
$\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}\phi$ hold if $\phi$
is true in all/some of the precisifications in $\mathsf{LC}$.

The logical statements (F1)–(F5), which formalise Example 1 by means of a
standpoint-enhanced description logic, are not inconsistent, so all axioms can
be jointly represented. Let us now illustrate the use of standpoint logic for
reasoning with the individual perspectives. First, assume the following
(globally agreed) facts about three instances, an ecosystem $e$, a parcel of
land $l$, and a city $c$:

  1. (F6)

$\small\mbox{\tt ForestEcosystem}(e)\qquad\small\mbox{\tt
hasLand}(e,l)\qquad\small\mbox{\tt ForestlandUse}(l)$

  2. (F7)

$\small\mbox{\tt Area}_{\geq 0.5\mathrm{ha}}(l)\qquad\small\mbox{\tt
MCON}(l)\qquad\small\mbox{\tt in}(l,\mathit{c})\qquad\small\mbox{\tt
City}(\mathit{c})$

It is clear from (F1) that according to $\mathsf{LC}$, $e$ is a forest,
written as
$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}[\small\mbox{\tt
Forest}(e)]$, since it is a forest ecosystem (F6) with an area larger than
$0.5\mathrm{ha}$ (F7). On the other hand, it is clear from (F3) that according
to $\mathsf{LU}$, $l$ is a forest,
$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LU}}}[\small\mbox{\tt
Forest}(l)]$, since it has a forest land use (F6) and it is a maximally
connected area (F7). More interestingly, we can also obtain _joint inferences_
: assuming the (generally accepted) background knowledge expressed by
$\small\mbox{\tt hasLand}\circ\small\mbox{\tt in}\sqsubseteq\small\mbox{\tt
in}$, we can infer

$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC\cup
LU}}}[(\small\mbox{\tt City}\sqcap\exists\small\mbox{\tt
in}^{-}.\small\mbox{\tt Forest})(\mathit{c})],$

which means that “according to both $\mathsf{LC}$ and $\mathsf{LU}$ there is
some forest in City $c$.” This holds for $\mathsf{LU}$ since $l$ is a forest
and is in $c$ (F7); and it holds for $\mathsf{LC}$ because $e$ is a forest in
the land $l$, which is in turn in $c$.

In contrast to the options of the ontology merging approach, using standpoint
logic prevents the multiplication (and corresponding “semantic detachment”) of
predicates from (Opt-Dup). It also avoids unintended consequences arising when
knowledge sources are weakened just enough to maintain satisfiability: In the
corresponding (Opt-Weak) scenario, after merging the knowlege sources of
$\mathsf{LU}$ and $\mathsf{LC}$ and removing (F5), we can consistently infer
$\small\mbox{\tt Forest}(e)$ from the standpoint-free versions of (F1), (F6)
and (F7) and $\small\mbox{\tt Forest}(l)$ from (F3), (F6) and (F7), similar to
the standpoint framework. But on top of that, reapplying (F1) and (F3) also
yields “$e$ is a forest, and its land $l$ is also a forest and an ecosystem,
and has some other associated land, bigger than $0.5\mathrm{ha}$” through the
following derivable assertions:

$\small\mbox{\tt Forest}(e)\ \ \ \small\mbox{\tt hasLand}(e,l)\ \ \
\small\mbox{\tt Forest}(l)\ \ \ \small\mbox{\tt ForestEcosystem}(l)\ \ \
\exists\small\mbox{\tt hasLand}.\small\mbox{\tt Area}_{\geq
0.5\mathrm{ha}}(l)$

This illustrates how, beyond the problem of inconsistency, naively merging
different models of a domain may lead to erroneous reasoning. In fact, other
non-clashing differences between the forest definitions (F1) and (F3) respond
to relevant nuances that relate to each standpoint and should also not be
naively merged. For instance, from the land cover perspective (F1), there is
no spatial connectedness requirement, since there are “mosaic forest
ecosystems” where the landscape displays forest patches that are sufficiently
close to constitute a single ecosystem. On the other hand, for $\mathsf{LU}$,
there is no minimum tree canopy (F3), since a temporarily cleared area still
has a “forest use”.

Standpoint logic preserves the independence of the perspectives and escapes
global inconsistency – without weakening the sources or duplicating entities –
because its model theory (cf. Section 2.1) requires consistency only within
standpoints and precisifications. Notwithstanding, it allows for the
specification of structures of standpoints and alignments between them.
Natural reasoning tasks over such multi-standpoint specifications include
gathering unequivocal or undisputed knowledge, determining knowledge that is
relative to a standpoint or a set of them, and contrasting the knowledge that
can be inferred from different standpoints.

Let us get an idea of the expressivity of the proposed logic. In spite of its
simple syntax, the language is remarkably versatile; it allows for specifying
knowledge relative (a) to a standpoint, e.g. (F1), (b) to the global
standpoint, denoted by $*$, e.g. (F3), and (c) to set-theoretic combinations
of standpoints, e.g. (F4). Additional language features can be defined in
terms of the former: $\mathcal{I}_{\scaleobj{0.8}{\mathsf{\mathsf{LC}}}}\phi$,
which means that, “according to $\mathsf{LC}$, it is inherently
_indeterminate_ whether $\phi$” can be defined by
$\mathcal{I}_{\scaleobj{0.8}{\mathsf{\mathsf{LC}}}}\phi\mathrel{\,:=\,}\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}\mkern-1.0mu\phi\mbox{$\
\wedge\
$}\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}\mkern-2.0mu\neg\phi$.
The _sharper_ operator $\preceq$ is used to establish hierarchies of
standpoints and constraints on the structure of precisifications, e.g. (F5),
and can be defined via
$\hbox{$\mathsf{s}$}_{1}\preceq\hbox{$\mathsf{s}$}_{2}\mathrel{\,:=\,}\mathop{\square}\nolimits_{\mathsf{\hbox{$\mathsf{s}$}_{1}\backslash\hbox{$\mathsf{s}$}_{2}}}[\top\sqsubseteq\bot]$.
Intuitively, $\hbox{$\mathsf{s}$}_{1}\preceq\hbox{$\mathsf{s}$}_{2}$ expresses
that standpoint $\hbox{$\mathsf{s}$}_{1}$ inherits the propositions of
$\hbox{$\mathsf{s}$}_{2}$, by virtue of
“$\hbox{$\mathsf{s}$}_{1}\subseteq\hbox{$\mathsf{s}$}_{2}$” holding for the
corresponding sets of precisifications. This type of statement comes handy to
“import” background knowledge from some ontology, such as the foundational
ontology BFO in our example. In combination, these modelling features allow
for expressing further constraints useful for knowledge integration scenarios,
e.g.,

  1. (F8)

$\mathsf{*}\preceq(\mathsf{LC\cup LU})\ \mbox{$\ \wedge\ $}\
\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}\mkern-1.0mu[\top{\,\sqsubseteq\,}\top]\
\wedge\
\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{LU}}}\mkern-1.0mu[\top{\,\sqsubseteq\,}\top],$

where the first conjunct allows us to specify that no interpretations beyond
the standpoints of interest are under consideration, by stating that the
universal standpoint is a subset of the union of $\mathsf{LC}$ and
$\mathsf{LU}$. The other two conjuncts enforce the non-emptiness of the
standpoints of interest, $\mathsf{LC}$ and $\mathsf{LU}$, ensuring that each
standpoint by itself is coherent. To illustrate a use case, consider the
statement $\mathop{\lozenge}\nolimits_{\mathsf{*}}[\small\mbox{\tt
Forest}(f)\mbox{$\ \wedge\ $}\mbox{$\neg$}\small\mbox{\tt MCON}(f)]$,
expressing that it is conceivable that $f$ is a non-spatially-connected
forest. From this, we can infer together with (F8) and the unfulfilled
requirement of connectedness of $\mathsf{LU}$ (F3), that $f$ must be
conceivable for $\mathsf{LC}$ instead, and thus $f$ must be a forest ecosystem
(F1):
$\mathop{\lozenge}\nolimits_{\scaleobj{0.8}{\mathsf{\mathsf{LC}}}}[\small\mbox{\tt
ForestEcosystem}(f)\mbox{$\ \wedge\ $}(\exists\hskip 1.0pt\small\mbox{\tt
hasLand}.\small\mbox{\tt Area}_{\geq 0.5\mathrm{ha}})(f)]$

Gómez Álvarez and Rudolph [8] have introduced the standpoint framework over a
propositional base logic. While they showed favourable complexity results
(standard reasoning tasks are NP-complete just like for plain propositional
logic), the framework is not expressive enough for knowledge integration
scenarios employing contemporary ontology languages. In this paper, we widen
the scope by (1) introducing the very general framework of _first-order_
standpoint logic (FOSL) and (2) allowing for more modelling flexibility on the
side of standpoint descriptions by introducing support for set-theoretical
combinations of standpoints (Section 2). We provide the syntax and semantics
of this generic framework, before focusing on the identification of FOSL
fragments with beneficial computational properties. To this end, we define the
_sentential_ fragment, which imposes restrictions on the use of standpoint
operators and guarantees a small model property (Section 2.2). Tailored to
this case, we introduce a polynomial satisfiability-preserving translation
(Section 2.3) that does not affect membership in diverse decidable fragments
of FO. This allows us to immediately obtain decidability and tight complexity
bounds for the standpoint versions of diverse FO fragments (e.g. the
2-variable counting fragment, the guarded negation fragment and the triguarded
fragment) (Section 3). In addition, it provides a way to leverage off-the-
shelf reasoners for practical reasoning in standpoint versions of popular
ontology languages. We demonstrate this by extending our results to a
standpoint logic based on the description logic $\mathcal{SROIQ}b_{s}$, a
semantic fragment of FO closely related to the OWL 2 DL ontology language
(Section 4). Finally, we revisit our example to discuss and illustrate
properties of our proposal (Section 5). An extended version of this paper
including proofs is available as a technical report [31].

##  2 First-Order Standpoint Logic

In this section we introduce the general framework of first order standpoint
logic (FOSL) as well as its sentential fragment and establish model theoretic
and computational properties. In addition to establishing various worthwhile
decidability and complexity results, this approach also provides us with a
clearer view on the underlying principles of our arguments, while avoiding
distractions brought about by some peculiarities of expressive ontology
languages, which we will address separately later on.

###  2.1 FOSL Syntax and Semantics

###### Definition 1

The syntax of first-order standpoint logic
(${\mathbb{S}_{\scaleobj{0.85}{\mathrm{FO}}}}$) is based on a _signature_
$\langle\mathcal{P},\mathcal{C},\mathcal{S}\rangle$, consisting of _predicate
symbols_ $\mathcal{P}$ (each associated with an arity $n\in\mathbb{N}$),
_constant symbols_ $\mathcal{C}$ and _standpoint symbols_ $\mathcal{S}$,
usually denoted with $\mathsf{s},\mathsf{s}^{\prime}$, as well as a set
$\mathcal{V}$ of _variables_ , typically denoted with $x,y,\ldots$ (possibly
annotated). These four sets are assumed to be countably infinite and pairwise
disjoint. The set $\mathcal{T}$ of _terms_ contains all constants and
variables, that is, $\mathcal{T}=\mathcal{C}\cup\mathcal{V}$.

The set $\mathcal{E}_{\mathcal{S}}$ of _standpoint expressions_ is defined as
follows:

$\mathsf{e}_{1},\mathsf{e}_{2}\mathrel{::=}*\mid\mathsf{s}\mid\mathsf{e}_{1}\cup\mathsf{e}_{2}\mid\mathsf{e}_{1}\cap\mathsf{e}_{2}\mid\mathsf{e}_{1}\setminus\mathsf{e}_{2}$

The set ${\mathbb{S}_{\scaleobj{0.85}{\mathrm{FO}}}}$ of FOSL _formulas_ is
then given by

$\phi,\psi\mathrel{::=}\small\mbox{\tt
P}(t_{1},\ldots,t_{k})\mid\neg\phi\mid\phi\mathrel{\wedge}\psi\mid\forall
x\phi\mid\mathop{\square}\nolimits_{\mathsf{e}}\phi,$

where $\small\mbox{\tt P}\in\mathcal{P}$ is an $k$-ary predicate symbol,
$t_{1},\dots,t_{k}\in\mathcal{T}$ are terms, $x\in\mathcal{V}$, and
$\mathsf{e}\in\mathcal{E}_{\mathcal{S}}$.

For a formula $\phi$, we denote the set of all of its subformulas by
$\mathit{Sub}(\phi)$. The _size_ of a formula is
$|\phi|\mathrel{\,:=\,}|\mathit{Sub}(\phi)|$. The connectives and operators
$\mathbf{t}$, $\mathbf{f}$, $\phi\mathrel{\vee}\psi$, $\phi\rightarrow\psi$,
$\exists x\phi$, and $\mathop{\lozenge}\nolimits_{\mathsf{\mathsf{e}}}\phi$
are introduced as syntactic macros as usual. As further useful syntactic
sugar, we introduce _sharpening_ statements
$\mathsf{e}_{1}\preceq\mathsf{e}_{2}$ to denote
$\mathop{\square}\nolimits_{\mathsf{\mathsf{e}_{1}\backslash\mathsf{e}_{2}}}\mathbf{f}$,
the _indeterminacy operator_ via
$\mathcal{I}_{\scaleobj{0.8}{\mathsf{\mathsf{e}}}}\phi:=\mathop{\lozenge}\nolimits_{\mathsf{\mathsf{e}}}\phi\mbox{$\
\wedge\ $}\mathop{\lozenge}\nolimits_{\mathsf{\mathsf{e}}}\mbox{$\neg$}\phi$,
and the _determinacy operator_ via
$\mathcal{D}_{\scaleobj{0.8}{\mathsf{\mathsf{e}}}}\phi:=\neg\mathcal{I}_{\scaleobj{0.8}{\mathsf{\mathsf{e}}}}\phi$.

###### Definition 2

Given a signature $\langle\mathcal{P},\mathcal{C},\mathcal{S}\rangle$, a
_first-order standpoint structure_ $\mathfrak{M}$ is a tuple
$\langle\Delta,\Pi,\sigma,\gamma\rangle$ where:

  * •

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

  * •

$\Pi$ is the non-empty set of _precisifications_ ;

  * •

$\sigma$ is a function mapping each standpoint symbol from $\mathcal{S}$ to a
set of precisifications (i.e., a subset of $\Pi$);

  * •

$\gamma$ is a function mapping each precisification from $\Pi$ to an ordinary
first-order structure $\mathcal{I}$ over the domain $\Delta$, whose
interpretation function $\cdot^{\mathcal{I}}$ maps:

    * –

each predicate symbol $\small\mbox{\tt P}{\,\in\,}\mathcal{P}$ of arity $k$ to
an $k$-ary relation $\small\mbox{\tt
P}^{\mathcal{I}}{\,\subseteq\,}\Delta^{k}$,

    * –

each constant symbol $a{\,\in\,}\mathcal{C}$ to a domain element
$a^{\mathcal{I}}{\,\in\,}\Delta$.

Moreover, for any two $\pi_{1},\pi_{2}\in\Pi$ and every $a\in\mathcal{C}$ we
require $a^{\gamma(\pi_{1})}=a^{\gamma(\pi_{2})}$.

Note that all first-order structures in all precisifications implicitly share
the same interpretation domain $\Delta$ given by the overarching first-order
standpoint structure $\mathfrak{M}$, that is, we adopt the _constant domain
assumption_.333This is not a substantial restriction, as other variants –
expanding domains, varying domains – can be emulated using constant domains
[30, Theorem 6]. Moreover, the last condition of Definition 2 also enforces
_rigid constants_ , that is, constants denote the same objects in different
standpoints (while clearly their properties could differ). For any predicate P
of arity $0$, the empty Cartesian product $\Delta^{0}$ is simply a one-element
set $\\{()\\}$ (whose only element is the unique zero-tuple $()$ of elements
from $\Delta$), so $\small\mbox{\tt P}^{\mathcal{I}}$ is either $\emptyset$
(interpreted as false) or $\Delta^{0}$ (interpreted as true), thus adequately
recovering the truth value assignments of the propositional atom P.

###### Definition 3

Let $\mathfrak{M}=\mbox{$\langle\Delta,\Pi,\sigma,\gamma\rangle$}$ be a first-
order standpoint structure for the signature
$\langle\mathcal{P},\mathcal{C},\mathcal{S}\rangle$ and $\mathcal{V}$ be a set
of variables. A _variable assignment_ is a function $v:\mathcal{V}\to\Delta$
mapping variables to domain elements. Given a variable assignment $v$, we
denote by $v_{\left\\{x\mapsto\delta\right\\}}$ the function mapping $x$ to
$\delta\in\Delta$ and any other variable $y$ to $v(y)$.

An interpretation function $\cdot^{\mathcal{I}}$ and a variable assignment
specify how to interpret terms by domain elements: We let
$t^{\mathcal{I},v}=v(x)$ if $t=x\in\mathcal{V}$, and
$t^{\mathcal{I},v}=a^{\mathcal{I}}$ if $t=a\in\mathcal{C}$.

To interpret standpoint expressions, we lift $\sigma$ from $\mathcal{S}$ to
all of $\mathcal{E}_{\mathcal{S}}$ by letting $\sigma(*)=\Pi$ and
$\sigma(\mathsf{e}_{1}\bowtie\mathsf{e}_{2})=\sigma(\mathsf{e}_{1})\bowtie\sigma(\mathsf{e}_{2})$
for ${\bowtie}\in\\{\cup,\cap,\setminus\\}$.

The satisfaction relation for formulas is defined in the usual way via
structural induction. In what follows, let $\pi\in\Pi$ and let
$v:\mathcal{V}\to\Delta$ be a variable assignment; we now establish the
definition of the satisfaction relation $\models$ for first-order standpoint
logic using pointed first-order standpoint structures:444We implicitly define
$\phi$ to be (globally) _satisfiable_ iff $\mathfrak{M}\models\phi$ for some
structure $\mathfrak{M}$. Local satisfiability (satisfiability in some
precisification) can be emulated via global satisfiability of
$\mathop{\lozenge}\nolimits_{\mathsf{*}}\mkern-2.0mu\phi$.

$\displaystyle\mathfrak{M},\\!\pi,\\!v\models\small\mbox{\tt
P}(t_{1},\ldots,t_{k})\\!\\!$ iff
$\displaystyle(t_{1}^{\gamma(\pi),v},\ldots,t_{k}^{\gamma(\pi),v})\in\small\mbox{\tt
P}^{\gamma(\pi)}$ $\displaystyle\mathfrak{M},\\!\pi,\\!v\models\neg\phi$ iff
$\displaystyle\mathfrak{M},\\!\pi,\\!v\not\models\phi$
$\displaystyle\mathfrak{M},\\!\pi,\\!v\models\phi\mathrel{\wedge}\psi$ iff
$\displaystyle\mathfrak{M},\\!\pi,\\!v\models\phi\text{ and
}\mathfrak{M},\pi,v\models\psi$
$\displaystyle\mathfrak{M},\\!\pi,\\!v\models\forall x\phi$ iff
$\displaystyle\mathfrak{M},\\!\pi,\\!v_{\left\\{x\mapsto\delta\right\\}}\models\phi\text{
for all }\delta{\,\in\,}\Delta$
$\displaystyle\mathfrak{M},\\!\pi,\\!v\models\mathop{\square}\nolimits_{\mathsf{\mathsf{e}}}\phi$
iff $\displaystyle\mathfrak{M},\\!\pi^{\prime}\\!,v\models\phi\text{ for all
}\pi^{\prime}\in\sigma(\mathsf{e})$
$\displaystyle\mathfrak{M},\\!\pi\models\phi$ iff
$\displaystyle\mathfrak{M},\\!\pi,\\!v\models\phi\text{ for all
}v:\mathcal{V}\to\Delta$ $\displaystyle\mathfrak{M}\models\phi$ iff
$\displaystyle\mathfrak{M},\\!\pi\models\phi\text{ for all }\pi\in\Pi$

As usual, $\mathfrak{M}$ is a _model_ for a formula $\phi$ iff
$\mathfrak{M}\models\phi$. As an aside, note that the modal-logic nature of
FOSL may become more evident upon realizing that an alternative definition of
its semantics via Kripke structures can be given (with
$\mathop{\square}\nolimits_{\mathsf{\mathsf{e}}}$ interpreted in the standard
way) by assigning every $\mathsf{e}\in\mathcal{E}_{\mathcal{S}}$ the
accessibility relation
$\\{(\pi,\pi^{\prime})\mid\pi,\pi^{\prime}\in\Pi,\pi^{\prime}\in\sigma(e)\\}$.

Later in this paper, we will consider cases where the number of
precisifications is fixed. Thus, we conclude this section by a corresponding
definition.

###### Definition 4

For a natural number $n\in\mathbb{N}$, a FOSL formula $\phi$ is _$n$
-satisfiable_ iff it has a model $\langle\Delta,\Pi,\sigma,\gamma\rangle$ with
$|\Pi|=n$.

###  2.2 Small Model Property of Sentential Formulas

One interesting aspect of standpoint logic is that its simplified Kripke
semantics brings about convenient model-theoretic properties that do not hold
for arbitrary (multi-)modal logics. For propositional standpoint logic, it is
known that standard reasoning tasks (such as checking satisfiability) are NP-
complete [8], in contrast to PSpace-completeness in related systems such as
K45n, KD45n and S5n. This result is in fact linked to a _small model property_
, according to which every satisfiable formula has a model with a “small”
number of precisifications. This beneficial property only holds in the single-
modal K45, KD45 and S5 [23] but applies to the multi-modal propositional
standpoint logic because of its stronger modal interaction. Fortunately, it
can also be shown to carry over to some fragments of FOSL and to the use of
standpoint expressions. In particular, in this section, we will show that if
we restrict the language to those formulas with no free variables in
subformulas of the form
$\mathop{\square}\nolimits_{\mathsf{e}}\mkern-1.0mu\phi$, then we can indeed
guarantee that every satisfiable FOSL formula has a model whose number of
precisifications is linear in the size of the formula.

###### Definition 5

Let $\phi$ be a formula of FOSL. We say that $\phi$ is _sentential_ iff for
all subformulas of $\phi$ of the form
$\mathop{\square}\nolimits_{\mathsf{e}}\mkern-1.0mu\psi$, all variables
occurring in $\psi$ are bound by a quantifier.

###### Theorem 2.1

A sentential FOSL formula $\phi$ is satisfiable iff it has a model with at
most $|\phi|$ precisifications. That is, for sentential FOSL, satisfiability
and $|\phi|$-satisfiability coincide.

###### Proof

The “if” direction holds trivially. For the “only if” direction, we consider
an arbitrary model
$\mathfrak{M}=\mbox{$\langle\Delta,\Pi,\sigma,\gamma\rangle$}$ of $\phi$, and
show that it can be “pruned” to obtain a small model
$\mathfrak{M}^{\prime}=\mbox{$\langle\Delta,\Pi_{\mathfrak{M},\phi},\sigma^{\prime},\gamma^{\prime}\rangle$}$
with $\mathfrak{M}^{\prime}\models\phi$.

First, we define a set of precisifications that will serve as witnesses for
the satisfaction of subformulas preceded by a diamond modality (that is, some
$\mathop{\square}\nolimits_{\mathsf{e}}$ in negative polarity).

To this end, let $\Pi_{\mathfrak{M},\phi}$ be a subset of $\Pi$ with the
following property: for each subformula
$\mathop{\square}\nolimits_{\mathsf{\mathsf{e}}}\psi\in\mathit{Sub}(\phi)$ not
satisfied in $\mathfrak{M}$ (i.e.,
$\mathfrak{M}\not\models\mathop{\square}\nolimits_{\mathsf{e}}\psi$),
$\Pi_{\mathfrak{M},\phi}$ contains one precisification $\pi\in\Pi$ for which
$\pi\in\sigma(\mathsf{e})$ and $\mathfrak{M},\pi\not\models\psi$ hold (note
that the existence of such a $\pi$ follows directly from the definition of
$\models$); should all
$\mathop{\square}\nolimits_{\mathsf{\mathsf{e}}}\psi\in\mathit{Sub}(\phi)$ be
satisfied in $\mathfrak{M}$, we put
$\Pi_{\mathfrak{M},\phi}=\left\\{\pi\right\\}$ for an arbitrary $\pi\in\Pi$.
The definition of $\mathfrak{M}^{\prime}$ then concludes by restricting
$\sigma$ and $\gamma$ to $\Pi_{\mathfrak{M},\phi}$, i.e., we let
$\sigma^{\prime}(s)=\sigma(s)\cap\Pi_{\mathfrak{M},\phi}$ for each
$s\in\mathcal{S}$ and $\gamma^{\prime}(\pi)=\gamma(\pi)$ for each
$\pi\in\Pi_{\mathfrak{M},\phi}$. An easy induction yields that, for any
$\mathsf{e}\in\mathcal{E}_{\mathcal{S}}$ and $\pi\in\Pi_{\mathfrak{M},\phi}$,
we get $\pi{\,\in\,}\sigma(\mathsf{e})$ iff
$\pi{\,\in\,}\sigma^{\prime}(\mathsf{e})$. This also implies
$\sigma^{\prime}(\mathsf{e}){\,\subseteq\,}\sigma(\mathsf{e})$. With this in
mind, another structural induction allows us to conclude
$\mathfrak{M}^{\prime}\models\phi$.

In the following, it will be convenient to assume that formulas are in
_standpoint standard normal form_ (SSNF), where no modal operator
$\mathop{\square}\nolimits_{\mathsf{e}}$ occurs inside the scope of another.
Any FOSL formula $\phi$ can be transformed into SSNF in polynomial time.

######  Definition 6 (Standpoint Standard Normal Form)

A first order standpoint logic formula $\phi$ is in _standpoint standard
normal form_ (SSNF) iff no modal operator
$\mathop{\square}\nolimits_{\mathsf{e}}$ occurs inside the scope of another.

###### Lemma 1

Each first-order standpoint logic formula $\phi$ can be transformed in
polynomial time into a formula in SSNF that is a conservative extension of
$\phi$.

Full formal details regarding the translation into SSNF can be found in
Appendix A. The transformation follows standard principles. For instance, the
formula $\mathop{\square}\nolimits_{\mathsf{e}}[\exists
x\mathop{\lozenge}\nolimits_{\mathsf{e}}[\small\mbox{\tt P}(x)]]$ is
transformed into $\mathop{\square}\nolimits_{\mathsf{e}}[\exists
x\,\small\mbox{\tt Q}(x)]\wedge\forall x\big{(}\small\mbox{\tt
Q}(x)\to\mathop{\lozenge}\nolimits_{\mathsf{e}}[\small\mbox{\tt
P}(x)]\big{)}$, where Q is a fresh, hitherto unused predicate symbol. We will
not delve into conservative extensions; for us it is sufficient that this
transformation is satisfiability-preserving. For the remainder of this paper
we assume that $\phi$ is in SSNF.

###  2.3 Translation to Plain First-Order Logic

In this section, we present a translation $\mathrm{Trans}_{n}$ mapping any
FOSL formula $\phi$ to a plain FO formula $\mathrm{Trans}_{n}(\phi)$ such that
$n$-satisfiability of $\phi$ coincides with satisfiability of
$\mathrm{Trans}_{n}(\phi)$. The translation will make explicit use of a fixed,
finite set $\Pi_{n}$ of precisifications with $|\Pi_{n}|=n$.

Our translation will map any $\phi$ into a formula of (standpoint-free) first-
order logic. The basic idea is to “emulate” standpoint structures
$\langle\Delta,\Pi_{n},\sigma,\gamma\rangle$ in plain first-order structures
over $\Delta$ by means of a “superposition” of all $\gamma(\pi)$, which
requires to introduce $n$ “copies” of the original set of predicates.
(Constants need not be duplicated as they are rigid, i.e., their
interpretation is standpoint-independent.) To this end, we define our first-
order vocabulary by
$\mathbb{V}_{\\!\scaleobj{0.85}{\mathrm{FO}}}(\mathcal{P},\mathcal{C},\mathcal{S},\Pi_{n})=\mbox{$\langle\mathcal{P}^{\prime},\mathcal{C}\rangle$}$
where $\mathcal{P}^{\prime}$ contains

  * •

for each predicate $\small\mbox{\tt P}\in\mathcal{P}$ and precisification
$\pi\in\Pi_{n}$, a predicate of the form $\small\mbox{\tt P}_{\pi}$ of the
same arity as P, intuitively expressing that $\small\mbox{\tt P}_{\pi}$ should
capture $\small\mbox{\tt P}^{\gamma(\pi)}$;

  * •

for each standpoint constant $\mathsf{s}\in\mathcal{S}$ and every
precisification $\pi\in\Pi_{n}$, a nullary predicate of the form
$\mathsf{s}_{\pi}$, intuitively expressing that $\pi\in\sigma(\mathsf{s})$.

The top-level translation is then defined to set:

$\mathrm{Trans}_{n}(\phi)=\textstyle\bigwedge_{\pi\in\Pi_{n}}\mathrm{trans}_{n}(\pi,\phi)\mathrel{\wedge}\textstyle\bigwedge_{\pi\in\Pi_{n}}{\hbox{$*$}}_{\pi},$

where $\mathrm{trans}_{n}$ is inductively defined by

$\displaystyle\mathrm{trans}_{n}(\pi,\small\mbox{\tt P}(t_{1},\ldots,t_{k}))$
$\displaystyle=\small\mbox{\tt P}_{\pi}(t_{1},\ldots,t_{k})$
$\displaystyle\mathrm{trans}_{n}(\pi,\lnot\psi)$
$\displaystyle=\lnot\mathrm{trans}_{n}(\pi,\psi)$
$\displaystyle\mathrm{trans}_{n}(\pi,\psi_{1}{\,\mathrel{\wedge}\,}\psi_{2})$
$\displaystyle=\mathrm{trans}_{n}(\pi,\psi_{1}){\,\mathrel{\wedge}\,}\mathrm{trans}_{n}(\pi,\psi_{2})$
$\displaystyle\mathrm{trans}_{n}(\pi,\forall x\psi)$ $\displaystyle=\forall
x(\mathrm{trans}_{n}(\pi,\psi))$
$\displaystyle\mathrm{trans}_{n}(\pi^{\prime}\\!,\mathop{\square}\nolimits_{\mathsf{\mathsf{e}}}\psi)$
$\displaystyle=\textstyle\bigwedge_{\pi\in\Pi_{n}}(\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e})\rightarrow\mathrm{trans}_{n}(\pi,\psi))$

Therein, $\mathrm{trans}_{\mathcal{E}}$ implements the semantics of standpoint
expressions, providing for each expression
$\mathsf{e}\in\mathcal{E}_{\mathcal{S}}$ a propositional formula
$\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e})$ over
$\left\\{s_{\pi}\mathrel{\left.\middle|\right.}\pi\in\Pi_{n}\right\\}$ as
follows:

$\displaystyle\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{s})$
$\displaystyle=\mathsf{s}_{\pi}$
$\displaystyle\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e}_{1}\cup\mathsf{e}_{2})$
$\displaystyle=\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e}_{1})\mathrel{\vee}\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e}_{2})$
$\displaystyle\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e}_{1}\cap\mathsf{e}_{2})$
$\displaystyle=\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e}_{1})\mathrel{\wedge}\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e}_{2})$
$\displaystyle\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e}_{1}\setminus\mathsf{e}_{2})$
$\displaystyle=\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e}_{1})\mathrel{\wedge}\neg\mathrm{trans}_{\mathcal{E}}(\pi,\mathsf{e}_{2})$

A routine inspection of the translation ensures that it can be done in
polynomial time and its output is of polynomial size, provided it is applied
to formulas in SSNF.

We now show that the translation is correct in the sense mentioned above.
Consider a translation $\mathrm{Trans}_{n}(\phi)$ of some standpoint formula
$\phi$. Given a “plain” first-order structure $\mathcal{I}$ of the resulting
vocabulary over a domain $\Delta$, the associated first-order standpoint
structure
$\mathfrak{M}_{\mathcal{I}}=\mbox{$\langle\Delta,\Pi_{n},\sigma,\gamma\rangle$}$
is clear:

  * •

$\sigma(s)=\left\\{\pi\in\Pi_{n}\mathrel{\left.\middle|\right.}s_{\pi}^{\mathcal{I}}\neq\emptyset\right\\}$
and

  * •

$\gamma(\pi)$ is the interpretation function defined by $\small\mbox{\tt
P}^{\gamma(\pi)}=\small\mbox{\tt P}_{\\!\pi}^{\mathcal{I}}$ for
$\small\mbox{\tt P}\in\mathcal{P}$ and $c^{\gamma(\pi)}=c^{\mathcal{I}}$ for
$c\in\mathcal{C}$.

For the converse direction, given some
$\mathfrak{M}=\mbox{$\langle\Delta,\Pi,\sigma,\gamma\rangle$}$ with $|\Pi|=n$,
we can w.l.o.g. assume $\Pi=\Pi_{n}$. We obtain the plain first-order
structure ${\mathcal{I}_{\mathfrak{M}}}$ over the domain $\Delta$ as follows:

  * •

For each $s\in\mathcal{S}$ and $\pi\in\Pi_{n}$, we set
$s_{\pi}^{\mathcal{I}_{\mathfrak{M}}}=\left\\{()\right\\}$ if
$\pi\in\sigma(s)$, and set $s_{\pi}^{\mathcal{I}_{\mathfrak{M}}}=\emptyset$
otherwise;

  * •

for every “original” predicate $\small\mbox{\tt P}\in\mathcal{P}$ and each
$\pi\in\Pi_{n}$, we let $\small\mbox{\tt
P}_{\\!\pi}^{\mathcal{I}_{\mathfrak{M}}}=\small\mbox{\tt P}^{\gamma(\pi)}$;
similarly in spirit, for each constant $c\in\mathcal{C}$ we let
$c^{\mathcal{I}_{\mathfrak{M}}}=c^{\gamma(\pi)}$ for an arbitrary
$\pi\in\Pi_{n}$.

  * •

for every $\pi\in\Pi_{n}$, we set
${\hbox{$*$}}_{\pi}^{\mathcal{I}}=\left\\{()\right\\}$.

These mappings pave the way for showing soundness and completeness (i.e.
correctness) of the proposed translation.

###### Lemma 2

Let $\mathbb{V}=\mbox{$\langle\mathcal{P},\mathcal{C},\mathcal{S}\rangle$}$ be
a standpoint signature and let
$\mathbb{V}^{\prime}=\mathbb{V}_{\\!\scaleobj{0.85}{\mathrm{FO}}}(\mathcal{P},\mathcal{C},\mathcal{S},\Pi_{n})$.
Then, we obtain the following for arbitrary standpoint formulas
$\psi\in{\mathbb{S}_{\scaleobj{0.85}{\mathrm{FO}}}}$, precisifications
$\pi\in\Pi_{n}$ and variable assignments $v:\mathcal{V}\to\Delta$:

  1. 1.

For any $\mathbb{V}$-standpoint structure
$\mathfrak{M}=\mbox{$\langle\Delta,\Pi_{n},\sigma,\gamma\rangle$}$ holds
$\left.\right.\ \mathfrak{M},\pi,v\models\psi\quad\text{if and only
if}\quad\mathcal{I}_{\mathfrak{M}},v\models\mathrm{trans}_{n}(\pi,\psi).$

  2. 2.

For any $\mathbb{V}^{\prime}$-interpretation $\mathcal{I}$ holds
$\mathfrak{M}_{\mathcal{I}},\pi,v\models\psi\quad\text{if and only if}\quad\ \
\ \mathcal{I},v\models\mathrm{trans}_{n}(\pi,\psi).\ \ $

Using this lemma, we can show the announced property.

###### Theorem 2.2

A formula $\phi$ is $n$-satisfiable in FOSL if and only if the formula
$\mathrm{Trans}_{n}(\phi)$ is satisfiable in first-order logic.

###### Proof

“if” (Soundness):

Let $\mathcal{I}\models\mathrm{Trans}_{n}(\phi)$. We use the interpretation
$\mathfrak{M}_{\mathcal{I}}$ defined before and show that
$\mathfrak{M}_{\mathcal{I}}\models\phi$. Firstly, we obtain
$\sigma(\hbox{$*$})=\Pi_{n}$ by the second conjunct. Since
$\mathfrak{M}_{\mathcal{I}}\models\phi$ iff
$\mathfrak{M}_{\mathcal{I}},\pi\models\phi$ for all $\pi\in\Pi_{n}$, we show
the latter. Consider any $\pi\in\Pi_{n}$. Clearly
$\mathcal{I}\models\mathrm{trans}_{n}(\pi,\phi)$ by assumption. By Lemma 2
above, $\mathfrak{M}_{\mathcal{I}},\pi\models\phi$.

“only if” (Completeness):

Let $\mathfrak{M}=\mbox{$\langle\Delta,\Pi_{n},\sigma,\gamma\rangle$}$ be such
that $\mathfrak{M}\models\phi$. We use the first-order structure
$\mathcal{I}_{\mathfrak{M}}$ defined above and show that
$\mathcal{I}_{\mathfrak{M}}\models\mathrm{Trans}_{n}(\phi)$.

  1. 1.

$\bigwedge_{\pi\in\Pi_{n}}\\!\mathrm{trans}_{n}(\pi,\phi)$: By assumption,
$\mathfrak{M}\models\phi$, that is, $\mathfrak{M},\pi\models\phi$ for each
$\pi\in\Pi_{n}$. By Lemma 2 above, in each such case we get that
$\mathcal{I}_{\mathfrak{M}}\models\mathrm{trans}_{n}(\pi,\phi)$. Overall, it
follows that
$\mathcal{I}_{\mathfrak{M}}\models\bigwedge_{\pi\in\Pi_{n}}\mathrm{trans}_{n}(\pi,\phi)$.

  2. 2.

$\bigwedge_{\pi\in\Pi_{n}}\\!{\hbox{$*$}}_{\pi}$: By definition,
$\mathcal{I}_{\mathfrak{M}}\models{\hbox{$*$}}_{\pi}$ for any $\pi\in\Pi_{n}$.

In fact, Theorem 2.2 provides us with a recipe for a satisfiability-preserving
translation for any formula that comes with a “small model guarantee”,
whenever a bound on the number of precisifications can be computed upfront. In
particular, leveraging Theorem 2.1, we obtain the following corollary.

###### Corollary 1

A formula $\phi$ is satisfiable in sentential first-order standpoint logic if
and only if the formula $\mathrm{Trans}_{|\phi|}(\phi)$ is satisfiable in
first-order logic.

##  3 Expressive Decidable FOSL Fragments

We note that even for the sentential version, first-order standpoint logic is
still a generalization of plain first-order logic, whence reasoning in it is
undecidable. Therefore, we will next look into some popular decidable FO
fragments and establish decidability and complexity results for reasoning in
their sentential standpoint versions.

###### Definition 7

Let $\mathcal{F}$ denote some FO fragment. Then the logic _sentential
Standpoint- $\mathcal{F}$_, denoted $\mathbb{S}_{[\mathcal{F}]}$, contains the
sentential FOSL formulas $\phi$ where:

  * •

all variables inside $\phi$ are bound by some quantifier,

  * •

for every subformula $\psi\in\mathit{Sub}(\mathrm{SSNF}(\phi))$ preceded by a
quantifier, $\psi\in\mathcal{F}$ holds.

Fragment $\mathcal{F}$ is _standpoint-friendly_ iff every
$\phi\in\mathbb{S}_{[\mathcal{F}]}$ satisfies
$\mathrm{Trans}_{|\phi|}(\mathrm{SSNF}(\phi))\in\mathcal{F}$.

###### Lemma 3

Let $\mathcal{F}$ be a standpoint-friendly fragment of FOL. Then the following
hold:

  1. 1.

Satisfiability for $\mathbb{S}_{[\mathcal{F}]}$ is decidable if and only if it
is for $\mathcal{F}$.

  2. 2.

If the satisfiability problem in $\mathcal{F}$ is at least NP-hard, then the
satisfiability problem in $\mathbb{S}_{[\mathcal{F}]}$ is of the same
complexity as in $\mathcal{F}$.

It turns out that many popular formalisms are standpoint-friendly. For
propositional logic (PL), this is straightforward: quantifiers and variables
are absent altogether, which is also the reason why sentential Standpoint-PL
and proper Standpoint-PL coincide. Thus, Lemma 3 yields an alternative
argument for the NP-completeness of the latter, which was established
previously [8].

On the expressive end of the logical spectrum, it is worthwhile to inspect
fragments of FO that are still decidable (as a minimal requirement for the
feasibility of automated reasoning). In fact, standpoint-friendliness can be
established by structural induction for many of those. Notable examples are:

  * •

the _counting 2-variable fragment_ $\mathrm{C}^{2}$ [10, 25], which subsumes
many _description logics_ and serves as a mathematical backbone for related
complexity results,

  * •

the _guarded negation fragment_ $\mathrm{GNFO}$ [3, 2], which encompasses both
the popular _guarded fragment_ as well as the ubiquitous class of _(unions of)
conjunctive queries_ also known as _existential positive FO_ , and

  * •

the triguarded fragment $\mathrm{TGF}$ [28, 14] (a more recent formalism
subsuming both the two-variable and the guarded fragment without equality).

Intuitively, standpoint-friendliness for all these (and presumably many more)
fragments follows from the fact that they are closed under Boolean
combinations of sentences and that the transformation does not affect the
structure of quantified formulas. We therefore immediately obtain that these
four popular decidable fragments of FOL allow for accommodating standpoints
without any increase in complexity.

###### Corollary 2

The sentential FOSL fragments $\mathbb{S}_{[\mathrm{PL}]}\
({=}\,\mathbb{S}_{\mathrm{PL}})$, $\mathbb{S}_{[\mathrm{C}^{2}]}$,
$\mathbb{S}_{[\mathrm{GNFO}]}$, and $\mathbb{S}_{[\mathrm{TGF}]}$ are all
decidable and the complexity of their satisfiability problem is complete for
NP, NExpTime, 2ExpTime, and N2ExpTime, respectively.

As an aside, we note that all these results remain valid when considering
_finite satisfiability_ (i.e., restricting to models with finite $\Delta$),
because for all considered fragments, companion results for the finite-model
case exist and the equisatisfiability argument for our translation preserves
(finiteness of) $\Delta$.

##  4 Sentential Standpoint-$\mathcal{SROIQ}b_{s}$

We next present the highly expressive yet decidable logic _(Sentential)
Standpoint- $\mathcal{SROIQ}b_{s}$_, which adds the feature of standpoint-
aware modelling to $\mathcal{SROIQ}b_{s}$, a description logic (DL) obtained
from the well-known DL $\mathcal{SROIQ}$ [13] by a gentle extension of its
expressivity, allowing safe Boolean role expressions over simple roles
[27].555Focusing on the mildly stronger $\mathcal{SROIQ}b_{s}$ instead of the
more mainstream $\mathcal{SROIQ}$ allows for a more coherent and economic
presentation, without giving up the good computational properties and the
availability of optimised algorithms and tools. The $\mathcal{SROIQ}$ family
serves as the logical foundation of popular ontology languages like OWL 2 DL.
In view of the fact that $\mathcal{SROIQ}b_{s}$ is a semantic fragment of FO,
we can leverage the previously established results and present a
satisfiability-preserving polynomial translation from
Standpoint-$\mathcal{SROIQ}b_{s}$ into plain $\mathcal{SROIQ}b_{s}$ knowledge
bases. On the theoretical side, this will directly provide us with favourable
and tight complexity results for reasoning in
Standpoint-$\mathcal{SROIQ}b_{s}$. On the practical side, this paves the way
towards practical reasoning in “Standpoint-OWL”, since it allows us to use
highly optimised OWL 2 DL reasoners off the shelf.

###  4.1 $\mathcal{SROIQ}b_{s}$: Syntax and Semantics

Let $\mathcal{C}$, $\mathcal{P}_{1}$, and $\mathcal{P}_{2}$ be finite,
mutually disjoint sets called _individual names_ , _concept names_ and _role
names_ , respectively. $\mathcal{P}_{2}$ is subdivided into _simple role
names_ $\mathcal{P}^{\mathrm{s}}_{2}$ and _non-simple role names_
$\mathcal{P}^{\mathrm{ns}}_{2}$, the latter containing the _universal role_
$\mathtt{u}$ and being strictly ordered by some strict order $\prec$. In the
original definition of $\mathcal{SROIQ}b_{s}$, simplicity of roles and $\prec$
are not given a priori, but meant to be implicitly determined by the set of
axioms. Our choice to fix them explicitly upfront simplifies the presentation
without restricting expressivity. Then, the set $\mathcal{R}^{\mathrm{s}}$ of
_simple role expressions_ is defined by
$r_{1},r_{2}\mathrel{::=}\mathtt{s}\mid\mathtt{s}^{-}\mid r_{1}\cup r_{2}\mid
r_{1}\cap r_{2}\mid r_{1}\setminus r_{2}$,
with $\mathtt{s}{\,\in\,}\mathcal{P}^{\mathrm{s}}_{2}$, while the set of
(arbitrary) _role expressions_ is
$\mathcal{R}{\,=\,}\mathcal{R}^{\mathrm{s}}{\,\cup\,}\mathcal{P}^{\mathrm{ns}}_{2}$.
The order $\prec$ is then extended to $\mathcal{R}$ by making all elements of
$\mathcal{R}^{\mathrm{s}}$ $\prec$-minimal. The syntax of _concept
expressions_ is given by

$\displaystyle C,D\mathrel{::=}\mathtt{A}\mid\\{a\\}\mid\top\mid\bot\mid\neg
C\mid C\sqcup D\mid C\sqcup D\mid\forall r.C\mid\exists r.C\mid\exists
r^{\prime}\\!.\mathit{Self}\mid\mathord{\leqslant}n\,r^{\prime}\\!.C\mid\mathord{\geqslant}n\,r^{\prime}\\!.C,$

with $\mathtt{A}\in\mathcal{P}_{1}$, $a\in\mathcal{C}$, $r\in\mathcal{R}$,
$r^{\prime}\in\mathcal{R}^{\mathrm{s}}$, and $n\in\mathbb{N}$. We note that
any concept expression can be put in negation normal form, where negation only
occurs in front of concept names, nominals, or $\mathit{Self}$ concepts. The
different types of $\mathcal{SROIQ}b_{s}$ sentences (called _axioms_) are
given in Table 1.666The original definition of $\mathcal{SROIQ}$ contained
more axioms (role transitivity, (a)symmetry, (ir)reflexivity and
disjointness), but these are syntactic sugar in our setting.

  | Name | Syntax | Semantics
---|---|---
inverse role | $\mathtt{s}^{-}$ | $\\{(\delta,\delta^{\prime})\in\Delta\times\Delta\mid(\delta^{\prime},\delta)\in\mathtt{s}^{\mathcal{I}}\\}$
role union | $r_{1}\cup r_{2}$ | $r_{1}^{\mathcal{I}}\cup r_{2}^{\mathcal{I}}$
role intersection | $r_{1}\cap r_{2}$ | $r_{1}^{\mathcal{I}}\cup r_{2}^{\mathcal{I}}$
role difference | $r_{1}\setminus r_{2}$ | $r_{1}^{\mathcal{I}}\setminus r_{2}^{\mathcal{I}}$
universal role | $\mathtt{u}$ | $\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$
nominal | $\\{a\\}$ | $\\{a^{\mathcal{I}}\\}$
top | $\top$ | $\Delta^{\mathcal{I}}$
bottom | $\bot$ | $\emptyset$
negation | $\neg C$ | $\Delta^{\mathcal{I}}\setminus C^{\mathcal{I}}$
conjunction | $C\sqcap D$ | $C^{\mathcal{I}}\cap D^{\mathcal{I}}$
disjunction | $C\sqcup D$ | $C^{\mathcal{I}}\cup D^{\mathcal{I}}$
univ. restriction | $\forall r.C$ | $\\{\delta\mid\forall y.(\delta,\delta^{\prime})\in r^{\mathcal{I}}\to\delta^{\prime}\in C^{\mathcal{I}}\\}$
exist. restriction | $\exists r.C$ | $\\{\delta\mid\exists y.(\delta,\delta^{\prime})\in r^{\mathcal{I}}\wedge\delta^{\prime}\in C^{\mathcal{I}}\\}$
$\mathit{Self}$ concept | $\exists r.\mathit{Self}$ | $\\{\delta\mid(\delta,\delta)\in r^{\mathcal{I}}\\}$
qualified number | $\mathord{\leqslant}n\,r.C$ | $\\{\delta\mid\\#\\{\delta^{\prime}\in C^{\mathcal{I}}\mid(\delta,\delta^{\prime})\in r^{\mathcal{I}}\\}\leq n\\}$
restrictions | $\mathord{\geqslant}n\,r.C$ | $\\{\delta\mid\\#\\{\delta^{\prime}\in C^{\mathcal{I}}\mid(\delta,\delta^{\prime})\in r^{\mathcal{I}}\\}\geq n\\}$

  | Name | Syntax | Semantics
---|---|---
concept assertion | $C(a)$ | $a^{\mathcal{I}}\in C^{\mathcal{I}}$
role assertion | $r(a,b)$ | $(a^{\mathcal{I}},b^{\mathcal{I}})\in\mathtt{r}^{\mathcal{I}}$
equality | $a\doteq b$ | $a^{\mathcal{I}}=b^{\mathcal{I}}$
inequality | $a\not\doteq b$ | $a^{\mathcal{I}}\neq b^{\mathcal{I}}$
general concept | $C{\,\sqsubseteq\,}D$ | $C^{\mathcal{I}}\subseteq D^{\mathcal{I}}$
inclusion (GCI) |  |
role inclusion | $r_{1}{\circ}\ldots{\circ}\hskip 1.0ptr_{n}{\,\sqsubseteq\,}\mathtt{r}$ | $r_{1}^{\mathcal{I}}{\circ}\ldots{\circ}\hskip 1.0ptr_{n}^{\mathcal{I}}{\,\subseteq\,}\mathtt{r}^{\mathcal{I}}$
axioms | $r_{1}{\circ}\ldots{\circ}\hskip 1.0ptr_{n}{\circ}\hskip 1.0pt\mathtt{r}{\,\sqsubseteq\,}\mathtt{r}$ | $r_{1}^{\mathcal{I}}{\circ}\ldots{\circ}\hskip 1.0ptr_{n}^{\mathcal{I}}{\circ}\hskip 1.0pt\mathtt{r}^{\mathcal{I}}{\,\subseteq\,}\mathtt{r}^{\mathcal{I}}$
(RIAs) | $\mathtt{r}{\circ}\hskip 1.0ptr_{1}{\circ}\ldots{\circ}\hskip 1.0ptr_{n}{\,\sqsubseteq\,}\mathtt{r}$ | $\mathtt{r}^{\mathcal{I}}{\circ}r_{1}^{\mathcal{I}}{\circ}\ldots{\circ}\hskip 1.0ptr_{n}^{\mathcal{I}}{\,\subseteq\,}\mathtt{r}^{\mathcal{I}}$
| $\mathtt{r}{\circ}\hskip 1.0pt\mathtt{r}{\,\sqsubseteq\,}\mathtt{r}$ | $\mathtt{r}^{\mathcal{I}}{\circ}\hskip 1.0pt\mathtt{r}^{\mathcal{I}}{\,\subseteq\,}\mathtt{r}^{\mathcal{I}}$
In RIAs, $\mathtt{r}\in\mathcal{P}^{\mathrm{ns}}_{2}$, while $r_{i}\in\mathcal{R}$ and $r_{i}\prec\mathtt{r}$ for all |  |
$i\in\\{1,\ldots,n\\}$. |  |

Table 1: $\mathcal{SROIQ}b_{s}$ role, concept expressions and axioms. $C\equiv
D$ abbreviates $C\sqsubseteq D$, $D\sqsubseteq C$.

Similar to FOL, the semantics of $\mathcal{SROIQ}b_{s}$ is defined via
interpretations $\mathcal{I}=(\Delta,\cdot^{\mathcal{I}})$ composed of a non-
empty set $\Delta$ called the _domain of $\mathcal{I}$_ and a function
$\cdot^{\mathcal{I}}$ mapping individual names to elements of $\Delta$,
concept names to subsets of $\Delta$, and role names to subsets of
$\Delta\times\Delta$. This mapping is extended to role and concept expressions
and finally used to define satisfaction of axioms (see Table 1).

###  4.2 Standpoint-$\mathcal{SROIQ}b_{s}$

The set
${\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$ of
_sentential Standpoint- $\mathcal{SROIQ}b_{s}$ sentences_ is now defined
inductively as follows:

  * •

if $\mathbf{Ax}$ is a $\mathcal{SROIQ}b_{s}$ axiom then
$\mathbf{Ax}\in{\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$,

  * •

if
$\phi,\psi\in{\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$
then $\neg\phi$, as well as $\phi{\,\mathrel{\wedge}\,}\psi$ and
$\phi{\,\mathrel{\vee}\,}\psi$ are in
${\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$,

  * •

if
$\phi\in{\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$
and $\mathsf{e}\in\mathcal{E}_{\mathcal{S}}$ then
$\mathop{\square}\nolimits_{\mathsf{e}}\phi\in{\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$
and
$\mathop{\lozenge}\nolimits_{\mathsf{e}}\phi\in{\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$.

The semantics of sentential Standpoint-$\mathcal{SROIQ}b_{s}$ is defined in
the obvious way, by “plugging” the semantics of $\mathcal{SROIQ}b_{s}$ axioms
into the semantics of ${\mathbb{S}_{\scaleobj{0.85}{\mathrm{[FO]}}}}$. We say
a ${\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$
sentence $\phi$ is in _negation normal form_ (NNF), if negation occurs only
inside or directly in front of $\mathcal{SROIQ}b_{s}$ axioms; obviously every
Standpoint-$\mathcal{SROIQ}b_{s}$ sentence can be efficiently transformed into
an equivalent one in NNF.

###  4.3 Coping with Peculiarities of $\mathcal{SROIQ}b_{s}$

In the following, we will provide a polynomial translation, mapping any
${\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$
sentence $\phi$ to an equisatisfiable set of $\mathcal{SROIQ}b_{s}$ axioms.
This translation is very much in the spirit of the one presented for
sentential FOSL, however, $\mathcal{SROIQ}b_{s}$ comes with diverse syntactic
impediments that we need to circumvent. Thus, before presenting the
translation, we will briefly discuss these issues and how to solve them.

First, $\mathcal{SROIQ}b_{s}$ does not provide nullary predicates (i.e.,
propositional symbols). As a surrogate, we use concept expressions of the form
$\forall\mathtt{u}.\mathtt{A}$ which have the pleasant property of holding
either for all domain individuals or for none. Second, $\mathcal{SROIQ}b_{s}$
does not directly allow for arbitrary Boolean combinations of axioms. For all
non-RIA axioms, a more or less straightforward equivalent encoding is possible
using nominals and the universal role; for instance the expression
$\neg[\mathtt{r}(a,b)]\vee[\mathtt{A}\sqsubseteq\mathtt{B}]$ can be converted
into $\top\ \sqsubseteq\
\neg\exists\mathtt{u}.(\\{a\\}\sqcap\exists\mathtt{r}.\\{b\\})\ \sqcup\
\forall\mathtt{u}.(\neg\mathtt{A}\sqcup\mathtt{B})$.

Dealing with RIAs requires auxiliary vocabulary; for negated RIAs, we
introduce a fresh nominal, say $\\{x\\}$, to mark the end of a “violating”
role chain, so $\neg[\mathtt{s}\circ\mathtt{s}\sqsubseteq\mathtt{r}]$
essentially becomes $\top\ \sqsubseteq\
\exists\mathtt{u}.\big{(}(\exists\mathtt{s}.\exists\mathtt{s}.\\{x\\})\sqcap(\neg\exists\mathtt{r}.\\{x\\})\big{)}.$

Unnegated RIAs are even trickier. There is no way of converting them into
GCIs, so we have to keep them, but we attach an additional “guard”, which
allows us to disable them whenever necessary. This guard can then be triggered
from within a GCI. For an example, consider the expression
$[\mathtt{t}\circ\mathtt{t}^{\prime}\sqsubseteq\mathtt{r}]\vee[\mathtt{t}^{\prime}\circ\mathtt{t}\sqsubseteq\mathtt{r}]$.
Then, introducing fresh “guard roles” $\mathtt{s}_{1}$ and $\mathtt{s}_{2}$,
we assert the three axioms
$\top\sqsubseteq(\forall\mathtt{u}.\exists\mathtt{s}_{1}.\mathit{Self})\sqcup(\forall\mathtt{u}.\exists\mathtt{s}_{2}.\mathit{Self})$
as well as
$\mathtt{s}_{1}\circ\mathtt{t}\circ\mathtt{t}^{\prime}\sqsubseteq\mathtt{r}$
and
$\mathtt{s}_{2}\circ\mathtt{t}^{\prime}\circ\mathtt{t}\sqsubseteq\mathtt{r}$.
With this arrangement, the first axiom will ensure that all domain elements
carry an $\mathtt{s}_{1}$-loop or all domain elements carry an
$\mathtt{s}_{2}$-loop. Depending on that choice, the corresponding RIA in the
second line will behave like its original, unguarded version, while the other
one may be entirely disabled.

The introduced strategy for handling positive RIAs has a downside: due to the
restricted shapes of RIAs (governed by $\prec$), axioms of the shape
$\mathtt{r}\circ\mathtt{r}\sqsubseteq\mathtt{r}$ (expressing transitivity)
cannot be endowed with guards. In order to overcome this nuisance, every
nonsimple role $\mathtt{r}$ has to be accompanied by a subrole
$\underline{\mathtt{r}}$, which acts as a “lower approximation” of
$\mathtt{r}$ and – whenever $\mathtt{r}$ is defined transitive – “feeds into”
$\mathtt{r}$ via tail recursion. This way of reformulating
$\mathtt{r}\circ\mathtt{r}\sqsubseteq\mathtt{r}$ allows to attach the wanted
guard, but requires adjustments in some axioms that mention $\mathtt{r}$.

###  4.4 Translation into Plain $\mathcal{SROIQ}b_{s}$

We now assume a given
${\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$
sentence $\phi$, w.l.o.g. in NNF, and provide the formal definition of the
translation. As before, we fix $\Pi_{|\phi|}$ and let our translation’s
vocabulary
${\mathbb{V}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}(\phi)$
consist of all individual names inside $\phi$, plus, for each
$\pi\in\Pi_{|\phi|}$, the following symbols: (a) a concept name
$\mathtt{A}^{\pi}$ for each $\mathtt{A}\in\mathcal{P}_{1}$; (b) a simple role
name $\mathtt{s}^{\pi}$ for each
$\mathtt{s}{\,\in\,}\mathcal{P}^{\mathrm{s}}_{2}$; (c) non-simple role names
$\mathtt{r}^{\pi}$ and $\underline{\mathtt{r}}^{\pi}$ for each
$\mathtt{r}{\,\in\,}\mathcal{P}^{\mathrm{ns}}_{2}\\!\setminus\\!\\{\mathtt{u}\\}$;
(d) a simple role name $\mathtt{s}^{\pi}_{\rho}$ for each unnegated RIA $\rho$
inside $\phi$; (e) a fresh constant name $a^{\pi}_{\rho}$ for each negated RIA
$\rho$ inside $\phi$; (f) a concept name $\mathtt{M}^{\mathsf{s}}_{\pi}$ for
each $\mathsf{s}\in\mathcal{S}$. Thereby, the non-simple role names inherit
their ordering $\prec$ from $\mathcal{P}^{\mathrm{ns}}_{2}$ and we also let
$\underline{\mathtt{r}}^{\pi}\prec\mathtt{r}^{\pi}$ for each
$\mathtt{r}{\,\in\,}\mathcal{P}^{\mathrm{ns}}_{2}\\!\setminus\\!\\{\mathtt{u}\\}$.

The translation $\mathrm{Trans}(\phi)$ of $\phi$ is then a set of
$\mathcal{SROIQ}$ axioms defined as follows: First, $\mathrm{Trans}(\phi)$
contains the RIA
$\underline{\mathtt{r}}^{\pi}{\,\sqsubseteq\,}\mathtt{r}^{\pi}$ for every
$\mathtt{r}{\,\in\,}\mathcal{P}^{\mathrm{ns}}_{2}\\!\setminus\\!\\{\mathtt{u}\\}$
and each $\pi\in\Pi_{|\phi|}$. Second, for every unnegated RIA $\rho$ inside
$\phi$ and each $\pi\in\Pi_{|\phi|}$, $\mathrm{Trans}(\phi)$ contains the RIA
$BG_{\pi}(\rho)$, with $BG_{\pi}$ defined by

$\displaystyle r_{1}{\circ}...{\circ}\hskip
1.0ptr_{n}{\,\sqsubseteq\,}\mathtt{r}\mapsto\hskip 3.87498pt$
$\displaystyle\mathtt{s}_{\rho}^{\pi}{\circ}\hskip
1.0ptr_{1}^{\pi}{\circ}...{\circ}\hskip
1.0ptr_{n}^{\pi}{\,\sqsubseteq\,}\underline{\mathtt{r}}^{\pi}$
$\displaystyle\hskip 1.0ptr_{1}{\circ}...{\circ}\hskip 1.0ptr_{n}{\circ}\hskip
1.0pt\mathtt{r}{\,\sqsubseteq\,}\mathtt{r}\mapsto\hskip 3.87498pt$
$\displaystyle\mathtt{s}_{\rho}^{\pi}\hskip 1.0pt{\circ}\hskip
1.0ptr_{1}^{\pi}{\circ}...{\circ}\hskip 1.0ptr_{n}^{\pi}{\circ}\hskip
1.0pt\underline{\mathtt{r}}^{\pi}{\,\sqsubseteq\,}\underline{\mathtt{r}}^{\pi}$
$\displaystyle\mathtt{r}\hskip 1.0pt{\circ}\hskip
1.0ptr_{1}{\circ}...{\circ}\hskip
1.0ptr_{n}{\,\sqsubseteq\,}\mathtt{r}\mapsto\hskip 3.87498pt$
$\displaystyle\underline{\mathtt{r}}^{\pi}\hskip 1.0pt{\circ}\hskip
1.0ptr_{1}^{\pi}{\circ}...{\circ}\hskip 1.0ptr_{n}^{\pi}{\circ}\hskip
1.0pt\mathtt{s}_{\rho}^{\pi}{\,\sqsubseteq\,}\underline{\mathtt{r}}^{\pi}$
$\displaystyle\mathtt{r}\hskip 1.0pt{\circ}\hskip
1.0pt\mathtt{r}{\,\sqsubseteq\,}\mathtt{r}\mapsto\hskip 3.87498pt$
$\displaystyle\mathtt{s}_{\rho}^{\pi}\hskip 1.0pt{\circ}\hskip
1.0pt\underline{\mathtt{r}}^{\pi}{\circ}\hskip
1.0pt{\mathtt{r}}^{\pi}{\,\sqsubseteq\,}\mathtt{r}^{\pi},\\!\\!$

whereby the role expression $r^{\pi}$ is obtained from $r$ by substituting
every role name $\mathtt{s}$ with $\mathtt{s}^{\pi}$ (except $\mathtt{u}$,
which remains unaltered). Third and last, $\mathrm{Trans}(\phi)$ contains the
GCI

$\top\sqsubseteq\textstyle\bigsqcap_{\pi\in\Pi_{|\phi|}}\mathrm{trans}(\pi,\phi)\sqcap\textstyle\bigsqcap_{\pi\in\Pi_{|\phi|}}\forall\mathtt{u}.\mathtt{M}^{\hbox{$*$}}_{\pi}$

where, by inductive definition,

$\displaystyle\mathrm{trans}(\pi\\!,\mathbf{Ax})$
$\displaystyle=\mathrm{trans}^{+}(\pi\\!,\mathbf{Ax})$
$\displaystyle\mathrm{trans}(\pi\\!,\neg\mathbf{Ax})$
$\displaystyle=\mathrm{trans}^{-}(\pi\\!,\mathbf{Ax})$
$\displaystyle\mathrm{trans}(\pi\\!,\psi_{1}\mathrel{\wedge}\psi_{2})$
$\displaystyle=\mathrm{trans}(\pi\\!,\psi_{1})\sqcap\mathrm{trans}(\pi\\!,\psi_{2})$
$\displaystyle\mathrm{trans}(\pi\\!,\psi_{1}\mathrel{\vee}\psi_{2})$
$\displaystyle=\mathrm{trans}(\pi\\!,\psi_{1})\sqcup\mathrm{trans}(\pi\\!,\psi_{2})$
$\displaystyle\mathrm{trans}(\pi^{\prime}\\!\\!,\mathop{\square}\nolimits_{\mathsf{\mathsf{e}}}\psi)$
$\displaystyle=\textstyle\bigsqcap_{\pi\in\Pi_{|\phi|}}(\neg\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e})\sqcup\mathrm{trans}(\pi\\!,\psi))$
$\displaystyle\mathrm{trans}(\pi^{\prime}\\!\\!,\mathop{\lozenge}\nolimits_{\mathsf{\mathsf{e}}}\psi)$
$\displaystyle=\textstyle\bigsqcup_{\pi\in\Pi_{|\phi|}}(\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e})\sqcap\mathrm{trans}(\pi\\!,\psi))$

We next present the translation of unnegated and negated $\mathcal{SROIQ}$
axioms ($\rho$ stands for an RIA $r_{1}{\circ}...{\circ}\hskip
1.0ptr_{m}{\,\sqsubseteq\,}\mathtt{r}$):

$\displaystyle\mathrm{trans}^{+}(\pi\\!,\rho)$
$\displaystyle=\forall\mathtt{u}.\exists\mathtt{s}^{\pi}_{\rho}.\mathit{Self}$
$\displaystyle\mathrm{trans}^{-}(\pi\\!,\rho)=\exists\mathtt{u}.\big{(}(\forall$
$\displaystyle\mathtt{r}^{\pi}\\!\\!.\neg\\{a_{\rho}^{\pi}\\})\sqcap(\exists\underline{r}_{1}^{\pi}\\!...\exists\underline{r}_{m}^{\pi}.\\{a_{\rho}^{\pi}\\})\big{)}$
$\displaystyle\mathrm{trans}^{+}(\pi\\!,C{\,\sqsubseteq\,}D)$
$\displaystyle=\forall\mathtt{u}.(\neg C\sqcup D)^{\pi}$
$\displaystyle\mathrm{trans}^{-}(\pi\\!,C{\,\sqsubseteq\,}D)$
$\displaystyle=\exists\mathtt{u}.(C\sqcap\neg D)^{\pi}$
$\displaystyle\mathrm{trans}^{+}(\pi\\!,C(a))$
$\displaystyle=\exists\mathtt{u}.\big{(}\\{a\\}\sqcap C^{\pi}\big{)}$
$\displaystyle\mathrm{trans}^{-}(\pi\\!,C(a))$
$\displaystyle=\exists\mathtt{u}.\big{(}\\{a\\}\sqcap(\neg C)^{\pi}\big{)}$
$\displaystyle\mathrm{trans}^{+}(\pi\\!,r(a,b))$
$\displaystyle=\exists\mathtt{u}.\big{(}\\{a\\}\sqcap\exists\underline{r}^{\pi}.\\{b\\}\big{)}$
$\displaystyle\mathrm{trans}^{-}(\pi\\!,r(a,b))$
$\displaystyle=\exists\mathtt{u}.\big{(}\\{a\\}\sqcap\forall
r^{\pi}.\neg\\{b\\}\big{)}$ $\displaystyle\mathrm{trans}^{+}(\pi\\!,a\doteq
b)$ $\displaystyle=\exists\mathtt{u}.\big{(}\\{a\\}\sqcap\\{b\\}\big{)}$
$\displaystyle\mathrm{trans}^{-}(\pi\\!,a\doteq b)$
$\displaystyle=\exists\mathtt{u}.\big{(}\\{a\\}\sqcap\neg\\{b\\}\big{)}$

Therein, for any role expression $r$, we let $\underline{r}$ denote
$\underline{\mathtt{r}}$ if $r=\mathtt{r}$ is a non-simple role name, and
otherwise $\underline{r}=r$. Moreover, $C^{\pi}$ denotes the concept
expression that is obtained from $C$ by transforming it into negation normal
form, replacing concept names $\mathtt{A}$ with $\mathtt{A}^{\pi}$ and role
expressions $\mathtt{r}$ by $\mathtt{r}^{\pi}$, and replacing every
$\exists\mathtt{r}$ for non-simple $\mathtt{r}$ with
$\exists\underline{\mathtt{r}}$.

As before, $\mathrm{trans}_{\mathcal{E}}$ implements the semantics of
standpoint expressions, but now adjusted to the new framework: each expression
$\mathsf{e}\in\mathcal{E}_{\mathcal{S}}$ is transformed into a concept
expression $\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e})$ over the
vocabulary
$\left\\{\mathtt{M}^{\mathsf{s}}_{\pi}\\!\\!\mathrel{\left.\middle|\right.}\\!\\!s\in\mathcal{S},\pi{\,\in\,}\Pi_{|\phi|}\right\\}$
as follows:

$\displaystyle\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{s})$
$\displaystyle=\forall\mathtt{u}.\mathtt{M}^{\mathsf{s}}_{\pi}$
$\displaystyle\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e}_{1}\cup\mathsf{e}_{2})$
$\displaystyle=\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e}_{1})\sqcup\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e}_{2})$
$\displaystyle\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e}_{1}\cap\mathsf{e}_{2})$
$\displaystyle=\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e}_{1})\sqcap\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e}_{2})$
$\displaystyle\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e}_{1}\setminus\mathsf{e}_{2})$
$\displaystyle=\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e}_{1})\sqcap\neg\mathrm{trans}_{\mathcal{E}}(\pi\\!,\mathsf{e}_{2})$

With all definitions in place, we obtain the desired result. Details can be
found in Appendix B.

###### Theorem 4.1

Given
$\phi\in{\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$,
the set $\mathrm{Trans}(\phi)$ (i) is a valid $\mathcal{SROIQ}b_{s}$ knowledge
base,  (ii) is equisatisfiable with $\phi$,  (iii) is of polynomial size wrt.
$\phi$, and  (iv) can be computed in polynomial time.

##  5 Example in the Forestry Domain

We consider an extension of Example 1 in Sentential
Standpoint-$\mathcal{SROIQ}b_{s}$ to illustrate the main reasoning tasks in
more detail. The following additional axiom specifies that forest land use and
urban land use are disjoint subclasses of land (F9).

  1. (F9)

$\mathop{\square}\nolimits_{\mathsf{*}}[\small\mbox{\tt
ForestlandUse}\sqcup\small\mbox{\tt
UrbanLandUse}{\,\sqsubseteq\,}\small\mbox{\tt Land}\ \wedge\ \small\mbox{\tt
ForestlandUse}\sqcap\small\mbox{\tt UrbanLandUse}{\,\sqsubseteq\,}\bot]$

Now, let us see how, through inferences in
${\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$, we
can gather unequivocal knowledge (Uneq), obtain knowledge that is relative to
a standpoint (Rel), and contrast the knowledge that can be inferred from
different standpoints (Cont). For unequivocal knowledge (Uneq), we can infer
unambiguously that forests are no urban-use lands:
$\mathop{\square}\nolimits_{\mathsf{*}}[\small\mbox{\tt
Forest}\sqsubseteq\neg\small\mbox{\tt UrbanLandUse}]$
This holds because each precisification must comply with $\mathsf{LC}$ or
$\mathsf{LU}$ (F8), and we have
$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}[\small\mbox{\tt
Forest}\sqsubseteq\neg\small\mbox{\tt UrbanLandUse}]$ from (F1) and (F5), and
$\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LU}}}[\small\mbox{\tt
Forest}\sqsubseteq\neg\small\mbox{\tt UrbanLandUse}]$ from (F3) and (F9).
Regarding relative (Rel) and contrasting (Cont) knowledge, if we now wanted to
query our knowledge base for instances of forest, we would obtain

$\displaystyle\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}[\small\mbox{\tt
Forest}(e)]\ \wedge\
\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}[\neg\small\mbox{\tt
Forest}(l)]\qquad\qquad\mathcal{I}_{*}[\small\mbox{\tt Forest}(e)]\ \wedge\
\mathcal{I}_{*}[\small\mbox{\tt Forest}(l)]$

The first deduced formula contains knowledge relative to $\mathsf{LC}$,
showing its stance on whether the instances constitute a forest, which happens
to be conclusive in both cases. The second formula states the global
indeterminacy of both $l$’s and $e$’s membership to the concept Forest. This
stems from the disagreement between the interpretations $\mathsf{LC}$ and
$\mathsf{LU}$, whose overall incompatibility
($\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC\cap
LU}}}[\top{\,\sqsubseteq\,}\bot]$) can also be inferred.

Finally, it is worth looking at the limitations of the sentential fragment of
Standpoint $\mathcal{SROIQ}b_{s}$. In a non-sentential setting, where
modalities can be used at the concept level, “complex alignments” or bridges
can be established between concepts according to possibly many standpoints.
For instance, one can write
$\small\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LU}}}[\small\mbox{\tt
Forest}]\sqsubseteq\mathop{\square}\nolimits_{\scaleobj{0.8}{\mathsf{LC}}}[\exists\small\mbox{\tt
hasLand}^{-}.\small\mbox{\tt
Forest}]\sqcup\mathop{\square}\nolimits_{\mathsf{*}}[\small\mbox{\tt
Cleared}]$
to express that the areas classified as forest according to $\mathsf{LU}$
belong to a forest according to $\mathsf{LC}$ or have been cleared (in which
case $\mathsf{LC}$ does not recognise them as forest). It is an objective of
future work of ours to study decidable fragments for which the restrictions on
the use of modalities are relaxed to express such kinds of axioms.

##  6 Related Work

A variety of formal representation systems have been proposed to model
perspectives in rather diverse areas of research and with heterogeneous
nomenclatures. Standpoint logic bears some similarities to _context logic_ in
the style proposed by McCarthy and Buvac [19], which has also been applied in
a description logic setting [15]. This tradition treats contexts as “first-
class citizens” of the logic, i.e., full-fledged formal objects over which one
can express first-order properties. In contrast, standpoint logic is suitable
when a formalisation of the contexts involved is unfeasible, or when the
interest resides in the content of the standpoints rather than the context in
which they occur.

Another related notion is that of _ontology views_ , where some works consider
potentially conflicting viewpoints [26, 12, 11]. Ribière and Dieng [26] and
Heman et al. [12, 11] implement the intuition of “viewpoints” via ad-hoc
extensions of the syntax and semantics of description logics, in a style
similar to the work on contextuality by Benslimane et al. [4]. Gorshkov et al.
[9] implement them using named graphs. Instead, the standpoint approach
extends the base language with modalities and provides a Kripke-style
semantics for it. This leads to a simpler, more recognisable and more
expressive framework that supports, for instance, hierarchies and combinations
of standpoints, inferences of partial truths, the preservation of consistency
with the established alignments and inferences about the standpoints
themselves. On a technical level, first-order standpoint logic can be seen as
a many-dimensional (multi-)modal logic [16], whence results from that area
apply to our setting. In particular, the search for non-trivial fragments of
first-order modal logics that are still decidable and even practically
relevant is an important endeavour, for which we believe that standpoint logic
can play useful role.

Finally, in the area of ontology modularity, different formalisms such as _DDL
bridge rules_ [5] and _$\varepsilon$ -connections_ [17, 18] have been proposed
to specify the interaction between independent knowledge sources. These can be
related to the present framework in that they provide mechanisms to establish
links between conceptual models that do not need to be entirely coherent with
each other. Yet the motivation is inherently different: while the standpoint
framework focuses on integrating possibly overlapping knowledge into a global
source (while preserving “standpoint-provenance” and thus enabling a peaceful
coexistence of conflicting information), DDL bridge rules and
$\varepsilon$-connections have been devised to establish a certain
synchronisation between modules that are and will remain separate. DDL bridge
rules could, however, be simulated within a standpoint framework.

##  7 Conclusions and Future Work

The diversity of human world views along with the semantic heterogeneity of
natural language are at the heart of well-recognised knowledge
interoperability challenges. As an alternative to the common strategy of
merging, we proposed the use of a logical formalism based on the notion of
_standpoint_ that is suitable for knowledge representation and reasoning with
sets of possibly conflicting characterisations of a domain.

Using first-order logic as an expressive underlying language, we proposed a
multi-modal framework by means of which different agents can establish their
individual standpoints (which typically involves specifying constraints and
relations), but which also allows for combining standpoints and establishing
alignments between them. Reasoning tasks over such multi-standpoint
specifications include gathering unequivocal knowledge, determining knowledge
that is relative to a standpoint or a set of them, and contrasting the
knowledge that can be inferred from different standpoints.

Remarkably, the simplified Kripke semantics allows us to establish a small
model property for the _sentential_ fragment of FOSL. This result gave rise to
a polynomial, satisfiability-preserving translation into the base logic, which
also maintains membership in diverse decidable fragments, immediately implying
that for a range of logics, reasoning in their standpoint-enhanced versions
does not increase their computational complexity. This indicates that the
framework can be applied to ontology alignment, concept negotiation, and
knowledge aggregation with inference systems built on top of existing, highly
optimised off-the-shelf reasoners.

Future work includes the study of the complexity of FOSL fragments allowing
the presence of free variables within the scope of modalities. Note however
that in the general case of FOSL, this leads to the loss of the small model
property.

###### Example 2

Consider the following (non-sentential) FOSL sentence, axiomatising "better"
(Btt) to be interpreted as a non-well-founded strict linear order and
requiring for every domain element $x$ (of infinitely many) the existence of
some precisification where $x$ is the (one and only) “best”:

$\displaystyle\forall xyz\big{(}(\small\mbox{\tt
Btt}(x,y)\mathrel{\wedge}\small\mbox{\tt Btt}(y,z))\rightarrow\small\mbox{\tt
Btt}(x,z)\big{)}$ $\displaystyle\mathrel{\wedge}$ $\displaystyle\forall
xy\neg(\small\mbox{\tt Btt}(x,y)\mathrel{\wedge}\small\mbox{\tt
Btt}(y,x))\mathrel{\wedge}$ $\displaystyle\forall xy\big{(}x\neq
y\rightarrow(\small\mbox{\tt Btt}(x,y)\mathrel{\vee}\small\mbox{\tt
Btt}(y,x))\big{)}$ $\displaystyle\mathrel{\wedge}$ $\displaystyle\forall
x\exists y\small\mbox{\tt Btt}(x,y)\mathrel{\wedge}\forall
x\mathop{\lozenge}\nolimits_{\mathsf{*}}\\!\neg\exists y\small\mbox{\tt
Btt}(y,x)$

Obviously, this sentence is satisfiable, but only in a model with infinitely
many precisifications; that is, the small model property is violated in the
worst possible way.

On the other hand, it is desirable from a modelling perspective to allow for
some interplay between FO quantifiers and standpoint modalities. E.g., the
non-sentential FOSL sentence $\forall x_{1}\cdots x_{k}\big{(}\small\mbox{\tt
P}(x_{1},\ldots,x_{k})\to\mathop{\square}\nolimits_{\mathsf{*}}\small\mbox{\tt
P}(x_{1},\ldots,x_{k})\big{)}$ expresses the rigidity of a predicate P,
thereby “synchronising” it over all precisifications.

Consequently, we will study how by imposing syntactic restrictions, we can
guarantee the existence of small (or at least reasonably-sized) models for
non-sentential standpoint formulas. Results in the field of many-dimensional
modal logics [16] show that reasoning is decidable for diverse fragments of
first-order modal logic such as the _monodic_ fragment (where modalities occur
only in front of formulas with at most one free variable). However, Example 2
already shows (by virtue of being within the monodic fragment) that we cannot
hope for a small model property even for this slight extension of the
sentential fragment. A detailed analysis of these issues as they apply to the
simplified semantics of standpoint logic is the object of current work.

Additionally, we intend to implement the proposed translations and perform
experiments to test the performance of the standpoint framework in scenarios
of Knowledge Integration. While sentential standpoints can be added at no
extra cost in complexity for the discussed fragments in this paper, we intend
to run experiments to assess the runtime impact on large knowledge bases with
off-the-shelf reasoners.

As another important topic toward the deployment of our framework, we will
look into conceptual modelling aspects. Reviewing documented recurrent
scenarios and patterns in the area of knowledge integration, we intend to
establish guiding principles for conveniently encoding those by using novel
strategies possible with structures of standpoints. Examples for such
scenarios include the disambiguation of knowledge sources by using
combinations of standpoints, and the establishment of bridge-like rules for
alignment. For the latter we will investigate their relationship to similar
constructs from other frameworks such as $\varepsilon$-connections,
distributed description logics, and others.

#### Acknowledgments:

Lucía Gómez Álvarez was supported by the _Bundesministerium für Bildung und
Forschung_ (BMBF) in the Center for Scalable Data Analytics and Artificial
Intelligence (ScaDS.AI). Sebastian Rudolph has received funding from the
European Research Council (Grant Agreement no. 771779, DeciGUT).

## References

  * [1] Arp, R., Smith, B., Spear, A.D.: Building ontologies with basic formal ontology. MIT Press (2015)
  * [2] Bárány, V., Benedikt, M., ten Cate, B.: Some model theory of guarded negation. Journal of Symbolic Logic 83(4), 1307–1344 (2018)
  * [3] Bárány, V., ten Cate, B., Segoufin, L.: Guarded negation. Journal of the ACM 62(3) (2015)
  * [4] Benslimane, D., Arara, A., Falquet, G., Maamar, Z., Thiran, P., Gargouri, F.: Contextual ontologies. Motivations, challenges, and solutions. In: Procs. of the 4th Int. Conf. on Advances in Information Systems. pp. 168–176. Springer (2006)
  * [5] Borgida, A., Serafini, L.: Distributed Description Logics: Assimilating information from peer sources. Journal on Data Semantics 2800, 153–184 (2003)
  * [6] Euzenat, J., Mocan, A., Scharffe, F.: Ontology alignments. In: Hepp, M., Leenheer, P.D., Moor, A.D., Sure, Y. (eds.) Ontology Management. Computing for Human Experience, vol. 7, pp. 177–206. Springer (2008)
  * [7] Fine, K.: Vagueness, truth and logic. Synthese 30(3-4), 265–300 (1975)
  * [8] Gómez Álvarez, L., Rudolph, S.: Standpoint logic: Multi-perspective knowledge representation. In: Neuhaus, F., Brodaric, B. (eds.) Procs. of the 12th Int. Conf. on Formal Ontology in Information Systems. FAIA, vol. 344, pp. 3–17. IOS Press (2021)
  * [9] Gorshkov, S., Kralin, S., Miroshnichenko, M.: Multi-viewpoint ontologies for decision-making support. In: Ngonga Ngomo, A.C., Křemen, P. (eds.) Knowledge Engineering and Semantic Web. pp. 3–17. Springer (2016)
  * [10] Grädel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Procs. of the 12th Annual IEEE Symposium on Logic in Computer Science. pp. 306–317. IEEE (1997)
  * [11] Hemam, M.: An extension of the ontology web language with multi-viewpoints and probabilistic reasoning. Int. Journal of Advanced Intelligence Paradigms 10(3), 247–265 (2018)
  * [12] Hemam, M., Boufaïda, Z.: MVP-OWL: A multi-viewpoints ontology language for the Semantic Web. Int. Journal of Reasoning-based Intelligent Systems 3(3-4), 147–155 (2011)
  * [13] Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) Procs. 10th Int. Conf. on Principles of Knowledge Representation and Reasoning. pp. 57–67. AAAI Press (2006)
  * [14] Kieronski, E., Rudolph, S.: Finite model theory of the triguarded fragment and related logics. In: Procs. of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 1–13. IEEE (2021)
  * [15] Klarman, S., Gutiérrez-Basulto, V.: Description logics of context. Journal of Logic and Computation 26(3), 817–854 (2013)
  * [16] Kurucz, A., Wolter, F., Zakharyaschev, M., Gabbay, D.M.: Many-Dimensional Modal Logics: Theory and Applications. Studies in Logics and the Foundations of Mathematics, Elsevier, 1st edn. (2003)
  * [17] Kutz, O., Lutz, C., Wolter, F., Zakharyaschev, M.: E-connections of description logics. Description Logics Workshop 81 (2003)
  * [18] Kutz, O., Lutz, C., Wolter, F., Zakharyaschev, M.: E-connections of abstract description systems. Artificial intelligence 156(1), 1–73 (2004)
  * [19] McCarthy, J., Buvac, S.: Formalizing context (expanded notes). CSLI Lecture Notes 81, 13–50 (1998)
  * [20] Osman, I., Ben Yahia, S., Diallo, G.: Ontology Integration: Approaches and Challenging Issues. Information Fusion 71, 38–63 (2021)
  * [21] Otero-Cerdeira, L., Rodríguez-Martínez, F.J., Gómez-Rodríguez, A.: Ontology matching: A literature review. Expert Systems with Applications 42(2) (2015)
  * [22] Pesquita, C., Faria, D., Santos, E., Couto, F.M.: To repair or not to repair: Reconciling correctness and coherence in ontology reference alignments. In: Procs. of the 8th Int. Conf. on Ontology Matching. vol. 1111, pp. 13–24. CEUR (2013)
  * [23] Pietruszczak, A.: Simplified Kripke style semantics for modal logics K45, KB4 and KD45. Bulletin of the Section of Logic 38(3/4), 163–171 (2009)
  * [24] Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. Journal of Symbolic Computation 2(3), 293–304 (1986)
  * [25] Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. Journal of Logic, Language, and Information 14(3), 369–395 (2005)
  * [26] Ribière, M., Dieng-Kuntz, R.: A viewpoint model for cooperative building of an Ontology. In: Procs. of the 10th Int. Conf. on Conceptual Structures. pp. 220–234. Springer (2002)
  * [27] Rudolph, S., Krötzsch, M., Hitzler, P.: Cheap Boolean role constructors for description logics. In: Hölldobler, S., Lutz, C., Wansing, H. (eds.) Procs. of the 11th European Conf. on Logics in Artificial Intelligence. vol. 5293, pp. 362–374. Springer (2008)
  * [28] Rudolph, S., Simkus, M.: The triguarded fragment of first-order logic. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) Procs. of the 22nd Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 57, pp. 604–619 (2018)
  * [29] Solimando, A., Jiménez-Ruiz, E., Guerrini, G.: Minimizing conservativity violations in ontology alignments. Knowledge and Information Systems 51(3) (2017)
  * [30] Wolter, F., Zakharyaschev, M.: On the decidability of description logics with modal operators. In: Cohn, A.G., Schubert, L.K., Shapiro, S.C. (eds.) Procs. of the Sixth Int. Conf. on Principles of Knowledge Representation and Reasoning. pp. 512–523. Morgan Kaufmann (1998)
  * [31] Álvarez, L.G., Rudolph, S., Strass, H.: How to Agree to Disagree: Managing Ontological Perspectives using Standpoint Logic. Tech. rep., arXiv.org (2022)

##  Appendix 0.A Translation to SSNF

Suppose $\phi$ is a FOSL formula to be translated to SSNF. We provide in what
follows a structure-preserving transformation in the spirit of Tseitin
transformations.

######  Definition 8 (Translation to SSNF)

Recall that a _literal_ is a formula of the form $P(\vec{t}\,)$ or $\neg
P(\vec{t}\,)$, where $P(\vec{t}\,)$ is an atom. For any FOSL formula $\psi$,
let $L_{\psi}$ denote a newly introduced literal $P_{\psi}(x_{1},\dots,x_{m})$
where $x_{1},\dots,x_{m}$ are the free variables in $\psi$, if $\psi$ is not
of the form $\neg\xi$. Otherwise, $L_{\psi}$ is $\neg L_{\xi}$.

The structure-preserving standard translation of a FOSL formula $\phi$,
denoted $SS(\phi)$ is defined by induction via $SS(\phi)=\phi$ for each
literal $\phi$, and for compound formulas via
$SS(\phi)=L_{\phi}\wedge\phi^{+}$, where

  * •

$(\psi\mbox{$\ \wedge\ $}\xi)^{+}=(L_{\psi\wedge\xi}\mbox{$\ \rightarrow\
$}L_{\psi}\mbox{$\ \wedge\ $}L_{\xi})\mbox{$\ \wedge\ $}\psi^{+}\mbox{$\
\wedge\ $}\xi^{+}$

  * •

$(\psi\mbox{$\ \vee\ $}\xi)^{+}=(L_{\psi\vee\xi}\mbox{$\ \rightarrow\
$}L_{\psi}\mbox{$\ \vee\ $}L_{\xi})\mbox{$\ \wedge\ $}\psi^{+}\mbox{$\ \wedge\
$}\xi^{+}$

  * •

$(\neg\psi)^{+}=(\psi)^{-}$

  * •

$(\forall x\psi)^{+}=(L_{\forall x\psi}\mbox{$\ \rightarrow\ $}\forall
xL_{\psi})\mbox{$\ \wedge\ $}\psi^{+}$

  * •

$(\exists x\psi)^{+}=(L_{\exists x\psi}\mbox{$\ \rightarrow\ $}\exists
xL_{\psi})\mbox{$\ \wedge\ $}\psi^{+}$

  * •

$(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{+}=(L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\mbox{$\
\rightarrow\ $}\mathop{\square}\nolimits_{\mathsf{e}}L_{\psi})\mbox{$\ \wedge\
$}\psi^{+}$

  * •

$(\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi)^{+}=(L_{\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi}\mbox{$\
\rightarrow\ $}\mathop{\lozenge}\nolimits_{\mathsf{e}}L_{\psi})\mbox{$\
\wedge\ $}\psi^{+}$

and their homologous negative polarity definitions:

  * •

$(\psi\mbox{$\ \wedge\ $}\xi)^{-}=(L_{\psi\wedge\xi}\leftarrow
L_{\psi}\mbox{$\ \wedge\ $}L_{\xi})\mbox{$\ \wedge\ $}\psi^{-}\mbox{$\ \wedge\
$}\xi^{-}$

  * •

$(\psi\mbox{$\ \vee\ $}\xi)^{-}=(L_{\psi\vee\xi}\leftarrow L_{\psi}\mbox{$\
\vee\ $}L_{\xi})\mbox{$\ \wedge\ $}\psi^{-}\mbox{$\ \wedge\ $}\xi^{-}$

  * •

$(\neg\psi)^{-}=(\psi)^{+}$

  * •

$(\forall x\psi)^{-}=(L_{\forall x\psi}\leftarrow\forall xL_{\psi})\mbox{$\
\wedge\ $}\psi^{-}$

  * •

$(\exists x\psi)^{-}=(L_{\exists x\psi}\leftarrow\exists xL_{\psi})\mbox{$\
\wedge\ $}\psi^{-}$

  * •

$(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{-}=(L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\leftarrow\mathop{\square}\nolimits_{\mathsf{e}}L_{\psi})\mbox{$\
\wedge\ $}\psi^{-}$

  * •

$(\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi)^{-}=(L_{\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi}\leftarrow\mathop{\lozenge}\nolimits_{\mathsf{e}}L_{\psi})\mbox{$\
\wedge\ $}\psi^{-}$

We now show the correctness of the transformation.

###### Lemma 4

For all first-order standpoint formulas $\phi$,

$\models(L_{\phi}\mbox{$\ \wedge\ $}\phi^{+})\mbox{$\ \rightarrow\
$}\phi\text{ and }\models(\neg L_{\phi}\mbox{$\ \wedge\ $}\phi^{-})\mbox{$\
\rightarrow\ $}\neg\phi.$

###### Proof

In this case, we refer to the proof provided by Plaisted and Greenbaum [24].
The proof is by induction on the structure of $\phi$, and needs to be extended
by showing that the following formulas are valid:

  * •

$L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\mbox{$\ \wedge\
$}(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{+}\mbox{$\ \rightarrow\
$}\mathop{\square}\nolimits_{\mathsf{e}}\psi$

  * •

$\neg L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\mbox{$\ \wedge\
$}(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{-}\mbox{$\ \rightarrow\
$}\neg\mathop{\square}\nolimits_{\mathsf{e}}\psi$

  * •

$L_{\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi}\mbox{$\ \wedge\
$}(\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi)^{+}\mbox{$\ \rightarrow\
$}\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi$

  * •

$\neg L_{\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi}\mbox{$\ \wedge\
$}(\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi)^{-}\mbox{$\ \rightarrow\
$}\neg\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi$

We first show that $L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\mbox{$\
\wedge\ $}(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{+}\mbox{$\
\rightarrow\ $}\mathop{\square}\nolimits_{\mathsf{e}}\psi$ is valid.

  1. 1.

By definition $(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{+}$ is
$(L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\mbox{$\ \rightarrow\
$}\mathop{\square}\nolimits_{\mathsf{e}}L_{\psi})\mbox{$\ \wedge\ $}\psi^{+}$.

  2. 2.

By induction hypothesis we know that $\models(L_{\psi}\mbox{$\ \wedge\
$}\psi^{+})\mbox{$\ \rightarrow\ $}\psi$.

  3. 3.

Let us then assume $L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\mbox{$\
\wedge\ $}(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{+}$.

  4. 4.

By (1), we get $(\mathop{\square}\nolimits_{\mathsf{e}}L_{\psi})\mbox{$\
\wedge\ $}\psi^{+}$.

  5. 5.

Now, note that $\psi^{+}$ is not embedded by any modal operator, and hence by
the semantics, $\psi^{+}$ holds for all precisifications.

  6. 6.

Then, by (4) and (5), $L_{\psi}\mbox{$\ \wedge\ $}\psi^{+}$ holds for all
precisifications belonging to $\mathsf{e}$.

  7. 7.

Thus, by (2), we get $\mathop{\square}\nolimits_{\mathsf{e}}\psi$ as desired.

We now show that $\neg L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\mbox{$\
\wedge\ $}(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{-}\mbox{$\
\rightarrow\ $}\neg\mathop{\square}\nolimits_{\mathsf{e}}\psi$ is valid.

  1. 1.

By definition $(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{-}$ is
$(L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\leftarrow\mathop{\square}\nolimits_{\mathsf{e}}L_{\psi})\mbox{$\
\wedge\ $}\psi^{-}$.

  2. 2.

By induction hypothesis we know that $\models(\neg L_{\psi}\mbox{$\ \wedge\
$}\psi^{-})\mbox{$\ \rightarrow\ $}\neg\psi$.

  3. 3.

Let us then assume $\neg
L_{\mathop{\square}\nolimits_{\mathsf{e}}\psi}\mbox{$\ \wedge\
$}(\mathop{\square}\nolimits_{\mathsf{e}}\psi)^{-}$.

  4. 4.

By (1), we get $(\neg\mathop{\square}\nolimits_{\mathsf{e}}L_{\psi})\mbox{$\
\wedge\ $}\psi^{-}$.

  5. 5.

Now, note that $\psi^{-}$ is not embedded by any modal operator, and hence by
the semantics, $\psi^{-}$ holds for all precisifications.

  6. 6.

Then, by (4) and (5),$\neg L_{\psi}\mbox{$\ \wedge\ $}\psi^{-}$ holds for all
precisifications belonging to $\mathsf{e}$.

  7. 7.

Thus, by (2), we get $\neg\mathop{\square}\nolimits_{\mathsf{e}}\psi$ as
desired.

The proof for the cases with $\mathop{\lozenge}\nolimits_{\mathsf{e}}\psi$ is
analogous to those with $\mathop{\square}\nolimits_{\mathsf{e}}\psi$.

###### Lemma 5

Suppose $\mathfrak{M}$ is a model of $\phi$. Let $\mathfrak{M}^{\prime}$ be an
interpretation such that for all subformulas $\psi$ of $\phi$,
$\mathfrak{M}^{\prime}\models L_{\psi}\leftrightarrow\psi$. Suppose
$\mathfrak{M}^{\prime}$ interprets any such $\psi$ to be true exactly when
$\mathfrak{M}$ does. Then for all subformulas $\psi$ of $\phi$,
$\mathfrak{M}^{\prime}\models\psi^{+}$ and
$\mathfrak{M}^{\prime}\models\psi^{-}$.

###### Proof

Again we extend the inductive proof of Plaisted and Greenbaum [24].

We consider the case for $\psi=\mathop{\square}\nolimits_{\mathsf{e}}\xi$ and
show $\mathfrak{M}^{\prime}\models\psi^{+}$, the other cases are analogous.
Recall that, by definition, $\psi^{+}$ is
$(L_{\mathop{\square}\nolimits_{\mathsf{e}}\xi}\mbox{$\ \rightarrow\
$}\mathop{\square}\nolimits_{\mathsf{e}}L_{\xi})\mbox{$\ \wedge\ $}\xi^{+}$.

  1. 1.

By induction, $\mathfrak{M}^{\prime}\models\xi^{+}$.

  2. 2.

By assumption, $\mathfrak{M}^{\prime}\models
L_{\mathop{\square}\nolimits_{\mathsf{e}}\xi}\leftrightarrow(\mathop{\square}\nolimits_{\mathsf{e}}\xi)$,

  3. 3.

By assumption also $\mathfrak{M}^{\prime}\models L_{\xi}\leftrightarrow\xi$.

  4. 4.

By (2) and (3) we obtain $\mathfrak{M}^{\prime}\models
L_{\mathop{\square}\nolimits_{\mathsf{e}}\xi}\mbox{$\ \rightarrow\
$}\mathop{\square}\nolimits_{\mathsf{e}}L_{\xi}$.

  5. 5.

Then, together with (1) we get
$\mathfrak{M}^{\prime}\models(L_{\mathop{\square}\nolimits_{\mathsf{e}}\xi}\mbox{$\
\rightarrow\ $}\mathop{\square}\nolimits_{\mathsf{e}}L_{\xi})\mbox{$\ \wedge\
$}\xi^{+}$ as desired.

###### Lemma 6

If $\phi$ is satisfiable, then so is $L_{\phi}\mbox{$\ \wedge\ $}\phi^{+}$. If
$\neg\phi$ is satisfiable, then so is $\neg L_{\phi}\mbox{$\ \wedge\
$}\phi^{-}$.

###### Proof

Let $\mathfrak{M}$ be a model of $\phi$. Let $\mathfrak{M}^{\prime}$ be as in
Lemma 5. Then, $\mathfrak{M}^{\prime}\models\phi^{+}$ by Lemma 5. Also,
$\mathfrak{M}^{\prime}\models L_{\phi}$ by the way it is defined. Thus,
$\mathfrak{M}^{\prime}\models L_{\phi}\mbox{$\ \wedge\ $}\phi^{+}$, which is
hence shown to be satisfiable. A similar argument works for
$\mathfrak{M}^{\prime}\models\neg L_{\phi}\mbox{$\ \wedge\ $}\phi^{-}$.

###### Theorem 0.A.1

A first-order standpoint formula $\phi$ is satisfiable iff $L_{\phi}\mbox{$\
\wedge\ $}\phi^{+}$ is satisfiable and $\neg\phi$ is satisfiable iff $\neg
L_{\phi}\mbox{$\ \wedge\ $}\phi^{-}$ is satisfiable.

###### Proof

Combine Lemma 4 and Lemma 6.

###### Corollary 3

A first-order standpoint formula $\phi$ is satisfiable iff $SS(\phi)$ is
satisfiable.

###### Lemma 7

The translation $SS(\phi)$ of a first-order standpoint formula $\phi$ is in
SSNF.

###### Proof

It is easy to see that the nesting depth of modal operators in $SS(\phi)$ is
at most 1, since it is a conjunction, where every conjunct contains at most
one such operator.

###### Remark 1

Note that if the standpoint formulas are given in NNF, then we can apply the
translation merely using the positive polarity.

##  Appendix 0.B $\mathcal{SROIQ}b_{s}$ Translation Equisatisfiability

Given a “plain” DL interpretation $\mathcal{I}$ of the resulting vocabulary
over a domain $\Delta$, the associated standpoint structure
$\mathfrak{M}_{\mathcal{I}}=\mbox{$\langle\Delta,\Pi_{n},\sigma,\gamma\rangle$}$
is as follows:

  * •

$c^{\gamma(\pi)}=c^{\mathcal{I}}$ for $c\in\mathcal{C}$.

  * •

$\sigma(s)=\left\\{\pi\in\Pi_{n}\mathrel{\left.\middle|\right.}(\mathtt{M}^{\mathsf{s}}_{\pi})^{\mathcal{I}}=\Delta\right\\}$
and

  * •

$\gamma(\pi)$ is the interpretation function defined by

    * –

$\mathtt{A}^{\gamma(\pi)}=\mathtt{A}_{\\!\pi}^{\mathcal{I}}$ for
$\mathtt{A}\in\mathcal{P}_{1}$,

    * –

$\mathtt{r}^{\gamma(\pi)}=\mathtt{r}_{\\!\pi}^{\mathcal{I}}$ for
$\mathtt{r}\in\mathcal{P}_{2}$,

    * –

$\mathtt{s}^{\gamma(\pi)}=\mathtt{s}_{\\!\pi}^{\mathcal{I}}$ for each
$\mathtt{s}{\,\in\,}\mathcal{P}^{\mathrm{s}}_{2}$;

    * –

for each $\mathtt{r}{\,\in\,}\mathcal{P}^{\mathrm{ns}}_{2}$, we let
$\mathtt{s}^{\gamma(\pi)}$ be the transitive closure of
$(\underline{\mathtt{r}}^{\pi})^{\mathcal{I}}$ whenever $\mathtt{r}\hskip
1.0pt{\circ}\hskip 1.0pt\mathtt{r}{\,\sqsubseteq\,}\mathtt{r}$ occurs in
$\phi$ and $\exists\mathtt{s}^{\pi}_{\mathtt{r}\hskip 1.0pt{\circ}\hskip
1.0pt\mathtt{r}{\,\sqsubseteq\,}\mathtt{r}}.\mathit{Self}^{\mathcal{I}}=\Delta$;
otherwise we let
$\mathtt{s}^{\gamma(\pi)}=(\underline{\mathtt{r}}^{\pi})^{\mathcal{I}}$.

For the converse direction, given some
$\mathfrak{M}=\mbox{$\langle\Delta,\Pi,\sigma,\gamma\rangle$}$ with $|\Pi|=n$,
we can w.l.o.g. assume $\Pi=\Pi_{n}$. We obtain the plain description logic
interpretation ${\mathcal{I}_{\mathfrak{M}}}$ over the domain $\Delta$ as
follows: For each constant $c\in\mathcal{C}$ we let
$c^{\mathcal{I}_{\mathfrak{M}}}=c^{\gamma(\pi)}$ for an arbitrary
$\pi\in\Pi_{n}$. Moreover, for each $\pi\in\Pi_{n}$ we define the following:

  * •

for any $s\in\mathcal{S}$, we set
${(\mathtt{M}^{\mathsf{s}}_{\pi})}^{\mathcal{I}_{\mathfrak{M}}}=\Delta$ if
$\pi\in\sigma(s)$, and set $s_{\pi}^{\mathcal{I}_{\mathfrak{M}}}=\emptyset$
otherwise;

  * •

we set
${(\mathtt{M}_{\pi}^{\hbox{$*$}})}^{\mathcal{I}_{\mathfrak{M}}}=\Delta$;

  * •

for any “original” concept name $\mathtt{A}\in\mathcal{P}_{1}$, let
$\mathtt{A}_{\\!\pi}^{\mathcal{I}_{\mathfrak{M}}}=\mathtt{A}^{\gamma(\pi)}$.

  * •

for any “original” simple role name
$\mathtt{s}{\,\in\,}\mathcal{P}^{\mathrm{s}}_{2}$, let
$\mathtt{s}_{\\!\pi}^{\mathcal{I}_{\mathfrak{M}}}=\mathtt{s}^{\gamma(\pi)}$;

  * •

for every “original” non-simple role name
$\mathtt{r}{\,\in\,}\mathcal{P}^{\mathrm{ns}}_{2}$, let
$\underline{\mathtt{r}}_{\\!\pi}^{\mathcal{I}_{\mathfrak{M}}}=\mathtt{r}_{\\!\pi}^{\mathcal{I}_{\mathfrak{M}}}=\mathtt{r}^{\gamma(\pi)}$;

  * •

for each unnegated RIA $\rho$ inside $\phi$, let
$(\mathtt{s}^{\pi}_{\rho})^{\mathcal{I}_{\mathfrak{M}}}=\\{(\delta,\delta)\mid\delta\in\Delta\\}$
if $\rho$ is satisfied by ${\gamma(\pi)}$ and
$(\mathtt{s}^{\pi}_{\rho})^{\mathcal{I}_{\mathfrak{M}}}=\emptyset$ otherwise;

  * •

for each negated RIA $\rho=r_{1}{\circ}...{\circ}\hskip
1.0ptr_{m}{\,\sqsubseteq\,}\mathtt{r}$ inside $\phi$, if $\rho$ is not
satisfied by ${\gamma(\pi)}$ pick some witnessing $(\delta,\delta^{\prime})\in
r_{1}^{\gamma(\pi)}{\circ}...{\circ}\hskip
1.0ptr_{m}^{\gamma(\pi)}\setminus\mathtt{r}^{\gamma(\pi)}$ and let
$(a^{\pi}_{\rho})^{\mathcal{I}_{\mathfrak{M}}}=\delta^{\prime}$; otherwise
(should $\rho$ be satisfied by ${\gamma(\pi)}$) pick
$(a^{\pi}_{\rho})^{\mathcal{I}_{\mathfrak{M}}}$ arbitrarily.

With these constructions we can establish the following lemma.

###### Lemma 8

Let
$\mathbb{V}=\mbox{$\langle\mathcal{P}_{1}\cup\mathcal{P}_{2},\mathcal{C},\mathcal{S}\rangle$}$
be a standpoint signature and let
$\mathbb{V}^{\prime}=\mathbb{V}_{\\!\scaleobj{0.85}{\mathcal{SROIQ}b_{s}}}(\mathcal{P}_{1}\cup\mathcal{P}_{2},\mathcal{C},\mathcal{S},\Pi_{n})$.
Then, we obtain the following for arbitrary sentential
Standpoint-$\mathcal{SROIQ}b_{s}$ sentences
$\phi\in{\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$:

  1. 1.

For any $\mathbb{V}$-standpoint structure
$\mathfrak{M}=\mbox{$\langle\Delta,\Pi_{n},\sigma,\gamma\rangle$}$ holds

$\ \mathfrak{M}\models\phi\quad\text{if and only
if}\quad\mathcal{I}_{\mathfrak{M}}\models\mathrm{Trans}(\phi).$

  2. 2.

For any $\mathbb{V}^{\prime}$-interpretation $\mathcal{I}$ holds

$\mathfrak{M}_{\mathcal{I}}\models\phi\quad\text{if and only if}\quad\ \ \
\mathcal{I}\models\mathrm{Trans}(\phi).\ \ $

From these correspondences, it follows that $\phi$ and $\mathrm{Trans}(\phi)$
are equisatisfiable for every
$\phi\in{\mathbb{S}_{\scaleobj{0.85}{[\mathcal{S\\!R\\!O\\!I\\!Q}b_{s}}\\!]}}$