# Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Oct 2019.

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

- [Automating Reasoning with Standpoint Logic via Nested Sequents](https://mlsanity.com/paper/2205.02749/) (2022)
- [Uniform and Modular Sequent Systems for Description Logics](https://mlsanity.com/paper/2206.09020/) (2022)
- [Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents](https://mlsanity.com/paper/2404.15840/) (2024)
- [Connecting Proof Theory and Knowledge Representation: Sequent Calculi and the Chase with Existential Rules](https://mlsanity.com/paper/2306.02521/) (2023)

## Abstract (arXiv)

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants.