论文标题
统一插值的可抛态逻辑
Uniform Interpolation in provability logics
论文作者
论文摘要
我们使用逻辑的分析和终止序列计算，证明了模态可预订性逻辑中的统一插值定理。在Grzegorczyk的逻辑GRZ的情况下，Gödel-Löb的逻辑GL的演算是标准序列微积分的变体，该微积分实现了受Heuerding工作启发的明确的环路预示机制。
We prove the uniform interpolation theorem in modal provability logics GL and Grz by a proof-theoretical method, using analytical and terminating sequent calculi for the logics. The calculus for Gödel-Löb's logic GL is a variant of the standard sequent calculus, in the case of Grzegorczyk's logic Grz, the calculus implements an explicit loop-preventing mechanism inspired by work of Heuerding.
