Two papers co-authored by our team member Ian Shillito have been published in the proceedings of the 13th International Joint Conference on Automated Reasoning (IJCAR 2026), held in Lisbon, Portugal, as part of FLoC 2026. Both papers extend Pitts’ proof-theoretic technique for uniform interpolation to new intuitionistic modal settings, and both come with full mechanisations in the Rocq proof assistant.
-
Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM by Hugo Férée and Ian Shillito. Pitts’ technique had so far only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. This paper adapts it to the intuitionistic multi-succedent setting, focusing on the intuitionistic modal logic KM: a novel multi-succedent sequent calculus is designed that terminates and eliminates cut, yielding decidability, and is then used to construct uniform interpolants for KM. By (re)proving the algebraisability of KM, the coherence of the class of KM-algebras follows.
[Read More]