{"id":"arxiv/2602.16445","url":"https://arxiv.org/abs/2602.16445","tags":["cs.LO","math.LO"],"score":0,"title":"Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM","domain":"cs.LO","source":"arxiv","authors":["Hugo Férée","Ian Shillito"],"reviews":0,"subject":"cs.LO","summary":"Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt the technique to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM. To do this, we design a novel multi-succedent sequent calculus for this logic which terminates, eliminates cut, and provides a decidability argument for KM. Then, we adapt Pitts' technique to our calculus to construct uniform interpolants for KM,…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-18","reactions":{}}