The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) G\"odel-L\"ob logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong L\"ob logic iSL, for which this is the first proof-theoretic construction of uniform interpolants. Our work also yields verified programs that allow one to compute the propositional quantifiers on any formula in this logic.

翻译：均匀插值性质在给定逻辑中可理解为命题量词的可定义性。我们实现了这些量词的计算，并在Coq证明辅助系统中验证了三种模态逻辑的正确性：(1) 模态逻辑K，其已有纸笔证明；(2) 哥德尔-洛布逻辑GL，我们的形式化工作澄清了现有但不完备的相继式风格证明中的一个重要要点；(3) 直觉主义强洛布逻辑iSL，这是首次通过证明论构造方式给出均匀插值项。我们的工作还产生了可验证的程序，能对该逻辑中任意公式计算命题量词。