Mechanised Uniform Interpolation for Modal Logics K, GL, and Intuitionistic Strong Löb Logic iSL

The authors mechanise the computation of propositional quantifiers and prove the correctness of uniform interpolation in the Coq proof assistant for three modal logics: the classical modal logic K, Gödel-Löb logic GL, and the intuitionistic modal logic iSL.