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——这是首个针对该逻辑均匀插值的证明论构造。我们的工作同时生成了可验证程序，允许用户对该逻辑中任意公式计算命题量词。