# Automating Reasoning with Standpoint Logic via Nested Sequents

Tim S. Lyon  Lucía Gómez Álvarez
Computational Logic Group, Faculty of Computer Science, TU Dresden
{timothy_stephen.lyon<EMAIL_ADDRESS>
###### Abstract

Standpoint logic is a recently proposed formalism in the context of knowledge
integration, which advocates a multi-perspective approach permitting reasoning
with a selection of diverse and possibly conflicting standpoints rather than
forcing their unification. In this paper, we introduce nested sequent calculi
for propositional standpoint logics—proof systems that manipulate trees whose
nodes are multisets of formulae—and show how to automate standpoint reasoning
by means of non-deterministic proof-search algorithms. To obtain worst-case
complexity-optimal proof-search, we introduce a novel technique in the context
of nested sequents, referred to as _coloring_ , which consists of taking a
formula as input, guessing a certain coloring of its subformulae, and then
running proof-search in a nested sequent calculus on the colored input. Our
technique lets us decide the validity of standpoint formulae in
$\mathrm{CoNP}$ since proof-search only produces a _partial_ proof relative to
each permitted coloring of the input. We show how all partial proofs can be
fused together to construct a complete proof when the input is valid, and how
certain partial proofs can be transformed into a counter-model when the input
is invalid. These “certificates” (i.e. proofs and counter-models) serve as
explanations of the (in)validity of the input.

##  1 Introduction

### Standpoint Logic.

The fact that knowledge bases (KBs) encode the standpoints of their creators
(e.g. in the form of viewpoints, contextual factors or semantic commitments)
is the source of well-known challenges in the area of knowledge integration.
Since semantic heterogeneity between the sources is to be expected,
inconsistencies may arise if we attempt to combine them into a single
conflict-free conceptual model. To illustrate this, consider three KBs:
$\mathsf{C}$, a ‘common-sense’ representation of colours; $\mathsf{H}$, a KB
by a _house painting_ business that reuses and extends $\mathsf{C}$; and
$\mathsf{R}$, a KB that formalizes the _RYB color model_ , from the fine arts
tradition.

######  Example 1.

According to $\mathsf{C}$, basic colours such as Blue and Green are disjoint.
$\mathsf{H}$ complies with $\mathsf{C}$ and further specifies that Teal is
Green. In contrast, according to $\mathsf{R}$ it is unequivocal that Teal is
both Green and Blue. Generally, it is conceivable that Blue holds.

These sources cannot be merged without the undesired effect of inconsistency,
and circumventing it requires either knowledge weakening or duplication (?).
Instead, one may wish to jointly reason with the KBs, treating them as
alternative standpoints on a domain.

BlueGreen$\perp$ $\mathsf{C}$BlueGreenTeal$\perp$
$\mathsf{H}$$\preceq$TealGreenBlue $\mathsf{R}$ Figure 1: Diagrams of
$\mathsf{C}$, $\mathsf{H}$ and $\mathsf{R}$. $\preceq$ indicates that
$\mathsf{H}$ extends $\mathsf{C}$.

Standpoint logic (?) is a simple multi-modal logic intended for the
representation of knowledge relative to different, possibly conflicting,
perspectives. The framework introduces the labeled modalities
$\mathop{\square}\nolimits_{s}$ and $\mathop{\lozenge}\nolimits_{s}$ for each
standpoint $s$, where $\mathop{\square}\nolimits_{s}\varphi$ is read as
“according to $s$, it is _unequivocal_ that $\varphi$” and
$\mathop{\lozenge}\nolimits_{s}\varphi$ as “according to $s$, it is
_conceivable_ that $\varphi$”. In addition, $s\preceq s^{\prime}$ indicates
that the standpoint $s$ is _sharper_ than $s^{\prime}$, that is, $s$ complies
with $s^{\prime}$ and further specifies it.

  1. (F1)

$\mathop{\square}\nolimits_{\mathsf{C}}\neg(\mbox{\tt Blue}\\!\mbox{$\ \wedge\
$}\\!\mbox{\tt Green})\mbox{$\ \wedge\
$}\mathop{\square}\nolimits_{\mathsf{R}}(\mbox{\tt
Teal}\\!\rightarrow\\!(\mbox{\tt Blue}\\!\mbox{$\ \wedge\ $}\\!\mbox{\tt
Green}))$

(F2) $(\hbox{$\mathsf{H}$}\\!\preceq\\!\hbox{$\mathsf{C}$})$ (F3)
$\mathop{\square}\nolimits_{\mathsf{H}}(\mbox{\tt
Teal}\\!\rightarrow\\!\mbox{\tt Green})$ (F4)
$\mathop{\lozenge}\nolimits_{\mathsf{*}}(\mbox{\tt Blue})$

The formulae (F1)-(F4) formalize Example 1, (illustrated in Figure 1) in
propositional standpoint logic. (F1) encodes that Blue and Green are
unequivocally disjoint according to standpoint $\mathsf{C}$, while according
to standpoint $\mathsf{R}$ it is unequivocal that Teal implies both Blue and
Green. (F2) encodes that $\mathsf{H}$ includes the knowledge of $\mathsf{C}$,
and (F3) that Teal is Green according to $\mathsf{H}$. Last, (F4) encodes that
Blue holds under some interpretations by using the universal standpoint $*$,
which sits atop any hierarchy of standpoints and is used to reference
knowledge that is unequivocally true or conceivable among all perspectives.

In addition to representing unequivocal and conceivable facts (e.g. (F3) and
(F4)), which may be relative to standpoints (e.g. (F1)), hold universally
(e.g. (F4)), or establish a hierarchy of standpoints (e.g. (F2)), one may also
express (in)determinate knowledge by means of the (definable) dual operators
$\mathcal{I}_{s}$ and $\mathcal{D}_{s}$. The indeterminacy operator
$\mathcal{I}_{s}\varphi:=\mathop{\lozenge}\nolimits_{s}\varphi\mbox{$\ \wedge\
$}\mathop{\lozenge}\nolimits_{s}\neg\varphi\ $ makes explicit that both
$\varphi$ and $\neg\varphi$ are conceivable in the context of $s$, thus making
$\varphi$ inherently indeterminate. Finally, the framework can be used to
establish correspondences or bridges between the standpoints themselves. For
instance, (F5) encodes that if something is Teal according to $\mathsf{R}$,
then it is Green for $\mathsf{C}$ and $\mathsf{R}$.

  1. (F5)

$\mathop{\square}\nolimits_{\mathsf{R}}(\mbox{\tt
Teal})\rightarrow(\mathop{\square}\nolimits_{\mathsf{C}}\mbox{\tt
Green}\mbox{$\ \wedge\ $}\mathop{\square}\nolimits_{\mathsf{R}}\mbox{\tt
Green})$

Natural reasoning tasks over 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. To illustrate, let us assume
$\mathop{\square}\nolimits_{\mathsf{*}}\mbox{\tt Teal}$ and examine some
inferences that we can draw from this in the setting of Example 1. On the one
hand, from (F5), (F3), and $\mathop{\square}\nolimits_{\mathsf{*}}\mbox{\tt
Teal}$ we obtain that green is unequivocal for the three standpoints:
$\mathop{\square}\nolimits_{\mathsf{C}}\mbox{\tt Green}$,
$\mathop{\square}\nolimits_{\mathsf{H}}\mbox{\tt Green}$ and
$\mathop{\square}\nolimits_{\mathsf{R}}\mbox{\tt Green}$. On the other hand,
we can infer the global indeterminacy of blue
$\mathcal{I}_{\hbox{$*$}}\mbox{\tt Blue}$, because (i) Teal holds universally,
(ii) it is unequivocal for $\mathsf{R}$ that Teal implies Blue (F1), hence
$\mathop{\lozenge}\nolimits_{\mathsf{*}}\mbox{\tt Blue}$, and (iii) we know
$\mathop{\square}\nolimits_{\mathsf{C}}\mbox{\tt Green}$, which together with
(F1) implies $\mathop{\square}\nolimits_{\mathsf{C}}\neg\mbox{\tt Blue}$ and
thus $\mathop{\lozenge}\nolimits_{\mathsf{*}}\neg\mbox{\tt Blue}$.

Conveniently, the satisfiability problem in propositional standpoint logic is
known to be $\mathrm{NP}$-complete (?), in pleasant contrast to the
$\mathrm{PSPACE}$-completeness normally exhibited by multi-modal epistemic
logics, such as the closely related $\mathsf{KD45}_{n}$.111Standpoint logic
introduces sharpenings and stronger interaction axioms than
$\mathsf{KD45}_{n}$, as discussed in (?). This result, obtained via a
translation to one-variable first-order logic, makes the framework attractive
in applied scenarios, and prompts our work to provide a suitable proof-theory
for standpoint logic. Not only can our proof systems be leveraged to provide a
proof-search procedure deciding the validity of standpoint formulae, but our
proof-theoretic approach yields _witnesses_ , that is, proofs of valid
formulae and counter-models of invalid formulae. Such “certificates” (i.e.
proofs and counter-models) possess explanatory value, and may be used, for
instance, to trace the standpoints involved in a certain inference; e.g. when
a global indeterminacy such as $\mathcal{I}_{\hbox{$*$}}\mbox{\tt Blue}$ is
inferred from a large collection of standpoints, we may want to gather the
standpoints that hold contrasting views (in this case $\mathsf{R}$ and
$\\{\hbox{$\mathsf{H}$},\hbox{$\mathsf{C}$}\\}$, which can be easily extracted
from a proof). Thus, our reliance on proof theory provides essential
information that may be used to answer “why” a certain piece of information
holds while still allowing “low” complexity reasoning.

### Nested Sequents and Proof Theory.

Since their inception, sequent systems—which consist of inference rules that
syntactically manipulate pairs of multisets of formulae—have proven themselves
fruitful in writing decision algorithms for logics (?; ?; ?; ?). A crucial
feature of such systems, and their use in decidability, is the so-called
_subformula property_ , which a sequent system has iff the premise(s) of each
inference rule only contain subformulae of the conclusion of the rule. (NB.
Systems with the subformula property are also referred to as _analytic_.) With
the goal of securing this property for proof systems for theories _beyond
classical propositional logic_ (e.g. the modal logics $\mathsf{Kt}$ and
$\mathsf{S5}$), more sophisticated sequent systems extending Gentzen’s
original formalism were eventually proposed; e.g., see (?; ?; ?). In this
paper, we employ one such extended formalism, viz. the _nested sequent
formalism_ (?; ?; ?; ?), which utilizes trees of multisets of formulae in
deriving theorems. Such systems have proven well-suited for automated
reasoning with modal and related logics, being used (for instance) in the
writing of decision/proof-search algorithms (?; ?) and the extraction of
interpolants (?; ?).

Drawing on ideas from the _structural refinement_ methodology, detailed in (?)
and used to provide nested sequent systems for diverse classes of modal and
constructive logics (see (?; ?; ?)), our first contribution in this paper is
the introduction of analytic nested sequent systems (each dubbed
$\mathsf{NS}(\mathcal{V})$ with $\mathcal{V}$ a certain parameter) for
propositional standpoint logics (?). For our second contribution, we exploit
our nested systems to write concrete, _worst-case complexity-optimal_ proof-
search algorithms (deciding the validity of propositional standpoint formulae
in $\mathrm{CoNP}$), which apply inference rules from
$\mathsf{NS}(\mathcal{V})$ _in reverse_ on an input formula with the goal of
building a proof thereof. Whereas typical proof-search algorithms operate
deterministically and attempt to build a _complete_ proof of the input, we
introduce a novel technique (our third contribution) referred to as _coloring_
, which performs proof-search _non-deterministically_ and which only
constructs a _partial_ proof of the input relative to each non-deterministic
choice. The technique of coloring involves first guessing a particular
labeling of the subformulae of an input formula with _active_ $\circ$ and
_inactive_ $\bullet$ labels, with the proof-search algorithm subsequently only
processing data deemed active. An interesting consequence of this technique is
the attainment of a $\mathrm{CoNP}$ proof-search algorithm as the partial
proofs constructed during proof-search are at most polynomially larger than
the input and only require polynomial time to compute. Moreover, in the
instance where the input formula is invalid, we show how to construct a
counter-model from failed proof-search, and in the instance where our input
formula is valid, we provide a procedure that generates a _complete_ proof
witnessing the validity of the input formula by patching together all
_partial_ proofs (our fourth contribution).

### Organization of Paper.

Our paper is organized as follows: Sect. 2 presents the syntax and semantics
of propositional standpoint logic. In Sect. 3, we introduce our nested sequent
systems for propositional standpoint logics, proving such systems sound and
concluding their completeness. In the penultimate section (Sect. 4), we
introduce the method of coloring and show how to automate reasoning with
standpoint logics, that is, we provide a (worst-case complexity-optimal)
proof-search algorithm deciding the validity of propositional standpoint
formulae in $\mathrm{CoNP}$. The final section (Sect. 5) concludes the paper
and discusses future work.

##  2 Standpoint Logic

Let us now specify the syntax of propositional standpoint logic (SL), denoted
by ${\mathbb{S}}$.

######  Definition 1 (Syntax of Standpoint Logic).

Let $\mathcal{V}=\langle\mathcal{P},\mathcal{S}\rangle$ be a _vocabulary_
where $\mathcal{P}$ is a non-empty set of propositional variables and
$\mathcal{S}$ is a set of standpoint symbols containing the distinguished
symbol $\ast$, i.e. the _universal standpoint_. We define the language
$\mathcal{L}_{\preceq}:=\\{s\preceq s^{\prime}\ |\
s,s^{\prime}\in\mathcal{S}\\}$, and refer to formulae in
$\mathcal{L}_{\preceq}$ as _sharpening statements_. The language
$\mathcal{L}_{\mathcal{V}}$ is defined via the following grammar in BNF:

$\varphi::=p\ |\ \neg p\ |\ (\varphi\lor\varphi)\ |\ (\varphi\land\varphi)\ |\
\mathop{\square}\nolimits_{s}\varphi\ |\
\mathop{\lozenge}\nolimits_{s}\varphi$

where $p\in\mathcal{P}$ and $s\in\mathcal{S}$. We also use $\top$ and $\bot$
as shorthands with the usual definitions.

Last, for $\Gamma\subseteq\mathcal{L}_{\preceq}$ and
$\varphi\in\mathcal{L}_{\mathcal{V}}$, we define a _standpoint implication_ to
be a formula of the form $\bigwedge\Gamma\rightarrow\varphi$, where
$\bigwedge\Gamma$ is a conjunction of all elements of $\Gamma$, which equals
$\top$ when $\Gamma$ is empty.

We make use of formulae in negation normal form as this will simplify the
structures present in our nested systems and enhance the readability of our
proof theory. To further simplify, we also assume w.l.o.g. that sets of
sharpening statements are (1) free of cycles $s_{1}\preceq
s_{2},\ldots,s_{n}\preceq s_{1}$ and (2) omit occurrences of $*$. Assumption
(1) is permitted since any standpoint implication containing a cycle
$s_{1}\preceq s_{2},\ldots,s_{n}\preceq s_{1}$ of standpoints is equivalent to
one where the cycle is deleted and all occurrences of $s_{1},\ldots,s_{n-1}$
are replaced by $s_{n}$ in the formula. Regarding assumption (2), any
sharpening statement with $*$ is either of the form $s\preceq\hbox{$*$}$, and
is thus trivial (see Def. 4 below), or is of the form $\hbox{$*$}\preceq s$,
in which case $s$ can be systematically replaced by $*$ in a standpoint
implication to obtain an equivalent one.

######  Definition 2 (Subformula and Size).

We define the set of _subformulae_ of $\varphi$, denoted
$\mathrm{sufo}(\varphi)$, recursively as follows:

  * •

$\mathrm{sufo}(p):=\\{p\\}$ and $\mathrm{sufo}(\neg p):=\\{\neg p\\}$;

  * •

$\mathrm{sufo}(\heartsuit\psi):=\\{\heartsuit\psi\\}\cup\mathrm{sufo}(\psi)$;

  * •

$\mathrm{sufo}(\psi\otimes\chi):=\\{\psi\otimes\chi\\}\cup\mathrm{sufo}(\psi)\cup\mathrm{sufo}(\chi)$.

with
$\heartsuit\in\\{\mathop{\lozenge}\nolimits_{s},\mathop{\square}\nolimits_{s}\
|\ s\in\mathcal{S}\\}$ and $\otimes\in\\{\lor,\land\\}$. We say that $\psi$ is
a _subformula_ of $\varphi$ iff $\psi\in\mathrm{sufo}(\varphi)$, and define
the _size_ of a formula $\varphi$ in $\mathcal{L}_{\mathcal{V}}$, denoted
$|\varphi|$, to be equal to $|\mathrm{sufo}(\varphi)|$, i.e. to the number of
its subformulae.

In what follows, we introduce the semantics of SL, defined over a structure of
precisifications, which is akin to the usual structure of possible worlds. A
_precisification_ is a complete and consistent way in which the state of
affairs can be described with a given vocabulary, and standpoints are modeled
as sets of precisifications considered admissible. This strategy of modelling
the variability of natural language as hyper-ambiguity is based on the theory
supervaluationism (?; ?), which standpoint logic draws from (?; ?).

######  Definition 3 (Standpoint Model).

Given a vocabulary $\mathcal{V}$, a model $\mathcal{M}$ (over $\mathcal{V}$)
is a triple $\langle\Pi,\sigma,\delta\rangle$, where $\Pi$ is a non-empty set
of precisifications, $\sigma:\mathcal{S}\to 2^{\Pi}$, and
$\delta:\mathcal{P}\to 2^{\Pi}$ with $\sigma(s)\neq\emptyset$ for all
$s\in\mathcal{S}$ and $\sigma(\ast)=\Pi$. The set of all such models is
denoted by $\mathfrak{M}_{{\mathbb{S}}}$.

######  Definition 4 (Semantic Clauses).

Let $\Gamma\subseteq\mathcal{L}_{\preceq}$ and
$\varphi,\psi\in\mathcal{L}_{\mathcal{V}}$. Moreover, let
$\mathcal{M}=\langle\Pi,\sigma,\delta\rangle$ be a standpoint model with
$\pi\in\Pi$. We recursively define the satisfaction of a formula on
$\mathcal{M}$ at $\pi$ accordingly:

  * •

$\mathcal{M},\pi\models p$ iff $\pi\in\delta(p)$;

  * •

$\mathcal{M},\pi\models\neg p$ iff $\pi\not\in\delta(p)$;

  * •

$\mathcal{M},\pi\models\varphi\land\psi$ iff $\mathcal{M},\pi\models\varphi$
and $\mathcal{M},\pi\models\psi$;

  * •

$\mathcal{M},\pi\models\varphi\lor\psi$ iff $\mathcal{M},\pi\models\varphi$ or
$\mathcal{M},\pi\models\psi$;

  * •

$\mathcal{M},\pi\models\mathop{\lozenge}\nolimits_{s}\varphi$ iff for some
$\pi^{\prime}\in\sigma(s)$, $\mathcal{M},\pi^{\prime}\models\varphi$;

  * •

$\mathcal{M},\pi\models\mathop{\square}\nolimits_{s}\varphi$ iff for all
$\pi^{\prime}\in\sigma(s)$, $\mathcal{M},\pi^{\prime}\models\varphi$;

  * •

$\mathcal{M},\pi\models s\preceq s^{\prime}$ iff
$\sigma(s)\subseteq\sigma(s^{\prime})$;

  * •

$\mathcal{M},\pi\models\bigwedge\Gamma$ iff $\mathcal{M},\pi\models s\preceq
s^{\prime}$ for all $s\preceq s^{\prime}\in\Gamma$;

  * •

$\mathcal{M},\pi\models\bigwedge\Gamma\rightarrow\varphi$ iff
$\mathcal{M},\pi\models\bigwedge\Gamma$ implies
$\mathcal{M},\pi\models\varphi$;

  * •

$\mathcal{M}\models\bigwedge\Gamma\rightarrow\varphi$ iff
$\mathcal{M},\pi\models\bigwedge\Gamma\rightarrow\varphi$ for all $\pi\in\Pi$.

A standpoint implication $\bigwedge\Gamma\rightarrow\varphi$ is defined to be
_valid_ (relative to a vocabulary $\mathcal{V}$) iff it is true on each model
$\mathcal{M}\in\mathfrak{M}_{{\mathbb{S}}}$; it is defined to be _invalid_
(relative to $\mathcal{V}$) otherwise.

For a vocabulary $\mathcal{V}$, the _standpoint logic_
${\mathbb{S}}(\mathcal{V})$ is the set of all valid standpoint implications
$\bigwedge\Gamma\rightarrow\varphi$ over $\mathfrak{M}_{{\mathbb{S}}}$.

It is worth remarking that the specification of sharpening statements in a
separate language (viz. $\mathcal{L}_{\preceq}$) and the above definition of
satisfiability and validity contrast with the original presentation in (?).
However, this specification simplifies our treatment of sharpening statements,
which previously served as atomic propositions in the language
$\mathcal{L}_{\mathcal{V}}$. In fact, these statements are obsolete in
extensions of the language allowing set theoretical combinations of
standpoints in modalities (which is the object of current research). Moreover,
in these extensions, the natural requirement of inner consistency (i.e. the
non-emptiness of $\sigma(s)$, for each $s\in\mathcal{S}$) of standpoints is
relaxed, which can be easily reflected in our nested sequent systems by
dropping the $(n_{s})$ rule (see Fig. 2 in Section 3).

##  3 Nested Sequent Systems

We define a _nested sequent_ (which we will also refer to as a _sequent_) to
be a formula of the form $\Gamma\vdash\Delta$ with $\Gamma$ and $\Delta$
defined via the following grammars in BNF:

$\Gamma::=s\preceq s^{\prime}\ |\ \emptyset\ |\
\Gamma,\Gamma\quad\Delta::=\Sigma\ |\ \Delta,(s)[\Sigma]_{\pi}$
$\Sigma::=\varphi\ |\ \emptyset\ |\ \Sigma,\Sigma$

where $s,s^{\prime}\in\mathcal{S}\setminus\\{\ast\\}$,
$\varphi\in\mathcal{L}_{\mathcal{V}}$, and $\pi$ is among a countably infinite
set of labels $\\{\pi_{i}\ |\ i\in\mathbb{N}\setminus\\{0\\}\\}$. We use
$\Phi$ and $\Psi$ (occasionally annotated) to denote nested sequents and note
that we employ the use of labels as this proves useful in extracting a
counter-model from failed proof-search (see Thm. 3). Moreover, each nested
sequent $\Gamma\vdash\Delta$ with
$\Delta=\Sigma_{0},(s_{1})[\Sigma_{1}]_{\pi_{1}},\ldots,(s_{n})[\Sigma_{n}]_{\pi_{n}}$
possesses a special structure; namely, the _antecedent_ $\Gamma$ is a set of
sharpening statements of the form $s\preceq s^{\prime}$, and the _consequent_
$\Delta$ is a multiset encoding a tree of depth 1 whose nodes are multisets of
formulae from $\mathcal{L}_{\mathcal{V}}$. The consequent $\Delta$ can be
expressed graphically as follows:

$\textstyle{\Sigma_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{s_{1}}$$\scriptstyle{s_{2}}$$\scriptstyle{s_{n-1}}$$\scriptstyle{s_{n}}$$\textstyle{\Sigma_{1}}$$\textstyle{\Sigma_{2}}$$\textstyle{\ldots}$$\textstyle{\Sigma_{n-1}}$$\textstyle{\Sigma_{n}}$
---

We refer to a multiset $\Sigma_{i}$ occurring in the consequent of a nested
sequent as a _component_ , and note that components (along with the antecedent
and consequent) are permitted to be empty $\emptyset$. Intuitively, components
correspond to precisifications in a standpoint model. It is also worthwhile to
define the relation $\preceq^{*}_{\Gamma}$ on standpoints as this will be used
as a side condition dictating applications of certain inference rules:

######  Definition 5.

For a nested sequent $\Gamma\vdash\Delta$, let
$\preceq^{*}_{\Gamma}\mathop{\subseteq}\mathcal{S}\times\mathcal{S}$ be the
minimal reflexive and transitive relation such that

  * •

$s\preceq^{*}_{\Gamma}s^{\prime}$ for every $s\preceq s^{\prime}\in\Gamma$,
and

  * •

$s\preceq^{*}_{\Gamma}*$ for every $s\in\mathcal{S}$.

A nice feature of nested sequents is that such objects typically permit a
formula translation, e.g. (?; ?; ?; ?), meaning that our logical semantics can
be lifted to the language of our proof systems without introducing an extended
semantics for nested sequents.

######  Definition 6 (Formula Interpretation).

We define the _formula interpretation_ of a nested sequent
$\Gamma\vdash\Delta$ with
$\Delta=\Sigma_{0},(s_{1})[\Sigma_{1}]_{\pi_{1}},\ldots,(s_{n})[\Sigma_{n}]_{\pi_{n}}$
as follows:

$\iota(\Gamma\vdash\Delta):=\bigwedge\Gamma\rightarrow\bigvee\Sigma_{0}\lor\bigvee_{1\leq
i\leq n}\mathop{\square}\nolimits_{s_{i}}(\bigvee\Sigma_{i})$

We define $\Gamma\vdash\Delta$ to be valid iff $\iota(\Gamma\vdash\Delta)$ is
valid. Also, we note that $\bigwedge\emptyset=\top$ and
$\bigvee\emptyset=\bot$, as usual.

A uniform presentation of our nested calculi is given in Fig. 2. We let
$\mathsf{NS}(\mathcal{V})$ denote the corresponding nested sequent calculus
over a vocabulary $\mathcal{V}$. Our inference rules make use of the brackets
‘$\\{$’ and ‘$\\}$’ in the consequent of a nested sequent to indicate that the
displayed formula(e) occur in some component. In particular, given a nested
sequent $\Gamma\vdash\Delta$, where $\Delta$ is of the form
$\Sigma_{0},(s_{1})[\Sigma_{1}]_{\pi_{1}},\ldots,(s_{i})[\Sigma_{i}]_{\pi_{i}},\ldots,(s_{n})[\Sigma_{n}]_{\pi_{n}}$,
the notation $\Gamma\vdash\Delta\\{\varphi\\}_{\pi_{i}}$ indicates that
$\varphi$ occurs in $\Sigma_{i}$; additionally, we use
$\Gamma\vdash\Delta\\{\varphi\\}_{\pi_{0}}$ to indicate that $\varphi$ occurs
in $\Sigma_{0}$, i.e. the label $\pi_{0}$ is used to reference the multiset
$\Sigma_{0}$ serving as the root of the tree encoded by the consequent.

$(id)$ $\Gamma\vdash\Delta\\{p,\neg p\\}_{\pi}$ |  $\Gamma\vdash\Delta\\{\varphi\\}_{\pi}$ $\Gamma\vdash\Delta\\{\psi\\}_{\pi}$ $(\land)$ $\Gamma\vdash\Delta\\{\varphi\land\psi\\}_{\pi}$
---|---

$\Gamma\vdash\Delta\\{\mathop{\square}\nolimits_{s}\varphi\\}_{\pi},(s)[\varphi]_{\pi^{\prime}}$ $(\mathop{\square}_{s})^{{\dagger}_{1}}$ $\Gamma\vdash\Delta\\{\mathop{\square}\nolimits_{s}\varphi\\}_{\pi}$ |  $\Gamma\vdash\Delta,(s)[\emptyset]_{\pi^{\prime}}$ $(n_{s})^{{\dagger}_{1}}$ $\Gamma\vdash\Delta$
---|---

$\Gamma\vdash\Delta\\{\mathop{\lozenge}\nolimits_{s}\varphi\\}_{\pi},(s^{\prime})[\Sigma,\varphi]_{\pi^{\prime}}$ $(\mathop{\lozenge}_{s}^{1})^{{\dagger}_{2}}$ $\Gamma\vdash\Delta\\{\mathop{\lozenge}\nolimits_{s}\varphi\\}_{\pi},(s^{\prime})[\Sigma]_{\pi^{\prime}}$ |  $\Gamma\vdash\varphi,\Delta\\{\mathop{\lozenge}\nolimits_{*}\varphi\\}_{\pi}$ $(\mathop{\lozenge}_{*})$ $\Gamma\vdash\Delta\\{\mathop{\lozenge}\nolimits_{*}\varphi\\}_{\pi}$
---|---

Figure 2: The nested calculus $\mathsf{NS}(\mathcal{V})$ with
$\mathcal{V}=\langle\mathcal{P},\mathcal{S}\rangle$ a vocabulary. We note that
$\pi$ is permitted to be any label from $\\{\pi_{i}\ |\
i\in\mathbb{N}\setminus\\{0\\}\\}$ and that $\mathsf{NS}(\mathcal{V})$
contains a copy of $(\mathop{\square}_{s})$, $(n_{s})$,
$(\mathop{\lozenge}_{s}^{1})$, and $(\mathop{\lozenge}_{s}^{2})$ for each
$s\in\mathcal{S}$. The side condition ${\dagger}_{1}$ stipulates that the rule
is applicable only if the label $\pi^{\prime}$ is fresh and ${\dagger}_{2}$
stipulates that the rule is applicable only if
$s^{\prime}\preceq^{*}_{\Gamma}s$.

To make the functionality of each rule in $\mathsf{NS}(\mathcal{V})$ precise,
we explicitly state the operation performed by each rule. With the exception
of the premise-free $(id)$ rule, we explain for each rule how the _premise(s)_
(the nested sequent(s) occurring above the horizontal inference line) are
obtained from the _conclusion_ (the nested sequent occurring below the
horizontal inference line). This explanation is consistent with how the rules
are applied (bottom-up) during proof-search as described in the following
section. Also, in accordance with standard proof-theoretic terminology (?; ?),
we refer to the formula that is explicitly displayed in the conclusion of a
rule as _principal_ , and indicate the principal formulae in our explanation
of the rules below to make this precise for the reader.

$(id)$

A nested sequent is _initial_ , and may be used to begin a derivation, so long
as some component contains both $p$ and $\neg p$ (the principal formulae);

$(\lor)$

If a component $\Sigma_{i}$ of the conclusion contains $\varphi\lor\psi$ (the
principal formula), then adding $\varphi$ and $\psi$ to $\Sigma_{i}$ yields
the premise;

$(\land)$

If a component $\Sigma_{i}$ of the conclusion contains $\varphi\land\psi$ (the
principal formula), then adding $\varphi$ to $\Sigma_{i}$ yields the left
premise and adding $\psi$ to $\Sigma_{i}$ yields the right premise;

$(\mathop{\square}_{s})$

For any $s\in\mathcal{S}$, if a component $\Sigma_{i}$ of the conclusion
contains $\mathop{\square}\nolimits_{s}\varphi$ (the principal formula), then
appending the consequent $\Delta$ with $(s)[\varphi]_{\pi^{\prime}}$, where
$\pi^{\prime}$ is fresh (i.e. it does not occur in the conclusion), yields the
premise;

$(n_{s})$

For any $s\in\mathcal{S}$, we may append the consequent of the conclusion with
$(s)[\emptyset]_{\pi^{\prime}}$ to obtain the premise so long as
$\pi^{\prime}$ is fresh;

$(\mathop{\lozenge}_{s}^{1})$

For any $s\in\mathcal{S}$, if a component $\Sigma_{i}$ of the conclusion
contains $\mathop{\lozenge}\nolimits_{s}\varphi$ (the principal formula), the
consequent contains a nesting $(s^{\prime})[\Sigma]_{\pi^{\prime}}$, and
$s^{\prime}\preceq^{*}_{\Gamma}s$, then adding $\varphi$ to the nesting
$(s^{\prime})[\Sigma]_{\pi^{\prime}}$ yields the premise;

$(\mathop{\lozenge}_{s}^{2})$

For any $s\in\mathcal{S}$, if the consequent contains a nesting of the form
$(s^{\prime})[\mathop{\lozenge}\nolimits_{s}\varphi,\Sigma]_{\pi^{\prime}}$
with $\mathop{\lozenge}\nolimits_{s}\varphi$ the principal formula, and
$s^{\prime}\preceq^{*}_{\Gamma}s$, then adding $\varphi$ to the nesting
$(s^{\prime})[\mathop{\lozenge}\nolimits_{s}\varphi,\Sigma]_{\pi^{\prime}}$
yields the premise;

$(\mathop{\lozenge}_{\ast})$

If a component $\Sigma_{i}$ of the conclusion contains
$\mathop{\lozenge}\nolimits_{\ast}\varphi$ (the principal formula), then
prepending the consequent $\Delta$ with $\varphi$ (i.e. adding $\varphi$ to
$\Sigma_{0}$) yields the premise.

######  Example 2.

Below, we provide an example of a nested sequent derivation. To minimize the
width of the proof, we let $\varphi$ denote
$\mathop{\lozenge}\nolimits_{s}\mathop{\lozenge}\nolimits_{\ast}\neg
p\lor\mathop{\square}\nolimits_{s^{\prime}}p$.

$(id)$ $s^{\prime}\preceq
s\vdash\varphi,\mathop{\lozenge}\nolimits_{s}\mathop{\lozenge}\nolimits_{\ast}\neg
p,\mathop{\square}\nolimits_{s^{\prime}}p,(s^{\prime})[\mathop{\lozenge}\nolimits_{\ast}\neg
p,\neg p,p]$ $(\mathop{\lozenge}_{\ast}^{2})$ $s^{\prime}\preceq
s\vdash\varphi,\mathop{\lozenge}\nolimits_{s}\mathop{\lozenge}\nolimits_{\ast}\neg
p,\mathop{\square}\nolimits_{s^{\prime}}p,(s^{\prime})[\mathop{\lozenge}\nolimits_{\ast}\neg
p,p]$ $(\mathop{\lozenge}_{s}^{1})$ $s^{\prime}\preceq
s\vdash\varphi,\mathop{\lozenge}\nolimits_{s}\mathop{\lozenge}\nolimits_{\ast}\neg
p,\mathop{\square}\nolimits_{s^{\prime}}p,(s^{\prime})[p]$
$(\mathop{\square}_{s^{\prime}})$ $s^{\prime}\preceq
s\vdash\varphi,\mathop{\lozenge}\nolimits_{s}\mathop{\lozenge}\nolimits_{\ast}\neg
p,\mathop{\square}\nolimits_{s^{\prime}}p$ $(\lor)$ $s^{\prime}\preceq
s\vdash\varphi$

Observe that $(\mathop{\lozenge}_{s}^{1})$ is applicable as
$s^{\prime}\preceq^{*}_{\Gamma}s$ holds due to the antecedent, and
$(\mathop{\lozenge}_{\ast}^{2})$ is applicable as
$s^{\prime}\preceq^{*}_{\Gamma}\ast$ holds by definition (see Def. 5).

We now prove that our calculi are sound (Thm. 1, building on Lem. 1), that is,
that every nested sequent derivable in $\mathsf{NS}(\mathcal{V})$ is valid. We
then state our completeness theorem, which is a consequence of the work in
Sect. 4.

######  Lemma 1.

Let $\Gamma\vdash\Delta$ be a sequent,
$\mathcal{M}=\langle\Pi,\sigma,\delta\rangle$ be a model with $\pi\in\Pi$, and
$s,s^{\prime}\in\mathcal{S}$. If $\mathcal{M},\pi\models\bigwedge\Gamma$ and
$s^{\prime}\preceq^{*}_{\Gamma}s$, then $\mathcal{M},\pi\models
s^{\prime}\preceq s$.

###### Proof.

Assume that $\mathcal{M},\pi\models\bigwedge\Gamma$ and
$s^{\prime}\preceq^{*}_{\Gamma}s$ for some $s^{\prime},s\in\mathcal{S}$. There
are four cases to consider:

  1. (1)

$s=\hbox{$*$}$. The result is immediate as $\sigma(\ast)=\Pi$, and therefore,
$\mathcal{M},\pi\models s^{\prime}\preceq\ast$ for every
$s^{\prime}\in\mathcal{S}$ by Def. 4.

  2. (2)

$s^{\prime}\preceq s\in\Gamma$. From the assumption that
$\mathcal{M},\pi\models\bigwedge\Gamma$ it follows that
$\mathcal{M},\pi\models s^{\prime}\preceq s$.

  3. (3)

$s=s^{\prime}$. Then, it is trivially implied that $\mathcal{M},\pi\models
s^{\prime}\preceq s$ since $\sigma(s^{\prime})=\sigma(s)\subseteq\sigma(s)$ by
Def. 4.

  4. (4)

There are some $s_{1},\ldots,s_{n}\in\mathcal{S}$ such that $s^{\prime}\preceq
s_{1},\in\Gamma$, $s_{i}\preceq s_{i+1}\in\Gamma$ for every $1\leq i\leq n-1$,
and $s_{n}\preceq s\in\Gamma$, that is, $s^{\prime}\preceq^{*}_{\Gamma}s$ is
obtained by transitivity on a path in $\mathcal{S}$. From this, together with
the assumption that $\mathcal{M},\pi\models\bigwedge\Gamma$, it directly
follows that $\mathcal{M},\pi\models s^{\prime}\preceq s$ by Def. 4. ∎

######  Theorem 1 (Soundness).

If $\Gamma\vdash\Delta$ is derivable in $\mathsf{NS}(\mathcal{V})$, then
$\Gamma\vdash\Delta$ is valid.

###### Proof.

We prove the result by induction on the number of inferences in a given
derivation, and assume that $\Delta$ is of the form
$\Sigma_{0},(s_{1})[\Sigma_{1}],\ldots,(s_{n})[\Sigma_{n}]$.

Base case. In the base case, our derivation consists of a single application
of the $(id)$ rule. Hence,

$\iota(\Gamma\vdash\Delta\\{p,\neg
p\\}_{\pi_{i}}):=\bigwedge\Gamma\rightarrow\bigvee\Sigma_{0}\lor\bigvee_{1\leq
i\leq n}\mathop{\square}\nolimits_{s_{i}}(\bigvee\Sigma_{i})$

where $p,\neg p\in\Sigma_{i}$, for some $0\leq i\leq n$. Regardless, the
consequent of the implication above will be satisfied in any model
$\mathcal{M}$, implying that the above implication is valid.

Inductive step. We make a case distinction based on the last rule applied, and
show that if the conclusion of the rule is invalid, then at least one of the
premises of the rule is invalid, that is to say, we show by contraposition
that if the premise(s) is (are) valid, then the conclusion is valid. We only
show the $(\mathop{\square}_{s})$ and $(\mathop{\lozenge}_{s}^{1})$ cases as
the remaining cases are simple or argued in a similar manner.

$(\mathop{\square}_{s})$. We assume that $\Sigma_{1}$ is of the form
$\mathop{\square}\nolimits_{s}\varphi,\Sigma_{1}^{\prime}$ with
$\mathop{\square}\nolimits_{s}\varphi$ principal; all remaining cases are
similar. Furthermore, let us suppose that
$\iota(\Gamma\vdash\Delta\\{\mathop{\square}\nolimits_{s}\varphi\\}_{\pi_{1}}):=$

$\bigwedge\Gamma\rightarrow\bigvee\Sigma_{0}\lor\mathop{\square}\nolimits_{s_{1}}(\mathop{\square}\nolimits_{s}\varphi\lor\bigvee\Sigma_{1}^{\prime})\lor\bigvee_{2\leq
i\leq n}\mathop{\square}\nolimits_{s_{i}}(\bigvee\Sigma_{i})$

is invalid. Then,
$\mathcal{M},\pi\not\models\mathop{\square}\nolimits_{s_{1}}(\mathop{\square}\nolimits_{s}\varphi\lor\bigvee\Sigma_{1}^{\prime})$
for some standpoint model $\mathcal{M}:=\langle\Pi,\sigma,\delta\rangle$ with
a precisification $\pi$. Hence, there exists a precisification
$\pi^{\prime}\in\sigma(s_{1})$ such that
$\mathcal{M},\pi^{\prime}\not\models\mathop{\square}\nolimits_{s}\varphi$,
implying that there exists a precisification $\pi^{\prime\prime}\in\sigma(s)$
such that $\mathcal{M},\pi^{\prime\prime}\not\models\varphi$. It thus follows
that $\mathcal{M},\pi\not\models\mathop{\square}\nolimits_{s}\varphi$, showing
that the premise of $(\mathop{\square}_{s})$ is invalid.

$(\mathop{\lozenge}_{s}^{1})$. Suppose that $\Sigma_{1}$ is of the form
$\mathop{\lozenge}\nolimits_{s}\varphi,\Sigma_{1}^{\prime}$ with
$\mathop{\lozenge}\nolimits_{s}\varphi$ principal; all remaining cases are
argued in a similar fashion. Assume that $s^{\prime}\preceq^{*}_{\Gamma}s$
holds and that the following is invalid:

$\displaystyle\iota(\Gamma\vdash\Delta\\{\mathop{\lozenge}\nolimits_{s}\varphi\\}_{\pi},(s^{\prime})[\Sigma]_{\pi^{\prime}}):=\bigwedge\Gamma\rightarrow\bigvee\Sigma_{0}\lor$
$\displaystyle\mathop{\square}\nolimits_{s_{1}}(\mathop{\lozenge}\nolimits_{s}\varphi\lor\bigvee\Sigma_{1}^{\prime})\lor\Big{(}\bigvee_{2\leq
i\leq
n}\\!\\!\\!\mathop{\square}\nolimits_{s_{i}}\big{(}\bigvee\Sigma_{i}\big{)}\Big{)}\lor\mathop{\square}\nolimits_{s^{\prime}}\big{(}\bigvee\Sigma\big{)}$

Therefore, there is a standpoint model
$\mathcal{M}:=\langle\Pi,\sigma,\delta\rangle$ with $\pi\in\Pi$ such that
$\mathcal{M},\pi\not\models\mathop{\square}\nolimits_{s^{\prime}}(\bigvee\Sigma)$
and
$\mathcal{M},\pi\not\models\mathop{\square}\nolimits_{s_{1}}(\mathop{\lozenge}\nolimits_{s}\varphi\lor\bigvee\Sigma_{1}^{\prime})$,
and such that $\sigma(s^{\prime})\subseteq\sigma(s)$, by
$s^{\prime}\preceq^{*}_{\Gamma}s$ and Lem. 1. This entails that there exists a
precisification $\pi^{\prime}\in\sigma(s^{\prime})$ such that
$\mathcal{M},\pi^{\prime}\not\models\bigvee\Sigma$, and that there exists a
precisification $\pi_{1}\in\sigma(s_{1})$ such that
$\mathcal{M},\pi_{1}\not\models\mathop{\lozenge}\nolimits_{s}\varphi$. The
latter further implies that for every precisification in $\sigma(s)$, and thus
for $\pi^{\prime}$ (since
$\pi^{\prime}\in\sigma(s^{\prime})\subseteq\sigma(s)$), that
$\mathcal{M},\pi^{\prime}\not\models\varphi$. Thus, the premise has been shown
invalid. ∎

######  Theorem 2 (Completeness).

If $\Gamma\vdash\Delta$ is valid, then $\Gamma\vdash\Delta$ is provable in
$\mathsf{NS}(\mathcal{V})$.

###### Proof.

The theorem follows from the correct (Thm. 3) and terminating (Thm. 4) proof-
search procedure given in the subsequent section (Sect. 4). ∎

##  4 Automating Standpoint Logic via Proof-Search

We now employ our nested calculi in an algorithm that decides the validity of
formulae for propositional standpoint logics. In particular, we design a
proof-search algorithm (see Alg. 1 below) which takes a vocabulary
$\mathcal{V}$ as a parameter and bottom-up applies rules from
$\mathsf{NS}(\mathcal{V})$ in attempt to construct a proof of a given input
sequent $\Gamma\vdash\varphi$. We may make the simplifying assumption that our
proof-search algorithm only receives inputs of the form $\Gamma\vdash\varphi$
as any nested sequent $\Gamma\vdash\Delta$ with
$\Delta=\Sigma_{0},(s_{1})[\Sigma_{1}],\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]$
is valid iff $\iota(\Gamma\vdash\Delta)$ is valid iff $\Gamma\vdash\varphi$ is
valid, where
$\varphi=\bigvee\Sigma_{0}\lor\mathop{\square}\nolimits_{s_{1}}(\bigvee\Sigma_{1})\lor\cdots\lor\mathop{\square}\nolimits_{s_{n}}(\bigvee\Sigma_{n})$.

To decrease the complexity of proof-search and obtain (worst-case) complexity-
optimality, we introduce a new technique in the context of nested sequents
which we refer to as _coloring_. In essence, given the input
$\Gamma\vdash\varphi$, the first step of proof-search guesses a _proper
coloring_ of the formula $\varphi$, that is, it labels the formula’s
subformulae with either an _active_ label $\circ$ or an _inactive_ label
$\bullet$ in a particular manner. Recall that, due to the $(\land)$ rule, a
proof in $\mathsf{NS}(\mathcal{V})$ has the structure of a binary tree, thus
giving rise to the possibility that proof-search is exponential; therefore,
our proof-search algorithm uses the aforementioned labels to only generate a
single path in this binary tree relative to each coloring, which yields a
worst-case complexity-optimal proof-search procedure in $\mathrm{CoNP}$ (for
the validity problem of ${\mathbb{S}}(\mathcal{V})$).

######  Definition 7 (Coloring).

We define a _colored formula_ to be a formula generated via the following
grammar in BNF:

$\widetilde{\varphi}::=p^{\ast}\ |\ \neg p^{\ast}\ |\
(\widetilde{\varphi}\lor\widetilde{\varphi})^{\ast}\ |\
(\widetilde{\varphi}\land\widetilde{\varphi})^{\ast}\ |\
(\mathop{\lozenge}\nolimits_{s}\widetilde{\varphi})^{\ast}\ |\
(\mathop{\square}\nolimits_{s}\widetilde{\varphi})^{\ast}$

with $\ast\in\\{\circ,\bullet\\}$. For any colored formula
$\widetilde{\varphi}$, we let $\varphi$ be the formula in
$\mathcal{L}_{\mathcal{V}}$ obtained by removing all labels $\circ$ and
$\bullet$ from $\widetilde{\varphi}$. A formula $\widetilde{\varphi}$ is
_properly colored_ iff $\widetilde{\varphi}=f_{\circ}(\varphi)$, where the
non-deterministic _coloring function_ $f_{\circ}$ and $f_{\bullet}$ are
defined accordingly with $\ast\in\\{\circ,\bullet\\}$:

  * •

$f_{\ast}(p)=p^{\ast}$

  * •

$f_{\ast}(\neg p)=\neg p^{\ast}$

  * •

$f_{\ast}(\varphi\lor\psi)=(f_{\ast}(\varphi)\lor f_{\ast}(\psi))^{\ast}$

  * •

$f_{\circ}(\varphi\land\psi)\in\\{(f_{\circ}(\varphi)\land
f_{\bullet}(\psi))^{\circ},(f_{\bullet}(\varphi)\land
f_{\circ}(\psi))^{\circ}\\}$

  * •

$f_{\bullet}(\varphi\land\psi)=(f_{\bullet}(\varphi)\land
f_{\bullet}(\psi))^{\bullet}$

  * •

$f_{\ast}(\mathop{\lozenge}\nolimits_{s}\varphi)=(\mathop{\lozenge}\nolimits_{s}f_{\ast}(\varphi))^{\ast}$

  * •

$f_{\ast}(\mathop{\square}\nolimits_{s}\varphi)=(\mathop{\square}\nolimits_{s}f_{\ast}(\varphi))^{\ast}$

We define $\mathrm{pcs}(\varphi)$ to be the set of all proper colorings of
$\varphi$, and define a _colored nested sequent_ to be a nested sequent that
uses colored formulae as opposed to formulae from $\mathcal{L}_{\mathcal{V}}$.

We now stipulate our _saturation conditions_. When such conditions are
unsatisfied during proof-search it signals that certain inference rules still
need to be applied bottom-up. Alternatively, once all such conditions are
satisfied this signals that proof-search ought to terminate.

######  Definition 8 (Saturation Conditions).

A colored nested sequent
$\Gamma\vdash\Sigma_{0},(s_{1})[\Sigma_{1}]_{\pi_{1}},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{1}]_{\pi_{n}}$
is _saturated_ iff for every
$i\in\\{0,\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},n\\}$
it satisfies the following conditions:

$id$

If $p^{\circ}\in\Sigma_{i}$, then $\neg p^{\circ}\not\in\Sigma_{i}$;

$\lor$

if $(\widetilde{\varphi}\lor\widetilde{\psi})^{\circ}\in\Sigma_{i}$, then
$\widetilde{\varphi}^{\circ},\widetilde{\psi}^{\circ}\in\Sigma_{i}$;

$\land$

if $(\widetilde{\varphi}\land\widetilde{\psi})^{\circ}\in\Sigma_{i}$, then
either $\widetilde{\varphi}^{\circ}\in\Sigma_{i}$ or
$\widetilde{\psi}^{\circ}\in\Sigma_{i}$;

$\mathop{\lozenge}\nolimits_{s}$

if $(\mathop{\lozenge}\nolimits_{s}\widetilde{\varphi})^{\circ}\in\Sigma_{i}$
and $s^{\prime}\preceq^{*}_{\Gamma}s$, then for each
$j\in\\{1,\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},n\\}$
such that $s_{j}=s^{\prime}$, $\widetilde{\varphi}^{\circ}\in\Sigma_{j}$;

$\mathop{\lozenge}\nolimits_{\ast}$

if
$(\mathop{\lozenge}\nolimits_{\ast}\widetilde{\varphi})^{\circ}\in\Sigma_{i}$,
then $\widetilde{\varphi}^{\circ}\in\Sigma_{0}$;

$\mathop{\square}\nolimits_{s}$

if $(\mathop{\square}\nolimits_{s}\widetilde{\varphi})^{\circ}\in\Sigma_{i}$,
then for some
$j\in\\{1,\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},n\\}$,
$s_{j}=s$, and $\widetilde{\varphi}^{\circ}\in\Sigma_{j}$;

$n_{s}$

for each $s\in\mathcal{S}$, there exists a
$j\in\\{1,\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},n\\}$
such that $s_{j}=s$.

Input: A Nested Sequent: $\Gamma\vdash\varphi$

Output: A Boolean: $\mathtt{True}$, $\mathtt{False}$

1

2Choose a proper coloring $\widetilde{\varphi}$ of $\varphi$;

3 return
$\mathtt{ProofSearch}_{\mathcal{V}}(\Gamma\vdash\widetilde{\varphi})$;

Algorithm 1 $\mathtt{Prove}_{\mathcal{V}}$

Input: A Colored Nested Sequent:
$\Phi:=\Gamma\vdash\Sigma_{0},(s_{1})[\Sigma_{1}]_{\pi_{1}},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]_{\pi_{n}}$

Output: A Boolean: $\mathtt{True}$, $\mathtt{False}$

1

2if  _for some $0\leq i\leq n$, $p^{\circ},\neg p^{\circ}\in\Sigma_{i}$_ then

3 return $\mathtt{True}$;

4 end if

5

6if  _$\Sigma$ is saturated_ then

7 return $\mathtt{False}$;

8 end if

9

10if  _for some $0\leq i\leq n$,
$(\widetilde{\varphi}\lor\widetilde{\psi})^{\circ}\in\Sigma_{i}$, but
$\widetilde{\varphi},\widetilde{\psi}\not\in\Sigma_{i}$_ then

11 Let $\Sigma_{i}^{\prime}:=\Sigma_{i},\widetilde{\varphi},\widetilde{\psi}$;

12 Let
$\Phi^{\prime}:=\Gamma\\!\vdash\\!\Sigma_{0},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{i})[\Sigma_{i}^{\prime}]_{\pi_{i}},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]_{\pi_{n}}$;

// Replace $\Sigma_{i}$ by $\Sigma_{i}^{\prime}$ to obtain $\Phi^{\prime}$.

13 return $\mathtt{Prove}_{\mathcal{V}}(\Phi^{\prime})$;

14 end if

15

16if  _for some $0\leq i\leq n$,
$(\widetilde{\varphi}^{\circ}\land\widetilde{\psi}^{\bullet})^{\circ}\in\Sigma_{i}$,
but $\widetilde{\varphi}^{\circ}\not\in\Sigma_{i}$_ then

17 Let $\Sigma_{i}^{\prime}:=\Sigma_{i},\widetilde{\varphi}^{\circ}$;

18 Let
$\Phi^{\prime}:=\Gamma\\!\vdash\\!\Sigma_{0},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{i})[\Sigma_{i}^{\prime}]_{\pi_{i}},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]_{\pi_{n}}$;

// Replace $\Sigma_{i}$ by $\Sigma_{i}^{\prime}$ to obtain $\Phi^{\prime}$.

19 return $\mathtt{Prove}_{\mathcal{V}}(\Phi^{\prime})$

20 end if

21

22if  _for some $0\leq i\leq n$,
$(\widetilde{\varphi}^{\bullet}\land\widetilde{\psi}^{\circ})^{\circ}\in\Sigma_{i}$,
but $\widetilde{\psi}^{\circ}\not\in\Sigma_{i}$_ then

23 Let $\Sigma_{i}^{\prime}:=\Sigma_{i},\widetilde{\psi}^{\circ}$;

24 Let
$\Phi^{\prime}:=\Gamma\\!\vdash\\!\Sigma_{0},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{i})[\Sigma_{i}^{\prime}]_{\pi_{i}},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]_{\pi_{n}}$;

// Replace $\Sigma_{i}$ by $\Sigma_{i}^{\prime}$ to obtain $\Phi^{\prime}$.

25 return $\mathtt{Prove}_{\mathcal{V}}(\Phi^{\prime})$

26 end if

27

Algorithm 2 $\mathtt{ProofSearch}_{\mathcal{V}}$ (Part I)

Let us comment on the functionality of our (non-deterministic) proof-search
algorithm $\mathtt{Prove}_{\mathcal{V}}$ (Alg. 1), which takes
$\mathtt{ProofSearch}_{\mathcal{V}}$ (Alg. 2) as a subroutine. (NB. Alg. 2 is
split between this page and the next due to its length.) As mentioned above,
given an input $\Gamma\vdash\varphi$, the algorithm
$\mathtt{Prove}_{\mathcal{V}}$ guesses a proper coloring $\widetilde{\varphi}$
of $\varphi$, and then returns the value of
$\mathtt{ProofSearch}_{\mathcal{V}}(\Gamma\vdash\widetilde{\varphi})$. We note
that $\mathtt{ProofSearch}_{\mathcal{V}}$ applies the rules from
$\mathsf{NS}(\mathcal{V})$ in a bottom-up manner (each corresponding to a
recursive call of the algorithm with the exception of $(id)$). The application
of each rule is as follows: $(id)$ corresponds to lines 1–3, $(\lor)$ to lines
7–11, $(\land)$ to lines 12–16 and 17–21, that respectively yields the left
and right premises of $(\land)$, $(\mathop{\lozenge}_{s}^{1})$ and
$(\mathop{\lozenge}_{s}^{2})$ to lines 22–25, $(\mathop{\lozenge}_{\ast})$ to
lines 26–29, $(\mathop{\square}_{s})$ to lines 30–33, and $(n_{s})$ to lines
34–37.

Moreover, $\mathtt{ProofSearch}_{\mathcal{V}}$ contrasts with typical proof-
search algorithms in that it utilizes the active and inactive labels $\circ$
and $\bullet$ in $\widetilde{\varphi}$ to guide its computation and only
constructs _a single thread_ of the proof.222A _thread_ in a proof is defined
in the usual fashion as a path of sequents from the conclusion of the proof to
an initial sequent (cf. (?, p. 14)). In other words, if a nested sequent
$\Gamma\vdash\varphi$ is derivable in $\mathsf{NS}(\mathcal{V})$, then the
sequent has a proof in $\mathsf{NS}(\mathcal{V})$ such that
$\mathtt{ProofSearch}_{\mathcal{V}}$ generates each thread of the proof
relative to each proper coloring of $\varphi$; as argued in the lemma below,
all such threads may be ‘zipped’ together to reconstruct a full proof of
$\Gamma\vdash\varphi$ in $\mathsf{NS}(\mathcal{V})$. In this way, our proof-
search algorithm may be used to construct certificates witnessing the validity
(by means of a proof in $\mathsf{NS}(\mathcal{V})$) or invalidity (by means of
a counter-model) of any input $\Gamma\vdash\varphi$ (see Thm. 3 below for
details).

######  Lemma 2.

Let $\Gamma\vdash\varphi$ be a sequent and $\mathrm{pcs}(\varphi)$ the
(finite) set of proper colorings of $\varphi$. If
$\mathtt{ProofSearch}_{\mathcal{V}}(\Gamma\vdash\widetilde{\varphi})=\mathtt{True}$
for all $\widetilde{\varphi}\in\mathrm{pcs}(\varphi)$, then there is a proof
of $\Gamma\vdash\varphi$ in $\mathsf{NS}(\mathcal{V})$.

###### Proof.

Assume that
$\mathtt{ProofSearch}_{\mathcal{V}}(\Gamma\vdash\widetilde{\varphi})=\mathtt{True}$
for every $\widetilde{\varphi}\in\mathrm{pcs}(\varphi)$, and the following
thread of colored nested sequents is generated during its execution:

$\displaystyle
T(\widetilde{\varphi}):=\Gamma\vdash\Delta_{0},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},\Gamma\vdash\Delta_{h}$

such that $\Delta_{0}=\widetilde{\varphi}$ and $\Gamma\vdash\Delta_{h}$ is an
instance of $(id)$ (by lines 1–3). Let $\mathcal{T}$ be the set of all such
threads.

For a thread
$\Gamma\vdash\Delta_{0},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},\Gamma\vdash\Delta_{h}\in\mathcal{T}$
and $0\leq k\leq h$, the colored nested sequent $\Gamma\vdash\Delta_{k}$ is:

  * •

_left conjunctive_ iff $\Gamma\vdash\Delta_{k+1}$ is obtained from
$\Gamma\vdash\Delta_{k}$ by applying $(\land)$ yielding the left premise
(lines 12–16), and

  * •

_right conjunctive_ iff $\Gamma\\!\vdash\\!\Delta_{k+1}$ is obtained from
$\Gamma\vdash\Delta_{k}$ by applying $(\land)$ yielding the right premise
(lines 17–21).

A colored nested sequent is _conjunctive_ iff it is left or right conjunctive.
We now explain how our threads may be transformed into a proof of
$\Gamma\vdash\varphi$ in $\mathsf{NS}(\mathcal{V})$.

We assume w.l.o.g. that the initial segments of all threads up to and
including the first conjunctive sequent $\Gamma\vdash\Delta_{k}$ are identical
(i.e. we assume that the subroutine $\mathtt{ProofSearch}_{\mathcal{V}}$
executes in a deterministic fashion). Hence, we may form the ‘pseudo-
derivation’ shown below left, by making use of the first $k$ sequents of any
given thread, where the rules
$(r_{1}),\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(r_{k-1})$
are determined on the basis of which lines of
$\mathtt{ProofSearch}_{\mathcal{V}}$ were executed.

$\Gamma\vdash\Delta_{k}$ $(r_{k-1})$ $\vdots$ $(r_{1})$ $\Gamma\vdash\varphi$ |  $\Gamma\vdash\Delta_{k+1}^{l}$ $\Gamma\vdash\Delta_{k+1}^{r}$ $(\land)$ $\Gamma\vdash\Delta_{k}$ $(r_{k-1})$ $\vdots$ $(r_{1})$ $\Gamma\vdash\varphi$
---|---

Let us define
$T^{k}(\widetilde{\varphi}):=\Gamma\vdash\Delta_{k+1},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},\Gamma\vdash\Delta_{h}$
to be the tail of a thread $T(\widetilde{\varphi})$ starting from $k+1$. Since
the $k^{th}$ colored nested sequent of every thread is conjunctive, we may
generate two sets of threads $\mathcal{T}_{L}$ and $\mathcal{T}_{R}$ from
$\mathcal{T}$:

$\displaystyle\mathcal{T}_{L}:=\\{T^{k}(\widetilde{\varphi})\ |\
\Gamma\vdash\Delta_{k}\in T(\widetilde{\varphi})\text{ is left
conjunctive}\\}$ $\displaystyle\mathcal{T}_{R}:=\\{T^{k}(\widetilde{\varphi})\
|\ \Gamma\vdash\Delta_{k}\in T(\widetilde{\varphi})\text{ is right
conjunctive}\\}$

We now extend the ‘pseudo-derivation’ shown above left, with a bottom-up
application of $(\land)$ to obtain the ‘pseudo-derivation’ shown above right,
where $\Gamma\vdash\Delta_{k+1}^{l}$ and $\Gamma\vdash\Delta_{k+1}^{r}$ are
the initial elements of each thread $\mathcal{T}_{L}$ and $\mathcal{T}_{R}$,
respectively. By successively repeating the above described process over
$\mathcal{T}_{L}$ and $\mathcal{T}_{R}$, a proof in $\mathsf{NS}(\mathcal{V})$
will eventually be built above $\Gamma\vdash\Delta_{k+1}^{l}$ and
$\Gamma\vdash\Delta_{k+1}^{r}$, giving a proof of $\Gamma\vdash\varphi$ in
$\mathsf{NS}(\mathcal{V})$. ∎

22

23if  _for some $0\leq i\leq n$,
$(\mathop{\lozenge}\nolimits_{s}\widetilde{\varphi})^{\circ}\in\Sigma_{i}$ and
$s^{\prime}\preceq^{*}_{\Gamma}s$, and for some $1\leq j\leq n$,
$s_{j}=s^{\prime}$, but $\widetilde{\varphi}\not\in\Sigma_{j}$_ then

24 Let
$\Phi^{\prime}:=\Gamma\\!\vdash\\!\Sigma_{0},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{j})[\Sigma_{j},\widetilde{\varphi}]_{\pi_{j}},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]_{\pi_{n}}$;

// Add $\widetilde{\varphi}$ to the $j^{th}$ nesting to obtain
$\Phi^{\prime}$.

25 return $\mathtt{Prove}_{\mathcal{V}}(\Phi^{\prime})$;

26 end if

27

28if  _for some $0\leq i\leq n$,
$(\mathop{\lozenge}\nolimits_{\ast}\widetilde{\varphi})^{\circ}\in\Sigma_{i}$,
but $\widetilde{\varphi}\not\in\Sigma_{0}$_ then

29 Let $\Phi^{\prime}:=\Gamma\vdash\
\widetilde{\varphi},\Sigma_{0},(s_{1})[\Sigma_{1}]_{\pi_{1}},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]_{\pi_{n}}$;

// Add $\widetilde{\varphi}$ to the $0^{th}$ component to obtain
$\Phi^{\prime}$.

30 return $\mathtt{Prove}_{\mathcal{V}}(\Phi^{\prime})$;

31 end if

32

33if  _for some $0\leq i\leq n$,
$(\mathop{\square}\nolimits_{s}\widetilde{\varphi})^{\circ}\in\Sigma_{i}$, but
for each $1\leq j\leq n$ such that $s_{j}=s$,
$\widetilde{\varphi}\not\in\Sigma_{j}$_ then

34 Let
$\Sigma^{\prime}:=\Gamma\vdash\Sigma_{0},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]_{\pi_{n}},(s)[\widetilde{\varphi}]_{\pi_{n+1}}$;

// Append $(s)[\widetilde{\varphi}]_{\pi_{n+1}}$ to obtain $\Phi^{\prime}$
with $\pi_{n+1}$ fresh.

35 return $\mathtt{Prove}_{\mathcal{V}}(\Phi^{\prime})$;

36 end if

37

38if  _for some $s\in\mathcal{S}$ there does not exist a $1\leq j\leq n$ such
that $s_{j}=s$_ then

39 Let
$\Phi^{\prime}:=\Gamma\vdash\Sigma_{0},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]_{\pi_{n}},(s)[\emptyset]_{\pi_{n+1}}$;

// Append $(s)[\emptyset]_{\pi_{n+1}}$ to obtain $\Phi^{\prime}$ with
$\pi_{n+1}$ fresh.

40 return $\mathtt{Prove}_{\mathcal{V}}(\Phi^{\prime})$;

41 end if

42

Algorithm 3 $\mathtt{ProofSearch}_{\mathcal{V}}$ (Part II)

######  Example 3.

To illustrate the procedure in Lem. 2 above, we provide an example of the
proof construction process of $\emptyset\vdash\varphi$ with
$\varphi:=\mathop{\square}\nolimits_{s}(p\lor(\neg p\land\neg
p))\land\mathop{\lozenge}\nolimits_{s}(q\lor\neg q)$. First, observe that
$\varphi$ has three proper colorings, given below:

$\widetilde{\varphi}^{1}:=$

$((\mathop{\square}\nolimits_{s}(p^{\circ}\lor(\neg p^{\circ}\land\neg
p^{\bullet})^{\circ})^{\circ})^{\circ}\land(\mathop{\lozenge}\nolimits_{s}(q^{\bullet}\lor\neg
q^{\bullet})^{\bullet})^{\bullet})^{\circ}$

$\widetilde{\varphi}^{2}:=$

$((\mathop{\square}\nolimits_{s}(p^{\circ}\lor(\neg p^{\bullet}\land\neg
p^{\circ})^{\circ})^{\circ})^{\circ}\land(\mathop{\lozenge}\nolimits_{s}(q^{\bullet}\lor\neg
q^{\bullet})^{\bullet})^{\bullet})^{\circ}$

$\widetilde{\varphi}^{3}:=$

$((\mathop{\square}\nolimits_{s}(p^{\bullet}\lor(\neg p^{\bullet}\land\neg
p^{\bullet})^{\bullet})^{\bullet})^{\bullet}\land(\mathop{\lozenge}\nolimits_{s}(q^{\circ}\lor\neg
q^{\circ})^{\circ})^{\circ})^{\circ}$

Each proper coloring $\widetilde{\varphi}^{i}$ with $i\in\\{1,2,3\\}$ gives
rise to a corresponding thread $T(i)$ (shown at the top of Fig. 3) when
$\mathtt{ProofSearch}_{\mathcal{V}}(\emptyset\vdash\widetilde{\varphi}^{i})$
is run. Note that in the figure we have omitted the active and inactive
labels, as well as labels of the form $\pi_{i}$, from each thread $T(i)$ to
improve readability, and each application of $(\land)$ is emphasized with a
dashed inference line. By making use of the proof construction process
described in Lem. 2, the three threads $T(1)$, $T(2)$, and $T(3)$ can be fused
together to generate a proof of $\emptyset\vdash\varphi$ shown at the bottom
of Fig. 3.

$T(1):=$ | $T(2):=$ | $T(3):=$
---|---|---
$(id)$ $\emptyset\vdash\varphi,\psi_{0},(s)[\psi_{1},p,\neg p,\psi_{2}]$ $(\land)$ $\emptyset\vdash\varphi,\psi_{0},(s)[\psi_{1},p,\neg p\land\neg p]$ $(\lor)$ $\emptyset\vdash\varphi,\psi_{0},(s)[p\lor(\neg p\land\neg p)]$ $(\mathop{\square}_{s})$ $\emptyset\vdash\varphi,\mathop{\square}\nolimits_{s}(p\lor(\neg p\land\neg p))$ $(\land)$ $\emptyset\vdash\varphi$ |  $(id)$ $\emptyset\vdash\varphi,\mathop{\lozenge}\nolimits_{s}(q\lor\neg q),(s)[\psi_{3},q,\neg q]$ $(\lor)$ $\emptyset\vdash\varphi,\mathop{\lozenge}\nolimits_{s}(q\lor\neg q),(s)[q\lor\neg q]$ $(\mathop{\lozenge}_{s})$ $\emptyset\vdash\varphi,\mathop{\lozenge}\nolimits_{s}(q\lor\neg q),(s)[\emptyset]$ $(n_{s})$ $\emptyset\vdash\varphi,\mathop{\lozenge}\nolimits_{s}(q\lor\neg q)$ $(\land)$ $\emptyset\vdash\varphi$ |

$(id)$ $\emptyset\vdash\varphi,\psi_{0},(s)[\psi_{1},p,\neg p,\psi_{2}]$
$(id)$ $\emptyset\vdash\varphi,\psi_{0},(s)[\psi_{1},p,\neg p,\psi_{2}]$
$(\land)$ $\emptyset\vdash\varphi,\psi_{0},(s)[\psi_{1},p,\neg p\land\neg p]$
$(\lor)$ $\emptyset\vdash\varphi,\psi_{0},(s)[p\lor(\neg p\land\neg p)]$
$(\mathop{\square}_{s})$
$\emptyset\vdash\varphi,\mathop{\square}\nolimits_{s}(p\lor(\neg p\land\neg
p))$ $(id)$ $\emptyset\vdash\varphi,\mathop{\lozenge}\nolimits_{s}(q\lor\neg
q),(s)[\psi_{3},q,\neg q]$ $(\lor)$
$\emptyset\vdash\varphi,\mathop{\lozenge}\nolimits_{s}(q\lor\neg
q),(s)[q\lor\neg q]$ $(\mathop{\lozenge}_{s})$
$\emptyset\vdash\varphi,\mathop{\lozenge}\nolimits_{s}(q\lor\neg
q),(s)[\emptyset]$ $(n_{s})$
$\emptyset\vdash\varphi,\mathop{\lozenge}\nolimits_{s}(q\lor\neg q)$ $(\land)$
$\emptyset\vdash\varphi$

Figure 3: An example of how the threads $T(1)$, $T(2)$, and $T(3)$ may be
‘zipped’ together to construct the derivation shown above bottom. Note that
$\varphi:=\mathop{\square}\nolimits_{s}(p\lor(\neg p\land\neg
p))\land\mathop{\lozenge}\nolimits_{s}(q\lor\neg q)$,
$\psi_{0}:=\mathop{\square}\nolimits_{s}(p\lor(\neg p\land\neg p))$,
$\psi_{1}:=p\lor(\neg p\land\neg p)$, $\psi_{2}:=\neg p\land\neg p$, and
$\psi_{3}:=q\lor\neg q$.

######  Theorem 3 (Correctness).

Let $\Gamma\vdash\varphi$ be a sequent.

  1. 1.

If
$\mathtt{ProofSearch}_{\mathcal{V}}(\Gamma\vdash\widetilde{\varphi})=\mathtt{True}$
for all proper colorings of $\varphi$, then a proof in
$\mathsf{NS}(\mathcal{V})$ may be constructed witnessing that
$\Gamma\vdash\varphi$ is valid.

  2. 2.

If
$\mathtt{ProofSearch}_{\mathcal{V}}(\Gamma\vdash\widetilde{\varphi})=\mathtt{False}$
for some proper coloring of $\varphi$, then a counter-model may be constructed
witnessing that $\Gamma\vdash\varphi$ is invalid.

###### Proof.

The first claim follows by Lem. 2 and the soundness of each nested calculus
(see Thm. 1); therefore, we focus on the second claim. Suppose that
$\mathtt{ProofSearch}_{\mathcal{V}}(\Gamma~{}\vdash~{}\widetilde{\varphi})=\mathtt{False}$
for some chosen proper coloring of $\varphi$. Then,
$\mathtt{ProofSearch}_{\mathcal{V}}$ generates a saturated nested sequent
$\Gamma\vdash\Delta$ with $\Delta$ of the form
$\Sigma_{0},(s_{1})[\Sigma_{1}]_{\pi_{1}},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},(s_{n})[\Sigma_{n}]_{\pi_{n}}$.
We will use $\Gamma\vdash\Delta$ to construct a counter-model for
$\Gamma\vdash\varphi$, thus proving the second claim. Let us define
$\mathcal{M}:=\langle\Pi,\sigma,\delta\rangle$ as:

  * •

$\Pi:=\\{\pi_{0},\pi_{1},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},\pi_{n}\\}$;

  * •

$\sigma(\ast):=\Pi$ and for each $s\in\mathcal{S}\setminus\\{\ast\\}$, we
define $\sigma(s)$:

    1. (i)

$\pi_{i}\in\sigma(s)$ for each
$i\in\\{1,\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},n\\}$
such that $s_{i}=s$, and

    2. (ii)

$\pi_{j}\in\sigma(s)$ for each $\pi_{j}\in\sigma(s^{\prime})$ such that
$s^{\prime}\preceq^{*}_{\Gamma}s$;

  * •

$\delta(p):=\\{\pi_{i}\ |\ p^{\circ}\not\in\Sigma_{i}\\}$.

We know that the recursive definition of $\sigma$ will eventually terminate
since $\mathcal{S}$ is finite.

Let us now prove that $\mathcal{M}$ is indeed a standpoint model; afterward,
we will show that $\mathcal{M},\pi_{0}\not\models\iota(\Gamma\vdash\Delta)$.
First, observe that the inclusion of $\pi_{0}$ in $\Pi$ ensures that the
domain of precisifications is non-empty. Furthermore, $\delta$ is a function
from $\mathcal{P}$ to $2^{\Pi}$, for each $s\in\mathcal{S}$, we have that
$\sigma(s)\neq\emptyset$ by the $n_{s}$ saturation condition, and
$\sigma(\ast)=\Pi$ by definition. We now show that (a) for each
$s^{\prime}\preceq s\in\Gamma$ and
$i\in\\{0,\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},n\\}$,
$\mathcal{M},\pi_{i}\models s^{\prime}\preceq s$, and (b) for each
$i\in\\{0,\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},n\\}$
and $\widetilde{\psi}\in\Sigma_{i}$, $\mathcal{M},\pi_{i}\not\models\psi$,
from which $\mathcal{M},\pi_{0}\not\models\iota(\Gamma\vdash\varphi)$ follows
as $\widetilde{\varphi}\in\Sigma_{0}$.

(a) Let $s^{\prime}\preceq s\in\Gamma$ and assume that
$\pi\in\sigma(s^{\prime})$. Then, by the second clause in the definition of
$\sigma(s)$ it follows that $\pi\in\sigma(s)$, thus showing that
$\mathcal{M},\pi\models s\preceq s^{\prime}$ for all $\pi\in\Pi$.

(b) By induction on the complexity of $\psi$.

Base case. First, let us suppose that $\psi$ is a propositional atom $p$ where
$p^{\circ}\in\Sigma_{i}$. Then, by the definition of $\delta$, we have that
$\pi_{i}\not\in\delta(p)$, i.e. $\mathcal{M},\pi_{i}\not\models p$. Similarly,
if $\psi$ is a negated atom $\neg p$ where $\neg p^{\circ}\in\Sigma_{i}$, then
by the $id$ saturation condition, we know that $p^{\circ}\not\in\Sigma_{i}$,
implying that $\pi_{i}\in\delta(p)$ by the definition of $\delta$, thus
showing that $\mathcal{M},\pi_{i}\not\models\neg p$.

Inductive step. We suppose that $\widetilde{\psi}^{\circ}\in\Sigma_{i}$ and we
show that $\mathcal{M},\pi_{i}\not\models\psi$ making a case distinction based
on the main connective of $\psi$.

$\psi=\chi\lor\xi$:

By the $\lor$ saturation condition,
$\widetilde{\chi}^{\circ},\widetilde{\xi}^{\circ}\in\Sigma_{i}$. By IH,
$\mathcal{M},\pi_{i}\not\models\chi$ and $\mathcal{M},\pi_{i}\not\models\xi$,
showing $\mathcal{M},\pi_{i}\not\models\psi$.

$\psi=\chi\land\xi$:

By the $\land$ saturation condition, $\widetilde{\chi}^{\circ}\in\Sigma_{i}$
or $\widetilde{\xi}^{\circ}\in\Sigma_{i}$. By IH,
$\mathcal{M},\pi_{i}\not\models\chi$ or $\mathcal{M},\pi_{i}\not\models\xi$,
so $\mathcal{M},\pi_{i}\not\models\psi$.

$\psi=\mathop{\lozenge}\nolimits_{s}\chi\text{ with
}s\in\mathcal{S}\setminus\\{\ast\\}$:

Assume that $\pi_{j}\in\sigma(s)$. By the definition of $\sigma(s)$, $\pi_{j}$
was added via the first (i) or second (ii) condition. If (i), then there is a
nesting $(s)\\{\Sigma_{j}\\}_{\pi_{j}}$ in $\Delta$, and by the
$\mathop{\lozenge}\nolimits_{s}$ saturation condition,
$\widetilde{\chi}^{\circ}\in\Sigma_{j}$. By IH then,
$\mathcal{M},\pi_{j}\not\models\chi$. If (ii), then there is a chain of
statements $s_{0}\preceq
s_{1},\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},s_{n}\preceq
s\in\Gamma$ such that a nesting of the form
$(s_{0})\\{\Sigma_{j}\\}_{\pi_{j}}$ exists in $\Delta$. Again, by the
$\mathop{\lozenge}\nolimits_{s}$ saturation condition, it follows that
$\widetilde{\chi}^{\circ}\in\Sigma_{j}$, which implies that
$\mathcal{M},\pi_{j}\not\models\chi$ by IH. Hence,
$\mathcal{M},\pi_{i}\not\models\mathop{\lozenge}\nolimits_{s}\chi$.

$\psi=\mathop{\lozenge}\nolimits_{\ast}\chi$:

Since $\ast$ is maximal relative to the $\preceq^{*}_{\Gamma}$ relation, i.e.
$s\preceq^{*}_{\Gamma}\ast$ for all $s\in\mathcal{S}$, we have
$\widetilde{\chi}^{\circ}\in\Sigma_{j}$ for each
$j\in\\{0,\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},n\\}$
by the $\mathop{\lozenge}\nolimits_{\ast}$ and
$\mathop{\lozenge}\nolimits_{s}$ saturation conditions, hence for all
$\pi_{j}\in\Pi$, $\mathcal{M},\pi_{j}\not\models\chi$, i.e.
$\mathcal{M},\pi_{i}\not\models\mathop{\lozenge}\nolimits_{\ast}\chi$.

$\psi=\mathop{\square}\nolimits_{s}\chi$:

By the $\mathop{\square}\nolimits_{s}$ saturation condition, we know that
there exists a
$j\in\\{1,\mathinner{\ldotp\kern-1.00006pt\ldotp\kern-1.00006pt\ldotp},n\\}$
such that $s_{j}=s$ and $\widetilde{\chi}^{\circ}\in\Sigma_{j}$. By IH,
$\mathcal{M},\pi_{j}\not\models\chi$, thus proving the case.∎

######  Example 4.

Let us provide an example of the counter-model construction procedure given in
Thm. 3. We assume that the (invalid) sequent $s\preceq
s^{\prime}\vdash\varphi$ with
$\varphi:=\mathop{\square}\nolimits_{s^{\prime}}p\lor\mathop{\lozenge}\nolimits_{s}\neg
p$ is input into $\mathtt{Prove}_{\mathcal{V}}$. Since $\varphi$ has one
proper coloring (with all subformulae active), only the following single
thread is generated, yielding the saturated sequent shown at the top of the
proof below. We omit the active labels for readability.

$s\preceq
s^{\prime}\vdash\varphi,\mathop{\square}\nolimits_{s^{\prime}}p,\mathop{\lozenge}\nolimits_{s}\neg
p,(s^{\prime})[p]_{\pi_{1}},(s)[\neg p]_{\pi_{2}},(*)[\emptyset]_{\pi_{3}}$
$(n_{*})$ $s\preceq
s^{\prime}\vdash\varphi,\mathop{\square}\nolimits_{s^{\prime}}p,\mathop{\lozenge}\nolimits_{s}\neg
p,(s^{\prime})[p]_{\pi_{1}},(s)[\neg p]_{\pi_{2}}$
$(\mathop{\lozenge}_{s}^{1})$ $s\preceq
s^{\prime}\vdash\varphi,\mathop{\square}\nolimits_{s^{\prime}}p,\mathop{\lozenge}\nolimits_{s}\neg
p,(s^{\prime})[p]_{\pi_{1}},(s)[\emptyset]_{\pi_{2}}$ $(n_{s})$ $s\preceq
s^{\prime}\vdash\varphi,\mathop{\square}\nolimits_{s^{\prime}}p,\mathop{\lozenge}\nolimits_{s}\neg
p,(s^{\prime})[p]_{\pi_{1}}$ $(\mathop{\square}_{s^{\prime}})$ $s\preceq
s^{\prime}\vdash\varphi,\mathop{\square}\nolimits_{s^{\prime}}p,\mathop{\lozenge}\nolimits_{s}\neg
p$ $(\lor)$ $s\preceq s^{\prime}\vdash\varphi$

Then, we may extract the following (counter-)model
$\mathcal{M}=\langle\Pi,\sigma,\delta\rangle$ from the top, saturated sequent
in the proof above.

  * •

$\Pi:=\\{\pi_{0},\pi_{1},\pi_{2},\pi_{3}\\}$;

  * •

$\sigma(\ast):=\Pi$, $\sigma(s):=\\{\pi_{2}\\}$, and
$\sigma(s^{\prime}):=\\{\pi_{1}\\}$;

  * •

$\delta(p):=\\{\pi_{0},\pi_{2},\pi_{3}\\}$.

It is readily verifiable that
$\mathcal{M},\pi_{0}\not\models\mathop{\square}\nolimits_{s^{\prime}}p\lor\mathop{\lozenge}\nolimits_{s}\neg
p$.

We now show that $\mathtt{ProofSearch}_{\mathcal{V}}$ (and hence
$\mathtt{Prove}_{\mathcal{V}}$) terminates after at most polynomially many
rule applications in the _size_ of the input sequent. For an input
$\Phi:=\Gamma\vdash\varphi$, its size is defined to be
$|\Phi|:=|\mathcal{S}|+|\varphi|$. That is, the size of $\Phi$ is the sum of
the cardinality of the set $\mathcal{S}$ of standpoints and the size of
$\varphi$. The size of a sequent incorporates a measure on the set
$\mathcal{S}$ from the associated vocabulary $\mathcal{V}$ as opposed to a
measure on the set $\Gamma$ of sharpening statements because $\Gamma$ only
plays a role in bottom-up applications of $(\mathop{\lozenge}_{s}^{1})$ and
$(\mathop{\lozenge}_{s}^{2})$, which are bounded in part by the cardinality of
$\mathcal{S}$ and in part by the number of $\mathop{\square}\nolimits_{s}$
modalities occurring in $\varphi$, as explained in the proof of Thm. 4 below.

######  Theorem 4 (Termination).

Let $\Phi:=\Gamma\vdash\varphi$ be a sequent. Then, the number of recursive
calls in
$\mathtt{ProofSearch}_{\mathcal{V}}(\Gamma\vdash\widetilde{\varphi})$, and
thus $\mathtt{Prove}_{\mathcal{V}}(\Gamma\vdash\varphi)$, is bounded by a
polynomial

$p(|\Phi|)=\mathcal{O}(|\Phi|^{2}).$

###### Proof.

Let $\Phi:=\Gamma\vdash\varphi$ be a nested sequent, and $N_{\oplus}$ be the
number of occurrences of the connectives
$\\{\lor,\land\\}\cup\\{\mathop{\lozenge}\nolimits_{s}\ |\ s\in\mathcal{S}\\}$
in $\varphi$. By the saturation conditions (Def. 8), we know that for each
$s\in\mathcal{S}$, the $(\mathop{\square}_{s})$ rule will be applied bottom-up
at most one time for each occurrence of $\mathop{\square}\nolimits_{s}$ in
$\varphi$, which are bounded by $|\varphi|$. Also, $(n_{s})$ will be applied
at most once for each $s\in\mathcal{S}$. Since only $(\mathop{\square}_{s})$
and $(n_{s})$ introduce nestings, the number of components (i.e. the nestings
plus the root) throughout the course of proof-search is bounded by:

$K:=1+|\mathcal{S}|+|\varphi|$

For each occurrence of $\lor$, $\land$, and $\mathop{\lozenge}\nolimits_{s}$
in $\varphi$ (with $s\in\mathcal{S}$), we know by the saturation conditions
that $(\lor)$, $(\land)$, $(\mathop{\lozenge}_{s}^{1})$,
$(\mathop{\lozenge}_{s}^{2})$, and $(\mathop{\lozenge}_{*})$ can be applied a
maximum number of $K$ times during proof search. Then, since
$N_{\lor}+N_{\land}+\sum_{s\in\mathcal{S}}N_{\mathop{\lozenge}\nolimits_{s}}\leq|\varphi|$,
the number of recursive calls (i.e. bottom-up applications of rules) during
proof-search is bounded by $N:=|\varphi|\cdot K$. Finally,
$|\mathcal{S}|,|\varphi|\leq|\Phi|$ holds trivially, implying:

$N\leq|\Phi|\cdot(1+|\Phi|+|\Phi|)$

Therefore, it follows that a polynomial $p(|\Phi|)=\mathcal{O}(|\Phi|^{2})$
bounds the number of recursive calls of $\mathtt{Prove}_{\mathcal{V}}(\Phi)$.
∎

######  Corollary 1.

Let $\mathcal{V}$ be a vocabulary. Then,

  1. 1.

${\mathbb{S}}(\mathcal{V})$ is decidable;

  2. 2.

${\mathbb{S}}(\mathcal{V})$ has the finite model property;

  3. 3.

$\mathtt{Prove}_{\mathcal{V}}$ is worst-case complexity-optimal, deciding the
validity problem for ${\mathbb{S}}(\mathcal{V})$ in $\mathrm{CoNP}$;

  4. 4.

The validity problem for ${\mathbb{S}}(\mathcal{V})$ is
$\mathrm{CoNP}$-complete.

###### Proof.

Statements 1 and 2 follow from the fact that $\mathtt{Prove}_{\mathcal{V}}$ is
a correct (Thm. 3) and terminating (Thm. 4) decision procedure for
${\mathbb{S}}(\mathcal{V})$ that, in particular, returns a finite counter-
model when the input is invalid.

To show statement 3, observe that $\mathtt{Prove}_{\mathcal{V}}$ is a non-
deterministic algorithm that takes a sequent $\Phi:=\Gamma\vdash\varphi$ as
input, guesses a proper coloring of $\varphi$, and constructs a thread. Each
such thread is polynomial in the size of its input, since the number of rule
applications (i.e. the length of the thread) is bounded by a polynomial
$p(|\Phi|)=\mathcal{O}(|\Phi|^{2})$, by Thm. 4. Moreover, since any sequent
generated during proof-search can have at most $K\leq
1+|\mathcal{S}|+|\varphi|$ many components (as stated in the proof of Thm. 4),
each of which can only be inhabited by at most
$|\mathrm{sufo}(\varphi)|=|\varphi|$ many formulae, it follows that the size
of each nested sequent in the thread is bounded by $\mathcal{O}(|\Phi|^{2})$
since $|\mathcal{S}|,|\varphi|\leq|\Phi|$. Taking the functionality of
$\mathtt{Prove}_{\mathcal{V}}$ into account, one can see that if
$\mathtt{Prove}_{\mathcal{V}}(\Phi)=\mathtt{False}$, then the corresponding
thread is generated in polynomial time and its size is bounded above by a
polynomial $q(|\Phi|)=\mathcal{O}(|\Phi|^{4})$. Additionally, note that
$\mathtt{Prove}_{\mathcal{V}}$ is worst-case complexity-optimal as the
validity problem for classical propositional logic is
$\mathrm{CoNP}$-complete, and can be solved by $\mathtt{Prove}_{\mathcal{V}}$
as $(id)$, $(\lor)$, and $(\land)$ form a sound and complete proof system for
propositional logic (cf. (?, App. B)). Last, statement 4 is an immediate
consequence of statement 3. ∎

##  5 Conclusion and Future Work

In this paper, we introduced and employed nested sequent systems to automate
reasoning with propositional standpoint logics. To obtain worst-case
complexity-optimal proof-search, we presented a novel proof-search technique,
referred to as _coloring_ , whereby the subformulae of an input formula are
non-deterministically colored with (in)active labels, yielding partial proofs
(i.e. _threads_) of the input. By means of our technique, we designed a non-
deterministic proof-search algorithm deciding the validity of standpoint
implications in $\mathrm{CoNP}$, showing how certain threads could be
transformed into a counter-model for an invalid input, and how all threads
could be transformed into a proof for a valid input. The attainment of these
“certificates” from proof-search serve as explanations for the (in)validity of
standpoint formulae, thus motivating our proof-theoretic approach.

For future work, we aim to extend our nested systems and proof-search
algorithm to cover (i) first-order standpoint logics that (ii) incorporate
complex standpoints, which have interesting applications in knowledge
integration scenarios. Regarding point (i), placing standpoint logic on a
first-order base increases the applicability of the framework along with its
expressivity to better match that of contemporary knowledge representation
languages. Our focus in this area is to provide results that can then be
extrapolated to widely used decidable fragments of FOL. Regarding point (ii),
we note that the set-theoretic interpretation of standpoints permits the
definition of complex standpoints built atop atomic ones; e.g. union
$s_{1}\cup s_{2}$ (integrating knowledge from multiple perspectives),
intersection $s_{1}\cap s_{2}$ (expressing the knowledge jointly shared
between multiple perspectives), and difference $s_{1}\setminus s_{2}$
(yielding the sharpening of $s_{1}$ by ignoring all precisfications of
$s_{2}$). Beyond providing nested systems for more expressive formulations of
standpoint logic, we also aim to write and evaluate theorem provers based on
our nested calculi.

Acknowledgments. Lucía Gómez Álvarez was supported by the Bundesministerium
fur Bildung und Forschung (BMBF, Federal Ministry of Education and Research)
in the Center for Scalable Data Analytics and Artificial Intelligence
(ScaDS.AI). Tim S. Lyon has received funding from the European Research
Council (Grant Agreement no. 771779, DeciGUT).

## References

  * Belnap 1982 Belnap, N. D.  1982\.  Display logic.  Journal of philosophical logic 11(4):375–417.
  * Brünnler 2009 Brünnler, K.  2009\.  Deep sequent systems for modal logic.  Arch. Math. Log. 48(6):551–577.
  * Bull 1992 Bull, R. A.  1992\.  Cut elimination for propositional dynamic logic without *.  Z. Math. Logik Grundlag. Math. 38(2):85–100.
  * Buss 1998 Buss, S. R.  1998\.  An introduction to proof theory.  Handbook of proof theory 137:1–78.
  * Dyckhoff 1992 Dyckhoff, R.  1992\.  Contraction-free sequent calculi for intuitionistic logic.  The Journal of Symbolic Logic 57(3):795–807.
  * Fine 1975 Fine, K.  1975\.  Vagueness, truth and logic.  Synthese 30(3-4):265–300.
  * Fitting and Kuznets 2015 Fitting, M., and Kuznets, R.  2015\.  Modal interpolation via nested sequents.  Annals of pure and applied logic 166(3):274–305.
  * Gentzen 1935a Gentzen, G.  1935a.  Untersuchungen über das logische Schließen. i.  Mathematische Zeitschrift 39(1):176–210.
  * Gentzen 1935b Gentzen, G.  1935b.  Untersuchungen über das logische Schließen. ii.  Mathematische Zeitschrift 39(1):405–431.
  * Gómez Álvarez and Bennett 2018 Gómez Álvarez, L., and Bennett, B.  2018\.  Dealing with conceptual indeterminacy: A framework based on supervaluation semantics.  In Joint Proceedings of MedRACER and WOMoCoE, volume 2237, 38–50.  CEUR.
  * Gómez Álvarez and Rudolph 2021 Gómez Álvarez, L., and Rudolph, S.  2021\.  Standpoint logic: Multi-perspective knowledge representation.  In Neuhaus, F., and Brodaric, B., eds., Proceedings of the 12th International Conference on Formal Ontology in Information Systems, volume 344 of FAIA, 3–17.  IOS Press.
  * Gómez Álvarez, Bennett, and Richard-Bollans 2017 Gómez Álvarez, L.; Bennett, B.; and Richard-Bollans, A.  2017\.  Talking about forests: An example of sharing information expressed with vague terms.  In Proceedings of the Joint Ontology Workshops 2017, volume 2050\.  CEUR.
  * Gómez Álvarez 2020 Gómez Álvarez, L.  2020\.  Standpoint logic: a logic for handling semantic variability, with applications to forestry information.  Ph.D. Dissertation, School of Computing, The University of Leeds.
  * Kashima 1994 Kashima, R.  1994\.  Cut-free sequent calculi for some tense logics.  Studia Logica 53(1):119–135.
  * Keefe and Smith 1997 Keefe, R., and Smith, P.  1997\.  Theories of vagueness.  The MIT press.
  * Lyon and van Berkel 2019 Lyon, T., and van Berkel, K.  2019\.  Automating agential reasoning: Proof-calculi and syntactic decidability for STIT logics.  In Baldoni, M.; Dastani, M.; Liao, B.; Sakurai, Y.; and Zalila Wenkstern, R., eds., Proceedings of the 22nd International Conference on Principles and Practice of Multi-Agent Systems, volume 11873, 202–218.  Springer.
  * Lyon et al. 2020 Lyon, T.; Tiu, A.; Goré, R.; and Clouston, R.  2020\.  Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents.  In Fernández, M., and Muscholl, A., eds., Proceedings of the 28th Annual Conference on Computer Science Logic, volume 152 of LIPIcs, 28:1–28:16.  Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
  * Lyon 2020 Lyon, T.  2020\.  On the correspondence between nested calculi and semantic systems for intuitionistic logics.  Journal of Logic and Computation 31(1):213–265.
  * Lyon 2021a Lyon, T.  2021a.  Refining Labelled Systems for Modal and Constructive Logics with Applications.  Ph.D. Dissertation, Technische Universität Wien.
  * Lyon 2021b Lyon, T. S.  2021b.  Nested sequents for intuitionistic modal logics via structural refinement.  In Das, A., and Negri, S., eds., Automated Reasoning with Analytic Tableaux and Related Methods, 409–427.  Cham: Springer.
  * Pesquita et al. 2013 Pesquita, C.; Faria, D.; Santos, E.; and Couto, F. M.  2013\.  To repair or not to repair: Reconciling correctness and coherence in ontology reference alignments.  In Proceedings of the 8th International Conference on Ontology Matching, volume 1111, 13–24.  CEUR.
  * Poggiolesi 2009 Poggiolesi, F.  2009\.  The method of tree-hypersequents for modal propositional logic.  In Makinson, D.; Malinowski, J.; and Wansing, H., eds., Towards Mathematical Philosophy, volume 28 of Trends in logic. Springer.  31–51.
  * Simpson 1994 Simpson, A. K.  1994\.  The proof theory and semantics of intuitionistic modal logic.  Ph.D. Dissertation, University of Edinburgh. College of Science and Engineering. School of Informatics.
  * Slaney 1997 Slaney, J. K.  1997\.  Minlog: A minimal logic theorem prover.  In McCune, W., ed., Proceedings of the 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes in Computer Science, 268–271.  Springer.
  * Takeuti 2013 Takeuti, G.  2013\.  Proof theory, volume 81.  Courier Corporation.
  * Tiu, Ianovski, and Goré 2012 Tiu, A.; Ianovski, E.; and Goré, R.  2012\.  Grammar logics in nested sequent calculus: Proof theory and decision procedures.  In Bolander, T.; Braüner, T.; Ghilardi, S.; and Moss, L. S., eds., Advances in Modal Logic 9, papers from the ninth conference on Advances in Modal Logic, 516–537.  College Publications.
  * Wansing 2002 Wansing, H.  2002\.  Sequent systems for modal logics.  In Gabbay, D. M., and Guenthner, F., eds., Handbook of Philosophical Logic: Volume 8. Springer.  61–145.