# Automating Reasoning with Standpoint Logic via Nested Sequents

arXiv: https://arxiv.org/abs/2205.02749 · HTML: https://mlsanity.com/paper/2205.02749/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 35 references that are in the map.
- First posted on arXiv 5 May 2022.

## Builds on (most cited first, 5 of 5)

- [Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents](https://mlsanity.com/paper/1910.05215/) (2019)
- [Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics](https://mlsanity.com/paper/1908.11360/) (2019)
- [Nested Sequents for Intuitionistic Modal Logics via Structural Refinement](https://mlsanity.com/paper/2107.01998/) (2021)
- [Refining Labelled Systems for Modal and Constructive Logics with Applications](https://mlsanity.com/paper/2107.14487/) (2021)
- [On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics](https://mlsanity.com/paper/2104.09215/) (2021)

## Built on by (most cited first, 3 of 3)

- [Standpoint Linear Temporal Logic](https://mlsanity.com/paper/2304.14243/) (2023)
- [Connecting Proof Theory and Knowledge Representation: Sequent Calculi and the Chase with Existential Rules](https://mlsanity.com/paper/2306.02521/) (2023)
- [Non-Monotonic S4F Standpoint Logic (Extended Version with Proofs)](https://mlsanity.com/paper/2511.10449/) (2025)

## Abstract (arXiv)

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 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.